Solution for Basic.triple_transfer
Lemma triple_transfer : forall (p q:loc) (n m:int),
triple (transfer p q)
(p ~~> n \* q ~~> m)
(fun _ => p ~~> (n + m) \* q ~~> 0).
Proof using.
xwp. xapp. xapp. xapp. xapp. xapp. xsimpl.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
