(* 1-assigns.ec *) (* two simple proofs involving assignments *) prover ["Z3"]. require import AllCore. module M = { var x, y : int var x', y' : int proc f() : unit = { x' <- y - 2; y' <- x + 2; } }. (* first lemma *) lemma foo : hoare[M.f : M.x + M.y = 10 ==> M.x' + M.y' = 10]. proof. proc; wp; skip; smt(). qed. (* second lemma *) lemma goo : hoare[M.f : M.x + 4 = M.y ==> M.x' = M.y']. proof. proc; wp; skip; smt(). qed.