Solution for Arrays.QuickSort.triple_quicksort_full
intros. xwp. xapp.
xchange harray_eq. intros ? ->.
xapp triple_quicksort. { rew_list*. } { math. }
intros L' (HP&HS). lets EL': permut_length HP.
xsimpl L'; rew_list*. rewrite* EL'.
xchange <- harray_eq. rew_list*.
Qed.
Click on the 'Next' button to reveal the proof step by step.
Please provide feedback
