(* This file was originally generated by why. It can be modified; only the generated parts will be overwritten. *) Load spec_imports. Import local_memory. (* Why obligation from file "InsertionSort_sort.why", characters 1637-1886 *) Lemma InsertionSort_sort_body_po_1 : forall (arr: value), forall (heap: store), forall (Pre17: (neqv arr Null) /\ (instanceof heap arr ArrIntType)), forall (lowest: Z), forall (Post17: lowest = 0), forall (j: Z), forall (Post16: j = 0), forall (i: Z), forall (Post15: i = 0), forall (i1: Z), forall (Post1: i1 = 0), forall (Variant1: Z), forall (i2: Z), forall (intA0: ((memarray) Z)), forall (Pre16: Variant1 = ((arraylength heap arr) - i2)), forall (Pre15: ((i2 >= 0 /\ i2 <= (arraylength heap arr)) /\ (forall (k:Z), (forall (j:Z), ((0 <= j /\ j < k) /\ k < i2 -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))) /\ (forall (k:Z), (forall (j:Z), (((0 <= j /\ j < i2) /\ k >= i2) /\ k < (arraylength heap arr) -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))), forall (Pre14: (neqv arr Null)), forall (Test6: i2 < (arraylength heap arr)), forall (lowest2: Z), forall (Post3: lowest2 = i2), forall (j2: Z), forall (Post4: j2 = (i2 + 1)), forall (Variant3: Z), forall (j3: Z), forall (lowest3: Z), forall (Pre7: Variant3 = ((arraylength heap arr) - j3)), forall (Pre6: (((j3 > i2 /\ j3 <= (arraylength heap arr)) /\ lowest3 >= i2) /\ lowest3 < (arraylength heap arr)) /\ (forall (k:Z), (i2 <= k /\ k < j3 -> (array_acc intA0 arr lowest3) <= (array_acc intA0 arr k)))), forall (Pre5: (neqv arr Null)), forall (Test5: j3 < (arraylength heap arr)), (is_valid_index heap arr j3). intuition. Qed. (* Why obligation from file "InsertionSort_sort.why", characters 1637-1886 *) Lemma InsertionSort_sort_body_po_2 : forall (arr: value), forall (heap: store), forall (Pre17: (neqv arr Null) /\ (instanceof heap arr ArrIntType)), forall (lowest: Z), forall (Post17: lowest = 0), forall (j: Z), forall (Post16: j = 0), forall (i: Z), forall (Post15: i = 0), forall (i1: Z), forall (Post1: i1 = 0), forall (Variant1: Z), forall (i2: Z), forall (intA0: ((memarray) Z)), forall (Pre16: Variant1 = ((arraylength heap arr) - i2)), forall (Pre15: ((i2 >= 0 /\ i2 <= (arraylength heap arr)) /\ (forall (k:Z), (forall (j:Z), ((0 <= j /\ j < k) /\ k < i2 -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))) /\ (forall (k:Z), (forall (j:Z), (((0 <= j /\ j < i2) /\ k >= i2) /\ k < (arraylength heap arr) -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))), forall (Pre14: (neqv arr Null)), forall (Test6: i2 < (arraylength heap arr)), forall (lowest2: Z), forall (Post3: lowest2 = i2), forall (j2: Z), forall (Post4: j2 = (i2 + 1)), forall (Variant3: Z), forall (j3: Z), forall (lowest3: Z), forall (Pre7: Variant3 = ((arraylength heap arr) - j3)), forall (Pre6: (((j3 > i2 /\ j3 <= (arraylength heap arr)) /\ lowest3 >= i2) /\ lowest3 < (arraylength heap arr)) /\ (forall (k:Z), (i2 <= k /\ k < j3 -> (array_acc intA0 arr lowest3) <= (array_acc intA0 arr k)))), forall (Pre5: (neqv arr Null)), forall (Test5: j3 < (arraylength heap arr)), forall (Pre3: (is_valid_index heap arr j3)), (is_valid_index heap arr lowest3). intuition. Qed. (* Why obligation from file "InsertionSort_sort.why", characters 1902-1913 *) Lemma InsertionSort_sort_body_po_3 : forall (arr: value), forall (heap: store), forall (Pre17: (neqv arr Null) /\ (instanceof heap arr ArrIntType)), forall (lowest: Z), forall (Post17: lowest = 0), forall (j: Z), forall (Post16: j = 0), forall (i: Z), forall (Post15: i = 0), forall (i1: Z), forall (Post1: i1 = 0), forall (Variant1: Z), forall (i2: Z), forall (intA0: ((memarray) Z)), forall (Pre16: Variant1 = ((arraylength heap arr) - i2)), forall (Pre15: ((i2 >= 0 /\ i2 <= (arraylength heap arr)) /\ (forall (k:Z), (forall (j:Z), ((0 <= j /\ j < k) /\ k < i2 -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))) /\ (forall (k:Z), (forall (j:Z), (((0 <= j /\ j < i2) /\ k >= i2) /\ k < (arraylength heap arr) -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))), forall (Pre14: (neqv arr Null)), forall (Test6: i2 < (arraylength heap arr)), forall (lowest2: Z), forall (Post3: lowest2 = i2), forall (j2: Z), forall (Post4: j2 = (i2 + 1)), forall (Variant3: Z), forall (j3: Z), forall (lowest3: Z), forall (Pre7: Variant3 = ((arraylength heap arr) - j3)), forall (Pre6: (((j3 > i2 /\ j3 <= (arraylength heap arr)) /\ lowest3 >= i2) /\ lowest3 < (arraylength heap arr)) /\ (forall (k:Z), (i2 <= k /\ k < j3 -> (array_acc intA0 arr lowest3) <= (array_acc intA0 arr k)))), forall (Pre5: (neqv arr Null)), forall (Test5: j3 < (arraylength heap arr)), forall (Pre3: (is_valid_index heap arr j3)), forall (Pre4: (is_valid_index heap arr lowest3)), forall (Test4: (array_acc intA0 arr j3) < (array_acc intA0 arr lowest3)), forall (lowest4: Z), forall (Post7: lowest4 = j3), (forall (j:Z), (j = (j3 + 1) -> ((((j > i2 /\ j <= (arraylength heap arr)) /\ lowest4 >= i2) /\ lowest4 < (arraylength heap arr)) /\ (forall (k:Z), (i2 <= k /\ k < j -> (array_acc intA0 arr lowest4) <= (array_acc intA0 arr k)))) /\ (Zwf 0 ((arraylength heap arr) - j) ((arraylength heap arr) - j3)))). intuition. rewrite Post7. assert (k = j3 \/ k < j3). omega. destruct H11. rewrite H11. omega. apply Zle_trans with (array_acc intA0 arr lowest3). omega. auto. Qed. (* Why obligation from file "InsertionSort_sort.why", characters 1929-1929 *) Lemma InsertionSort_sort_body_po_4 : forall (arr: value), forall (heap: store), forall (Pre17: (neqv arr Null) /\ (instanceof heap arr ArrIntType)), forall (lowest: Z), forall (Post17: lowest = 0), forall (j: Z), forall (Post16: j = 0), forall (i: Z), forall (Post15: i = 0), forall (i1: Z), forall (Post1: i1 = 0), forall (Variant1: Z), forall (i2: Z), forall (intA0: ((memarray) Z)), forall (Pre16: Variant1 = ((arraylength heap arr) - i2)), forall (Pre15: ((i2 >= 0 /\ i2 <= (arraylength heap arr)) /\ (forall (k:Z), (forall (j:Z), ((0 <= j /\ j < k) /\ k < i2 -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))) /\ (forall (k:Z), (forall (j:Z), (((0 <= j /\ j < i2) /\ k >= i2) /\ k < (arraylength heap arr) -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))), forall (Pre14: (neqv arr Null)), forall (Test6: i2 < (arraylength heap arr)), forall (lowest2: Z), forall (Post3: lowest2 = i2), forall (j2: Z), forall (Post4: j2 = (i2 + 1)), forall (Variant3: Z), forall (j3: Z), forall (lowest3: Z), forall (Pre7: Variant3 = ((arraylength heap arr) - j3)), forall (Pre6: (((j3 > i2 /\ j3 <= (arraylength heap arr)) /\ lowest3 >= i2) /\ lowest3 < (arraylength heap arr)) /\ (forall (k:Z), (i2 <= k /\ k < j3 -> (array_acc intA0 arr lowest3) <= (array_acc intA0 arr k)))), forall (Pre5: (neqv arr Null)), forall (Test5: j3 < (arraylength heap arr)), forall (Pre3: (is_valid_index heap arr j3)), forall (Pre4: (is_valid_index heap arr lowest3)), forall (Test3: (array_acc intA0 arr j3) >= (array_acc intA0 arr lowest3)), forall (result5: unit), forall (Post6: result5 = tt), (forall (j:Z), (j = (j3 + 1) -> ((((j > i2 /\ j <= (arraylength heap arr)) /\ lowest3 >= i2) /\ lowest3 < (arraylength heap arr)) /\ (forall (k:Z), (i2 <= k /\ k < j -> (array_acc intA0 arr lowest3) <= (array_acc intA0 arr k)))) /\ (Zwf 0 ((arraylength heap arr) - j) ((arraylength heap arr) - j3)))). intuition. assert (k = j3 \/ k < j3). omega. destruct H11. rewrite H11. omega. auto. Qed. (* Why obligation from file "InsertionSort_sort.why", characters 1074-1974 *) Lemma InsertionSort_sort_body_po_5 : forall (arr: value), forall (heap: store), forall (Pre17: (neqv arr Null) /\ (instanceof heap arr ArrIntType)), forall (lowest: Z), forall (Post17: lowest = 0), forall (j: Z), forall (Post16: j = 0), forall (i: Z), forall (Post15: i = 0), forall (i1: Z), forall (Post1: i1 = 0), forall (Variant1: Z), forall (i2: Z), forall (intA0: ((memarray) Z)), forall (Pre16: Variant1 = ((arraylength heap arr) - i2)), forall (Pre15: ((i2 >= 0 /\ i2 <= (arraylength heap arr)) /\ (forall (k:Z), (forall (j:Z), ((0 <= j /\ j < k) /\ k < i2 -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))) /\ (forall (k:Z), (forall (j:Z), (((0 <= j /\ j < i2) /\ k >= i2) /\ k < (arraylength heap arr) -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))), forall (Pre14: (neqv arr Null)), forall (Test6: i2 < (arraylength heap arr)), forall (lowest2: Z), forall (Post3: lowest2 = i2), forall (j2: Z), forall (Post4: j2 = (i2 + 1)), forall (Variant3: Z), forall (j3: Z), forall (lowest3: Z), forall (Pre7: Variant3 = ((arraylength heap arr) - j3)), forall (Pre6: (((j3 > i2 /\ j3 <= (arraylength heap arr)) /\ lowest3 >= i2) /\ lowest3 < (arraylength heap arr)) /\ (forall (k:Z), (i2 <= k /\ k < j3 -> (array_acc intA0 arr lowest3) <= (array_acc intA0 arr k)))), forall (Pre5: (neqv arr Null)), forall (Test2: j3 >= (arraylength heap arr)), (forall (result:Z), (result = (array_acc intA0 arr i2) -> (forall (result0:Z), (result0 = (array_acc intA0 arr lowest3) -> (forall (intA:((memarray) Z)), (intA = (array_update intA0 arr i2 result0) -> (forall (intA0:((memarray) Z)), (intA0 = (array_update intA arr lowest3 result) -> (forall (i:Z), (i = (i2 + 1) -> (((i >= 0 /\ i <= (arraylength heap arr)) /\ (forall (k:Z), (forall (j:Z), ((0 <= j /\ j < k) /\ k < i -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))) /\ (forall (k:Z), (forall (j:Z), (((0 <= j /\ j < i) /\ k >= i) /\ k < (arraylength heap arr) -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))) /\ (Zwf 0 ((arraylength heap arr) - i) ((arraylength heap arr) - i2)))))) /\ (is_valid_index heap arr lowest3))) /\ (is_valid_index heap arr i2))) /\ (is_valid_index heap arr lowest3))) /\ (is_valid_index heap arr i2). intuition. assert (forall n, 0 <= n -> n < i2 -> array_acc intA1 arr n = array_acc intA0 arr n). intros. apply sym_eq. rewrite H13. rewrite H12. apply sym_eq. assert (array_acc (array_update (array_update intA0 arr i2 result0) arr lowest3 result) arr n = array_acc (array_update intA0 arr i2 result0) arr n). apply array_acc_update_other. right. omega. rewrite H20. apply array_acc_update_other. right. omega. assert (k < i2 \/ k = i2). omega. destruct H19. rewrite (H16 j0). rewrite (H16 k). auto. omega. omega. omega. omega. rewrite H19. rewrite (H16 j0). rewrite H13. rewrite H12. assert (lowest3 = i2 \/ lowest3 <> i2). omega. destruct H20. assert (array_acc (array_update (array_update intA0 arr i2 result0) arr lowest3 result) arr i2 = result). rewrite H20. apply array_acc_update. rewrite H21. rewrite H3. apply H2. omega. assert (array_acc (array_update (array_update intA0 arr i2 result0) arr lowest3 result) arr i2 = result0). assert (array_acc (array_update intA0 arr i2 result0) arr i2 = result0). apply array_acc_update_eq. trivial. trivial. assert (array_acc (array_update (array_update intA0 arr i2 result0) arr lowest3 result) arr i2 = array_acc (array_update intA0 arr i2 result0) arr i2). apply array_acc_update_other. right. omega. rewrite H21 in H22. trivial. rewrite H21. rewrite H11. apply H2. omega. trivial. omega. assert (forall n, 0 <= n -> n < arraylength heap arr -> n <> lowest3 -> n <> i2 -> array_acc intA1 arr n = array_acc intA0 arr n). intros. apply sym_eq. rewrite H13. rewrite H12. apply sym_eq. assert (array_acc (array_update (array_update intA0 arr i2 result0) arr lowest3 result) arr n = array_acc (array_update intA0 arr i2 result0) arr n). apply array_acc_update_other. right. omega. rewrite H23. apply array_acc_update_other. right. omega. assert (exists k0, k0 >= i2 /\ k0 < arraylength heap arr /\ array_acc intA1 arr k = array_acc intA0 arr k0). assert (k = lowest3 \/ k <> lowest3). omega. destruct H20. exists i2. split. omega. split. omega. rewrite H13. rewrite H12. assert (lowest3 = i2 \/ lowest3 <> i2). omega. destruct H21. rewrite H20. rewrite H21. rewrite H3. apply array_acc_update. rewrite H3. rewrite H20. apply array_acc_update. exists k. split. omega. rewrite (H15 k). trivial. omega. trivial. trivial. omega. trivial. trivial. omega. destruct H20. destruct H20. destruct H21. rewrite H22. assert (j0 = i2 \/ j0 < i2). omega. destruct H23. assert (array_acc intA1 arr j0 = array_acc intA0 arr lowest3). rewrite H13. rewrite H12. assert (i2 = lowest3 \/ i2 <> lowest3). omega. destruct H24. rewrite <- H24. rewrite H3. rewrite H23. apply array_acc_update. rewrite H23. assert (array_acc (array_update intA0 arr i2 result0) arr i2 = result0). apply array_acc_update. rewrite H11. assert (array_acc (array_update (array_update intA0 arr i2 (array_acc intA0 arr lowest3)) arr lowest3 result) arr i2 = array_acc (array_update intA0 arr i2 (array_acc intA0 arr lowest3)) arr i2). apply array_acc_update_other. right. omega. rewrite H26. apply array_acc_update. rewrite H24. apply H6. omega. replace (array_acc intA1 arr j0) with (array_acc intA0 arr j0). apply H2. omega. apply sym_eq. apply (H15 j0). trivial. omega. omega. omega. Qed. (* Why obligation from file "InsertionSort_sort.why", characters 1235-1568 *) Lemma InsertionSort_sort_body_po_6 : forall (arr: value), forall (heap: store), forall (Pre17: (neqv arr Null) /\ (instanceof heap arr ArrIntType)), forall (lowest: Z), forall (Post17: lowest = 0), forall (j: Z), forall (Post16: j = 0), forall (i: Z), forall (Post15: i = 0), forall (i1: Z), forall (Post1: i1 = 0), forall (Variant1: Z), forall (i2: Z), forall (intA0: ((memarray) Z)), forall (Pre16: Variant1 = ((arraylength heap arr) - i2)), forall (Pre15: ((i2 >= 0 /\ i2 <= (arraylength heap arr)) /\ (forall (k:Z), (forall (j:Z), ((0 <= j /\ j < k) /\ k < i2 -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))) /\ (forall (k:Z), (forall (j:Z), (((0 <= j /\ j < i2) /\ k >= i2) /\ k < (arraylength heap arr) -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))), forall (Pre14: (neqv arr Null)), forall (Test6: i2 < (arraylength heap arr)), forall (lowest2: Z), forall (Post3: lowest2 = i2), forall (j2: Z), forall (Post4: j2 = (i2 + 1)), (((j2 > i2 /\ j2 <= (arraylength heap arr)) /\ lowest2 >= i2) /\ lowest2 < (arraylength heap arr)) /\ (forall (k:Z), (i2 <= k /\ k < j2 -> (array_acc intA0 arr lowest2) <= (array_acc intA0 arr k))). intuition. assert (k = i2). omega. rewrite Post3. rewrite H3. omega. Qed. (* Why obligation from file "InsertionSort_sort.why", characters 302-2573 *) Lemma InsertionSort_sort_body_po_7 : forall (arr: value), forall (heap: store), forall (Pre17: (neqv arr Null) /\ (instanceof heap arr ArrIntType)), forall (lowest: Z), forall (Post17: lowest = 0), forall (j: Z), forall (Post16: j = 0), forall (i: Z), forall (Post15: i = 0), forall (i1: Z), forall (Post1: i1 = 0), forall (Variant1: Z), forall (i2: Z), forall (intA0: ((memarray) Z)), forall (Pre16: Variant1 = ((arraylength heap arr) - i2)), forall (Pre15: ((i2 >= 0 /\ i2 <= (arraylength heap arr)) /\ (forall (k:Z), (forall (j:Z), ((0 <= j /\ j < k) /\ k < i2 -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))) /\ (forall (k:Z), (forall (j:Z), (((0 <= j /\ j < i2) /\ k >= i2) /\ k < (arraylength heap arr) -> (array_acc intA0 arr j) <= (array_acc intA0 arr k))))), forall (Pre14: (neqv arr Null)), forall (Test1: i2 >= (arraylength heap arr)), (forall (j:Z), (forall (i:Z), ((0 <= i /\ i < j) /\ j < (arraylength heap arr) -> (array_acc intA0 arr i) <= (array_acc intA0 arr j)))). intuition. Qed. (* Why obligation from file "InsertionSort_sort.why", characters 399-902 *) Lemma InsertionSort_sort_body_po_8 : forall (arr: value), forall (heap: store), forall (intA: ((memarray) Z)), forall (Pre17: (neqv arr Null) /\ (instanceof heap arr ArrIntType)), forall (lowest: Z), forall (Post17: lowest = 0), forall (j: Z), forall (Post16: j = 0), forall (i: Z), forall (Post15: i = 0), forall (i1: Z), forall (Post1: i1 = 0), ((i1 >= 0 /\ i1 <= (arraylength heap arr)) /\ (forall (k:Z), (forall (j:Z), ((0 <= j /\ j < k) /\ k < i1 -> (array_acc intA arr j) <= (array_acc intA arr k))))) /\ (forall (k:Z), (forall (j:Z), (((0 <= j /\ j < i1) /\ k >= i1) /\ k < (arraylength heap arr) -> (array_acc intA arr j) <= (array_acc intA arr k)))). intuition. rewrite Post1. apply arraylength_always_pos. Qed.