diff options
| author | Camil Staps | 2016-03-23 22:48:31 +0100 |
|---|---|---|
| committer | Camil Staps | 2016-03-23 22:48:31 +0100 |
| commit | dc939bc8e5e2578b325f748537f4f8591e07be3e (patch) | |
| tree | e3d164368dd704e9fee5029e915f9e10b6e3a2bf | |
| parent | Assignment 7 (diff) | |
Start assignment 8
| -rw-r--r-- | assignment8/qs.prf | 1706 | ||||
| -rw-r--r-- | assignment8/qs.pvs | 150 |
2 files changed, 1856 insertions, 0 deletions
diff --git a/assignment8/qs.prf b/assignment8/qs.prf new file mode 100644 index 0000000..1467ace --- /dev/null +++ b/assignment8/qs.prf @@ -0,0 +1,1706 @@ +(my_list_induction + (less_wf 0 + (less_wf-1 nil 3667405436 + ("" (expand "well_founded?") + (("" (skolem 1 P) + (("" (flatten) + (("" (skolem -1 Y) + (("" (expand "less") + (("" (lemma naturalnumbers.wf_nat) + (("" (expand "well_founded?") + (("" + (inst -1 "(LAMBDA(n:nat):EXISTS(l:(P)):length(l)=n)") + (("" (split) + (("1" (skosimp*) + (("1" (typepred y!1) + (("1" (skolem -1 L) + (("1" (inst 1 L) + (("1" (skolem 1 G) + (("1" + (inst -2 "length(G)") + (("1" (assert) nil nil) + ("2" + (typepred G) + (("2" (inst 1 G) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (grind) + (("2" (inst 1 "length(Y)") + (("2" (inst 1 Y) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((well_founded? const-decl "bool" orders nil) + (less const-decl "bool" my_list_induction nil) + (NOT const-decl "[bool -> bool]" booleans nil) + (P skolem-const-decl "pred[list[X]]" my_list_induction nil) + (G skolem-const-decl "(P)" my_list_induction nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (length def-decl "nat" list_props nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (list type-decl nil list_adt nil) + (X formal-type-decl nil my_list_induction nil) + (pred type-eq-decl nil defined_types nil) + (nat nonempty-type-eq-decl nil naturalnumbers 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) + (wf_nat formula-decl nil naturalnumbers nil)) + shostak)) + (list_length_induction 0 + (list_length_induction-1 nil 3667403384 + ("" (lemma "wf_induction[list[X],less].wf_induction") + (("1" (propax) nil nil) ("2" (rewrite less_wf) nil nil)) nil) + ((less_wf formula-decl nil my_list_induction nil) + (pred type-eq-decl nil defined_types nil) + (well_founded? const-decl "bool" orders nil) + (wf_induction formula-decl nil wf_induction nil) + (X formal-type-decl nil my_list_induction nil) + (list type-decl nil list_adt nil) + (boolean nonempty-type-decl nil booleans nil) + (bool nonempty-type-eq-decl nil booleans nil) + (less const-decl "bool" my_list_induction nil)) + shostak))) +(my_list_props + (occ_TCC1 0 + (occ_TCC1-1 nil 3667035231 ("" (termination-tcc) nil nil) + ((real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (length def-decl "nat" list_props nil)) + nil)) + (occ_TCC2 0 + (occ_TCC2-1 nil 3667035231 ("" (termination-tcc) nil nil) + ((real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (length def-decl "nat" list_props nil)) + nil)) + (occ_nth 0 + (occ_nth-1 nil 3667035247 + ("" (induct l) + (("1" (grind) nil nil) + ("2" (skolem 1 (HD TL)) + (("2" (flatten) + (("2" (expand nth 1) + (("2" (skeep) + (("2" (expand occ -2) + (("2" (lift-if) + (("2" (split -2) + (("1" (flatten) + (("1" (inst 1 0) + (("1" (assert) (("1" (grind) nil nil)) nil)) + nil)) + nil) + ("2" (flatten) + (("2" (inst -2 x) + (("2" (assert) + (("2" (skolem -2 I) + (("2" (flatten) + (("2" (inst 2 "I+1") + (("2" + (assert) + (("2" (grind) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (real_gt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (list_induction formula-decl nil list_adt nil) + (X formal-type-decl nil my_list_props nil) + (nth def-decl "T" list_props nil) + (below type-eq-decl nil nat_types nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (length def-decl "nat" list_props nil) + (< const-decl "bool" reals nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (occ def-decl "nat" my_list_props nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (>= const-decl "bool" reals 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) + (> const-decl "bool" reals 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) + (number nonempty-type-decl nil numbers nil) + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (bool nonempty-type-eq-decl nil booleans nil) + (boolean nonempty-type-decl nil booleans nil) + (list type-decl nil list_adt nil)) + shostak)) + (nth_occ 0 + (nth_occ-1 nil 3667036386 + ("" (induct l) + (("1" (grind) nil nil) + ("2" (skolem 1 (HD TL)) + (("2" (flatten) + (("2" (skeep) + (("2" (expand nth 1) + (("2" (lift-if 1) + (("2" (expand occ 1) + (("2" (split 1) + (("1" (assert) + (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) + ("2" (flatten) + (("2" (lift-if 2) + (("2" (split 2) + (("1" (flatten) + (("1" (inst -2 "i-1") + (("1" (split -2) + (("1" (assert) nil nil) + ("2" + (expand length -2) + (("2" (assert) nil nil)) + nil)) + nil) + ("2" (assert) nil nil)) + nil)) + nil) + ("2" (flatten) + (("2" (inst -1 "i-1") + (("1" (split) + (("1" (propax) nil nil) + ("2" + (expand length -1) + (("2" (assert) nil nil)) + nil)) + nil) + ("2" (assert) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((real_gt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (- const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (int_minus_int_is_int application-judgement "int" integers nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (list_induction formula-decl nil list_adt nil) + (X formal-type-decl nil my_list_props nil) + (nth def-decl "T" list_props nil) + (below type-eq-decl nil nat_types nil) + (occ def-decl "nat" my_list_props nil) + (> const-decl "bool" reals nil) + (length def-decl "nat" list_props nil) + (< const-decl "bool" reals nil) + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (nat nonempty-type-eq-decl nil naturalnumbers 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) + (number nonempty-type-decl nil numbers nil) + (boolean nonempty-type-decl nil booleans nil) + (list type-decl nil list_adt nil)) + shostak)) + (perm_null 0 + (perm_null-1 nil 3667035958 + ("" (skeep) + (("" (lemma "list_cons_eta[X]") + (("" (inst -1 l) + (("1" (replace -1 -2 rl) + (("1" (expand "perm?") + (("1" (inst -2 "car(l)") + (("1" (expand "occ") (("1" (assert) nil nil)) nil)) nil)) + nil)) + nil) + ("2" (assert) nil nil)) + nil)) + nil)) + nil) + ((X formal-type-decl nil my_list_props nil) + (list_cons_eta formula-decl nil list_adt nil) + (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (occ def-decl "nat" my_list_props nil) + (perm? const-decl "bool" my_list_props nil) + (list type-decl nil list_adt nil) + (boolean nonempty-type-decl nil booleans nil) + (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil)) + shostak)) + (perm_commutative 0 + (perm_commutative-1 nil 3667035748 + ("" (skeep) + (("" (expand "perm?") + (("" (skeep) (("" (inst -1 x) (("" (assert) nil nil)) nil)) nil)) + nil)) + nil) + ((perm? const-decl "bool" my_list_props nil) + (X formal-type-decl nil my_list_props nil)) + shostak)) + (append_occ 0 + (append_occ-1 nil 3667035804 + ("" (induct l1) + (("1" (grind) nil nil) + ("2" (skolem 1 (HD TL)) + (("2" (flatten) + (("2" (skeep) + (("2" (skeep) + (("2" (expand append 1) + (("2" (expand occ 1 (1 2)) + (("2" (lift-if) + (("2" (inst -1 l2) + (("2" (inst -1 x) (("2" (assert) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (list_induction formula-decl nil list_adt nil) + (X formal-type-decl nil my_list_props nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (append def-decl "list[T]" list_props nil) + (occ def-decl "nat" my_list_props nil) + (nat nonempty-type-eq-decl nil naturalnumbers 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) + (= const-decl "[T, T -> boolean]" equalities nil) + (number nonempty-type-decl nil numbers nil) + (boolean nonempty-type-decl nil booleans nil) + (list type-decl nil list_adt nil)) + shostak)) + (length_append 0 + (length_append-1 nil 3667457451 ("" (induct-and-simplify l1) nil nil) + ((list type-decl nil list_adt nil) + (boolean nonempty-type-decl nil booleans nil) + (number nonempty-type-decl nil numbers nil) + (= const-decl "[T, T -> boolean]" equalities 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) + (length def-decl "nat" list_props nil) + (append def-decl "list[T]" list_props nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (X formal-type-decl nil my_list_props nil) + (list_induction formula-decl nil list_adt nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil)) + shostak)) + (nth_append_TCC1 0 + (nth_append_TCC1-1 nil 3667447307 + ("" (skeep) + (("" (lemma length_append) + (("" (inst? -1) (("" (assert) nil nil)) nil)) nil)) + nil) + ((length_append formula-decl nil my_list_props nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (list type-decl nil list_adt nil) + (X formal-type-decl nil my_list_props nil)) + nil)) + (nth_append_TCC2 0 + (nth_append_TCC2-1 nil 3667447307 ("" (subtype-tcc) nil nil) + ((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) + (int_minus_int_is_int application-judgement "int" integers nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (minus_odd_is_odd application-judgement "odd_int" integers nil)) + nil)) + (nth_append 0 + (nth_append-1 nil 3667447318 + ("" (induct l1) + (("1" (grind) nil nil) + ("2" (skolem 1 (H T)) + (("2" (flatten) + (("2" (skeep) + (("2" (skeep) + (("2" (inst -1 l2) + (("2" (expand append 1) + (("2" (lift-if 1) + (("2" (split 1) + (("1" (flatten 1) + (("1" (expand nth 1) + (("1" (lift-if) + (("1" (split) + (("1" (propax) nil nil) + ("2" (flatten) + (("2" + (inst -2 "i-1") + (("1" + (expand length -3 1) + (("1" + (split -2) + (("1" + (lift-if -1) + (("1" + (split -1) + (("1" (flatten -1) nil nil) + ("2" + (flatten -1) + (("2" (grind) nil nil)) + nil)) + nil)) + nil) + ("2" + (assert 1) + (("2" (grind 1) nil nil)) + nil)) + nil)) + nil) + ("2" + (expand length -1) + (("2" + (expand length -2 1) + (("2" (assert) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (flatten) + (("2" (assert 1) (("2" (grind 1) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("3" (skeep 1) (("3" (grind 1) nil nil)) nil) + ("4" (skeep 1) + (("4" (lemma length_append) + (("4" (inst? -1) + (("4" (replace -1 1) (("4" (propax) nil nil)) nil)) nil)) + nil)) + nil)) + nil) + ((minus_odd_is_odd application-judgement "odd_int" integers nil) + (int_minus_int_is_int application-judgement "int" integers nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (append def-decl "list[T]" list_props nil) + (length def-decl "nat" list_props nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (< const-decl "bool" reals nil) + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (nat nonempty-type-eq-decl nil naturalnumbers 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) + (list type-decl nil list_adt nil) + (- const-decl "[numfield, numfield -> numfield]" number_fields nil) + (NOT const-decl "[bool -> bool]" booleans nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (below type-eq-decl nil nat_types nil) + (nth def-decl "T" list_props nil) + (IF const-decl "[boolean, T, T -> T]" if_def nil) + (X formal-type-decl nil my_list_props nil) + (list_induction formula-decl nil list_adt nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (i skolem-const-decl "nat" my_list_props nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (int_plus_int_is_int application-judgement "int" integers nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (length_append formula-decl nil my_list_props nil)) + shostak))) +(SPLIT + (split_TCC1 0 + (split_TCC1-1 nil 3667407453 ("" (termination-tcc) nil nil) + ((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) + (PRED type-eq-decl nil defined_types nil) + (list type-decl nil list_adt nil) + (AND const-decl "[bool, bool -> bool]" 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) + (>= const-decl "bool" reals nil) + (int nonempty-type-eq-decl nil integers nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (length def-decl "nat" list_props nil)) + nil)) + (split_length 0 + (split_length-1 nil 3667407485 ("" (induct-and-simplify l) nil nil) + ((list type-decl nil list_adt nil) + (PRED type-eq-decl nil defined_types nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (length def-decl "nat" list_props nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (split def-decl "[list[nat], list[nat]]" SPLIT nil) + (nat nonempty-type-eq-decl nil naturalnumbers 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) + (list_induction formula-decl nil list_adt nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil)) + shostak)) + (split_occ 0 + (split_occ-1 nil 3667407525 ("" (induct-and-simplify l) nil nil) + ((list type-decl nil list_adt nil) + (PRED type-eq-decl nil defined_types nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (occ def-decl "nat" my_list_props nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (split def-decl "[list[nat], list[nat]]" SPLIT nil) + (nat nonempty-type-eq-decl nil naturalnumbers 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) + (list_induction formula-decl nil list_adt nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil)) + shostak)) + (split_lwb_upb 0 + (split_lwb_upb-1 nil 3667407762 + ("" (assert) + (("" (induct l) + (("1" (grind) nil nil) + ("2" (skolem 1 (H T)) + (("2" (flatten) (("2" (postpone) nil nil)) nil)) nil)) + nil)) + nil) + ((list type-decl nil list_adt nil) + (PRED type-eq-decl nil defined_types nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (upb const-decl "bool" SPLIT nil) + (split def-decl "[list[nat], list[nat]]" SPLIT nil) + (lwb const-decl "bool" SPLIT nil) + (nat nonempty-type-eq-decl nil naturalnumbers 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) + (list_induction formula-decl nil list_adt nil) + (length def-decl "nat" list_props nil) + (nth def-decl "T" list_props nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (int_minus_int_is_int application-judgement "int" integers nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (- const-decl "[numfield, numfield -> numfield]" number_fields nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil)) + shostak))) +(QS + (qs_TCC1 0 + (qs_TCC1-1 nil 3329457968 + ("" (skosimp*) + (("" (lemma split_length) + (("" (inst? -1) + (("" (assert) + (("" (replace -2) + (("" (expand length 1 2) (("" (assert) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((split_length formula-decl nil SPLIT nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (length def-decl "nat" list_props nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (PRED type-eq-decl nil defined_types nil) + (list type-decl nil list_adt nil) + (nat nonempty-type-eq-decl nil naturalnumbers 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)) + nil)) + (qs_TCC2 0 + (qs_TCC2-1 nil 3329457968 + ("" (skosimp*) + (("" (replace -1) + (("" (expand length 1 2) + (("" (lemma split_length) + (("" (inst? -1) (("" (assert) nil nil)) nil)) nil)) + nil)) + nil)) + nil) + ((split_length formula-decl nil SPLIT nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (PRED type-eq-decl nil defined_types nil) + (list type-decl nil list_adt nil) + (nat nonempty-type-eq-decl nil naturalnumbers 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) + (length def-decl "nat" list_props nil)) + nil))) +(SORTED + (sorted?_TCC1 0 + (sorted?_TCC1-1 nil 3667449016 ("" (termination-tcc) nil nil) + ((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) + (PRED type-eq-decl nil defined_types nil) + (list type-decl nil list_adt nil) + (AND const-decl "[bool, bool -> bool]" 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) + (>= const-decl "bool" reals nil) + (int nonempty-type-eq-decl nil integers nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil)) + nil)) + (sorted_append 0 + (sorted_append-1 nil 3667449025 + ("" (skeep) + (("" (expand sorted? 1) + (("" (skeep) + (("" (lemma nth_append) + (("" (inst -1 l1 l2 i) + (("" (lemma nth_append) + (("" (inst -1 l1 l2 j) + (("" (split -2) + (("1" (lift-if -1) + (("1" (split -1) + (("1" (flatten -1) + (("1" (replace -2 1) + (("1" (split -3) + (("1" (lift-if -1) + (("1" + (split -1) + (("1" + (flatten -1) + (("1" + (replace -2 1) + (("1" + (expand sorted? -5) + (("1" + (inst -5 i j) + (("1" + (split -5) + (("1" (propax) nil nil) + ("2" (propax) nil nil) + ("3" (propax) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" + (flatten -1) + (("2" + (lemma length_append) + (("2" + (inst -1 l1 l2) + (("2" + (replace -1 -10) + (("2" + (assert) + (("2" (grind 1) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (lemma length_append) + (("2" + (inst -1 l1 l2) + (("2" + (replace -1 -9) + (("2" (propax) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (flatten -1) + (("2" (replace -1 2) + (("2" (split -2) + (("1" (lift-if -1) + (("1" + (split -1) + (("1" + (flatten -1) + (("1" (assert) nil nil)) + nil) + ("2" + (flatten -1) + (("2" + (lemma length_append) + (("2" + (inst -1 l1 l2) + (("2" + (replace -1 -9) + (("2" + (assert 1) + (("2" + (replace -2 3) + (("2" + (assert 3) + (("2" + (expand sorted? -5) + (("2" + (inst + -5 + (i-length (l1)) + (j-length (l1))) + (("1" + (split -5) + (("1" + (propax) + nil + nil) + ("2" + (assert 1) + (("2" + (grind 1) + nil + nil)) + nil) + ("3" + (grind 1) + nil + nil)) + nil) + ("2" + (assert) + nil + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (lemma length_append) + (("2" + (inst -1 l1 l2) + (("2" + (replace -1 -8) + (("2" (propax) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (split -1) + (("1" (lift-if -1) + (("1" (split -1) + (("1" (flatten -1) + (("1" (assert 1) (("1" (grind 1) nil nil)) + nil)) + nil) + ("2" (lemma length_append) + (("2" (inst -1 l1 l2) + (("2" (replace -1 -8) + (("2" + (assert 1) + (("2" (grind 1) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (lemma length_append) + (("2" (inst -1 l1 l2) + (("2" (replace -1 -7) (("2" (propax) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((list type-decl nil list_adt nil) + (PRED type-eq-decl nil defined_types nil) + (every adt-def-decl "boolean" list_adt nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (int_plus_int_is_int application-judgement "int" integers nil) + (i skolem-const-decl "nat" SORTED nil) + (l1 skolem-const-decl "list[nat]" SORTED nil) + (length_append formula-decl nil my_list_props nil) + (nth def-decl "T" list_props nil) (upb const-decl "bool" SPLIT nil) + (lwb const-decl "bool" SPLIT nil) + (length def-decl "nat" list_props nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (- const-decl "[numfield, numfield -> numfield]" number_fields nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (int_minus_int_is_int application-judgement "int" integers nil) + (minus_odd_is_odd application-judgement "odd_int" integers nil) + (real_le_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (nth_append formula-decl nil my_list_props 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) + (sorted? const-decl "bool" SORTED nil)) + shostak))) +(QS_props + (qs_perm 0 + (qs_perm-1 nil 3658125991 + ("" (lemma list_length_induction) + (("" (inst? -1) + (("" (copy -1) + (("" (split -1) + (("1" (propax) nil nil) + ("2" (skeep 1) + (("2" (expand qs 1) + (("2" (lift-if 1) + (("2" (split 1) + (("1" (flatten 1) (("1" (grind 1) nil nil)) nil) + ("2" (flatten 1) + (("2" (assert 2) + (("2" (expand perm? 2) + (("2" (skeep 2) + (("2" (lemma append_occ) + (("2" + (inst -1 "qs(split(car(g),cdr(g))`1)" + "cons(car(g),qs(split(car(g),cdr(g))`2))" + x) + (("2" + (replace -1 2) + (("2" + (lemma split_occ) + (("2" + (inst -1 "car(g)" "cdr(g)") + (("2" + (assert -1) + (("2" + (inst -1 x) + (("2" + (lemma split_length) + (("2" + (inst -1 "car(g)" "cdr(g)") + (("2" + (assert -1) + (("2" + (expand occ 2 3) + (("2" + (lift-if 2) + (("2" + (split 2) + (("1" + (flatten 1) + nil + nil) + ("2" + (flatten 1) + (("2" + (split 2) + (("1" + (flatten 1) + (("1" + (expand + occ + 1 + 2) + (("1" + (lift-if + 1) + (("1" + (split + 1) + (("1" + (flatten + 1) + (("1" + (assert + 1) + (("1" + (copy + -6) + (("1" + (inst + -1 + "split(car(g),cdr(g))`1") + (("1" + (split + -1) + (("1" + (inst + -7 + "split(car(g),cdr(g))`2") + (("1" + (split + -7) + (("1" + (expand + perm? + (-1 + -2)) + (("1" + (inst + -1 + x) + (("1" + (inst + -2 + x) + (("1" + (replace + -1 + 1) + (("1" + (replace + -2 + 1) + (("1" + (assert + 1) + (("1" + (replace + -6 + 1) + (("1" + (propax) + nil + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" + (expand + less + 1) + (("2" + (grind + 1) + nil + nil)) + nil)) + nil)) + nil) + ("2" + (grind + 1) + nil + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" + (flatten + 1) + nil + nil)) + nil)) + nil)) + nil)) + nil) + ("2" + (flatten 1) + (("2" + (expand + occ + 2 + 2) + (("2" + (lift-if + 2) + (("2" + (split + 2) + (("1" + (flatten + 1) + nil + nil) + ("2" + (flatten + 1) + (("2" + (copy + -4) + (("2" + (inst + -1 + "split(car(g),cdr(g))`1") + (("2" + (inst + -5 + "split(car(g),cdr(g))`2") + (("2" + (split + -1) + (("1" + (expand + perm? + -1) + (("1" + (inst + -1 + x) + (("1" + (replace + -1 + 2) + (("1" + (split + -5) + (("1" + (expand + perm? + -1) + (("1" + (inst + -1 + x) + (("1" + (replace + -1 + 2) + (("1" + (replace + -4 + 2) + (("1" + (propax) + nil + nil)) + nil)) + nil)) + nil)) + nil) + ("2" + (grind + 1) + nil + nil)) + nil)) + nil)) + nil)) + nil) + ("2" + (grind + 1) + nil + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((list type-decl nil list_adt nil) + (PRED type-eq-decl nil defined_types nil) + (every adt-def-decl "boolean" list_adt nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (pred type-eq-decl nil defined_types nil) + (perm? const-decl "bool" my_list_props nil) + (qs def-decl "list[nat]" QS nil) + (occ def-decl "nat" my_list_props nil) + (split def-decl "[list[nat], list[nat]]" SPLIT nil) + (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) + (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) + (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) + (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) + (split_occ formula-decl nil SPLIT nil) + (split_length formula-decl nil SPLIT nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (length def-decl "nat" list_props nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (less const-decl "bool" my_list_induction nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (append_occ formula-decl nil my_list_props nil) + (list_length_induction formula-decl nil my_list_induction 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)) + shostak)) + (occ_upb 0 + (occ_upb-1 nil 3658132514 + ("" (induct l) + (("1" (grind) nil nil) + ("2" (skolem 1 (H T)) + (("2" (flatten) + (("2" (skeep) + (("2" (skeep) + (("2" (inst? -1) + (("2" (split) + (("1" (expand occ -3) + (("1" (lift-if) + (("1" (split) + (("1" (flatten) + (("1" (expand upb -4) + (("1" (inst -4 0) + (("1" (expand length -4) + (("1" + (assert) + (("1" + (split) + (("1" (grind) nil nil) + ("2" (grind) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (flatten) + (("2" (inst -2 x) (("2" (assert) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (expand upb -1) + (("2" (expand upb 1) + (("2" (skeep) + (("2" (inst -2 "i+1") + (("2" (split) + (("1" (expand nth -1) + (("1" (propax) nil nil)) nil) + ("2" (expand length 1) + (("2" (assert) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((numfield nonempty-type-eq-decl nil number_fields nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (nth def-decl "T" list_props nil) + (real_gt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (length def-decl "nat" list_props nil) + (list_induction formula-decl nil list_adt 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) + (occ def-decl "nat" my_list_props nil) + (> const-decl "bool" reals nil) (upb const-decl "bool" SPLIT nil) + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (PRED type-eq-decl nil defined_types nil) + (list type-decl nil list_adt nil)) + shostak)) + (occ_lwb 0 + (occ_lwb-1 nil 3658137865 + ("" (induct l) + (("1" (grind) nil nil) + ("2" (skolem 1 (H T)) + (("2" (flatten) + (("2" (skolem 1 N) + (("2" (flatten) + (("2" (skolem 1 X) + (("2" (flatten) + (("2" (inst? -1) + (("2" (split) + (("1" (expand occ -3) + (("1" (lift-if) + (("1" (split) + (("1" (expand "lwb") + (("1" (inst -3 0) + (("1" + (expand length -3) + (("1" + (assert) + (("1" + (split) + (("1" (grind) nil nil) + ("2" (assert) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (flatten) + (("2" (inst -2 X) (("2" (assert) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (expand lwb -1) + (("2" (expand lwb 1) + (("2" (skolem 1 I) + (("2" (flatten) + (("2" (inst -3 "I+1") + (("2" + (expand length -3) + (("2" + (assert) + (("2" + (expand nth 1) + (("2" (propax) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (nth def-decl "T" list_props nil) + (real_gt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (length def-decl "nat" list_props nil) + (list_induction formula-decl nil list_adt 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) + (NOT const-decl "[bool -> bool]" booleans nil) + (occ def-decl "nat" my_list_props nil) + (> const-decl "bool" reals nil) (lwb const-decl "bool" SPLIT nil) + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (PRED type-eq-decl nil defined_types nil) + (list type-decl nil list_adt nil)) + nil)) + (upb_perm 0 + (upb_perm-1 nil 3658132945 + ("" (skosimp*) + (("" (lemma occ_upb) + (("" (inst? -1) + (("" (assert) + (("" (expand "upb") + (("" (skosimp*) + (("" (expand "perm?") + (("" (lemma nth_occ) + (("" (inst? -1) + (("" (assert) + (("" (inst? -3) + (("" (lemma occ_nth) + (("" (inst -1 l!1 "nth(lp!1, i!1)") + (("" (assert) + (("" + (skosimp*) + (("" + (inst? -4) + (("" (assert) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((occ_upb formula-decl nil QS_props nil) + (nth_occ formula-decl nil my_list_props nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (occ_nth formula-decl nil my_list_props nil) + (real_gt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (< const-decl "bool" reals nil) + (length def-decl "nat" list_props nil) + (below type-eq-decl nil nat_types nil) + (nth def-decl "T" list_props nil) + (perm? const-decl "bool" my_list_props nil) + (upb const-decl "bool" SPLIT nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (PRED type-eq-decl nil defined_types nil) + (list type-decl nil list_adt nil) + (nat nonempty-type-eq-decl nil naturalnumbers 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)) + shostak)) + (lwb_perm 0 + (lwb_perm-1 nil 3658138209 + ("" (skosimp*) + (("" (lemma occ_lwb) + (("" (inst? -1) + (("" (assert) + (("" (expand "lwb") + (("" (skosimp*) + (("" (expand "perm?") + (("" (lemma nth_occ) + (("" (inst? -1) + (("" (assert) + (("" (inst? -3) + (("" (lemma occ_nth) + (("" (inst -1 l!1 "nth(lp!1, i!1)") + (("" (assert) + (("" + (skosimp*) + (("" + (inst? -4) + (("" (assert) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((occ_lwb formula-decl nil QS_props nil) + (nth_occ formula-decl nil my_list_props nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (occ_nth formula-decl nil my_list_props nil) + (real_gt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (< const-decl "bool" reals nil) + (length def-decl "nat" list_props nil) + (below type-eq-decl nil nat_types nil) + (nth def-decl "T" list_props nil) + (perm? const-decl "bool" my_list_props nil) + (lwb const-decl "bool" SPLIT nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (PRED type-eq-decl nil defined_types nil) + (list type-decl nil list_adt nil) + (nat nonempty-type-eq-decl nil naturalnumbers 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)) + nil)) + (qs_sorted 0 + (qs_sorted-1 nil 3658128963 + ("" (lemma list_length_induction) (("" (postpone) nil nil)) nil) + ((list type-decl nil list_adt nil) + (PRED type-eq-decl nil defined_types nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (pred type-eq-decl nil defined_types nil) + (sorted? const-decl "bool" SORTED nil) + (qs def-decl "list[nat]" QS nil) + (split_lwb_upb formula-decl nil SPLIT nil) + (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) + (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) + (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) + (split_length formula-decl nil SPLIT nil) + (sorted_append formula-decl nil SORTED nil) + (lwb_perm formula-decl nil QS_props nil) + (qs_perm formula-decl nil QS_props nil) + (perm_commutative formula-decl nil my_list_props nil) + (nth def-decl "T" list_props nil) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (real_le_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (- const-decl "[numfield, numfield -> numfield]" number_fields nil) + (int_minus_int_is_int application-judgement "int" integers nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (lwb const-decl "bool" SPLIT nil) + (upb_perm formula-decl nil QS_props nil) + (less const-decl "bool" my_list_induction nil) + (split def-decl "[list[nat], list[nat]]" SPLIT nil) + (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (length def-decl "nat" list_props nil) + (list_length_induction formula-decl nil my_list_induction 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)) + shostak))) + diff --git a/assignment8/qs.pvs b/assignment8/qs.pvs new file mode 100644 index 0000000..086321a --- /dev/null +++ b/assignment8/qs.pvs @@ -0,0 +1,150 @@ +my_list_induction[X:TYPE] : THEORY +BEGIN + less(l1,l2: list[X]) : bool = length(l1) < length(l2) + + less_wf: LEMMA well_founded?(less) % :-) + + list_length_induction :LEMMA % :-) + (FORALL (p:pred[list[X]]): + (FORALL (g:list[X]): + (FORALL (s:list[X]): + less(s,g) IMPLIES p(s)) + IMPLIES p(g)) + IMPLIES (FORALL (l:list[X]): p(l))) + +END my_list_induction + +my_list_props[X:TYPE] : THEORY +BEGIN + occ(x:X,l:list[X]) : RECURSIVE nat = + CASES l + OF null : 0 , + cons(y,l) : IF x=y THEN occ(x,l)+1 ELSE occ(x,l) ENDIF + ENDCASES + MEASURE length(l) + + occ_nth: LEMMA + FORALL(l:list[X]): FORALL(x:X): occ(x,l) > 0 IMPLIES + EXISTS(i:nat): i<length(l) AND nth(l,i) = x + + nth_occ: LEMMA + FORALL(l:list[X]): FORALL(i:nat): i<length(l) IMPLIES occ(nth(l,i),l) > 0 + + perm?( l1,l2 : list[X]) : bool = FORALL(x:X): occ(x,l1) = occ(x,l2) + + perm_null: LEMMA % :-) + FORALL(l:list[X]): perm?(null, l) IMPLIES l = null + + perm_commutative: LEMMA % :-) + FORALL(l1,l2: list[X]):perm?(l1,l2) IMPLIES perm?(l2,l1) + + append_occ: LEMMA % :-) + FORALL( l1,l2:list[X] ): FORALL(x:X): occ(x,append(l1,l2)) = occ(x,l1)+occ(x,l2) + + length_append: LEMMA % :-) + FORALL( l1,l2:list[X] ):length(append(l1,l2)) = length(l1) + length(l2) + + nth_append: LEMMA % :-( to be done + FORALL( l1,l2:list[X] ): FORALL(i:nat): i < length(l1)+length(l2) IMPLIES + nth(append(l1,l2),i) = IF i < length(l1) THEN nth(l1,i) ELSE nth(l2,i-length(l1)) ENDIF + +END my_list_props + + +SPLIT : THEORY +BEGIN + IMPORTING my_list_props + + split (m: nat, l : list[nat]) : RECURSIVE [list[nat], list[nat]] = + CASES l OF + null : (null, null), + cons(h,t) : LET + (l,r) = split (m, t) + IN + IF h < m + THEN (cons(h,l),r) + ELSE (l,cons(h,r)) + ENDIF + ENDCASES + MEASURE (length(l)) + + split_length: LEMMA % :-) + FORALL( m:nat, l:list[nat] ): LET s = split(m,l) IN length(l) = length(s`1) + length(s`2) + + split_occ: LEMMA % :-) + FORALL( n: nat, l:list[nat] ): LET s = split(n, l) IN FORALL(x:nat):occ(x,l) = occ(x,s`1)+occ(x,s`2) + + upb( g:nat, l:list[nat] ): bool = + FORALL(i:nat): i < length(l) IMPLIES nth(l,i) < g + + lwb( s:nat, l:list[nat] ): bool = + FORALL(i:nat): i < length(l) IMPLIES NOT nth(l,i) < s + + split_lwb_upb: LEMMA % :-( to be done + FORALL( m:nat, l:list[nat] ): LET s = split(m,l) IN upb(m,s`1) AND lwb(m,s`2) + +END SPLIT + +QS : THEORY +BEGIN + IMPORTING SPLIT + qs (l : list[nat]) : RECURSIVE list[nat] = + CASES l OF + null : null, + cons(h,t) : LET + (l,r) = split (h, t) + IN + append(qs(l),cons(h,qs(r))) + ENDCASES + MEASURE (length(l)) + +END QS + +SORTED: THEORY +BEGIN + IMPORTING my_list_props[nat] + IMPORTING SPLIT + + sorted?(l:list[nat]) : bool = + FORALL (i,j: nat): i < j AND j < length(l) IMPLIES nth(l,i) <= nth(l,j) + + sorted_append: LEMMA % :-( to be done + FORALL( m:nat, l1,l2:list[nat] ): + sorted?(l1) AND sorted?(l2) and upb(m,l1) AND lwb(m,l2) + IMPLIES sorted?(append(l1,l2)) +END SORTED + +QS_props : THEORY +BEGIN + IMPORTING QS, SORTED + IMPORTING my_list_props[nat], my_list_induction[nat] + + qs_perm: LEMMA % :-( to be done + FORALL(l:list[nat]):perm?(qs(l),l) + + occ_upb: LEMMA % :-) + FORALL( n: nat, l:list[nat] ): upb(n,l) IMPLIES + (FORALL(x:nat):occ(x,l) > 0 IMPLIES x < n) + + occ_lwb: LEMMA % :-) + FORALL( n: nat, l:list[nat] ): lwb(n,l) IMPLIES + (FORALL(x:nat):occ(x,l) > 0 IMPLIES NOT x < n) + + upb_perm: LEMMA % :-) + FORALL(l, lp: list[nat]): perm?(l,lp) IMPLIES + FORALL(n:nat): upb(n,l) IMPLIES upb(n,lp) + + lwb_perm: LEMMA % :-) + FORALL(l, lp: list[nat]): perm?(l,lp) IMPLIES + FORALL(n:nat): lwb(n,l) IMPLIES lwb(n,lp) + + qs_sorted :LEMMA % :-( to be done + FORALL (l:list[nat]): sorted?(qs(l)) + +% tl : VAR list[nat] + +% test : LEMMA +% qs ((:4,3,6,2,5:)) = tl + + +END QS_props |