Solution for Basic.triple_repeat_incr'
intros. gen n. induction_wf IH: (downto 0) m.
xwp. xapp. xif; intros C.
{ xapp. xapp. xapp. { math. }
xsimpl. repeat rewrite max_r; math. }
{ xval. xsimpl. rewrite max_l; math. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
