Library quicksort3_QuickSort_WP_parameter_quick_sort1_2

Theorem WP_parameter_quick_sort1 : forall (a:Z) (lo:Z) (hi:Z),
  forall (a1:(map.Map.map Z Z)), ((0%Z <= a)%Z /\ (((0%Z <= lo)%Z /\
  (lo <= a)%Z) /\ ((0%Z <= hi)%Z /\ (hi <= a)%Z))) ->
  ((lo < (hi - 1%Z)%Z)%Z -> (((lo + 1%Z)%Z <= (hi - 1%Z)%Z)%Z -> forall (i:Z)
  (a2:(map.Map.map Z Z)), (((((lo < i)%Z /\
  (i <= ((hi - 1%Z)%Z + 1%Z)%Z)%Z) /\ forall (k:Z), (((lo + 1%Z)%Z <= k)%Z /\
  (k < i)%Z) -> ((map.Map.get a2 k) <= (map.Map.get a2 lo))%Z) /\
  forall (k':Z), ((i <= k')%Z /\ (k' < ((hi - 1%Z)%Z + 1%Z)%Z)%Z) ->
  ((map.Map.get a2 lo) <= (map.Map.get a2 k'))%Z) /\
  (map.MapPermut.permut_sub a1 a2 (lo + 1%Z)%Z hi)) -> (((0%Z <= a)%Z /\
  (((0%Z <= lo)%Z /\ (lo < a)%Z) /\ ((0%Z <= (i - 1%Z)%Z)%Z /\
  ((i - 1%Z)%Z < a)%Z))) -> forall (a3:(map.Map.map Z Z)), ((0%Z <= a)%Z /\
  (map.MapPermut.exchange a2 a3 lo (i - 1%Z)%Z)) -> ((div_sub (mk_array a a3)
  lo (i - 1%Z)%Z hi) -> ((((0%Z <= lo)%Z /\ (lo <= a)%Z) /\
  ((0%Z <= (i - 1%Z)%Z)%Z /\ ((i - 1%Z)%Z <= a)%Z)) ->
  forall (a4:(map.Map.map Z Z)), ((0%Z <= a)%Z /\ ((sorted_sub a4 lo
  (i - 1%Z)%Z) /\ (map.MapPermut.permut_sub a3 a4 lo (i - 1%Z)%Z))) ->
  ((((0%Z <= i)%Z /\ (i <= a)%Z) /\ ((0%Z <= hi)%Z /\ (hi <= a)%Z)) ->
  forall (a5:(map.Map.map Z Z)), ((0%Z <= a)%Z /\ ((sorted_sub a5 i hi) /\
  (map.MapPermut.permut_sub a4 a5 i hi))) -> ((div_sub (mk_array a a5) lo
  (i - 1%Z)%Z hi) -> (map.MapPermut.permut_sub a1 a5 lo hi)))))))).

 move=> a g d a1 [h1 [[h2 h3] [h4 h5]]] h6 h7 i a2 [[[[h8 h9] h10]
h11] a1_to_a2] [h13 [[h14 h15] [h16 h17]]] a3 [h18 a2_to_a3] h20 [[h21
h22] [h23 h24]] a4 [h25 [h26 a3_to_a4]] [[h28 h29] [h30 h31]] a5 [h32
[h33 a4_to_a5]] h35; compress.

apply (MapPermut.permut_weakening _ _ g d) in a1_to_a2; [|omega].
apply (MapPermut.permut_exchange _ _ g d) in a2_to_a3; [|omega|omega].
apply (MapPermut.permut_weakening _ _ g d) in a3_to_a4; [|omega].
apply (MapPermut.permut_weakening _ _ g d) in a4_to_a5; [|omega].
apply (MapPermut.permut_trans _ a2 _).
- exact a1_to_a2.
- apply (MapPermut.permut_trans a2 a3 a5).
  + exact a2_to_a3.
  + apply (MapPermut.permut_trans a3 a4 a5).
    - exact a3_to_a4.
    - exact a4_to_a5.
Qed.