diff options
| -rw-r--r-- | assignment8/qs.prf | 1508 | ||||
| -rw-r--r-- | assignment8/qs.status | 46 |
2 files changed, 1067 insertions, 487 deletions
diff --git a/assignment8/qs.prf b/assignment8/qs.prf index 1467ace..a7790ca 100644 --- a/assignment8/qs.prf +++ b/assignment8/qs.prf @@ -74,32 +74,32 @@ (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) + ((less const-decl "bool" my_list_induction nil) (bool nonempty-type-eq-decl nil booleans nil) - (less const-decl "bool" my_list_induction nil)) + (boolean nonempty-type-decl nil booleans nil) + (list type-decl nil list_adt nil) + (X formal-type-decl nil my_list_induction nil) + (wf_induction formula-decl nil wf_induction nil) + (well_founded? const-decl "bool" orders nil) + (pred type-eq-decl nil defined_types nil) + (less_wf formula-decl nil 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) + ((length def-decl "nat" list_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) - (length def-decl "nat" list_props nil)) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_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) + ((length def-decl "nat" list_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) - (length def-decl "nat" list_props nil)) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil)) nil)) (occ_nth 0 (occ_nth-1 nil 3667035247 @@ -141,42 +141,42 @@ nil)) nil)) nil) - ((nnint_plus_posint_is_posint application-judgement "posint" - integers nil) - (real_gt_is_strict_total_order name-judgement + ((list type-decl nil list_adt nil) + (boolean nonempty-type-decl nil booleans nil) + (bool nonempty-type-eq-decl nil booleans nil) + (IMPLIES const-decl "[bool, 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) + (>= const-decl "bool" reals nil) + (nat nonempty-type-eq-decl nil naturalnumbers nil) + (occ def-decl "nat" my_list_props nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (< const-decl "bool" reals nil) + (length def-decl "nat" list_props nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (below type-eq-decl nil nat_types nil) + (nth def-decl "T" list_props nil) + (X formal-type-decl nil my_list_props nil) + (list_induction formula-decl nil list_adt nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields 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_lt_is_strict_total_order name-judgement + (real_gt_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)) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil)) shostak)) (nth_occ 0 (nth_occ-1 nil 3667036386 @@ -229,41 +229,42 @@ nil)) nil)) nil) - ((real_gt_is_strict_total_order name-judgement + ((list type-decl nil list_adt nil) + (boolean nonempty-type-decl nil 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) + (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) + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (< const-decl "bool" reals nil) + (length def-decl "nat" list_props nil) + (> const-decl "bool" reals nil) + (occ def-decl "nat" my_list_props nil) + (below type-eq-decl nil nat_types nil) + (nth def-decl "T" list_props 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) + (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) + (i skolem-const-decl "nat" my_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_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)) + (real_gt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil)) shostak)) (perm_null 0 (perm_null-1 nil 3667035958 @@ -280,16 +281,17 @@ 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) + ((l skolem-const-decl "list[X]" my_list_props nil) + (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) + (boolean nonempty-type-decl nil booleans nil) + (list type-decl nil list_adt nil) + (perm? const-decl "bool" my_list_props nil) + (occ def-decl "nat" my_list_props 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)) + (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) + (list_cons_eta formula-decl nil list_adt nil) + (X formal-type-decl nil my_list_props nil)) shostak)) (perm_commutative 0 (perm_commutative-1 nil 3667035748 @@ -298,8 +300,8 @@ (("" (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)) + ((X formal-type-decl nil my_list_props nil) + (perm? const-decl "bool" my_list_props nil)) shostak)) (append_occ 0 (append_occ-1 nil 3667035804 @@ -323,35 +325,6 @@ 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) @@ -368,56 +341,85 @@ (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) + (occ def-decl "nat" my_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" + (posint_plus_nnint_is_posint application-judgement "posint" integers nil) - (nnint_plus_posint_is_posint application-judgement "posint" + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) shostak)) + (length_append 0 + (length_append-1 nil 3667457451 ("" (induct-and-simplify l1) nil nil) + ((nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + 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) + (length def-decl "nat" 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)) (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) + ((X formal-type-decl nil my_list_props 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) + (length_append formula-decl nil my_list_props nil)) + nil)) + (nth_append_TCC2 0 + (nth_append_TCC2-1 nil 3667447307 ("" (subtype-tcc) nil nil) + ((minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) - (minus_odd_is_odd application-judgement "odd_int" 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) + (int_minus_int_is_int application-judgement "int" integers nil) + (nat nonempty-type-eq-decl nil naturalnumbers 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) + (NOT const-decl "[bool -> bool]" booleans nil) + (bool nonempty-type-eq-decl nil booleans nil) + (boolean nonempty-type-decl nil booleans nil)) nil)) (nth_append 0 (nth_append-1 nil 3667447318 @@ -541,46 +543,16 @@ (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) + ((length def-decl "nat" list_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) + (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) (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) + (>= const-decl "bool" reals 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) @@ -589,49 +561,82 @@ (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) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (every adt-def-decl "boolean" list_adt nil) + (list type-decl nil list_adt nil) + (PRED type-eq-decl nil defined_types 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" + (NOT const-decl "[bool -> bool]" booleans nil) + (bool nonempty-type-eq-decl nil booleans nil) + (boolean nonempty-type-decl nil booleans nil)) + nil)) + (split_length 0 + (split_length-1 nil 3667407485 ("" (induct-and-simplify l) nil nil) + ((posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (nnint_plus_posint_is_posint application-judgement "posint" 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" + (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) + (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) + (split def-decl "[list[nat], list[nat]]" SPLIT nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (length def-decl "nat" list_props nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (every adt-def-decl "boolean" list_adt nil) + (PRED type-eq-decl nil defined_types nil) + (list type-decl nil list_adt 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" + ((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) - (posint_plus_nnint_is_posint application-judgement "posint" - integers nil)) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers 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) + (split def-decl "[list[nat], list[nat]]" SPLIT nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (occ def-decl "nat" my_list_props nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (every adt-def-decl "boolean" list_adt nil) + (PRED type-eq-decl nil defined_types nil) + (list type-decl nil list_adt nil)) shostak)) (split_lwb_upb 0 (split_lwb_upb-1 nil 3667407762 @@ -639,41 +644,140 @@ (("" (induct l) (("1" (grind) nil nil) ("2" (skolem 1 (H T)) - (("2" (flatten) (("2" (postpone) nil nil)) nil)) nil)) + (("2" (flatten) + (("2" (skeep 1) + (("2" (split 1) + (("1" (expand split 1) + (("1" (lift-if 1) + (("1" (split 1) + (("1" (flatten 1) + (("1" (expand upb 1) + (("1" (skeep 1) + (("1" (expand nth 1) + (("1" (lift-if 1) + (("1" + (split 1) + (("1" (flatten 1) nil nil) + ("2" + (flatten 1) + (("2" + (inst -3 "m") + (("2" + (flatten -3) + (("2" + (expand upb -3) + (("2" + (inst -3 "i-1") + (("1" + (split -3) + (("1" (propax) nil nil) + ("2" + (assert) + (("2" (grind 1) nil nil)) + nil)) + nil) + ("2" (assert) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (flatten) + (("2" (inst -1 m) (("2" (flatten -1) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (inst -1 m) + (("2" (flatten -1) + (("2" (expand split 1) + (("2" (lift-if 1) + (("2" (split 1) + (("1" (flatten 1) nil nil) + ("2" (flatten 1) + (("2" (expand lwb 2) + (("2" (skeep 2) + (("2" + (expand nth -2) + (("2" + (lift-if -2) + (("2" + (split -2) + (("1" (flatten -1) nil nil) + ("2" + (flatten -1) + (("2" + (expand lwb -4) + (("2" + (inst -4 "i-1") + (("1" + (split -4) + (("1" (propax) nil nil) + ("2" (grind 1) nil nil)) + nil) + ("2" (assert) 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) - (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) + ((i skolem-const-decl "nat" SPLIT 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" + (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement - "(strict_total_order?[real])" real_props nil)) + "(strict_total_order?[real])" real_props nil) + (i skolem-const-decl "nat" SPLIT 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) + (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) + (lwb const-decl "bool" SPLIT nil) + (split def-decl "[list[nat], list[nat]]" SPLIT nil) + (upb const-decl "bool" SPLIT nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (every adt-def-decl "boolean" list_adt nil) + (PRED type-eq-decl nil defined_types nil) + (list type-decl nil list_adt nil)) shostak))) (QS (qs_TCC1 0 @@ -689,31 +793,32 @@ 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" + ((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) + (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) + (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_props nil) - (posint_plus_nnint_is_posint application-judgement "posint" + (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)) + (real_lt_is_strict_total_order name-judgement + "(strict_total_order?[real])" real_props nil) + (split_length formula-decl nil SPLIT nil)) nil)) (qs_TCC2 0 (qs_TCC2-1 nil 3329457968 @@ -725,20 +830,43 @@ nil)) nil)) nil) - ((split_length formula-decl nil SPLIT nil) - (posint_plus_nnint_is_posint application-judgement "posint" + ((length def-decl "nat" 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) + (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) + (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_nnint_is_nnint application-judgement "nonneg_int" + (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) + (split_length formula-decl nil SPLIT nil)) + nil))) +(SORTED + (sorted?_TCC1 0 + (sorted?_TCC1-1 nil 3667449016 ("" (termination-tcc) nil 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) (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) + (>= const-decl "bool" reals 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) @@ -747,35 +875,14 @@ (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) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (every adt-def-decl "boolean" list_adt nil) + (list type-decl nil list_adt nil) + (PRED type-eq-decl nil defined_types 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)) + (bool nonempty-type-eq-decl nil booleans nil) + (boolean nonempty-type-decl nil booleans nil)) nil)) (sorted_append 0 (sorted_append-1 nil 3667449025 @@ -960,8 +1067,8 @@ (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) + (i skolem-const-decl "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) @@ -1277,47 +1384,47 @@ 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" + ((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_length_induction formula-decl nil my_list_induction nil) + (append_occ formula-decl nil my_list_props nil) + (posint_plus_nnint_is_posint application-judgement "posint" 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" + (less const-decl "bool" 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) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" 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)) + (split_length formula-decl nil SPLIT nil) + (split_occ formula-decl nil SPLIT nil) + (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt 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 def-decl "[list[nat], list[nat]]" SPLIT nil) + (occ def-decl "nat" my_list_props nil) + (qs def-decl "list[nat]" QS nil) + (perm? const-decl "bool" my_list_props nil) + (pred type-eq-decl nil defined_types nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (every adt-def-decl "boolean" list_adt nil) + (PRED type-eq-decl nil defined_types nil) + (list type-decl nil list_adt nil)) shostak)) (occ_upb 0 (occ_upb-1 nil 3658132514 @@ -1376,40 +1483,41 @@ 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 + ((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) + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (upb const-decl "bool" SPLIT nil) (> const-decl "bool" reals nil) + (occ def-decl "nat" my_list_props nil) + (< const-decl "bool" reals 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) + (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_lt_is_strict_total_order name-judgement + (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) - (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)) + (nth def-decl "T" list_props 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)) shostak)) (occ_lwb 0 (occ_lwb-1 nil 3658137865 @@ -1477,41 +1585,42 @@ 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 + ((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) + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (lwb const-decl "bool" SPLIT nil) (> const-decl "bool" reals nil) + (occ def-decl "nat" my_list_props nil) + (NOT const-decl "[bool -> bool]" booleans nil) + (< const-decl "bool" reals 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) + (real_gt_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 + (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) - (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)) + (posint_plus_nnint_is_posint application-judgement "posint" + integers 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)) nil)) (upb_perm 0 (upb_perm-1 nil 3658132945 @@ -1550,36 +1659,37 @@ 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 + ((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) + (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) + (upb const-decl "bool" SPLIT nil) + (perm? const-decl "bool" my_list_props nil) + (nth def-decl "T" list_props nil) + (below type-eq-decl nil nat_types nil) + (length def-decl "nat" list_props nil) + (< const-decl "bool" reals nil) + (real_gt_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 + (real_lt_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)) + (nth_occ formula-decl nil my_list_props nil) + (occ_upb formula-decl nil QS_props nil)) shostak)) (lwb_perm 0 (lwb_perm-1 nil 3658138209 @@ -1618,23 +1728,461 @@ 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 + ((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) + (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) + (lwb const-decl "bool" SPLIT nil) + (perm? const-decl "bool" my_list_props nil) + (nth def-decl "T" list_props nil) + (below type-eq-decl nil nat_types nil) + (length def-decl "nat" list_props nil) + (< const-decl "bool" reals nil) + (real_gt_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 + (real_lt_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) + (nth_occ formula-decl nil my_list_props nil) + (occ_lwb formula-decl nil QS_props nil)) + nil)) + (qs_sorted 0 + (qs_sorted-1 nil 3658128963 + ("" (lemma list_length_induction) + (("" (inst? -1) + (("" (split -1) + (("1" (propax) nil nil) + ("2" (skeep 1) + (("2" (expand qs 1) + (("2" (lift-if 1) + (("2" (split 1) + (("1" (grind 1) nil nil) + ("2" (flatten 1) + (("2" (assert 2) + (("2" (lemma sorted_append) + (("2" + (inst -1 "car(g)" "qs(split(car(g),cdr(g))`1)" + "cons(car(g),qs(split(car(g),cdr(g))`2))") + (("2" (split -1) + (("1" (propax) nil nil) + ("2" (copy -1) + (("2" (inst -1 "split(car(g),cdr(g))`1") + (("2" + (split -1) + (("1" (propax) nil nil) + ("2" + (lemma split_length) + (("2" + (inst -1 "car(g)" "cdr(g)") + (("2" + (assert -1) + (("2" + (expand less 1) + (("2" + (assert 1) + (("2" (grind 1) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("3" (expand sorted? 1) + (("3" (skeep 1) + (("3" + (expand nth 1) + (("3" + (lift-if 1) + (("3" + (split 1) + (("1" + (flatten 1) + (("1" + (lift-if 1) + (("1" + (split 1) + (("1" + (flatten 1) + (("1" (assert) nil nil)) + nil) + ("2" + (flatten 1) + (("2" + (lemma split_lwb_upb) + (("2" + (inst + -1 + "car(g)" + "cdr(g)") + (("2" + (assert -1) + (("2" + (flatten -1) + (("2" + (lemma lwb_perm) + (("2" + (inst + -1 + "split(car(g),cdr(g))`2" + "qs(split(car(g),cdr(g))`2)") + (("2" + (split -1) + (("1" + (inst + -1 + "car(g)") + (("1" + (split + -1) + (("1" + (expand + lwb + -1) + (("1" + (inst + -1 + "j-1") + (("1" + (split + -1) + (("1" + (assert) + nil + nil) + ("2" + (assert) + (("2" + (grind + 1) + nil + nil)) + nil)) + nil) + ("2" + (assert) + nil + nil)) + nil)) + nil) + ("2" + (propax) + nil + nil)) + nil)) + nil) + ("2" + (lemma + qs_perm) + (("2" + (inst + -1 + "split(car(g),cdr(g))`2") + (("2" + (lemma + perm_commutative) + (("2" + (inst + -1 + "qs(split(car(g),cdr(g))`2)" + "split(car(g),cdr(g))`2") + (("2" + (split + -1) + (("1" + (propax) + nil + nil) + ("2" + (propax) + nil + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" + (flatten 1) + (("2" + (lift-if 2) + (("2" + (split 2) + (("1" + (flatten 1) + (("1" (grind) nil nil)) + nil) + ("2" + (flatten 1) + (("2" + (inst + -3 + "split(car(g),cdr(g))`2") + (("2" + (split -3) + (("1" + (expand sorted? -1) + (("1" + (inst + -1 + "i-1" + "j-1") + (("1" + (split -1) + (("1" + (propax) + nil + nil) + ("2" + (assert) + nil + nil) + ("3" + (assert) + (("3" + (grind 1) + nil + nil)) + nil)) + nil) + ("2" + (assert) + nil + nil) + ("3" + (assert) + nil + nil)) + nil)) + nil) + ("2" + (lemma split_length) + (("2" + (inst? -1) + (("2" + (assert -1) + (("2" + (grind 1) + nil + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("4" (lemma split_lwb_upb) + (("4" (inst -1 "car(g)" "cdr(g)") + (("4" + (assert -1) + (("4" + (flatten -1) + (("4" + (lemma upb_perm) + (("4" + (inst + -1 + "split(car(g),cdr(g))`1" + "qs(split(car(g),cdr(g))`1)") + (("4" + (split -1) + (("1" + (inst -1 "car(g)") + (("1" + (split -1) + (("1" (propax) nil nil) + ("2" (propax) nil nil)) + nil)) + nil) + ("2" + (lemma qs_perm) + (("2" + (inst? -1) + (("2" + (lemma perm_commutative) + (("2" + (inst + -1 + "qs(split(car(g),cdr(g))`1)" + "split(car(g),cdr(g))`1") + (("2" + (split -1) + (("1" + (propax) + nil + nil) + ("2" + (propax) + nil + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("5" (lemma split_lwb_upb) + (("5" (inst -1 "car(g)" "cdr(g)") + (("5" + (assert -1) + (("5" + (flatten -1) + (("5" + (lemma lwb_perm) + (("5" + (inst + -1 + "split(car(g),cdr(g))`2" + "qs(split(car(g),cdr(g))`2)") + (("5" + (split -1) + (("1" + (inst -1 "car(g)") + (("1" + (split -1) + (("1" + (expand lwb 1) + (("1" + (skeep 1) + (("1" + (expand nth -5) + (("1" + (lift-if -5) + (("1" + (split -5) + (("1" + (assert -1) + nil + nil) + ("2" + (flatten -1) + (("2" + (expand + lwb + -2) + (("2" + (inst + -2 + "i-1") + (("1" + (split + -2) + (("1" + (propax) + nil + nil) + ("2" + (assert) + (("2" + (grind + 1) + nil + nil)) + nil)) + nil) + ("2" + (assert) + nil + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("2" (propax) nil nil)) + nil)) + nil) + ("2" + (lemma qs_perm) + (("2" + (inst + -1 + "split(car(g),cdr(g))`2") + (("2" + (lemma perm_commutative) + (("2" + (inst + -1 + "qs(split(car(g),cdr(g))`2)" + "split(car(g),cdr(g))`2") + (("2" + (split -1) + (("1" + (propax) + nil + nil) + ("2" + (propax) + 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) + ((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) @@ -1647,60 +2195,46 @@ (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) + (number nonempty-type-decl nil numbers nil) + (list_length_induction formula-decl nil my_list_induction nil) + (length def-decl "nat" list_props 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) + (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) + (split def-decl "[list[nat], list[nat]]" SPLIT nil) + (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) + (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) + (i skolem-const-decl "nat" QS_props nil) + (upb_perm formula-decl nil QS_props nil) + (nth def-decl "T" list_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) + (lwb const-decl "bool" SPLIT nil) (upb const-decl "bool" SPLIT nil) + (j skolem-const-decl "nat" QS_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) - (lwb const-decl "bool" SPLIT nil) - (upb_perm formula-decl nil QS_props nil) + (lwb_perm formula-decl nil QS_props nil) + (split_lwb_upb formula-decl nil SPLIT nil) + (real_le_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (i skolem-const-decl "nat" 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_posint_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) - (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)) + (split_length formula-decl nil SPLIT nil) + (sorted_append formula-decl nil SORTED nil) + (qs def-decl "list[nat]" QS nil) + (sorted? const-decl "bool" SORTED nil) + (pred type-eq-decl nil defined_types nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (every adt-def-decl "boolean" list_adt nil) + (PRED type-eq-decl nil defined_types nil) + (list type-decl nil list_adt nil)) shostak))) diff --git a/assignment8/qs.status b/assignment8/qs.status new file mode 100644 index 0000000..763c95b --- /dev/null +++ b/assignment8/qs.status @@ -0,0 +1,46 @@ + Proof summary for theory my_list_induction + less_wf...............................proved - complete [shostak](0.04 s) + list_length_induction.................proved - complete [shostak](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.05 s) + + Proof summary for theory my_list_props + occ_TCC1..............................proved - complete [shostak](0.01 s) + occ_TCC2..............................proved - complete [shostak](0.03 s) + occ_nth...............................proved - complete [shostak](0.11 s) + nth_occ...............................proved - complete [shostak](0.10 s) + perm_null.............................proved - complete [shostak](0.03 s) + perm_commutative......................proved - complete [shostak](0.01 s) + append_occ............................proved - complete [shostak](0.07 s) + length_append.........................proved - complete [shostak](0.11 s) + nth_append_TCC1.......................proved - complete [shostak](0.04 s) + nth_append_TCC2.......................proved - complete [shostak](0.05 s) + nth_append............................proved - complete [shostak](0.30 s) + Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.86 s) + + Proof summary for theory SPLIT + split_TCC1............................proved - complete [shostak](0.04 s) + split_length..........................proved - complete [shostak](0.13 s) + split_occ.............................proved - complete [shostak](0.14 s) + split_lwb_upb.........................proved - complete [shostak](0.18 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.50 s) + + Proof summary for theory QS + qs_TCC1...............................proved - complete [shostak](0.07 s) + qs_TCC2...............................proved - complete [shostak](0.06 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.12 s) + + Proof summary for theory SORTED + sorted?_TCC1..........................proved - complete [shostak](0.03 s) + sorted_append.........................proved - complete [shostak](0.53 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.56 s) + + Proof summary for theory QS_props + qs_perm...............................proved - complete [shostak](1.35 s) + occ_upb...............................proved - complete [shostak](0.12 s) + occ_lwb...............................proved - complete [shostak](0.10 s) + upb_perm..............................proved - complete [shostak](0.08 s) + lwb_perm..............................proved - complete [shostak](0.08 s) + qs_sorted.............................proved - complete [shostak](0.74 s) + Theory totals: 6 formulas, 6 attempted, 6 succeeded (2.48 s) + +Grand Totals: 27 proofs, 27 attempted, 27 succeeded (4.56 s) |