Why3.thy 102 Bytes