diff options
Diffstat (limited to 'assignment7/E.prf')
| -rw-r--r-- | assignment7/E.prf | 386 |
1 files changed, 386 insertions, 0 deletions
diff --git a/assignment7/E.prf b/assignment7/E.prf new file mode 100644 index 0000000..38c0cb0 --- /dev/null +++ b/assignment7/E.prf @@ -0,0 +1,386 @@ +(th_E + (fac_TCC1 0 + (fac_TCC1-1 nil 3667132061 ("" (subtype-tcc) nil nil) nil nil)) + (fac_TCC2 0 + (fac_TCC2-1 nil 3667132061 ("" (termination-tcc) nil nil) nil nil)) + (thm_E_0 0 + (thm_E_0-1 nil 3667136110 + ("" (induct k) + (("1" (flatten) (("1" (assert) nil nil)) nil) + ("2" (skeep) + (("2" (split -1) + (("1" (expand fac 1 2) (("1" (assert) nil nil)) nil) + ("2" (case "j=0") + (("1" (expand fac 2) + (("1" (expand fac 2) + (("1" (assert 2) + (("1" (expand fac 2) + (("1" (assert 2) (("1" (grind 2) nil nil)) nil)) + nil)) + nil)) + nil)) + nil) + ("2" (assert) nil nil)) + nil)) + nil)) + nil)) + nil) + ((= const-decl "[T, T -> boolean]" equalities nil) + (minus_odd_is_odd application-judgement "odd_int" 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) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_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) + (real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (nat_induction formula-decl nil naturalnumbers nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (fac def-decl "nat" th_E 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) + (nnint_plus_posint_is_posint application-judgement "posint" + integers nil)) + shostak)) + (thm_E_1 0 + (thm_E_1-1 nil 3667132062 + ("" (induct k) + (("1" (assert) (("1" (grind) nil nil)) nil) + ("2" (skeep) (("2" (expand fac 1) (("2" (assert) nil nil)) nil)) + nil)) + nil) + ((mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (real_le_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (nat_induction formula-decl nil naturalnumbers nil) + (fac def-decl "nat" th_E nil) (<= const-decl "bool" reals 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)) + (thm_E_2 0 + (thm_E_2-1 nil 3667133505 + ("" (induct k) + (("1" (expand fac) (("1" (assert) nil nil)) nil) + ("2" (skeep) + (("2" (lemma thm_E_0) + (("2" (inst -1 j) + (("2" (split -1) + (("1" (assert) nil nil) + ("2" (assert) + (("2" (case "j=0") + (("1" (expand fac 2) + (("1" (expand fac 2) (("1" (assert 2) nil nil)) nil)) + nil) + ("2" (assert) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (posint_plus_nnint_is_posint application-judgement "posint" + integers nil) + (= const-decl "[T, T -> boolean]" equalities 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) + (thm_E_0 formula-decl nil th_E nil) + (real_le_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (nat_induction formula-decl nil naturalnumbers nil) + (fac def-decl "nat" th_E nil) (<= const-decl "bool" reals 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)) + (tfac_TCC1 0 + (tfac_TCC1-1 nil 3667133493 ("" (subtype-tcc) nil nil) nil nil)) + (tfac_TCC2 0 + (tfac_TCC2-1 nil 3667133493 ("" (termination-tcc) nil nil) nil nil)) + (lemma_E_3 0 + (lemma_E_3-1 nil 3667135000 + ("" (induct m) + (("1" (skeep) + (("1" (expand tfac) + (("1" (expand fac) (("1" (propax) nil nil)) nil)) nil)) + nil) + ("2" (skeep) + (("2" (skeep 1) + (("2" (expand tfac 1) + (("2" (inst -1 "j*n+n") + (("2" (replace -1 1) + (("2" (expand fac 1 2) (("2" (propax) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + 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) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat_induction formula-decl nil naturalnumbers nil) + (fac def-decl "nat" th_E nil) + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (numfield nonempty-type-eq-decl nil number_fields nil) + (tfac def-decl "nat" th_E 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)) + (th_E_4 0 + (th_E_4-1 nil 3667136822 + ("" (skeep) + (("" (lemma lemma_E_3) + (("" (inst -1 k 1) (("" (assert) nil nil)) nil)) nil)) + nil) + ((lemma_E_3 formula-decl nil th_E nil) + (mult_divides2 application-judgement "(divides(m))" divides nil) + (mult_divides1 application-judgement "(divides(n))" divides nil) + (nnint_times_nnint_is_nnint application-judgement "nonneg_int" + integers 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)) + (fib_TCC1 0 + (fib_TCC1-1 nil 3667132061 ("" (subtype-tcc) nil nil) nil nil)) + (fib_TCC2 0 + (fib_TCC2-1 nil 3667132061 ("" (termination-tcc) nil nil) nil nil)) + (lem_E_Camil_1 0 + (lem_E_Camil_1-1 nil 3667137364 + ("" (induct i) + (("1" (skeep) + (("1" (expand tfib) + (("1" (expand fib) (("1" (propax) nil nil)) nil)) nil)) + nil) + ("2" (skeep) + (("2" (skeep 1) + (("2" (expand tfib 1) (("2" (postpone) nil nil)) nil)) nil)) + nil)) + nil) + nil shostak)) + (lem_E_Camil_2_TCC1 0 + (lem_E_Camil_2_TCC1-1 nil 3667140798 ("" (subtype-tcc) nil nil) nil + nil)) + (lem_E_Camil_2_TCC2 0 + (lem_E_Camil_2_TCC2-1 nil 3667140798 ("" (subtype-tcc) nil nil) nil + nil)) + (lem_E_Camil_2 0 + (lem_E_Camil_2-1 nil 3667137463 + ("" (induct i) + (("1" (skeep) (("1" (expand tfib) (("1" (propax) nil nil)) nil)) + nil) + ("2" (skeep) + (("2" (skeep 1) + (("2" (case "j=0") + (("1" (assert) + (("1" (expand tfib) + (("1" (expand tfib) (("1" (propax) nil nil)) nil)) nil)) + nil) + ("2" (assert 2) + (("2" (expand tfib 2) + (("2" (inst -1 p (m+p)) + (("2" (replace -1 2) + (("2" (case "j=1") + (("1" (assert) + (("1" (expand fib 2) (("1" (assert) nil nil)) + nil)) + nil) + ("2" (assert 3) + (("2" (lift-if) + (("2" (assert) + (("2" (expand fib 3 3) + (("2" (propax) nil nil)) nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ("3" (skeep 1) (("3" (assert) nil nil)) nil) + ("4" (skeep 1) (("4" (assert) nil nil)) nil)) + nil) + ((real_ge_is_total_order name-judgement "(total_order?[real])" + real_props nil) + (nnint_plus_posint_is_posint application-judgement "posint" + integers 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) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (nat_induction formula-decl nil naturalnumbers nil) + (fib def-decl "nat" th_E nil) + (* const-decl "[numfield, numfield -> numfield]" number_fields nil) + (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) + (IF const-decl "[boolean, T, T -> T]" if_def nil) + (tfib def-decl "nat" th_E nil) + (pred type-eq-decl nil defined_types 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) + (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) + (AND const-decl "[bool, bool -> bool]" booleans nil) + (NOT const-decl "[bool -> bool]" booleans nil) + (= const-decl "[T, T -> boolean]" equalities 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)) + shostak)) + (thm_E_6 0 + (thm_E_6-1 nil 3667137014 + ("" (skeep) + (("" (lemma lem_E_Camil_2) + (("" (inst -1 i 1 1) + (("" (assert) + (("" (replace -1 1) + (("" (assert) + (("" (case "i=0") + (("1" (assert) + (("1" (expand fib 1) (("1" (propax) nil nil)) nil)) + nil) + ("2" (case "i=1") + (("1" (assert) + (("1" (expand fib 2) (("1" (propax) nil nil)) nil)) + nil) + ("2" (assert) + (("2" (expand fib 3 3) (("2" (propax) nil nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil)) + nil) + ((lem_E_Camil_2 formula-decl nil th_E nil) + (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" + integers nil) + (int_minus_int_is_int application-judgement "int" integers nil) + (fib def-decl "nat" th_E nil) + (= const-decl "[T, T -> boolean]" equalities 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))) + |