(sorting_tutorial_2 (occurrences_TCC1 0 (occurrences_TCC1-1 nil 3349976468 3351272131 ("" (subtype-tcc) nil nil) unfinished nil 172 120 nil nil)) (occurrences_TCC2 0 (occurrences_TCC2-1 nil 3349976468 3351272131 ("" (termination-tcc) nil nil) unchecked nil 80 80 nil nil)) (permutation_lemma_1 0 (permutation_lemma_1-1 nil 3350843671 3351254980 ("" (postpone) nil nil) unfinished nil 12 10 t shostak)) (permutation_lemma_2 0 (permutation_lemma_2-1 nil 3351265855 3351270791 ("" (measure-induct+ "u-l" ("l" "u")) (("" (skolem 1 ("A" "J" "K")) (("" (case "x!1=x!2") (("1" (expand "permutation?" 1) (("1" (skolem 1 "Z") (("1" (replace -1 1) (("1" (expand "occurrences" 1) (("1" (typepred "J") (("1" (typepred "K") (("1" (case "A(x!2)=Z") (("1" (assert) (("1" (expand "occurrences" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "occurrences" 2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "permutation?" 2) (("2" (skolem 2 "Z") (("2" (expand "occurrences" 2) (("2" (lift-if) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 4785070 14580 t shostak)) (generalized_sorted? 0 (generalized_sorted?-1 nil 3350667499 3351254982 ("" (skolem 1 ("A" "L" "U")) (("" (prop) (("1" (measure-induct+ "j + k" ("j" "k")) (("1" (expand "sorted?") (("1" (inst -3 "x!1") (("1" (inst -1 "x!1+1" "x!2") (("1" (prop) (("1" (assert) nil nil) ("2" (typepred "x!1") (("2" (typepred "x!2") (("2" (typepred "x!1 + 1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (typepred "x!1") (("3" (typepred "x!2") (("3" (hide 1) (("3" (case "x!1 < x!2") (("1" (ground) (("1" (comment " Opps! The induction is set up improperly. `j+k' should have been `k-j' ") (("1" (postpone) nil ";;; ;;; Opps! The induction is set up improperly. ;;; `j+k' should have been `k-j' ;;; ")) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil) ("2" (typepred "x!1") (("2" (typepred "x!2") (("2" (expand "<=" -6) (("2" (split) (("1" (hide -2 -4 -5 -6 2) (("1" (postpone) nil nil)) nil) ("2" (hide -2 -3 -4 -5 -6 1) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "sorted?") (("2" (skolem 1 "J") (("2" (inst -1 "J" "1+J") (("2" (prop) (("2" (hide 2) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 1542 1290 t shostak)) (BS_inner_loop_TCC1 0 (BS_inner_loop_TCC1-1 nil 3349976468 3351272132 ("" (well-founded-tcc) nil nil) unfinished nil 433 370 nil nil)) (BS_inner_loop_TCC2 0 (BS_inner_loop_TCC2-1 nil 3349976468 3351272132 ("" (termination-tcc) nil nil) unchecked ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil)) 347 310 nil nil)) (BS_inner_loop_TCC3 0 (BS_inner_loop_TCC3-1 nil 3349976468 3351272132 ("" (termination-tcc) nil nil) unchecked ((extend const-decl "R" extend nil)) 123 120 nil nil)) (BS_inner_loop_TCC4 0 (BS_inner_loop_TCC4-1 nil 3350756608 3351272132 ("" (subtype-tcc) nil nil) unchecked ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil)) 344 300 nil nil)) (BS_inner_loop_TCC5 0 (BS_inner_loop_TCC5-1 nil 3350756608 3351272132 ("" (termination-tcc) nil nil) unchecked ((extend const-decl "R" extend nil)) 128 130 nil nil)) (BS_outer_loop_TCC1 0 (BS_outer_loop_TCC1-1 nil 3349976468 3351272133 ("" (well-founded-tcc) nil nil) unchecked ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil)) 127 100 nil nil)) (BS_outer_loop_TCC2 0 (BS_outer_loop_TCC2-1 nil 3349976468 3351272133 ("" (subtype-tcc) nil nil) unchecked ((extend const-decl "R" extend nil)) 140 120 nil nil)) (BS_inner_loop_no_side_effects 0 (BS_inner_loop_no_side_effects-1 nil 3351093145 3351254985 ("" (measure-induct+ "u-l" ("l" "u")) (("" (skolem 1 "A") (("" (skolem 1 "K") (("" (case "x!1=x!2" "1+x!1=x!2") (("1" (assert) nil nil) ("2" (expand "BS_inner_loop" 2) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil) ("3" (expand "BS_inner_loop" 2) (("3" (lift-if) (("3" (assert) (("3" (case "A(x!1) > A(1 + x!1)") (("1" (assert) (("1" (typepred "K") (("1" (inst -3 "1+x!1" "x!2") (("1" (assert) (("1" (inst -3 " A WITH [(x!1) := A(1 + x!1), (1 + x!1) := A(x!1)]") (("1" (inst -3 "K") (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -1 "1+x!1" "x!2") (("2" (assert) (("2" (inst -1 "A") (("2" (inst -1 "K") (("2" (typepred "K") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (> const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (BS_inner_loop def-decl "[nat -> int]" sorting_tutorial_2 nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) 1333 1150 t shostak)) (BS_inner_loop_permutes 0 (BS_inner_loop_permutes-2 "" 3350844736 3351265406 ("" (measure-induct+ "u-l" ("l" "u")) (("" (skolem 1 "A") (("" (case "x!1 = x!2") (("1" (expand "BS_inner_loop" 1) (("1" (lift-if) (("1" (assert) (("1" (expand "permutation?" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "BS_inner_loop" 2) (("2" (lift-if) (("2" (ground) (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 1185859 3640 t shostak) (BS_inner_loop_permutes-1 nil 3350843227 3350843631 ("" (measure-induct+ "u-l" ("l" "u")) (("1" (skolem 1 "A") (("1" (expand "permutation?" 1) (("1" (skolem 1 "Z") (("1" (expand "occurrences" 1) (("1" (case "x!1 > x!2") (("1" (assert) nil nil) ("2" (assert) (("2" (lift-if 2) (("2" (case "A(x!1) = Z") (("1" (assert) (("1" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil) ("4" (postpone) nil nil) ("5" (postpone) nil nil) ("6" (postpone) nil nil) ("7" (postpone) nil nil) ("8" (postpone) nil nil)) nil) unfinished nil 403906 2760 t shostak)) (BS_inner_loop_permutes_corollary 0 (BS_inner_loop_permutes_corollary-1 nil 3351096297 3351264206 ("" (skolem 1 ("L" "U" "A")) (("" (use "BS_inner_loop_permutes" (l "L" u "U" a "A")) (("" (use "permutation_lemma_1" (a "A" b "BS_inner_loop(L, U, A)" l "L" u "U")) (("" (ground) (("" (skolem!) (("" (inst? -1) (("" (skolem! -1) (("" (inst?) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((BS_inner_loop_permutes formula-decl nil sorting_tutorial_2 nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (BS_inner_loop def-decl "[nat -> int]" sorting_tutorial_2 nil) (permutation_lemma_1 formula-decl nil sorting_tutorial_2 nil)) 312438 1060 t shostak)) (BS_inner_loop_correct 0 (BS_inner_loop_correct-1 nil 3350842969 3351263757 ("" (measure-induct+ "u-l" ("l" "u")) (("" (skolem 1 "A") (("" (skolem 1 "K") (("" (assert) (("" (expand "BS_inner_loop" 1) (("" (case "x!1 = x!2") (("1" (ground) nil nil) ("2" (ground) (("2" (lemma "BS_inner_loop_permutes_corollary" ("l" "1+x!1" "u" "x!2")) (("2" (lemma "BS_inner_loop_no_side_effects" ("l" "1+x!1" "u" "x!2")) (("2" (case " A(x!1) > A(1 + x!1)") (("1" (assert) (("1" (name "AA" " A WITH [(x!1) := A(1 + x!1), (1 + x!1) := A(x!1)]") (("1" (replace -1) (("1" (inst -3 "AA" "_") (("1" (inst -4 "AA" "_") (("1" (inst -5 "1+x!1" "x!2") (("1" (assert) (("1" (inst -5 "AA") (("1" (case "K=x!1") (("1" (replace -1) (("1" (inst -4 "x!1") (("1" (replace -4 2 rl) (("1" (replace -2 2 rl) (("1" (ground) (("1" (replace -2 2) (("1" (inst -5 "1+x!1") (("1" (skolem -5 "J") (("1" (inst-cp -6 "1+x!1") (("1" (inst -6 "J") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -5 "K") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst -3 "1+x!1" "x!2") (("2" (ground) (("2" (inst -1 "A") (("2" (inst -3 "A" "_") (("2" (case "K=x!1") (("1" (replace -1) (("1" (inst -3 "A" "x!1") (("1" (replace -3 3 rl) (("1" (inst -4 "1+x!1") (("1" (skolem -4 "J") (("1" (inst-cp -2 "1+x!1") (("1" (inst -2 "J") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -1 "K") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((pred type-eq-decl nil defined_types nil) (well_founded? const-decl "bool" orders nil) (measure_induction formula-decl nil measure_induction nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (wf_nat formula-decl nil naturalnumbers nil) (BS_inner_loop def-decl "[nat -> int]" sorting_tutorial_2 nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (BS_inner_loop_no_side_effects formula-decl nil sorting_tutorial_2 nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (BS_inner_loop_permutes_corollary formula-decl nil sorting_tutorial_2 nil)) 1039426 5920 t shostak)) (BS_outer_loop_no_side_effects 0 (BS_outer_loop_no_side_effects-1 nil 3351273060 3351273968 ("" (measure-induct+ "u-l" ("l" "u")) (("" (skolem 1 "A") (("" (skolem 1 "K") (("" (case "x!1=x!2") (("1" (replace -1 1 rl) (("1" (expand "BS_outer_loop" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (expand "BS_outer_loop" 2) (("2" (assert) (("2" (inst -1 "x!1" "x!2-1") (("2" (assert) (("2" (typepred "K") (("2" (inst -2 "BS_inner_loop(x!1, x!2, A)") (("2" (inst -2 "K") (("1" (lemma "BS_inner_loop_no_side_effects" (l "x!1" u "x!2" a "A")) (("1" (inst -1 "K") (("1" (ground) nil nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((BS_inner_loop def-decl "[nat -> int]" sorting_tutorial_2 nil) (BS_inner_loop_no_side_effects formula-decl nil sorting_tutorial_2 nil) (x!1 skolem-const-decl "nat" sorting_tutorial_2 nil) (x!2 skolem-const-decl "{i: nat | x!1 <= i}" sorting_tutorial_2 nil) (K skolem-const-decl "{i: nat | i < x!1 OR x!2 < i}" sorting_tutorial_2 nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (BS_outer_loop def-decl "[nat -> int]" sorting_tutorial_2 nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (wf_nat formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (naturalnumber type-eq-decl nil naturalnumbers nil) (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (measure_induction formula-decl nil measure_induction nil) (well_founded? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil)) 908630 4260 t shostak)) (BS_outer_loop_sorts 0 (BS_outer_loop_sorts-1 nil 3351271695 3351275084 ("" (measure-induct+ "u-l" ("l" "u")) (("" (skolem 1 "A") (("" (case "x!1=x!2") (("1" (replace -1 1 rl) (("1" (expand "BS_outer_loop" 1) (("1" (expand "sorted?" 1) (("1" (skolem 1 "J") nil nil)) nil)) nil)) nil) ("2" (expand "BS_outer_loop" 2) (("2" (lift-if) (("2" (assert) (("2" (inst -1 "x!1" "x!2-1") (("2" (assert) (("2" (inst -1 "BS_inner_loop(x!1, x!2, A)") (("2" (lemma "BS_inner_loop_correct") (("2" (inst -1 "x!1" "x!2" "A") (("2" (beta) (("2" (name-replace "AA" "BS_inner_loop(x!1, x!2, A)") (("2" (expand "sorted?" 2) (("2" (skolem 2 "J") (("2" (typepred "J") (("2" (expand "sorted?" -4) (("2" (inst -4 "J") (("2" (case "J = x!2-1") (("1" (replace -1) (("1" (simplify) (("1" (inst -4 "x!2-1") (("1" (ground) (("1" (reveal -6) (("1" (inst -1 "x!1" "x!2") (("1" (ground) (("1" (inst -1 "AA") (("1" (postpone) nil nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished nil 1086505 4080 t shostak)) (BS_sorted 0 (BS_sorted-1 nil 3351270883 3351271107 ("" (skolem 1 "A") (("" (expand "BSort" 1) (("" (postpone) nil nil)) nil)) nil) unfinished nil 83318 250 t shostak)))