| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/exact_real_arith/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 657 kB |
|
Quelle prelude_A4.prfSprache: Lisp |
|||||||||||||||
|
(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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trich_lt formula-decl nil real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_distributes formula-decl nil real_props nil) (posreal_expt judgement-tcc nil exponentiation nil) (div_times formula-decl nil real_props nil) (div_cancel1 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (lt_le_transitivity formula-decl nil prelude_aux nil) (lt_times_lt_pos1 formula-decl nil real_props nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_plus formula-decl nil exponentiation 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) (int_minus_int_is_int application-judgement "int" integers nil) (both_sides_plus1 formula-decl nil real_props nil) (A4_1 formula-decl nil prelude_A4 nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (A4_4 formula-decl nil prelude_A4 nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (lt_times_lt_nn1 formula-decl nil prelude_aux nil) (nnreal type-eq-decl nil real_types nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (even_plus_odd_is_odd application-judgement "odd_int" 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) (real_div_nzreal_is_real application-judgement "real" reals nil) (both_sides_plus_lt1 formula-decl nil 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) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (div_mult_pos_lt2 formula-decl nil real_props 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) (expt def-decl "real" exponentiation nil) (nat_induction formula-decl nil naturalnumbers nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans 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 "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) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (A4_5nn_TCC1 0 (A4_5nn_TCC1-1 nil 3287311368 ("" (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) (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)) shostak)) (A4_5nn 0 (A4_5nn-1 nil 3287307975 ("" (skolem!) (("" (flatten) (("" (induct "pn") (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp*) (("3" (lemma "lt_times_lt_np1" ("x" "y!1" "npy" "0" "z" "y!1" "npw" "0")) (("3" (replace -5) (("3" (simplify -1) (("3" (lemma "both_sides_plus_lt1" ("x" "0" "y" "y!1 * y!1" "z" "y!1")) (("3" (lemma "both_sides_plus_lt1" ("x" "-1" "y" "y!1" "z" "1")) (("3" (replace -6) (("3" (replace -3) (("3" (simplify (-1 -2)) (("3" (lemma "div_mult_pos_lt1" ("z" "y!1" "x" "y!1" "py" "1+y!1")) (("1" (replace -3 -1) (("1" (simplify -1) (("1" (hide (-3 -4)) (("1" (lemma "trich_lt" ("x" "j!1" "y" "0")) (("1" (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")) (("2" (lemma "lt_le_transitivity" ("x" "x!1" "y" "y!1 / (1 + y!1)" "z" "y!1")) (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "both_sides_plus_lt1" ("x" "-1" "y" "x!1" "z" "1")) (("3" (replace -10 -1) (("3" (simplify -1) (("3" (lemma "expt_plus" ("n0x" "1 + x!1" "i" "j!1" "j" "1")) (("1" (replace -1 1) (("1" (lemma "posreal_expt") (("1" (inst - "j!1" "1+x!1") (("1" (name "AA" "(1 + x!1) ^ j!1") (("1" (replace -1) (("1" (expand "^" -1) (("1" (replace -1) (("1" (hide (-1 -3)) (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (expand ">" -6) (("1" (replace -3 -6) (("1" (name "z!1" "j!1*y!1/(j!1+1+y!1)") (("1" (lemma "A4_4" ("z" "z!1" "y" "y!1" "pn" "j!1" "x" "x!1")) (("1" (replace -2 -1) (("1" (replace -10) (("1" (simplify -1) (("1" (replace -12 -1) (("1" (simplify -1) (("1" (inst - "z!1") (("1" (replace -1 -8) (("1" (lemma "A4_2" ("z" "z!1" "y" "y!1" "n" "j!1")) (("1" (replace -11) (("1" (replace -3 -1) (("1" (replace -1) (("1" (lemma "posreal_div_posreal_is_posreal") (("1" (inst - "j!1" "j!1 + 1 + y!1") (("1" (expand ">") (("1" (lemma "both_sides_times_neg_lt1" ("y" "0" "x" "j!1 / (1 + j!1 + y!1)" "nz" "y!1")) (("1" (replace -2 -1) (("1" (simplify -1) (("1" (replace -5) (("1" (replace -1 -11) (("1" (simplify -11) (("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 -13 rl) (("1" (lemma "div_mult_pos_lt2" ("x" "x!1" "py" "(1 + y!1) * (j!1 + 1)" "z" "y!1")) (("1" (replace -18 -1) (("1" (lemma "both_sides_div_pos_lt1" ("x" "y!1 / (1 + y!1)" "y" "y!1" "pz" "1+j!1")) (("1" (replace -13 -1) (("1" (rewrite "div_div2" -1) (("1" (lemma "lt_le_transitivity" ("x" "x!1" "y" "y!1 / ((1 + y!1) * (j!1 + 1))" "z" "y!1 / (1 + j!1)")) (("1" (expand "<=" -1) (("1" (simplify (-2 -3)) (("1" (replace -2 -1) (("1" (replace -3 -1) (("1" (lemma "both_sides_plus_lt1" ("x" "x!1" "y" "y!1 / (1 + j!1)" "z" "(1 + j!1)/(1 + j!1)")) (("1" (replace -2 -1) (("1" (rewrite "div_distributes" -1) (("1" (rewrite "div_simp" -1) (("1" (simplify -1) (("1" (lemma "lt_times_lt_nn1" ("nnx" "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" (replace -18 -1) (("1" (replace -2 -1) (("1" (lemma "div_times" ("x" "(1 + j!1) * (1 + y!1)" "n0x" "1 + j!1 + y!1" "y" "1 + j!1 + y!1" "n0y" "1 + j!1")) (("1" (replace -1 -2) (("1" (hide -1) (("1" (lemma "div_cancel1" ("x" "1 + y!1" "n0z" "(1 + j!1 + y!1) * (1 + j!1)")) (("1" (replace -1 -2) (("1" (grind) nil nil)) nil) ("2" (lemma "lt_times_lt_nn1" ("nnx" "0" "y" "1+j!1" "nnz" "0" "w" "1 + j!1 + y!1")) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) 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) 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)) nil)) nil) ("2" (lemma "lt_plus_lt1" ("x" "0" "y" "1+y!1" "z" "0" "w" "j!1")) (("2" (grind) nil nil)) nil)) nil) ("2" (lemma "lt_plus_lt1" ("x" "0" "y" "1+y!1" "z" "0" "w" "j!1")) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "lt_plus_lt1" ("x" "0" "y" "1+y!1" "z" "0" "w" "j!1")) (("2" (grind) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (lemma "lt_plus_lt1" ("x" "0" "y" "j!1" "z" "0" "w" "1+y!1")) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (both_sides_plus_lt1 formula-decl nil real_props nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (expt def-decl "real" exponentiation nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (lt_le_transitivity formula-decl nil prelude_aux nil) (expt_plus formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (posreal_expt judgement-tcc nil exponentiation nil) (= const-decl "[T, T -> boolean]" equalities nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (j!1 skolem-const-decl "nat" prelude_A4 nil) (y!1 skolem-const-decl "real" prelude_A4 nil) (both_sides_times_neg_lt1 formula-decl nil real_props nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (both_sides_plus1 formula-decl nil real_props nil) (div_simp formula-decl nil real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (div_div2 formula-decl nil real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (div_times formula-decl nil real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (div_cancel1 formula-decl nil real_props nil) (nnreal type-eq-decl nil real_types nil) (lt_times_lt_nn1 formula-decl nil prelude_aux nil) (int_minus_int_is_int application-judgement "int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (div_distributes formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (lt_plus_lt1 formula-decl nil real_props nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (A4_2 formula-decl nil prelude_A4 nil) (A4_4 formula-decl nil prelude_A4 nil) (x!1 skolem-const-decl "real" prelude_A4 nil) (trich_lt formula-decl nil real_props nil) (real_div_nzreal_is_real application-judgement "real" reals 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) (div_mult_pos_lt1 formula-decl nil real_props 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) (npreal type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (lt_times_lt_np1 formula-decl nil prelude_aux 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) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nat_induction formula-decl nil naturalnumbers nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (A4_5nn_general_TCC1 0 (A4_5nn_general_TCC1-1 nil 3250069458 ("" (grind) nil nil) ((/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (A4_5nn_general 0 (A4_5nn_general-1 nil 3250069458 ("" (skosimp*) (("" (lemma "trich_lt" ("x" "n!1" "y" "0")) (("" (split) (("1" (assert) nil nil) ("2" (replace -1) (("2" (grind) nil nil)) nil) ("3" (lemma "both_sides_minus_lt1" ("x" "(1 + y!1) * n!1 * x!1" "y" "y!1" "z" "y!1*n!1*x!1")) (("3" (copy -6) (("3" (replace -2 -7 rl) (("3" (simplify -7) (("3" (hide -2) (("3" (lemma "negreal_times_negreal_is_posreal" ("nx" "-n!1" "ny" "x!1")) (("1" (lemma "both_sides_plus_gt1" ("x" "-n!1 * x!1" "y" "0" "z" "1")) (("1" (replace -2 -1) (("1" (simplify -1) (("1" (lemma "div_mult_pos_lt2" ("x" "-1" "py" "1-n!1*x!1" "z" "n!1*x!1")) (("1" (lemma "div_mult_pos_lt1" ("x" "y!1" "py" "1-n!1*x!1" "z" "n!1 * x!1")) (("1" (replace -10 -1) (("1" (lemma "lt_le_transitivity") (("1" (inst - "-1" "n!1 * x!1 / (1 - n!1 * x!1)" "y!1") (("1" (expand "<=" -1) (("1" (flatten -2) (("1" (replace -2 -1) (("1" (replace -3 -1) (("1" (simplify -1) (("1" (lemma "A4_5nn" ("x" "x!1")) (("1" (bash) (("1" (bash) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) 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) (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) (trich_lt formula-decl nil real_props 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) (both_sides_minus_lt1 formula-decl nil real_props nil) (both_sides_plus_gt1 formula-decl nil 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) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (lt_le_transitivity formula-decl nil prelude_aux nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (A4_5nn formula-decl nil prelude_A4 nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield -> numfield]" 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) (negreal_times_negreal_is_posreal judgement-tcc nil real_types nil) (minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals 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)) nil)) (A4_5_TCC1 0 (A4_5_TCC1-1 nil 3250069458 ("" (grind) nil nil) ((/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (A4_5 0 (A4_5-1 nil 3250069458 ("" (skosimp*) (("" (lemma "trich_lt" ("x" "x!1" "y" "0")) (("" (split -1) (("1" (lemma "trich_lt" ("x" "y!1" "y" "0")) (("1" (split -1) (("1" (lemma "A4_5nn" ("x" "x!1")) (("1" (bash) (("1" (bash) nil nil)) nil)) nil) ("2" (replace -1) (("2" (lemma "both_sides_expt_lt1_lt" ("lt1x" "1+x!1" "j" "0" "i" "pn!1")) (("1" (grind) nil nil) ("2" (assert) nil nil)) nil)) nil) ("3" (lemma "both_sides_times_pos_lt1" ("x" "x!1" "y" "0" "pz" "(1 + y!1) * pn!1")) (("1" (lemma "lt_le_transitivity" ("x" "(1 + y!1) * pn!1 * x!1" "y" "0" "z" "y!1")) (("1" (replace -3) (("1" (replace -4) (("1" (simplify (-1 -2)) (("1" (expand "<=" -1) (("1" (replace -2 -1) (("1" (simplify -1) (("1" (lemma "both_sides_expt_lt1_lt" ("lt1x" "1+x!1" "j" "0" "i" "pn!1")) (("1" (bash) (("1" (expand "^" -1 2) (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "lt_times_lt_nn1" ("nnx" "0" "y" "1+y!1" "nnz" "0" "w" "pn!1")) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (lemma "expt_1i" ("i" "pn!1")) (("2" (replace -1) (("2" (simplify -5) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (lemma "trich_lt" ("x" "y!1" "y" "0")) (("3" (split -1) (("1" (lemma "both_sides_times_pos_lt1" ("x" "0" "y" "x!1" "pz" "(1 + y!1) * pn!1")) (("1" (replace -3 -1) (("1" (simplify -1) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "lt_times_lt_nn1" ("nnx" "0" "y" "pn!1" "nnz" "0" "w" "1+y!1")) (("2" (grind) nil nil)) nil)) nil) ("2" (replace -1) (("2" (lemma "both_sides_times_pos_lt1" ("x" "0" "y" "x!1" "pz" "pn!1")) (("2" (bash) nil nil)) nil)) nil) ("3" (lemma "A4_5pp" ("x" "x!1")) (("3" (replace -3) (("3" (simplify -1) (("3" (inst - "pn!1") (("3" (inst - "y!1") (("3" (replace -2) (("3" (simplify -1) (("3" (replace -6 -1) (("3" (simplify -1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (trich_lt formula-decl nil real_props nil) (A4_5pp formula-decl nil prelude_A4 nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (posint_exp application-judgement "posint" exponentiation nil) (expt_1i formula-decl nil exponentiation nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (<= const-decl "bool" reals nil) (lt_le_transitivity formula-decl nil prelude_aux nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnreal type-eq-decl nil real_types nil) (lt_times_lt_nn1 formula-decl nil prelude_aux nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (^ const-decl "real" exponentiation nil) (expt def-decl "real" exponentiation 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) (both_sides_expt_lt1_lt formula-decl nil exponentiation nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (A4_5nn formula-decl nil prelude_A4 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) (real_plus_real_is_real application-judgement "real" reals 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)) nil)) (A4_6pp_TCC1 0 (A4_6pp_TCC1-1 nil 3250069458 ("" (grind) nil nil) ((/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (A4_6pp 0 (A4_6pp-1 nil 3250069458 ("" (skolem!) (("" (flatten) (("" (induct "n") (("1" (skosimp*) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "y!1" "py" "1+x!1")) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "trich_lt" ("x" "j!1" "y" "0")) (("2" (split -1) (("1" (assert) nil nil) ("2" (replace -1) (("2" (lemma "both_sides_plus_lt1" ("x" "0" "y" "x!1" "z" "1")) (("2" (lemma "div_mult_pos_lt1" ("z" "x!1" "py" "1+x!1" "x" "1")) (("1" (lemma "div_mult_pos_lt2" ("x" "y!1" "py" "1+x!1" "z" "x!1")) (("1" (lemma "both_sides_times_pos_lt1" ("x" "1" "y" "x!1+1" "pz" "x!1")) (("1" (lemma "div_mult_pos_lt1" ("x" "x!1" "py" "1+x!1" "z" "x!1")) (("1" (grind) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("3" (name "z!1" "j!1*y!1/(j!1+1)") (("3" (inst - "z!1") (("3" (bash) (("1" (lemma "expt_plus" ("n0x" "1 + x!1" "i" "1" "j" "j!1")) (("1" (replace -1) (("1" (name-replace "AA" "(1 + x!1) ^ j!1") (("1" (hide -1) (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (lemma "both_sides_times_neg_lt1" ("y" "0" "x" "x!1" "nz" "-j!1")) (("1" (lemma "both_sides_plus_lt1" ("y" "x!1" "x" "x!1* -j!1" "z" "1")) (("1" (lemma "both_sides_times_pos_lt1" ("y" "x!1 + 1" "x" "1 - x!1 * j!1" "pz" "y!1")) (("1" (lemma "div_mult_pos_lt1" ("x" "x!1" "py" "j!1+1" "z" "(1-x!1 * j!1) * y!1")) (("1" (lemma "minus_div1" ("x" "1" "n0x" "1" "y" "j!1*(1+x!1)" "n0y" "j!1+1")) (("1" (rewrite "div_simp" -1) (("1" (lemma "both_sides_plus_lt1" ("x" "y!1*(1 - (j!1 * (1 + x!1) / (j!1 + 1)))" "y" "x!1" "z" "y!1*j!1 * (1 + x!1) / (j!1 + 1)")) (("1" (replace -7 -9 rl) (("1" (replace -12 -6) (("1" (simplify -6) (("1" (lemma "lt_le_transitivity") (("1" (inst-cp - "x!1 * -j!1" "0" "x!1") (("1" (expand "<=") (("1" (replace -8 -2) (("1" (simplify -2) (("1" (replace -7) (("1" (replace -2) (("1" (simplify -6) (("1" (inst - "y!1 - j!1 * x!1 * y!1" "x!1 * y!1 + y!1" "j!1 * x!1 + x!1") (("1" (replace -13) (("1" (replace -6) (("1" (simplify -1) (("1" (replace -1) (("1" (simplify -5) (("1" (hide (-1 -2 -6 -7 -8)) (("1" (simplify -2) (("1" (replace -2 -1) (("1" (replace -3 -1) (("1" (hide (-2 -3)) (("1" (lemma "lt_le_transitivity" ("x" "1+y!1" "y" "1+x!1 + y!1 * j!1 * (1 + x!1) / (j!1 + 1)" "z" "AA + AA * x!1")) (("1" (lemma "both_sides_times_pos_lt2" ("x" "1 + j!1 * y!1 / (1 + j!1)" "y" "AA" "pz" "1+x!1")) (("1" (replace -6 -1) (("1" (simplify -1) (("1" (replace -1 -2) (("1" (lemma "both_sides_plus_lt1" ("x" "y!1 * ((1 - j!1 * x!1) / (1 + j!1)) + y!1 * j!1 * (1 + x!1) / (j!1 + 1)" "y" "x!1 + y!1 * j!1 * (1 + x!1) / (j!1 + 1)" "z" "1")) (("1" (replace -4 -1) (("1" (hide (-4)) (("1" (simplify -1) (("1" (hide -2) (("1" (lemma "div_distributes" ("x" "(j!1 * x!1 * y!1 + j!1 * y!1)" "y" "y!1 *(1 - j!1 * x!1)" "n0z" "1 + j!1")) (("1" (rewrite "times_div1" -2) (("1" (name-replace "B" "(j!1 * x!1 * y!1 + j!1 * y!1) / (1 + j!1)") (("1" (name-replace "C" "(y!1 - j!1 * x!1 * y!1) / (1 + j!1)") (("1" (simplify -1) (("1" (lemma "div_cancel1" ("n0z" "1+j!1" "x" "y!1")) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind) (("2" (replace -1 1 rl) (("2" (lemma "div_mult_pos_lt1" ("py" "j!1+1" "x" "x!1" "z" "x!1 * y!1 + y!1")) (("2" (lemma "both_sides_times_pos_lt2" ("x" "(x!1 * y!1 + y!1) / (j!1 + 1)" "y" "x!1" "pz" "j!1")) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "lt_times_lt_nn1" ("nnx" "0" "y" "j!1 / (j!1 + 1)" "nnz" "0" "w" "y!1")) (("3" (lemma "posreal_div_posreal_is_posreal" ("px" "j!1" "py" "j!1+1")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((both_sides_plus_lt1 formula-decl nil real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (expt def-decl "real" exponentiation nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (nnreal type-eq-decl nil real_types nil) (lt_times_lt_nn1 formula-decl nil prelude_aux nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (expt_plus formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (div_simp formula-decl nil real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (both_sides_times_pos_lt2 formula-decl nil real_props nil) (times_div1 formula-decl nil real_props nil) (div_cancel1 formula-decl nil real_props nil) (div_distributes formula-decl nil real_props nil) (lt_le_transitivity formula-decl nil prelude_aux nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (minus_div1 formula-decl nil real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (negreal nonempty-type-eq-decl nil real_types 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_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (trich_lt formula-decl nil real_props 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) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (nat_induction formula-decl nil naturalnumbers nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans 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 "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) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (A4_6pp_general_TCC1 0 (A4_6pp_general_TCC1-1 nil 3250069458 ("" (grind) nil nil) ((/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (A4_6pp_general 0 (A4_6pp_general-1 nil 3250069458 ("" (skosimp*) (("" (lemma "trich_lt" ("x" "y!1" "y" "0")) (("" (split) (("1" (lemma "both_sides_expt_gt1_le" ("gt1x" "1+x!1" "i" "0" "j" "n!1")) (("1" (simplify -1) (("1" (expand "^" -1 1) (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace -1) (("2" (lemma "trich_lt" ("x" "n!1" "y" "0")) (("2" (split) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (lemma "both_sides_expt_gt1_lt" ("gt1x" "1+x!1" "i" "0" "j" "n!1")) (("1" (expand "^" -1 1) (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (lemma "A4_6pp" ("x" "x!1")) (("3" (replace -3) (("3" (simplify -1) (("3" (inst - "n!1") (("3" (inst - "y!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (trich_lt formula-decl nil real_props nil) (A4_6pp formula-decl nil prelude_A4 nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (both_sides_expt_gt1_lt formula-decl nil exponentiation 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 "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (both_sides_expt_gt1_le formula-decl nil exponentiation nil) (real_plus_real_is_real application-judgement "real" reals 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation 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) (expt def-decl "real" exponentiation nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (A4_6nn_TCC1 0 (A4_6nn_TCC1-1 nil 3250069458 ("" (grind) nil nil) ((/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (A4_6nn 0 (A4_6nn-1 nil 3250069458 ("" (skosimp) (("" (induct "n") (("1" (skosimp*) (("1" (grind) nil nil)) nil) ("2" (skosimp*) (("2" (lemma "trich_lt" ("x" "j!1" "y" "0")) (("2" (split) (("1" (assert) nil nil) ("2" (replace -1) (("2" (lemma "negreal_times_negreal_is_posreal" ("nx" "x!1" "ny" "y!1")) (("1" (lemma "lt_minus_lt1" ("x" "y!1 * (1 + x!1)" "y" "x!1" "w" "0" "z" "x!1 * y!1")) (("1" (expand "<=" -1) (("1" (replace -7 -1) (("1" (expand ">" -2) (("1" (replace -2 -1) (("1" (simplify -1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil) ("3" (name "z!1" "j!1*y!1/(j!1+1)") (("3" (inst - "z!1") (("3" (lemma "expt_plus" ("n0x" "1 + x!1" "i" "1" "j" "j!1")) (("1" (replace -1) (("1" (name-replace "AA" "(1 + x!1) ^ j!1") (("1" (hide -1) (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (lemma "div_mult_pos_lt1" ("z" "j!1" "x" "1" "py" "j!1 + 1")) (("1" (simplify -1) (("1" (lemma "both_sides_div_pos_lt1" ("x" "0" "y" "j!1" "pz" "j!1+1")) (("1" (simplify -1) (("1" (replace -4 -1) (("1" (simplify -1) (("1" (lemma "lt_times_lt_np1" ("x" "-1" "npy" "y!1" "npw" "-1*j!1/ (1 + j!1)" "z" "-1")) (("1" (lemma "lt_times_lt_np1" ("x" "y!1" "npy" "0" "z" "-1*j!1/ (1 + j!1)" "npw" "0")) (("1" (lemma "both_sides_times_neg_lt1" ("nz" "-1")) (("1" (inst-cp - "j!1 / (1 + j!1)" "0") (("1" (inst-cp - "1" "j!1 / (1 + j!1)") (("1" (inst-cp - "0" "y!1 * j!1 / (1 + j!1)") (("1" (inst - "y!1 * j!1 / (1 + j!1)" "-1") (("1" (replace -13) (("1" (replace -12) (("1" (replace -8) (("1" (replace -7) (("1" (flatten (-3 -4)) (("1" (replace -3) (("1" (replace -4) (("1" (simplify (-5 -6)) (("1" (replace -5) (("1" (replace -6) (("1" (flatten (-1 -2)) (("1" (replace -9) (("1" (replace -1) (("1" (replace -2) (("1" (simplify -11) (("1" (hide (-1 -2 -3 -4 -5 -6 -7 -8)) (("1" (lemma "both_sides_times_pos_lt1" ("x" "y!1 * (1 + x!1)" "y" "(j!1 + 1) * x!1" "pz" "j!1")) (("1" (lemma "div_mult_pos_lt1" ("x" "x!1 * j!1" "py" "j!1+1" "z" "(1 + x!1)*j!1 * y!1")) (("1" (replace -1 -2 rl) (("1" (replace -8 -2) (("1" (flatten -2) (("1" (hide -1) (("1" (replace -2 -4 rl) (("1" (simplify -4) (("1" (rewrite "times_div1" -4) (("1" (rewrite "div_distributes" -4) (("1" (replace -1 -4) (("1" (simplify -4) (("1" (hide (-1 -2)) (("1" (lemma "lt_le_transitivity" ("x" "1+y!1" "y" "(1 + j!1 * y!1 / (1 + j!1))*(1+x!1)" "z" "(1+x!1)*AA")) (("1" (lemma "both_sides_times_pos_lt1" ("x" "1 + j!1 * y!1 / (1 + j!1)" "y" "AA" "pz" "1+x!1")) (("1" (replace -1 -4 rl) (("1" (replace -4 -2) (("1" (hide (-1 -4)) (("1" (expand "<=" -1) (("1" (lemma "lt_le_transitivity" ("x" "1+x!1" "y" "1" "z" "1-j!1*x!1")) (("1" (expand "<=" -1) (("1" (simplify -1) (("1" (lemma "both_sides_plus_lt1" ("x" "x!1" "y" "0" "z" "1")) (("1" (replace -1 -2) (("1" (replace -9) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "j!1" "py" "-x!1")) (("1" (expand ">" -1) (("1" (lemma "both_sides_plus_lt1" ("x" "0" "y" "j!1 * -x!1" "z" "1")) (("1" (replace -2 -1) (("1" (simplify -1) (("1" (replace -1 -4) (("1" (simplify -4) (("1" (hide (-1 -2 -3)) (("1" (lemma "both_sides_times_neg_lt2" ("y" "1 + x!1" "x" "1 - j!1 * x!1" "nz" "y!1")) (("1" (replace -1 -2 rl) (("1" (lemma "lt_le_transitivity" ("x" "y!1 * (1 - j!1 * x!1)" "y" "y!1 * (1 + x!1)" "z" "(j!1 + 1) * x!1")) (("1" (replace -8 -1) (("1" (expand "<=" -1) (("1" (replace -3 -1) (("1" (simplify -1) (("1" (hide (-2 -3)) (("1" (lemma "div_mult_pos_lt1" ("z" "y!1*(1-j!1*x!1)" "x" "x!1" "py" "j!1+1")) (("1" (replace -2 -1) (("1" (hide -2) (("1" (flatten -1) (("1" (lemma "minus_div2" ("x" "j!1+1" "n0x" "j!1+1" "y" "j!1*(1+x!1)")) (("1" (rewrite "div_simp" -1) (("1" (simplify -1) (("1" (lemma "times_div1" ("x" "y!1" "y" "1 - j!1 * x!1" "n0z" "j!1 + 1")) (("1" (replace -1 -3 rl) (("1" (replace -2 -3 rl) (("1" (hide (-1 -2)) (("1" (name "B" "(j!1 * x!1 + j!1) / (1 + j!1)") (("1" (replace -1 -2) (("1" (lemma "both_sides_plus_lt1" ("x" "y!1 * (1 - B)" "y" "x!1" "z" "y!1*B")) (("1" (replace -1 -3 rl) (("1" (simplify -3) (("1" (lemma "commutative_mult" ("x" "y!1" "y" "B")) (("1" (replace -1) (("1" (simplify -4) (("1" (replace -3 -4 rl) (("1" (hide (-1 -2 -3)) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (nat_induction formula-decl nil naturalnumbers nil) (expt def-decl "real" exponentiation 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) (trich_lt formula-decl nil real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (expt_plus formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div1 formula-decl nil real_props nil) (both_sides_plus_lt1 formula-decl nil real_props nil) (both_sides_times_neg_lt2 formula-decl nil real_props nil) (minus_div2 formula-decl nil real_props nil) (commutative_mult formula-decl nil number_fields nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (div_simp formula-decl nil real_props nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (minus_real_is_real application-judgement "real" reals nil) (minus_even_is_even application-judgement "even_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (lt_le_transitivity formula-decl nil prelude_aux nil) (div_distributes formula-decl nil real_props nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (both_sides_times_neg_lt1 formula-decl nil real_props nil) (npreal type-eq-decl nil real_types nil) (lt_times_lt_np1 formula-decl nil prelude_aux nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (both_sides_div_pos_lt1 formula-decl nil 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_lt1 formula-decl nil real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (lt_minus_lt1 formula-decl nil real_props nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (> const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (negreal_times_negreal_is_posreal judgement-tcc nil real_types nil)) nil)) (A4_6nn_general_TCC1 0 (A4_6nn_general_TCC1-1 nil 3250069458 ("" (grind) nil nil) ((/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (A4_6nn_general 0 (A4_6nn_general-1 nil 3250069458 ("" (skosimp*) (("" (lemma "trich_lt" ("x" "y!1" "y" "-1")) (("" (split) (("1" (lemma "posreal_exp" ("i" "n!1" "x" "1+x!1")) (("1" (name-replace "AA" "(1 + x!1) ^ n!1") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (replace -1) (("2" (lemma "posreal_exp" ("i" "n!1" "x" "1+x!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("3" (lemma "A4_6nn" ("x" "x!1")) (("3" (replace -3) (("3" (replace -4) (("3" (simplify -1) (("3" (inst - "n!1") (("3" (inst - "y!1") (("3" (replace -2) (("3" (grind) nil nil)) 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) (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) (trich_lt formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (A4_6nn formula-decl nil prelude_A4 nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_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) (posreal_exp judgement-tcc nil exponentiation nil) (real_plus_real_is_real application-judgement "real" reals 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) (AND const-decl "[bool, bool -> bool]" booleans 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) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil)) nil)) (A4_sqrt_ineq1 0 (A4_sqrt_ineq1-1 nil 3250069458 ("" (lemma "sq_lt" ("nna" "sqrt(2)" "nnb" "3/2")) (("" (rewrite "sq_sqrt") (("" (expand "sq") (("" (assert) nil nil)) nil)) nil)) nil) ((sq_sqrt formula-decl nil sqrt "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sq const-decl "nonneg_real" sq "reals/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (sq_lt formula-decl nil sq "reals/") (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types 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) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)) nil)) (A4_sqrt_ineq2 0 (A4_sqrt_ineq2-1 nil 3250069458 ("" (lemma "sq_lt" ("nna" "1/sqrt(2)" "nnb" "7/8")) (("" (rewrite "sq_div") (("" (rewrite "sq_1") (("" (rewrite "sq_sqrt") (("" (expand "sq") (("" (expand "^") (("" (expand "expt") (("" (expand "expt") (("" (expand "expt") (("" (expand "expt") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_div formula-decl nil sq "reals/") (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_1 formula-decl nil sq "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (posnat_expt application-judgement "posnat" exponentiation nil) (^ const-decl "real" exponentiation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (expt def-decl "real" 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) (posint_times_posint_is_posint application-judgement "posint" integers nil) (sq const-decl "nonneg_real" sq "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (sq_lt formula-decl nil sq "reals/") (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real 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) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")) nil)) (A4_sqrt_ineq3 0 (A4_sqrt_ineq3-1 nil 3250069458 ("" (lemma "sq_lt" ("nna" "1/8" "nnb" "1/sqrt(2)")) (("" (rewrite "sq_div") (("" (rewrite "sq_div") (("" (rewrite "sq_1") (("" (rewrite "sq_sqrt") (("" (expand "sq") (("" (expand "^") (("" (expand "expt") (("" (expand "expt") (("" (expand "expt") (("" (expand "expt") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq_div formula-decl nil sq "reals/") (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_1 formula-decl nil sq "reals/") (sq const-decl "nonneg_real" sq "reals/") (posint_times_posint_is_posint application-judgement "posint" 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) (expt def-decl "real" exponentiation nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (^ const-decl "real" exponentiation nil) (posnat_expt application-judgement "posnat" exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sq_sqrt formula-decl nil sqrt "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sq_lt formula-decl nil sq "reals/") (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real 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) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")) nil)) (A4_logsize 0 (A4_logsize-1 nil 3250069458 ("" (skosimp*) (("" (lemma "expt_x1" ("x" "2")) (("" (replace -1 -2 rl) (("" (lemma "posreal_exp" ("x" "2")) (("" (inst-cp - "l!1") (("" (inst - "-l!1") (("" (lemma "both_sides_times_pos_le1" ("pz" "2^-l!1" "x" "2^1" "y" "pn!1")) (("" (assert) (("" (lemma "expt_plus" ("n0x" "2" "i" "1" "j" "-l!1")) (("" (replace -1 -2 rl) (("" (hide -1) (("" (lemma "lt_le_transitivity" ("x" "2 ^ (1 + -l!1)" "y" "pn!1 * 2 ^ -l!1" "z" "2")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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_x1 formula-decl nil exponentiation nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (posreal_exp judgement-tcc nil exponentiation nil) (minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_exp application-judgement "posint" exponentiation nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (lt_le_transitivity formula-decl nil prelude_aux nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_plus formula-decl nil exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil 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)) nil)) (A4_lemma_ineq1 0 (A4_lemma_ineq1-1 nil 3250069458 ("" (skosimp*) (("" (case "1 <= n!1") (("1" (hide -1) (("1" (lemma "both_sides_sqrt_lt1" ("nnx" "2" "nny" "2")) (("1" (lemma "both_sides_div_pos_lt2" ("pz" "1" "px" "2" "py" "sqrt(2)")) (("1" (assert) (("1" (assert) (("1" (lemma "posreal_exp" ("x" "2" "i" "-n!1")) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "2^-n!1" "py" "sqrt(2)")) (("1" (lemma "both_sides_expt_lt1_lt" ("lt1x" "x!1" "j" "2" "i" "pn!1")) (("1" (assert) (("1" (expand "^" -1 2) (("1" (expand "expt") (("1" (expand "expt") (("1" (expand "expt") (("1" (lemma "div_mult_pos_le1" ("z" "2^-n!1" "py" "sqrt(2)" "x" "x!1")) (("1" (lemma "both_sides_expt_gt1_le" ("gt1x" "2" "i" "-n!1" "j" "-1")) (("1" (expand "^" -1 2) (("1" (expand "expt") (("1" (expand "expt") (("1" (lemma "both_sides_times_pos_lt1" ("x" "x!1" "y" "1/2" "pz" "x!1")) (("1" (lemma "A4_sqrt_ineq1") (("1" (lemma "both_sides_times_pos_lt1" ("x" "1/2" "y" "2-sqrt(2)" "pz" "x!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "both_sides_expt_gt1_lt" ("gt1x" "2" "i" "-n!1" "j" "0")) (("2" (assert) (("2" (rewrite "expt_x0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "both_sides_sqrt_lt3" ("nnx" "0" "nny" "2")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) 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 "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) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_div_pos_lt2 formula-decl nil real_props nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (posint_exp application-judgement "posint" exponentiation nil) (expt_x0 formula-decl nil exponentiation nil) (both_sides_expt_gt1_lt formula-decl nil exponentiation nil) (expt def-decl "real" exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (both_sides_expt_gt1_le formula-decl nil exponentiation nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (A4_sqrt_ineq1 formula-decl nil prelude_A4 nil) (posnat_expt application-judgement "posnat" exponentiation nil) (div_mult_pos_le1 formula-decl nil real_props 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) (< const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (both_sides_expt_lt1_lt formula-decl nil exponentiation nil) (- const-decl "[numfield -> numfield]" number_fields nil) (posreal_exp judgement-tcc nil exponentiation nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil)) nil)) (A4_lemma_ineq2 0 (A4_lemma_ineq2-1 nil 3250069458 ("" (skosimp*) (("" (hide -4) (("" (lemma "posreal_exp" ("x" "2" "i" "-n!1")) (("" (lemma "both_sides_expt_lt1_lt" ("lt1x" "x!1" "j" "1" "i" "pn!1")) (("1" (rewrite "expt_x1") (("1" (lemma "lt_plus_lt1" ("x" "2 ^ -n!1" "y" "x!1" "z" "x!1 ^ pn!1" "w" "x!1")) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((both_sides_expt_lt1_lt formula-decl nil exponentiation nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (lt_plus_lt1 formula-decl nil real_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (expt_x1 formula-decl nil exponentiation nil) (minus_int_is_int application-judgement "int" integers nil) (posreal_exp judgement-tcc 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil)) nil)) (A4_lemma_large_UB_0_TCC1 0 (A4_lemma_large_UB_0_TCC1-1 nil 3250069458 ("" (skosimp*) (("" (assert) nil nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_int_is_int application-judgement "int" integers nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (A4_lemma_large_UB_0 0 (A4_lemma_large_UB_0-1 nil 3250069458 ("" (skosimp*) (("" (lemma "sqrt_lt" ("nny" "sq(1)" "nnz" "2")) (("" (lemma "sqrt_lt" ("nny" "2" "nnz" "sq(2)")) (("" (rewrite "sqrt_sq") (("" (rewrite "sqrt_sq") (("" (expand "sq") (("" (lemma "both_sides_div_pos_lt2" ("pz" "1" "px" "2" "py" "sqrt(2)")) (("" (lemma "sq_le" ("nna" "1 / sqrt(2)" "nnb" "x!1")) (("1" (rewrite "sq_div" -1) (("1" (rewrite "sq_sqrt") (("1" (expand "sq") (("1" (assert) (("1" (case "0 < x!1 * x!1 - 1 + x!1") (("1" (lemma "lt_times_lt_nn1" ("nnx" "0" "y" "1-x!1" "nnz" "0" "w" "x!1 * x!1 - 1 + x!1")) (("1" (replace -2 -1) (("1" (split -1) (("1" (simplify -1) (("1" (simplify -1) (("1" (lemma "both_sides_expt_lt1_le" ("lt1x" "x!1" "i" "pn!1" "j" "3")) (("1" (lemma "both_sides_plus_lt1" ("x" "0" "y" "-1*(x!1 * x!1 * x!1) + 2*x!1 - 1" "z" "x!1 * x!1 * x!1 + 1")) (("1" (expand "^" -2 2) (("1" (expand "expt") (("1" (expand "expt") (("1" (expand "expt") (("1" (expand "expt") (("1" (lemma "posreal_exp" ("i" "pn!1" "x" "x!1")) (("1" (lemma "A4_5" ("x" "2 ^ -(2 + l!1)/x!1" "y" "1/x!1 ^ pn!1" "pn" "pn!1")) (("1" (assert) (("1" (hide -3) (("1" (lemma "posreal_div_posreal_is_posreal") (("1" (inst-cp - "1" "x!1 ^ pn!1") (("1" (lemma "posreal_exp" ("x" "2" "i" "-(l!1+1)")) (("1" (inst - "2 ^ -(2 + l!1)" "x!1") (("1" (assert) (("1" (lemma "div_mult_pos_lt1" ("z" "((pn!1*2 ^ -(2 + l!1))/x!1) *(x!1 ^ pn!1 + 1)" "py" "x!1 ^ pn!1" "x" "1/x!1 ^ pn!1")) (("1" (rewrite "div_cancel2" -1) (("1" (replace -1 -5) (("1" (hide -1) (("1" (lemma "div_mult_pos_lt1" ("z" "pn!1 * 2 ^ -(2 + l!1) * (x!1 ^ pn!1 + 1)" "py" "x!1" "x" "1")) (("1" (replace -1 -5) (("1" (hide -1) (("1" (lemma "expt_plus" ("n0x" "2" "i" "-l!1" "j" "-2")) (("1" (case "2^-2 = 1/4") (("1" (replace -1) (("1" (replace -2) (("1" (lemma "both_sides_div_pos_lt1" ("x" "pn!1 * 2 ^ -l!1" "y" "2" "pz" "4")) (("1" (lemma "div_mult_pos_lt1" ("z" "x!1 ^ pn!1 + 1" "py" "2" "x" "x!1")) (("1" (lemma "both_sides_times_pos_lt1" ("pz" "(x!1 ^ pn!1 + 1)" "x" "pn!1 * 2 ^ -l!1 / 4" "y" "1/2")) (("1" (lemma "expt_product" ("n0x" "1 + 2 ^ -l!1 * (1 / 4) / x!1" "n0y" "x!1" "i" "pn!1")) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "both_sides_times_pos_lt1" ("x" "(1 + 2 ^ -l!1 * (1 / 4) / x!1) ^ pn!1" "y" "1 + 1 / x!1 ^ pn!1" "pz" "x!1^pn!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sq const-decl "nonneg_real" sq "reals/") (nonneg_real nonempty-type-eq-decl nil real_types 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) (sqrt_lt formula-decl nil sqrt "reals/") (sqrt_sq formula-decl nil sqrt "reals/") (sqrt_pos application-judgement "posreal" sqrt "reals/") (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sq_le formula-decl nil sq "reals/") (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (both_sides_expt_lt1_le 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil 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) (^ const-decl "real" exponentiation nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (A4_5 formula-decl nil prelude_A4 nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (expt_product formula-decl nil prelude_aux nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (even_minus_even_is_even application-judgement "even_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (posnat_expt application-judgement "posnat" exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_plus formula-decl nil exponentiation nil) (minus_even_is_even application-judgement "even_int" integers nil) (div_cancel2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_exp judgement-tcc nil exponentiation nil) (expt def-decl "real" exponentiation nil) (- const-decl "[numfield -> numfield]" number_fields nil) (both_sides_plus_lt1 formula-decl nil real_props nil) (lt_times_lt_nn1 formula-decl nil prelude_aux nil) (real_minus_real_is_real application-judgement "real" reals 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) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (sq_sqrt formula-decl nil sqrt "reals/") (sq_1 formula-decl nil sq "reals/") (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_div formula-decl nil sq "reals/") (both_sides_div_pos_lt2 formula-decl nil real_props nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nnreal type-eq-decl nil real_types 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) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")) nil)) (A4_lemma_large_UB_TCC1 0 (A4_lemma_large_UB_TCC1-1 nil 3250069458 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (real_div_nzreal_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals 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_plus_posint_is_posint application-judgement "posint" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_int_is_int application-judgement "int" integers nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil)) nil)) (A4_lemma_large_UB 0 (A4_lemma_large_UB-1 nil 3250069458 ("" (skosimp*) (("" (case "1 <= n!1") (("1" (lemma "A4_lemma_ineq1" ("n" "n!1" "pn" "pn!1" "x" "x!1")) (("1" (lemma "A4_lemma_ineq2" ("pn" "pn!1" "l" "l!1" "x" "x!1" "n" "n!1")) (("1" (lemma "posreal_exp" ("i" "-n!1" "x" "2")) (("1" (lemma "posreal_exp" ("i" "-(2 + l!1 + n!1)" "x" "2")) (("1" (lemma "sqrt_lt" ("nny" "2" "nnz" "sq(2)")) (("1" (lemma "sqrt_lt" ("nny" "1" "nnz" "2")) (("1" (rewrite "sqrt_1") (("1" (rewrite "sqrt_sq") (("1" (expand "sq") (("1" (assert) (("1" (lemma "both_sides_div_pos_lt2" ("pz" "1" "px" "2" "py" "sqrt(2)")) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "e2!1" "py" "sqrt(2)")) (("1" (lemma "posreal_exp" ("i" "pn!1" "x" "x!1")) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "e1!1" "py" "x!1")) (("1" (lemma "A4_5pp" ("x" "e1!1/x!1")) (("1" (assert) (("1" (inst - "pn!1") (("1" (inst - "e2!1/x!1 ^ pn!1") (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "e2!1" "py" "x!1^pn!1")) (("1" (assert) (("1" (lemma "expt_product" ("n0x" "1+e1!1 / x!1" "n0y" "x!1" "i" "pn!1")) (("1" (replace -1) (("1" (lemma "div_mult_pos_lt2" ("x" "(1 + e1!1 / x!1) ^ pn!1" "z" "x!1 ^ pn!1 + e2!1" "py" "x!1 ^ pn!1")) (("1" (replace -1 1 rl) (("1" (hide -1 -2) (("1" (lemma "div_distributes" ("x" "x!1 ^ pn!1" "y" "e2!1" "n0z" "x!1 ^ pn!1")) (("1" (rewrite "div_simp" -1) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (lemma "expt_plus" ("n0x" "2")) (("1" (inst-cp - "-n!1" "-(l!1+2)") (("1" (inst - "-l!1" "-2") (("1" (case "2^-2=1/4") (("1" (replace -1) (("1" (replace -2) (("1" (replace -3) (("1" (replace -23 * rl) (("1" (lemma "posreal_exp" ("i" "-l!1" "x" "2")) (("1" (lemma "both_sides_times_pos_lt1" ("x" "pn!1 * 2 ^ -l!1" "y" "2" "pz" "2 ^ -n!1*2^-2 / x!1")) (("1" (lemma "both_sides_times_pos_lt1" ("x" "2 ^ -n!1 + x!1 ^ pn!1" "y" "2*x!1" "pz" "2 ^ -n!1/(x!1*2*x!1 ^ pn!1)")) (("1" (lemma "div_cancel1" ("n0z" "2 * x!1" "x" "2 ^ -n!1 /x!1 ^ pn!1")) (("1" (replace -1 -2) (("1" (hide -1) (("1" (simplify -1) (("1" (lemma "div_cancel1" ("n0z" "x!1 ^ pn!1" "x" "2 ^ -n!1 / (2 * x!1)")) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "lt_times_lt_pos1" ("px" "pn!1 * 2 ^ -l!1*2^-2" "y" "1/2" "nnz" "2 ^ -n!1 * (2 ^ -n!1 / (2 * (x!1 ^ pn!1 * x!1))) + 2 ^ -n!1 / (2 * x!1)" "w" "2 ^ -n!1 / x!1 ^ pn!1")) (("1" (lemma "both_sides_times_pos_lt1" ("x" "pn!1 * 2 ^ -l!1" "y" "2" "pz" "2^-2")) (("1" (replace -6) (("1" (replace -26) (("1" (flatten -1) (("1" (split -2) (("1" (flatten -4) (("1" (replace -28 * rl) (("1" (case "2 ^ -n!1 <= x!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-25 1)) (("2" (lemma "both_sides_div_pos_lt1" ("pz" "4" "x" "pn!1 * 2 ^ -l!1" "y" "2")) (("2" (assert) nil nil)) nil)) nil) ("3" (hide 2) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal" ("px" "2 ^ -n!1 * 2 ^ -n!1" "py" "2 * x!1 ^ pn!1 * x!1")) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "2 ^ -n!1" "py" "2 * x!1")) (("1" (hide-all-but (-1 -2 1)) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but (-10 1 -21 -16 -13)) (("2" (lemma "posreal_times_posreal_is_posreal" ("px" "2*x!1" "py" "x!1^pn!1")) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "posreal_times_posreal_is_posreal" ("px" "2*x!1" "py" "x!1^pn!1")) (("3" (hide-all-but (-1 1)) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_times_posreal_is_posreal" ("px" "2*x!1" "py" "x!1^pn!1")) (("2" (replace -26 * rl) (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "e2!1" "py" "2 * x!1 * x!1 ^ pn!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "posreal_times_posreal_is_posreal" ("px" "2*x!1" "py" "x!1^pn!1")) (("3" (hide-all-but (-1 -2)) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -2) (("2" (replace -24 * rl) (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "e2!1" "py" "4*x!1")) (("2" (hide-all-but (-1 1)) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "n!1=0") (("1" (rewrite "expt_x0") (("1" (replace -8) (("1" (lemma "A4_lemma_large_UB_0" ("pn" "pn!1" "x" "x!1" "l" "l!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil 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 "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) (A4_lemma_ineq2 formula-decl nil prelude_A4 nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt_sq formula-decl nil sqrt "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_times_real_is_real application-judgement "real" reals nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (div_distributes formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (expt_plus formula-decl nil exponentiation nil) (minus_even_is_even application-judgement "even_int" integers nil) (posnat_expt application-judgement "posnat" exponentiation nil) (posint_times_posint_is_posint application-judgement "posint" 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) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (even_minus_even_is_even application-judgement "even_int" integers nil) (expt def-decl "real" exponentiation nil) (NOT const-decl "[bool -> bool]" booleans nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (lt_times_lt_pos1 formula-decl nil real_props nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (div_cancel1 formula-decl nil real_props nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (div_simp formula-decl nil real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_product formula-decl nil prelude_aux nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (A4_5pp formula-decl nil prelude_A4 nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types nil) (both_sides_div_pos_lt2 formula-decl nil real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sqrt_1 formula-decl nil sqrt "reals/") (sq const-decl "nonneg_real" sq "reals/") (sqrt_lt formula-decl nil sqrt "reals/") (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal_exp judgement-tcc nil exponentiation nil) (minus_int_is_int application-judgement "int" integers nil) (A4_lemma_ineq1 formula-decl nil prelude_A4 nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (expt_x0 formula-decl nil exponentiation nil) (A4_lemma_large_UB_0 formula-decl nil prelude_A4 nil)) nil)) (A4_lemma_large_LB_TCC1 0 (A4_lemma_large_LB_TCC1-1 nil 3250069458 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (real_div_nzreal_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals 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_plus_posint_is_posint application-judgement "posint" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_int_is_int application-judgement "int" integers nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil)) nil)) (A4_lemma_large_LB 0 (A4_lemma_large_LB-1 nil 3250069458 ("" (skosimp*) (("" (lemma "posreal_exp" ("i" "-n!1" "x" "2")) (("" (lemma "sqrt_pos" ("px" "2")) (("" (lemma "posreal_div_posreal_is_posreal" ("px" "e2!1" "py" "sqrt(2)")) (("1" (lemma "posreal_exp" ("x" "2" "i" "-(n!1 + l!1 + 2)")) (("1" (lemma "sqrt_lt" ("nny" "2" "nnz" "sq(2)")) (("1" (rewrite "sqrt_sq") (("1" (expand "sq") (("1" (lemma "both_sides_div_pos_lt2" ("pz" "1" "px" "2" "py" "sqrt(2)")) (("1" (lemma "expt_plus" ("n0x" "2" "i" "-n!1" "j" "-(l!1+2)")) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "both_sides_expt_gt1_lt" ("gt1x" "2" "i" "-(l!1 + 2)" "j" "-1")) (("1" (assert) (("1" (expand "^" -1 2) (("1" (expand "expt") (("1" (expand "expt") (("1" (lemma "posreal_exp" ("x" "x!1" "i" "pn!1")) (("1" (lemma "A4_6nn_general" ("x" "-e1!1/x!1" "y" "-e2!1/x!1 ^ pn!1" "n" "pn!1")) (("1" (lemma "expt_product" ("n0x" "1-e1!1 / x!1" "n0y" "x!1" "i" "pn!1")) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "div_mult_pos_lt1" ("z" "x!1 ^ pn!1 - e2!1" "x" "(1 - e1!1 / x!1) ^ pn!1" "py" "x!1 ^ pn!1")) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (lemma "div_distributes_minus" ("x" "x!1 ^ pn!1" "y" "e2!1" "n0z" "x!1 ^ pn!1")) (("1" (rewrite "div_simp" -1) (("1" (replace -1 1 rl) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "e2!1" "py" "x!1^pn!1")) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "e1!1" "py" "x!1")) (("1" (lemma "both_sides_times_neg_gt2" ("x" "0" "nz" "-1")) (("1" (inst-cp - "e1!1 / x!1") (("1" (simplify -2) (("1" (replace -3 -2) (("1" (simplify -2) (("1" (inst - "e2!1 / x!1 ^ pn!1") (("1" (replace -4 -1) (("1" (simplify -1) (("1" (expand ">") (("1" (replace -1) (("1" (replace -2) (("1" (lemma "div_mult_pos_lt2" ("x" "-1" "z" "-e1!1" "py" "x!1")) (("1" (lemma "both_sides_times_neg_lt1" ("nz" "-1" "y" "e1!1" "x" "x!1")) (("1" (lemma "both_sides_times_pos_lt1" ("x" "2 ^ -(2 + l!1)" "y" "1/2" "pz" "2^-n!1")) (("1" (lemma "both_sides_times_pos_lt1" ("pz" "e2!1" "x" "1/2" "y" "1/sqrt(2)")) (("1" (lemma "both_sides_times_neg_lt1" ("y" "pn!1 *e1!1/x!1" "x" "e2!1/x!1^pn!1 - e1!1 /x!1 *(e2!1/x!1 ^ pn!1)" "nz" "-1")) (("1" (lemma "div_mult_pos_lt2" ("x" "pn!1 * e1!1 / x!1" "z" "e2!1 *(1-e1!1/x!1)" "py" "x!1 ^ pn!1")) (("1" (lemma " expt_plus" ("n0x" "2" "i" "-l!1" "j" "-2")) (("1" (lemma "both_sides_times_pos_lt1" ("x" "pn!1* 2 ^ -l!1" "y" "2" "pz" "2 ^ -n!1* 2 ^ -2")) (("1" (assert) (("1" (hide 2) (("1" (replace -2) (("1" (case-replace "2^-2=1/4") (("1" (replace -5 1) (("1" (replace -4 1) (("1" (hide -1 -3 -4 -5 -8) (("1" (lemma "both_sides_times_pos_lt1" ("x" "e1!1 * pn!1" "y" "2^-n!1 /2" "pz" "x!1 ^ pn!1")) (("1" (lemma "both_sides_div_pos_lt1" ("x" "pn!1 * e1!1*x!1 ^ pn!1" "y" "e2!1 * (x!1-e1!1)" "pz" "x!1")) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "both_sides_expt_lt1_lt" ("lt1x" "x!1" "j" "1" "i" "pn!1")) (("1" (rewrite "expt_x1") (("1" (lemma "lt_plus_lt1" ("x" "x!1 ^ pn!1" "y" "x!1" "z" "2*e1!1" "w" "x!1")) (("1" (lemma "both_sides_expt_gt1_le" ("gt1x" "2" "i" "-l!1" "j" "0")) (("1" (rewrite "expt_x0") (("1" (assert) (("1" (lemma "both_sides_times_pos_le1" ("x" "2 ^ -l!1" "y" "1" "pz" "2*2 ^ -n!1* 2 ^ -2")) (("1" (assert) (("1" (lemma "both_sides_times_pos_lt1" ("x" "x!1 ^ pn!1" "y" "2*(x!1-e1!1)" "pz" "e2!1/2")) (("1" (expand "^" -2 1) (("1" (expand "^" -2 3) (("1" (expand "expt") (("1" (expand "expt") (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "/=") (("2" (lemma "div_cancel3") (("2" (inst - "x!1" "e1!1" "1") (("2" (case "e1!1<x!1") (("1" (assert) nil nil) ("2" (lemma "both_sides_div_pos_lt2" ("pz" "e2!1" "px" "2" "py" "sqrt(2)")) (("2" (hide -2 -3 -4 -8) (("2" (lemma "both_sides_times_pos_lt1" ("pz" "e2!1" "x" "2 ^ -(2 + l!1)" "y" "1 / 2")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (posreal_exp judgement-tcc nil exponentiation nil) (minus_int_is_int application-judgement "int" integers nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (nnreal type-eq-decl nil real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (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) (AND const-decl "[bool, bool -> bool]" booleans nil) (sqrt_lt formula-decl nil sqrt "reals/") (sq const-decl "nonneg_real" sq "reals/") (expt_plus formula-decl nil exponentiation nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (expt def-decl "real" exponentiation nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (expt_product formula-decl nil prelude_aux nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (div_distributes_minus formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (minus_even_is_even application-judgement "even_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (even_minus_even_is_even application-judgement "even_int" integers nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (expt_x1 formula-decl nil exponentiation nil) (both_sides_expt_gt1_le formula-decl nil exponentiation nil) (posnat_expt application-judgement "posnat" exponentiation nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (expt_x0 formula-decl nil exponentiation nil) (lt_plus_lt1 formula-decl nil real_props nil) (both_sides_expt_lt1_lt formula-decl nil exponentiation nil) (both_sides_times_neg_lt1 formula-decl nil real_props nil) (real_times_real_is_real application-judgement "real" reals 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) (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_gt2 formula-decl nil real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (div_simp formula-decl nil real_props nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (div_cancel3 formula-decl nil real_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (A4_6nn_general formula-decl nil prelude_A4 nil) (^ const-decl "real" exponentiation nil) (both_sides_expt_gt1_lt formula-decl nil exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (both_sides_div_pos_lt2 formula-decl nil real_props nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sqrt_sq formula-decl nil sqrt "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (sqrt_pos judgement-tcc nil sqrt "reals/")) nil)) (A4_lemma_large_ge3 0 (A4_lemma_large_ge3-1 nil 3250069458 ("" (skosimp*) (("" (lemma "A4_lemma_large_UB" ("x" "x!1" "pn" "pn!1" "n" "n!1" "e1" "e1!1" "e2" "e2!1" "l" "l!1")) (("" (lemma "A4_lemma_large_LB" ("x" "x!1" "pn" "pn!1" "n" "n!1" "e1" "e1!1" "e2" "e2!1" "l" "l!1")) (("" (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) (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_lemma_large_UB formula-decl nil prelude_A4 nil) (real_minus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (posrat_exp application-judgement "posrat" exponentiation nil) (minus_int_is_int application-judgement "int" integers nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (real_div_nzreal_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (A4_lemma_large_LB formula-decl nil prelude_A4 nil)) nil)) (A4_lemma_large_lt3_TCC1 0 (A4_lemma_large_lt3_TCC1-1 nil 3250069458 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (real_div_nzreal_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals 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_plus_posint_is_posint application-judgement "posint" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_int_is_int application-judgement "int" integers nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil)) nil)) (A4_lemma_large_lt3_TCC2 0 (A4_lemma_large_lt3_TCC2-1 nil 3250069458 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (real_div_nzreal_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals 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_plus_posint_is_posint application-judgement "posint" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_int_is_int application-judgement "int" integers nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil)) nil)) (A4_lemma_large_lt3 0 (A4_lemma_large_lt3-1 nil 3250069458 ("" (skosimp*) (("" (split -1) (("1" (replace -1) (("1" (rewrite "expt_x1") (("1" (rewrite "expt_x1") (("1" (rewrite "expt_x1") (("1" (lemma "posreal_exp" ("x" "2")) (("1" (inst-cp - "-n!1") (("1" (inst - "-(n!1 + l!1 + 2)") (("1" (lemma "both_sides_expt_gt1_lt" ("gt1x" "2" "i" "-(n!1 + l!1 + 2)" "j" "-n!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "^" 1) (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (simplify 1) (("2" (lemma "both_sides_expt_gt1_le" ("gt1x" "2" "i" "-n!1" "j" "0")) (("2" (assert) (("2" (rewrite "expt_x0") (("2" (lemma "posreal_exp" ("x" "2" "i" "-n!1")) (("2" (lemma "expt_plus" ("n0x" "2" "i" "-n!1" "j" "-(l!1+2)")) (("2" (replace -1) (("2" (hide -1) (("2" (name-replace "AA" "2 ^ -n!1") (("2" (replace -9) (("2" (hide -9) (("2" (lemma "sqrt_lt" ("nny" "1" "nnz" "2")) (("2" (assert) (("2" (rewrite "sqrt_1") (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "AA" "py" "sqrt(2)")) (("2" (expand ">" -1) (("2" (lemma "le_lt_transitivity" ("x" "0" "y" "AA / sqrt(2)" "z" "x!1")) (("2" (replace -2 -1) (("2" (replace -7 -1) (("2" (simplify -1) (("2" (hide (-2 -3 -7)) (("2" (lemma "A4_logsize" ("pn" "pn!1" "l" "l!1")) (("2" (assert) (("2" (hide (-7 -8)) (("2" (hide -5) (("2" (lemma "posreal_exp" ("i" "-(2 + l!1)" "x" "2")) (("2" (lemma "both_sides_expt_gt1_le" ("gt1x" "2" "i" "-(2 + l!1)" "j" "-3")) (("2" (assert) (("2" (name-replace "B" "2 ^ -(2 + l!1)") (("2" (replace -8) (("2" (expand "^") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (hide (-3 -8)) (("2" (lemma "both_sides_plus_lt1" ("z" "x!1 * x!1")) (("2" (inst-cp - "- AA" "AA * B * (AA * B) - 2 * (AA * B * x!1)") (("2" (replace -2) (("2" (inst - "AA * B * (AA * B) + 2 * (AA * B * x!1)" "AA") (("2" (replace -1) (("2" (hide (-1 -2)) (("2" (lemma "both_sides_times_pos_lt1" ("pz" "AA")) (("2" (inst-cp - "-1" "B *(AA * B - 2*x!1)") (("2" (replace -2) (("2" (inst - "B * (AA*B + 2*x!1)" "1") (("2" (replace -1) (("2" (hide (-1 -2)) (("2" (lemma "le_times_le_pos" ("nnx" "AA" "y" "1" "nnz" "B" "w" "1/8")) (("2" (assert) (("2" (lemma "both_sides_times_pos_lt1" ("x" "x!1" "y" "1" "pz" "2")) (("2" (replace -1 -8 rl) (("2" (hide -1) (("2" (lemma "lt_plus_lt1" ("x" "AA * B" "y" "1/8" "z" "x!1 * 2" "w" "2")) (("2" (replace -2 -1) (("2" (replace -8 -1) (("2" (lemma "lt_times_lt_pos2" ("pz" "B" "w" "1/8" "nnx" "AA * B + x!1 * 2" "y" "1 / 8 + 2")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((expt_x1 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_int_is_int application-judgement "int" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield -> numfield]" number_fields 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) (both_sides_expt_gt1_lt formula-decl nil exponentiation nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (posreal_exp judgement-tcc nil exponentiation nil) (real_minus_real_is_real application-judgement "real" reals 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) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (^ const-decl "real" exponentiation nil) (posint_exp application-judgement "posint" exponentiation nil) (posrat nonempty-type-eq-decl nil rationals nil) (nonneg_rat nonempty-type-eq-decl nil rationals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sqrt_1 formula-decl nil sqrt "reals/") (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (both_sides_plus_lt1 formula-decl nil real_props nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (le_times_le_pos formula-decl nil real_props nil) (posrat_plus_nnrat_is_posrat application-judgement "posrat" rationals nil) (lt_times_lt_pos2 formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (lt_plus_lt1 formula-decl nil real_props nil) (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (A4_logsize formula-decl nil prelude_A4 nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (le_lt_transitivity formula-decl nil prelude_aux nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (sqrt_lt formula-decl nil sqrt "reals/") (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (expt_plus formula-decl nil exponentiation nil) (expt_x0 formula-decl nil exponentiation nil) (both_sides_expt_gt1_le formula-decl nil exponentiation nil) (expt def-decl "real" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (A4_lemma_small_UB_TCC1 0 (A4_lemma_small_UB_TCC1-1 nil 3250069458 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (real_div_nzreal_is_real application-judgement "real" reals 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_int_is_int application-judgement "int" integers nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil)) nil)) (A4_lemma_small_UB 0 (A4_lemma_small_UB-1 nil 3250069458 ("" (skosimp*) (("" (lemma "both_sides_sqrt_lt3" ("nnx" "0" "nny" "2")) (("" (assert) (("" (lemma "posreal_exp" ("i" "-n!1" "x" "2")) (("" (lemma "posreal_exp" ("i" "-(2 + l!1 + n!1)" "x" "2")) (("" (lemma "both_sides_plus_lt1" ("x" "x!1" "y" "e2!1 / sqrt(2)" "z" "e1!1")) (("" (lemma "expt_plus" ("n0x" "2" "i" "-n!1" "j" "-(l!1+2)")) (("" (replace -1) (("" (hide -1) (("" (lemma "both_sides_expt_gt1_le" ("gt1x" "2" "i" "-(l!1 + 2)" "j" "-3")) (("" (lemma "posreal_exp" ("i" "-(l!1+2)" "x" "2")) (("" (lemma "both_sides_expt_pos_lt" ("pm" "pn!1" "px" "x!1 + e1!1" "py" "e2!1*(1/sqrt(2)+2 ^ -(l!1 + 2))")) (("1" (replace -13 (-12 -5 -6) rl) (("1" (replace -12) (("1" (replace -4 -1) (("1" (simplify -1) (("1" (lemma "expt_product" ("n0x" "2 ^ -(2 + l!1)+ 1 / sqrt(2)" "n0y" "e2!1" "i" "pn!1")) (("1" (lemma "both_sides_expt_pos_le" ("pm" "pn!1" "px" "2 ^ -(2 + l!1) + 1 / sqrt(2)" "py" "2^-3+ 1 / sqrt(2)")) (("1" (lemma "both_sides_plus_le1" ("x" "2 ^ -(l!1 + 2)" "y" "2 ^ -3" "z" "1 / sqrt(2)")) (("1" (lemma "A4_sqrt_ineq2") (("1" (lemma "both_sides_expt_pos_lt" ("px" "1 / sqrt(2) + 2 ^ -3" "py" "1" "pm" "pn!1")) (("1" (rewrite "expt_1i") (("1" (assert) (("1" (lemma "both_sides_times_pos_lt1" ("x" "(2 ^ -(2 + l!1) + 1 / sqrt(2)) ^ pn!1" "y" "1" "pz" "e2!1 ^ pn!1")) (("1" (case "n!1=0") (("1" (replace -1) (("1" (rewrite "expt_x0") (("1" (replace -20) (("1" (assert) (("1" (rewrite "expt_1i") (("1" (lemma "both_sides_expt_lt1_le" ("lt1x" "x!1" "i" "pn!1" "j" "2")) (("1" (expand "^" -1 2) (("1" (expand "expt" -1) (("1" (expand "expt" -1) (("1" (expand "expt" -1) (("1" (lemma "lt_times_lt_pos1" ("px" "x!1" "y" "1 / sqrt(2)" "nnz" "x!1" "w" "1 / sqrt(2)")) (("1" (assert) (("1" (rewrite "div_times" -1) (("1" (lemma "sqrt_square1" ("nnx" "2")) (("1" (expand "square") (("1" (replace -1) (("1" (assert) (("1" (name-replace "AA" "2^ -(2+l!1)") (("1" (name-replace "B" "sqrt(2)") (("1" (name-replace "C" "2^ -3") (("1" (lemma "posreal_exp" ("i" "pn!1" "x" "x!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "1<=n!1") (("1" (lemma "both_sides_expt_gt1_le" ("gt1x" "2" "i" "-n!1" "j" "-1")) (("1" (assert) (("1" (expand "^" -1 2) (("1" (expand "expt" -1) (("1" (expand "expt" -1) (("1" (replace -21 -1 rl) (("1" (lemma "both_sides_expt_lt1_lt" ("lt1x" "e2!1" "j" "1" "i" "pn!1")) (("1" (assert) (("1" (rewrite "expt_x1") (("1" (assert) (("1" (lemma "lt_times_lt_pos1" ("px" "e2!1 ^ pn!1" "y" "e2!1" "nnz" "(2 ^ -(2 + l!1) + 1 / sqrt(2)) ^ pn!1" "w" "1")) (("1" (lemma "posreal_exp" ("i" "pn!1" "x" "x!1")) (("1" (assert) nil nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "sqrt(2)")) (("2" (lemma "expt_pos" ("px" "2" "i" "-(2+l!1)")) (("2" (lemma "expt_pos" ("px" "2 ^ -(2 + l!1) + 1 / sqrt(2)" "i" "pn!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "expt_pos" ("px" "e2!1" "i" "pn!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "expt_pos" ("px" "2" "i" "-3")) (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "sqrt(2)")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "sqrt(2)")) (("2" (lemma "expt_pos" ("px" "2" "i" "-3")) (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "sqrt(2)")) (("3" (lemma "expt_pos" ("px" "2" "i" "-(2+l!1)")) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "sqrt(2)")) (("2" (lemma "expt_pos" ("px" "2" "i" "-(2+l!1)")) (("2" (assert) (("2" (lemma "posreal_plus_nnreal_is_posreal" ("px" "2^ -(2+l!1)" "nny" "1/sqrt(2)")) (("2" (assert) (("2" (hide-all-but (-1 1)) (("2" (name-replace "AA" "2 ^ -(2 + l!1) + 1 / sqrt(2)") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "sqrt(2)")) (("2" (lemma "expt_pos" ("px" "2" "i" "-(2+l!1)")) (("2" (lemma "posreal_times_posreal_is_posreal" ("px" "2^ -(2+l!1) + 1/sqrt(2)" "py" "e2!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (real_div_nzreal_is_real application-judgement "real" reals 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (expt_plus formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (expt_product formula-decl nil prelude_aux nil) (both_sides_plus_le1 formula-decl nil real_props nil) (expt_pos formula-decl nil exponentiation nil) (expt_x0 formula-decl nil exponentiation nil) (both_sides_expt_lt1_le formula-decl nil exponentiation nil) (< const-decl "bool" reals nil) (expt def-decl "real" exponentiation nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (nonneg_rat nonempty-type-eq-decl nil rationals nil) (posrat nonempty-type-eq-decl nil rationals nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (div_times formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (lt_times_lt_pos1 formula-decl nil real_props nil) (<= const-decl "bool" reals nil) (both_sides_expt_lt1_lt formula-decl nil exponentiation nil) (expt_x1 formula-decl nil exponentiation nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (expt_1i formula-decl nil exponentiation nil) (A4_sqrt_ineq2 formula-decl nil prelude_A4 nil) (both_sides_expt_pos_le formula-decl nil exponentiation nil) (posreal_exp application-judgement "posreal" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (both_sides_expt_pos_lt formula-decl nil exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (both_sides_expt_gt1_le formula-decl nil exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnreal type-eq-decl nil real_types 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_plus_lt1 formula-decl nil real_props nil) (posreal_exp judgement-tcc 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil)) nil)) (A4_lemma_small_LB_TCC1 0 (A4_lemma_small_LB_TCC1-1 nil 3250069458 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (real_div_nzreal_is_real application-judgement "real" reals 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_int_is_int application-judgement "int" integers nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil)) nil)) (A4_lemma_small_LB 0 (A4_lemma_small_LB-1 nil 3250069458 ("" (skosimp*) (("" (lemma "posreal_exp" ("i" "-n!1" "x" "2")) (("" (lemma "posreal_exp" ("i" "-(l!1+2)" "x" "2")) (("" (lemma "posreal_exp" ("i" "pn!1" "x" "x!1")) (("1" (lemma "expt_plus" ("n0x" "2" "i" "-n!1" "j" "-(l!1+2)")) (("1" (replace -1) (("1" (lemma "both_sides_expt_gt1_le" ("gt1x" "2" "i" "-(l!1 + 2)" "j" "-3")) (("1" (assert) (("1" (hide -2) (("1" (name-replace "B" "2 ^ -(2 + l!1)") (("1" (expand "^" -1) (("1" (expand "expt") (("1" (expand "expt") (("1" (expand "expt") (("1" (expand "expt") (("1" (lemma "sqrt_lt" ("nny" "1" "nnz" "2")) (("1" (rewrite "sqrt_1") (("1" (lemma "div_mult_pos_lt1" ("x" "1" "py" "sqrt(2)" "z" "1")) (("1" (assert) (("1" (lemma "both_sides_expt_gt1_le" ("gt1x" "2" "i" "-n!1" "j" "0")) (("1" (rewrite "expt_x0") (("1" (assert) (("1" (name-replace "AA" "2^-n!1") (("1" (replace -12) (("1" (replace -13) (("1" (lemma "lt_times_lt_pos1" ("px" "AA" "y" "1" "nnz" "1 / sqrt(2)" "w" "1")) (("1" (assert) (("1" (lemma "both_sides_expt_pos_lt" ("pm" "pn!1" "px" "x!1" "py" "1")) (("1" (assert) (("1" (rewrite "expt_1i") (("1" (lemma "trich_lt" ("x" "x!1" "y" "AA*B")) (("1" (lemma "both_sides_expt_lt1_le" ("lt1x" "x!1" "i" "pn!1" "j" "2")) (("1" (assert) (("1" (expand "^" -1 2) (("1" (expand "expt") (("1" (expand "expt") (("1" (expand "expt") (("1" (lemma "lt_times_lt_pos1" ("px" "x!1" "y" "AA / sqrt(2)" "nnz" "x!1" "w" "AA / sqrt(2)")) (("1" (assert) (("1" (rewrite "div_times" -1) (("1" (lemma "sqrt_sq" ("x" "2")) (("1" (expand "sq") (("1" (lemma "both_sides_div_pos_le1" ("x" "AA" "y" "1" "pz" "2")) (("1" (lemma "both_sides_minus_le1" ("x" "AA/2" "y" "1/2" "z" "1")) (("1" (lemma "both_sides_times_pos_le1" ("x" "AA / 2 - 1" "y" "-1/2" "pz" "AA")) (("1" (assert) (("1" (split -7) (("1" (case "even?(pn!1)") (("1" (lemma "expt_neg_even" ("n" "pn!1" "nx" "x!1 - AA * B")) (("1" (assert) (("1" (replace -1) (("1" (lemma "posreal_exp" ("i" "pn!1" "x" "-(x!1-AA*B)")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (rewrite "odd_even") (("2" (lemma "expt_neg_odd" ("n" "pn!1" "nx" "x!1 - AA * B")) (("1" (assert) (("1" (replace -1) (("1" (hide (-1 -5 -6)) (("1" (hide -1) (("1" (lemma "lt_times_lt_pos1" ("px" "AA" "y" --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.761 Sekunden (vorverarbeitet am 2026-04-26) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26