Why3.thy 112 Bytes