diff options
Diffstat (limited to 'assignment7/D.prf')
| -rw-r--r-- | assignment7/D.prf | 414 |
1 files changed, 414 insertions, 0 deletions
diff --git a/assignment7/D.prf b/assignment7/D.prf new file mode 100644 index 0000000..d41d2b2 --- /dev/null +++ b/assignment7/D.prf @@ -0,0 +1,414 @@ +(th_D + (sum_TCC1 0 + (sum_TCC1-1 nil 3667129223 ("" (subtype-tcc) nil nil) nil nil)) + (sum_TCC2 0 + (sum_TCC2-1 nil 3667129223 ("" (termination-tcc) nil nil) nil nil)) + (D_1 0 + (D_1-1 nil 3667129225 + ("" (induct n) + (("1" (assert) (("1" (grind) nil nil)) nil) + ("2" (skeep) (("2" (expand sum 1) (("2" (assert) nil nil)) nil)) + nil)) + nil) + ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (even_plus_odd_is_odd application-judgement "odd_int" integers nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (even_times_int_is_even application-judgement "even_int" integers + nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat_induction formula-decl nil naturalnumbers nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + nil + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (= const-decl "[T, T -> boolean]" equalities 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)) + shostak)) + (D_2 0 + (D_2-1 nil 3667129345 + ("" (induct n) + (("1" (grind) nil nil) + ("2" (skeep) + (("2" (expand sum 1) + (("2" (expand id 1 1) (("2" (grind) nil nil)) nil)) nil)) + nil)) + nil) + ((nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (id_preserves application-judgement "S" identity_props nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (even_plus_odd_is_odd application-judgement "odd_int" integers nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (even_times_int_is_even application-judgement "even_int" integers + nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat_induction formula-decl nil naturalnumbers nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (id const-decl "(bijective?[T, T])" identity nil) + (bijective? const-decl "bool" functions nil) nil + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (= const-decl "[T, T -> boolean]" equalities 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)) + shostak)) + (pow_TCC1 0 + (pow_TCC1-1 nil 3667129223 ("" (skeep) (("" (assert) nil nil)) nil) + ((int_minus_int_is_int application-judgement "int" integers nil) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil)) + nil)) + (pow_TCC2 0 + (pow_TCC2-1 nil 3667144387 ("" (termination-tcc) nil nil) nil nil))) +(th_Da + (Da_1 0 + (Da_1-1 nil 3667129545 + ("" (induct n1) + (("1" (expand sum) + (("1" (expand square) (("1" (propax) nil nil)) nil)) nil) + ("2" (skeep) + (("2" (expand sum 1) + (("2" (replace -1 1) + (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) + nil)) + nil)) + nil) + ((posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (odd_plus_even_is_odd application-judgement "odd_int" integers nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (posint_times_posint_is_posint application-judgement "posint" + integers nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (even_times_int_is_even application-judgement "even_int" integers + nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat_induction formula-decl nil naturalnumbers nil) + (square const-decl "nat" th_Da nil) + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) nil + (= const-decl "[T, T -> boolean]" equalities 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) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (even_plus_odd_is_odd application-judgement "odd_int" integers + nil)) + shostak)) + (Da_2 0 + (Da_2-1 nil 3667129831 + ("" (induct n) + (("1" (grind) nil nil) + ("2" (skeep) + (("2" (expand sum 1) + (("2" (replace -1 1) (("2" (grind) nil nil)) nil)) nil)) + nil)) + nil) + ((posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (even_plus_even_is_even application-judgement "even_int" integers + nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (posint_times_posint_is_posint application-judgement "posint" + integers nil) + (even_plus_odd_is_odd application-judgement "odd_int" integers nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (even_times_int_is_even application-judgement "even_int" integers + nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat_induction formula-decl nil naturalnumbers nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (square const-decl "nat" th_Da nil) nil + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (= const-decl "[T, T -> boolean]" equalities 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)) + shostak)) + (Da_3 0 + (Da_3-1 nil 3667129862 + ("" (induct n) + (("1" (grind) nil nil) + ("2" (skeep) + (("2" (expand sum 1 1) + (("2" (expand sum 1 2) + (("2" (replace -1 1) + (("2" (expand square 1) + (("2" (expand cube 1) + (("2" (lemma D_1) + (("2" (inst -1 j) + (("2" (replace -1 1) (("2" (grind) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((mult_divides2 application-judgement "(divides(m))" divides nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (D_1 formula-decl nil th_D nil) + (even_plus_even_is_even application-judgement "even_int" integers + nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (even_times_int_is_even application-judgement "even_int" integers + nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat_induction formula-decl nil naturalnumbers nil) nil + (square const-decl "nat" th_Da nil) + (cube const-decl "nat" th_Da nil) nil + (= const-decl "[T, T -> boolean]" equalities 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)) + shostak)) + (Da_4 0 + (Da_4-1 nil 3667130517 + ("" (induct n1) + (("1" (grind) nil nil) + ("2" (skeep) + (("2" (expand sum 1) + (("2" (replace -1 1) + (("2" (expand pow 1 3) (("2" (propax) nil nil)) nil)) nil)) + nil)) + nil)) + nil) + ((nnint_plus_posint_is_posint application-judgement "posint" + integers 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) + (pred type-eq-decl nil defined_types nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (sum def-decl "nat" th_D nil) (pow def-decl "nat" th_D nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (- const-decl "[numfield, numfield -> numfield]" number_fields nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (nat_induction formula-decl nil naturalnumbers nil) + (int_minus_int_is_int application-judgement "int" integers nil) + (even_plus_odd_is_odd application-judgement "odd_int" integers nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (even_times_int_is_even application-judgement "even_int" integers + nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (odd_minus_odd_is_even application-judgement "even_int" integers + nil)) + shostak)) + (Da_5 0 + (Da_5-1 nil 3667130601 + ("" (induct n1) + (("1" (expand sum 1) (("1" (propax) nil nil)) nil) + ("2" (skeep) (("2" (expand sum 1) (("2" (propax) nil nil)) nil)) + nil)) + nil) + ((nat_induction formula-decl nil naturalnumbers nil) nil + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (= const-decl "[T, T -> boolean]" equalities 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) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (mult_divides2 application-judgement "(divides(m))" divides nil)) + shostak))) +(th_Db + (geom_TCC1 0 + (geom_TCC1-1 nil 3667129224 ("" (subtype-tcc) nil nil) nil nil)) + (geom_TCC2 0 + (geom_TCC2-1 nil 3667129224 ("" (subtype-tcc) nil nil) nil nil)) + (geom_TCC3 0 + (geom_TCC3-1 nil 3667129224 ("" (termination-tcc) nil nil) nil nil)) + (geom_sum 0 + (geom_sum-1 nil 3667130791 + ("" (induct a) + (("1" (induct n) + (("1" (grind) nil nil) + ("2" (skeep) + (("2" (split -1) + (("1" (expand geom 1) + (("1" (replace -1 1) (("1" (grind) nil nil)) nil)) nil) + ("2" (propax) nil nil)) + nil)) + nil)) + nil) + ("2" (skeep) + (("2" (induct n) + (("1" (grind) nil nil) + ("2" (skolem 1 k) + (("2" (flatten 1) + (("2" (split -1) + (("1" (expand geom 1) + (("1" (replace -1 1) + (("1" (expand pow 1 3) (("1" (propax) nil nil)) nil)) + nil)) + nil) + ("2" (propax) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) + (even_minus_odd_is_odd application-judgement "odd_int" integers + nil) + (nzint_times_nzint_is_nzint application-judgement "nzint" integers + nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (int_minus_int_is_int application-judgement "int" integers nil) + (minus_odd_is_odd application-judgement "odd_int" integers nil) + (nat_induction formula-decl nil naturalnumbers nil) + (pow def-decl "nat" th_D nil) (geom def-decl "posnat" th_Db nil) + (posnat nonempty-type-eq-decl nil integers nil) + (nonneg_int nonempty-type-eq-decl nil integers nil) + (- const-decl "[numfield, numfield -> numfield]" number_fields nil) + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (= const-decl "[T, T -> boolean]" equalities nil) + (> const-decl "bool" reals nil) + (IMPLIES const-decl "[bool, bool -> bool]" booleans 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)) + shostak))) + |