Why3.thy 50 Bytes