Solution for Arrays.QuickSort.triple_quicksort_safety
xwp. xapp. xif; intros C.
{ xapp triple_pivot_safety; try math.
intros j x L' L1 L2 (E&->&Hj). rew_list in E.
xchange hseg_app. xchange hseg_cons.
math_rewrite (i + length L1 + 1 = j + 1).
xapp. xapp; try math. intros L1' EQ1.
xapp. xapp. xapp. xapp; try math. intros L2' EQ2.
xchange (>> hseg_cons_r L2'). { math. } xchange hseg_app_r. { math. }
xsimpl (L1' ++ val_int x :: L2'). { rew_list. math. } }
{ xval. xsimpl*. }
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
