|
(prelude_A4
(expt_neg_even_TCC1 0
(expt_neg_even_TCC1-1 nil 3250069458 ("" (grind) nil nil)
((even? const-decl "bool" integers nil)) nil))
(expt_neg_even_TCC2 0
(expt_neg_even_TCC2-1 nil 3250069458 ("" (grind) nil nil)
((even? const-decl "bool" integers nil)) nil))
(expt_neg_even 0
(expt_neg_even-1 nil 3250069458
("" (expand "even?")
(("" (skosimp*)
(("" (replace -1)
(("" (hide -1)
(("" (rewrite "expt_times")
(("" (rewrite "expt_times")
(("" (case-replace "(-nx!1) ^ 2 = nx!1 ^ 2")
(("" (hide 2) (("" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(expt def-decl "real" exponentiation nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" reals nil)
(^ const-decl "real" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal 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)
(expt_times formula-decl nil exponentiation nil)
(even? const-decl "bool" integers nil))
nil))
(expt_neg_odd_TCC1 0
(expt_neg_odd_TCC1-1 nil 3250069458 ("" (grind) nil 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? const-decl "bool" integers nil))
nil))
(expt_neg_odd_TCC2 0
(expt_neg_odd_TCC2-1 nil 3250069458 ("" (grind) nil 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? const-decl "bool" integers nil))
nil))
(expt_neg_odd 0
(expt_neg_odd-1 nil 3250069458
("" (expand "odd?")
(("" (skosimp*)
(("" (replace -1)
(("" (case "j!1 >=0")
(("1" (rewrite "expt_plus")
(("1" (rewrite "expt_plus")
(("1" (rewrite "expt_x1")
(("1" (rewrite "expt_x1")
(("1"
(lemma "expt_neg_even" ("nx" "nx!1" "n" "2*j!1"))
(("1" (split -1)
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (expand "even?")
(("2" (inst + "j!1") nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "n!1") (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
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)
(bool nonempty-type-eq-decl nil booleans 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)
(- const-decl "[numfield -> numfield]" number_fields nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(even? const-decl "bool" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(expt_neg_even formula-decl nil prelude_A4 nil)
(expt_x1 formula-decl nil exponentiation nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(expt_plus formula-decl nil exponentiation nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(odd? const-decl "bool" integers nil)
(nzreal_exp application-judgement "nzreal" exponentiation 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))
nil))
(expt_0pn 0
(expt_0pn-1 nil 3250069458 ("" (grind) nil nil)
((expt def-decl "real" exponentiation nil)
(^ const-decl "real" exponentiation nil)
(nat_expt application-judgement "nat" exponentiation nil))
nil))
(expt_inverse_inv_TCC1 0
(expt_inverse_inv_TCC1-1 nil 3250069458 ("" (grind) nil nil) nil
nil))
(expt_inverse_inv 0
(expt_inverse_inv-1 nil 3250069458
("" (skosimp*)
(("" (rewrite "div_expt") (("" (rewrite "expt_1i") nil nil)) nil))
nil)
((div_expt formula-decl nil exponentiation 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)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(expt_1i formula-decl nil exponentiation nil))
nil))
(expt_product_n0i_TCC1 0
(expt_product_n0i_TCC1-1 nil 3250069458 ("" (grind) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(expt_product_n0i_TCC2 0
(expt_product_n0i_TCC2-1 nil 3250069458 ("" (grind) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(expt_product_n0i 0
(expt_product_n0i-1 nil 3250069458
("" (skosimp*)
(("" (case-replace "x!1=0")
(("1" (expand "^" 1 2)
(("1" (expand "^" 1 1)
(("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil))
nil)
("2" (case-replace "y!1=0")
(("1" (expand "^" 2 1)
(("1" (expand "^" 2 2)
(("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (rewrite "mult_expt") nil nil))
nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(expt def-decl "real" exponentiation nil)
(^ const-decl "real" exponentiation nil)
(mult_expt formula-decl nil exponentiation 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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals 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)
(nat_expt application-judgement "nat" exponentiation nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(expt_division_TCC1 0
(expt_division_TCC1-1 nil 3250069458 ("" (grind) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(expt_division_TCC2 0
(expt_division_TCC2-1 nil 3250069458 ("" (grind) nil nil) nil nil))
(expt_division 0
(expt_division-1 nil 3250069458
("" (skosimp*)
((""
(lemma "expt_product_n0i" ("x" "x!1" "y" "1/n0y!1" "pn" "pn!1"))
(("" (rewrite "expt_inverse_inv" -1) (("" (assert) nil nil))
nil))
nil))
nil)
((nzreal nonempty-type-eq-decl nil reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers 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)
(expt_product_n0i formula-decl nil prelude_A4 nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(expt_inverse_inv formula-decl nil prelude_A4 nil))
nil))
(A4_0_TCC1 0
(A4_0_TCC1-1 nil 3250069458 ("" (grind) 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)
(real_plus_real_is_real application-judgement "real" reals 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(A4_0 0
(A4_0-1 nil 3250069458
("" (skosimp*)
(("" (case "n!1 + 1 + y!1 > 0")
(("1" (rewrite "div_mult_pos_le2")
(("1" (rewrite "div_mult_pos_lt1") (("1" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
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 "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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_plus_real_is_real application-judgement "real" reals nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals 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)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil))
nil))
(A4_1_TCC1 0
(A4_1_TCC1-1 nil 3250069458 ("" (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)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(real_plus_real_is_real application-judgement "real" reals 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(A4_1 0
(A4_1-1 nil 3250069458
("" (skosimp*)
(("" (typepred "pn!1")
(("" (lemma "A4_0" ("y" "y!1" "n" "pn!1"))
(("" (assert) (("" (flatten -1) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(A4_0 formula-decl nil prelude_A4 nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(A4_2 0
(A4_2-1 nil 3250069458
("" (skosimp*)
(("" (lemma "A4_0" ("y" "y!1" "n" "n!1"))
(("" (lemma "trich_lt" ("x" "y!1" "y" "0"))
(("" (split -1)
(("1"
(lemma "both_sides_times_neg_lt1"
("y" "-1" "x" "y!1" "nz" "-1"))
(("1"
(lemma "lt_times_lt_pos1"
("px" "y!1 * -1" "y" "1" "nnz" "n!1 / (n!1 + 1 + y!1)"
"w" "1"))
(("1"
(lemma "both_sides_times_neg_lt1"
("y" "-1" "x" "z!1" "nz" "-1"))
(("1" (grind) nil nil)) nil)
("2" (assert) nil nil) ("3" (assert) nil nil)
("4" (assert) nil nil))
nil))
nil)
("2" (replace -1) (("2" (grind) nil nil)) nil)
("3" (lemma "trich_lt" ("x" "n!1" "y" "0"))
(("3" (split -1)
(("1" (assert) nil nil)
("2" (replace -1) (("2" (assert) nil nil)) nil)
("3" (lemma "A4_1" ("y" "y!1" "pn" "n!1"))
(("1"
(lemma "lt_times_lt_nn1"
("nnx" "0" "y" "n!1 / (n!1 + 1 + y!1)" "nnz" "0" "w"
"y!1"))
(("1" (grind) nil nil) ("2" (assert) nil nil)) nil)
("2" (assert) 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)
(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)
(A4_0 formula-decl nil prelude_A4 nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(lt_times_lt_pos1 formula-decl nil real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(odd_times_odd_is_odd application-judgement "odd_int" integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(<= const-decl "bool" reals nil)
(both_sides_times_neg_lt1 formula-decl nil real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(even_plus_odd_is_odd application-judgement "odd_int" integers nil)
(lt_times_lt_nn1 formula-decl nil prelude_aux nil)
(nnreal type-eq-decl nil real_types nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(A4_1 formula-decl nil prelude_A4 nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(trich_lt formula-decl nil real_props nil))
nil))
(A4_3_n 0
(A4_3_n-1 nil 3250069458
("" (skosimp*)
(("" (lemma "A4_1" ("y" "y!1" "pn" "pn!1"))
((""
(lemma "both_sides_times_neg_lt1"
("y" "pn!1 / (pn!1 + 1 + y!1)" "x" "1" "nz" "y!1"))
(("1" (grind) nil nil) ("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil)
((posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers 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)
(A4_1 formula-decl nil prelude_A4 nil)
(real_times_real_is_real application-judgement "real" reals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(both_sides_times_neg_lt1 formula-decl nil real_props nil)
(<= const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
nil))
(A4_3_0_TCC1 0
(A4_3_0_TCC1-1 nil 3250069458 ("" (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)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(A4_3_0 0
(A4_3_0-1 nil 3250069458 ("" (grind) 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)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil))
nil))
(A4_3_p_TCC1 0
(A4_3_p_TCC1-1 nil 3250069458 ("" (grind) 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)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(A4_3_p 0
(A4_3_p-1 nil 3250069458
("" (skosimp*)
(("" (lemma "A4_1" ("pn" "pn!1" "y" "y!1"))
(("" (assert)
(("" (flatten -1)
((""
(lemma "both_sides_times_pos_lt1"
("pz" "y!1" "x" "pn!1 / (1 + pn!1 + y!1)" "y" "1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers 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)
(A4_1 formula-decl nil prelude_A4 nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_gt_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)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" 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)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil))
nil))
(A4_4 0
(A4_4-1 nil 3250069458
("" (skosimp*)
(("" (lemma "A4_1" ("y" "y!1" "pn" "pn!1"))
((""
(lemma "both_sides_plus_lt1" ("x" "-1" "y" "y!1" "z" "pn!1+1"))
((""
(lemma "lt_le_transitivity"
("x" "0" "y" "pn!1" "z" "1+pn!1+y!1"))
((""
(lemma "both_sides_plus1"
("x" "z!1" "y" "pn!1 * y!1 / (pn!1 + 1 + y!1)" "z"
"(pn!1 + 1 + y!1)/(pn!1 + 1 + y!1)"))
(("1" (copy -6)
(("1" (replace -2 -7 rl)
(("1" (rewrite "div_distributes" -7)
(("1" (rewrite "div_simp" -7)
(("1" (replace -7 1)
(("1" (replace -1 1)
(("1" (hide (-1 -2 -7))
(("1"
(lemma "both_sides_div_pos_lt1"
("x" "pn!1 * x!1 * (1 + pn!1) * (1+y!1)"
"y" "pn!1 * y!1" "pz" "pn!1 + 1 + y!1"))
(("1"
(lemma "both_sides_times_pos_lt1"
("x"
"(pn!1 + 1) * x!1 * (1 + y!
1)"
"y"
"y!1"
"pz"
"pn!1"))
(("1" (grind) nil nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers 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)
(A4_1 formula-decl nil prelude_A4 nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(lt_le_transitivity formula-decl nil prelude_aux nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_distributes formula-decl nil real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_gt_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)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(both_sides_div_pos_lt1 formula-decl nil real_props nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(div_simp formula-decl nil real_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(both_sides_plus1 formula-decl nil real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(both_sides_plus_lt1 formula-decl nil real_props nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
nil))
(A4_5pp_TCC1 0
(A4_5pp_TCC1-1 nil 3250069458
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_plus_real_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(A4_5pp 0
(A4_5pp-1 nil 3250069458
("" (skolem!)
(("" (flatten)
(("" (induct "n")
(("1" (skosimp*) (("1" (grind) nil nil)) nil)
("2" (skolem!)
(("2" (skosimp*)
(("2" (lemma "trich_lt" ("x" "j!1" "y" "0"))
(("2" (split -1)
(("1" (assert) nil nil)
("2" (replace -1)
(("2"
(lemma "div_mult_pos_lt2"
("x" "x!1" "py" "1+y!1" "z" "y!1"))
(("1"
(lemma "lt_times_lt_nn1"
("nnx" "0" "y" "y!1" "nnz" "0" "w" "y!1"))
(("1"
(lemma "both_sides_plus_lt1"
("x" "0" "y" "y!1 * y!1" "z" "y!1"))
(("1"
(lemma "div_mult_pos_lt1"
("z" "y!1" "py" "1+y!1" "x" "y!1"))
(("1" (grind) nil nil)) nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("3" (name "z!1" "j!1*y!1/(j!1+1+y!1)")
(("1"
(lemma "A4_4"
("y" "y!1" "z" "z!1" "pn" "j!1" "x" "x!1"))
(("1" (inst - "z!1")
(("1" (lemma "A4_1" ("y" "y!1" "pn" "j!1"))
(("1"
(lemma "lt_times_lt_nn1"
("nnx" "0" "y" "j!1 / (j!1 + 1 + y!1)" "nnz"
"0" "w" "y!1"))
(("1" (replace -4)
(("1" (bash -3)
(("1"
(lemma
"both_sides_plus1"
("y"
"z!1"
"x"
"j!1 * y!1 / (j!1 + 1 + y!1)"
"z"
"(j!1 + 1 + y!1)/(j!1 + 1 + y!1)"))
(("1"
(copy -6)
(("1"
(replace -2 -7 rl)
(("1"
(rewrite "div_distributes" -7)
(("1"
(rewrite "div_simp" -7)
(("1"
(replace -7 -9 rl)
(("1"
(lemma
"lt_times_lt_nn1"
("nnx"
"0"
"y"
"y!1"
"nnz"
"0"
"w"
"y!1"))
(("1"
(lemma
"both_sides_plus_lt1"
("x"
"0"
"y"
"y!1 * y!1"
"z"
"y!1"))
(("1"
(lemma
"div_mult_pos_lt1"
("z"
"y!1"
"x"
"y!1"
"py"
"1+y!1"))
(("1"
(lemma
"div_mult_pos_lt2"
("x"
"x!1*(1+j!1)"
"py"
"1+y!1"
"z"
"y!1"))
(("1"
(lemma
"expt_plus"
("n0x"
"1+x!1"
"i"
"1"
"j"
"j!1"))
(("1"
(replace -1 1)
(("1"
(name-replace
"AA"
"(1 + x!1) ^ j!1")
(("1"
(hide -1)
(("1"
(replace
-14)
(("1"
(simplify
-4)
(("1"
(replace
-4)
(("1"
(simplify
-3)
(("1"
(replace
-3)
(("1"
(simplify
-2)
(("1"
(replace
-15
-1)
(("1"
(simplify
-1)
(("1"
(reveal
-2)
(("1"
(lemma
"posreal_expt")
(("1"
(inst
-
"j!1"
"1+x!1")
(("1"
(expand
"^")
(("1"
(replace
-2
-1)
(("1"
(hide
-2)
(("1"
(expand
"expt")
(("1"
(expand
"expt")
(("1"
(lemma
"lt_times_lt_pos1"
("px"
"AA"
"y"
"((1+j!1)*(1+y!1))/(1 + j!1 + y!1)"
"nnz"
"1+x!1"
"w"
"(1 + j!1 + y!1)/(1+j!1)"))
(("1"
(lemma
"div_times"
("x"
"(1 + y!1)*(1 + j!1)"
"n0x"
"(1 + j!1 + y!1)"
"y"
"(1 + j!1 + y!1)"
"n0y"
"1 + j!1"))
(("1"
(replace
-1
-2)
(("1"
(lemma
"div_cancel1"
("x"
"1+y!1"
"n0z"
"(1 + j!1 + y!1) * (1 + j!1)"))
(("1"
(replace
-1
-3)
(("1"
(hide
(-1
-2))
(("1"
(lemma
"div_mult_pos_lt2"
("x"
"x!1"
"py"
"(1+y!1)*(1+j!1)"
"z"
"y!1"))
(("1"
(replace
-18
-1)
(("1"
(lemma
"both_sides_plus_lt1"
("x"
"y!1 / (1 + y!1)"
"y"
"y!1"
"z"
"1+j!1"))
(("1"
(replace
-6
-1)
(("1"
(lemma
"lt_le_transitivity"
("x"
"(1+j!1)*x!1"
"y"
"y!1 / (1 + y!1)"
"z"
"y!1"))
(("1"
(lemma
"both_sides_plus_lt1"
("x"
"(1 + j!1) * x!1"
"y"
"y!1"
"z"
"1 + j!1"))
(("1"
(lemma
"div_mult_pos_lt2"
("x"
"x!1+1"
"py"
"1 + j!1"
"z"
"y!1+1+j!1"))
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"lt_times_lt_nn1"
("nnx"
"0"
"y"
"1+j!1"
"nnz"
"0"
"w"
"1+y!1"))
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma
"lt_times_lt_nn1"
("nnx"
"0"
"y"
"1 + j!1 + y!1"
"nnz"
"0"
"w"
"1 + j!1"))
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.77 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
