Solution for WPsem.TexanTriples.wp_incr
Lemma wp_incr : forall (p:loc) (n:int) Q,
(p ~~> n) \* (p ~~> (n+1) \-* Q val_unit) ==> wp (incr p) Q.
Proof using.
intros. rewrite wp_equiv. applys triple_conseq_frame.
{ applys triple_incr. } { xsimpl. } { xsimpl. intros ? ->. auto. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
