| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/lnexp_fnd/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 507 kB |
|
Quelle ln_series.prfSprache: Lisp |
|||||||||||||||
|
(ln_series (noa_posreal 0 (noa_posreal-1 nil 3477843250 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst + "x!1 + 1") (("" (assert) nil nil)) nil)) nil)) 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) (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_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) shostak)) (noa_gt_m1 0 (noa_gt_m1-1 nil 3477843265 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst + "x!1 + 1") (("" (assert) nil nil)) nil)) nil)) 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) (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) shostak)) (conn_gt_m1 0 (conn_gt_m1-1 nil 3477843280 ("" (expand "connected?") (("" (skosimp*) (("" (assert) nil nil)) nil)) 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (connected? const-decl "bool" deriv_domain_def "analysis/")) shostak)) (conn_posreal 0 (conn_posreal-1 nil 3477843288 ("" (expand "connected?") (("" (skosimp*) (("" (assert) nil nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected? const-decl "bool" deriv_domain_def "analysis/")) shostak)) (conn_abslt1 0 (conn_abslt1-1 nil 3477843296 ("" (expand "connected?") (("" (skosimp*) (("" (assert) (("" (typepred "y!1") (("" (typepred "x!1") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((abslt1 type-eq-decl nil ln_series nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (real_le_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) (connected? const-decl "bool" deriv_domain_def "analysis/")) shostak)) (noa_abslt1 0 (noa_abslt1-1 nil 3477843230 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst-cp + "1/2") (("1" (inst + "1/4") (("1" (assert) nil nil) ("2" (grind) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil) ((/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (abslt1 type-eq-decl nil ln_series 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) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) nil)) (deriv_domain_gtm1 0 (deriv_domain_gtm1-1 nil 3477843360 ("" (expand "deriv_domain?") (("" (skosimp*) (("" (inst + "e!1/2") (("" (grind) nil nil)) nil)) nil)) nil) ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs 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) (>= const-decl "bool" reals nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (- const-decl "[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) (bool nonempty-type-eq-decl nil booleans nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (nderiv_ln_TCC1 0 (nderiv_ln_TCC1-1 nil 3563622659 ("" (assert) nil nil) ((deriv_domain_posreal formula-decl nil deriv_domain "analysis/")) nil)) (nderiv_ln_TCC2 0 (nderiv_ln_TCC2-1 nil 3563622659 ("" (assert) nil nil) ((noa_posreal formula-decl nil ln_series nil)) nil)) (nderiv_ln 0 (nderiv_ln-2 nil 3445354085 ("" (case "FORALL (n: nat): derivable_n_times?[posreal](ln, n) & nderiv[posreal](n,ln) = (("1" (skosimp*) (("1" (inst - "n!1") (("1" (flatten) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (expand "derivable_n_times?") (("1" (propax) nil nil)) nil) ("2" (expand "nderiv") (("2" (propax) nil nil)) nil) ("3" (skosimp*) (("3" (case-replace "j!1=0") (("1" (lemma "ln_derivable") (("1" (flatten -1) (("1" (expand "derivable_n_times?") (("1" (expand "derivable_n_times?") (("1" (expand "nderiv" 1) (("1" (expand "nderiv" 1) (("1" (lemma "extensionality" ("f" "deriv(ln)" "g" "(LAMBDA (x: posreal): -factorial(1) / (-x) ^ 1)")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide 2) (("2" (replace -2) (("2" (skosimp*) (("2" (expand "factorial") (("2" (expand "factorial") (("2" (rewrite "expt_x1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "ln_derivable") (("2" (flatten -1) (("2" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "const_derivable_fun[posreal]" ("b" "-factorial(j!1)")) (("1" (lemma "deriv_id_fun[posreal]") (("1" (lemma "deriv_const_fun[posreal]" ("b" "-factorial(j!1)")) (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "neg_derivable_fun[posreal]" ("f" "LAMBDA (x: posreal): x")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_neg_fun[posreal]" ("ff" "LAMBDA (x: posreal): x")) (("1" (replace -4) (("1" (expand "-" -1) (("1" (lemma "inv_derivable_fun[posreal]" ("g" "LAMBDA (x_1: posreal): -x_1")) (("1" (assert) (("1" (expand "/") (("1" (lemma "deriv_inv_fun[posreal]" ("gg" "LAMBDA (x_1: posreal): -x_1")) (("1" (replace -3) (("1" (expand "/") (("1" (expand "*") (("1" (expand "-" -1) (("1" (lemma "extensionality" ("f" "LAMBDA (x: posreal): --1 / (-x * -x)" "g" "LAMBDA (x: posreal): 1 / (x * x)")) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "deriv_exp_fun[posreal]" ("f" "LAMBDA (x: posreal): 1 / -x" "n" "j!1")) (("1" (assert) (("1" (flatten -1) (("1" (lemma "scal_derivable_fun[posreal]" ("f" "(LAMBDA (x: posreal): 1 / -x) ^ j!1" "b" "-factorial(j!1 - 1)")) (("1" (replace -2) (("1" (lemma "deriv_scal_fun[posreal]" ("ff" "(LAMBDA (x: posreal): 1 / -x) ^ j!1" "b" "-factorial(j!1 - 1)")) (("1" (replace -4 -1) (("1" (replace -5) (("1" (lemma "extensionality" ("f" "-factorial(j!1 - 1) * (LAMBDA (x: posreal): 1 / -x) ^ j!1" "g" "LAMBDA (x: posreal): -factorial(j!1 - 1) / (-x) ^ j!1")) (("1" (split -1) (("1" (replace -1 * rl) (("1" (replace -17 * rl) (("1" (lemma "extensionality" ("f" "-factorial(j!1 - 1) * (j!1 * (LAMBDA (x: posreal): 1 / -x) ^ (j!1 - 1) * (LAMBDA (x: posreal): 1 / (x * x)))" "g" "LAMBDA (x: posreal): -factorial(j!1) / (-x) ^ (1 + j!1)")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "nderiv_derivable_eqv[posreal]" ("f" "ln" "n" "j!1")) (("1" (replace -18 -1) (("1" (replace -5 -1) (("1" (flatten -1) (("1" (lemma "nderiv_derivable_aux[posreal]" ("f" "ln" "n" "j!1")) (("1" (replace -2) (("1" (replace -5 -1) (("1" (replace -1 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (skosimp*) (("2" (expand "factorial" 1 2) (("2" (expand "*" 1) (("2" (expand "^" 1 1) (("2" (rewrite "div_expt" 1) (("2" (hide-all-but (1 2)) (("2" (lemma "expt_plus" ("n0x" "-x!1" "i" "j!1-1" "j" "2")) (("2" (replace -1) (("2" (case "(-x!1) ^ 2=x!1*x!1") (("1" (replace -1) (("1" (assert) 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) ("2" (hide 3) (("2" (skosimp*) (("2" (expand "*" 1) (("2" (expand "^" 1 1) (("2" (rewrite "div_expt" 1) (("2" (assert) 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)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (hide 3) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (lemma "deriv_domain_posreal") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (hide 1) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ((const_derivable_fun formula-decl nil derivatives "analysis/") (deriv_const_fun formula-decl nil derivatives "analysis/") (neg_derivable_fun formula-decl nil derivatives "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (inv_derivable_fun formula-decl nil derivatives "analysis/") (nzreal nonempty-type-eq-decl nil reals nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (deriv_exp_fun formula-decl nil derivatives "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (posint_exp application-judgement "posint" exponentiation nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (expt def-decl "real" exponentiation nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (expt_plus formula-decl nil exponentiation nil) (expt_1i formula-decl nil exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (minus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (div_expt formula-decl nil exponentiation nil) (nderiv_derivable_aux formula-decl nil nth_derivatives "analysis/") (nderiv_derivable_eqv formula-decl nil nth_derivatives "analysis/") (deriv_scal_fun formula-decl nil derivatives "analysis/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (^ const-decl "[T -> real]" real_fun_ops "reals/") (scal_derivable_fun formula-decl nil derivatives "analysis/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (nz_deriv_fun type-eq-decl nil derivatives "analysis/") (deriv_inv_fun formula-decl nil derivatives "analysis/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (deriv_neg_fun formula-decl nil derivatives "analysis/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (I const-decl "(bijective?[T, T])" identity nil) (deriv_id_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (ln_derivable formula-decl nil ln_exp nil) (extensionality formula-decl nil functions nil) (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (deriv const-decl "[T -> real]" derivatives "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (factorial_1 formula-decl nil factorial "ints/") (expt_x1 formula-decl nil exponentiation nil) (factorial_0 formula-decl nil factorial "ints/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (int_minus_int_is_int application-judgement "int" integers nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_exp application-judgement "nzreal" 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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (derivable_n_times? def-decl "bool" nth_derivatives "analysis/") (ln const-decl "real" ln_exp nil) (= const-decl "[T, T -> boolean]" equalities nil) (nderiv_fun type-eq-decl nil nth_derivatives "analysis/") (nderiv def-decl "[T -> real]" nth_derivatives "analysis/") (numfield nonempty-type-eq-decl nil number_fields nil) (IF const-decl "[boolean, T, T -> T]" if_def 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]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (factorial def-decl "posnat" factorial "ints/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil)) nil) (nderiv_ln-1 nil 3302280454 ("" (case "FORALL (n: nat): derivable_n_times[posreal](ln, n) & nderiv[posreal](n,ln) = I (("1" (skosimp*) (("1" (inst - "n!1") (("1" (flatten) nil nil)) nil)) nil) ("2" (hide 2) (("2" (induct "n") (("1" (expand "derivable_n_times?") (("1" (propax) nil nil)) nil) ("2" (expand "nderiv") (("2" (propax) nil nil)) nil) ("3" (skosimp*) (("3" (case-replace "j!1=0") (("1" (lemma "ln_derivable") (("1" (flatten -1) (("1" (expand "derivable_n_times?") (("1" (expand "derivable_n_times?") (("1" (expand "nderiv" 1) (("1" (expand "nderiv" 1) (("1" (lemma "extensionality" ("f" "deriv(ln)" "g" "(LAMBDA (x: posreal): -factorial(1) / (-x) ^ 1)")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide 2) (("2" (replace -2) (("2" (skosimp*) (("2" (expand "factorial") (("2" (expand "factorial") (("2" (rewrite "expt_x1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "ln_derivable") (("2" (flatten -1) (("2" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "const_derivable_fun[posreal]" ("b" "-factorial(j!1)")) (("1" (lemma "deriv_id_fun[posreal]") (("1" (lemma "deriv_const_fun[posreal]" ("b" "-factorial(j!1)")) (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "neg_derivable_fun[posreal]" ("f" "LAMBDA (x: posreal): x")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_neg_fun[posreal]" ("ff" "LAMBDA (x: posreal): x")) (("1" (replace -4) (("1" (expand "-" -1) (("1" (lemma "inv_derivable_fun[posreal]" ("g" "LAMBDA (x_1: posreal): -x_1")) (("1" (assert) (("1" (expand "/") (("1" (lemma "deriv_inv_fun[posreal]" ("gg" "LAMBDA (x_1: posreal): -x_1")) (("1" (replace -3) (("1" (expand "/") (("1" (expand "*") (("1" (expand "-" -1) (("1" (lemma "extensionality" ("f" "LAMBDA (x: posreal): --1 / (-x * -x)" "g" "LAMBDA (x: posreal): 1 / (x * x)")) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "deriv_exp_fun[posreal]" ("f" "LAMBDA (x: posreal): 1 / -x" "n" "j!1")) (("1" (assert) (("1" (flatten -1) (("1" (lemma "scal_derivable_fun[posreal]" ("f" "(LAMBDA (x: posreal): 1 / -x) ^ j!1" "b" "-factorial(j!1 - 1)")) (("1" (replace -2) (("1" (lemma "deriv_scal_fun[posreal]" ("ff" "(LAMBDA (x: posreal): 1 / -x) ^ j!1" "b" "-factorial(j!1 - 1)")) (("1" (replace -4 -1) (("1" (replace -5) (("1" (lemma "extensionality" ("f" "-factorial(j!1 - 1) * (LAMBDA (x: posreal): 1 / -x) ^ j!1" "g" "LAMBDA (x: posreal): -factorial(j!1 - 1) / (-x) ^ j!1")) (("1" (split -1) (("1" (replace -1 * rl) (("1" (replace -17 * rl) (("1" (lemma "extensionality" ("f" "-factorial(j!1 - 1) * (j!1 * (LAMBDA (x: posreal): 1 / -x) ^ (j!1 - 1) * (LAMBDA (x: posreal): 1 / (x * x)))" "g" "LAMBDA (x: posreal): -factorial(j!1) / (-x) ^ (1 + j!1)")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "nderiv_derivable_eqv[posreal]" ("f" "ln" "n" "j!1")) (("1" (replace -18 -1) (("1" (replace -5 -1) (("1" (flatten -1) (("1" (lemma "nderiv_derivable_aux[posreal]" ("f" "ln" "n" "j!1")) (("1" (replace -2) (("1" (replace -5 -1) (("1" (replace -1 2) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (skosimp*) (("2" (expand "factorial" 1 2) (("2" (expand "*" 1) (("2" (expand "^" 1 1) (("2" (rewrite "div_expt" 1) (("2" (hide-all-but (1 2)) (("2" (lemma "expt_plus" ("n0x" "-x!1" "i" "j!1-1" "j" "2")) (("2" (replace -1) (("2" (case "(-x!1) ^ 2=x!1*x!1") (("1" (replace -1) (("1" (assert) 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) ("2" (hide 3) (("2" (skosimp*) (("2" (expand "*" 1) (("2" (expand "^" 1 1) (("2" (rewrite "div_expt" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) 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) ("2" (skosimp*) (("2" (assert) (("2" (hide 3) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (hide 1) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ((const_derivable_fun formula-decl nil derivatives "analysis/") (deriv_const_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (deriv_neg_fun formula-decl nil derivatives "analysis/") (deriv_inv_fun formula-decl nil derivatives "analysis/") (nz_deriv_fun type-eq-decl nil derivatives "analysis/") (scal_derivable_fun formula-decl nil derivatives "analysis/") (^ const-decl "[T -> real]" real_fun_ops "reals/") (deriv_scal_fun formula-decl nil derivatives "analysis/") (nderiv_derivable_eqv formula-decl nil nth_derivatives "analysis/") (nderiv_derivable_aux formula-decl nil nth_derivatives "analysis/") (deriv_exp_fun formula-decl nil derivatives "analysis/") (inv_derivable_fun formula-decl nil derivatives "analysis/") (neg_derivable_fun formula-decl nil derivatives "analysis/") (deriv_id_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (ln_derivable formula-decl nil ln_exp nil) (deriv_fun type-eq-decl nil derivatives "analysis/") (deriv const-decl "[T -> real]" derivatives "analysis/") (ln const-decl "real" ln_exp nil) (nderiv_fun type-eq-decl nil nth_derivatives "analysis/") (nderiv def-decl "[T -> real]" nth_derivatives "analysis/")) nil)) (ln_nderiv_TCC1 0 (ln_nderiv_TCC1-1 nil 3302282771 ("" (skosimp*) (("" (lemma "nderiv_ln") (("" (inst?) nil nil)) nil)) nil) ((nderiv_ln formula-decl nil ln_series 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)) shostak)) (ln_nderiv_TCC2 0 (ln_nderiv_TCC2-1 nil 3302282771 ("" (skosimp*) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (ln_nderiv_TCC3 0 (ln_nderiv_TCC3-1 nil 3302282771 ("" (skosimp*) (("" (assert) nil nil)) nil) ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (ln_nderiv 0 (ln_nderiv-3 nil 3352447309 ("" (induct "n") (("1" (expand "nderiv") (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (lemma "nderiv_ln" ("n" "j!1+1")) (("2" (lemma "nderiv_derivable_aux[posreal]" ("f" "ln" "n" "j!1")) (("2" (replace -2) (("2" (replace -1) (("2" (replace -3 1) (("2" (hide-all-but 1) (("2" (case-replace "j!1=0") (("1" (lemma "ln_derivable") (("1" (flatten -1) (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "deriv_id_fun[posreal]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "neg_derivable_fun[posreal]" ("f" "LAMBDA (x: posreal): x")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_neg_fun[posreal]" ("ff" "LAMBDA (x: posreal): x")) (("1" (replace -3) (("1" (expand "-" -1) (("1" (lemma "inv_derivable_fun[posreal]" ("g" "LAMBDA (x_1: posreal): -x_1")) (("1" (replace -3) (("1" (expand "/") (("1" (lemma "deriv_inv_fun[posreal]" ("gg" "LAMBDA (x_1: posreal): -x_1")) (("1" (replace -3) (("1" (expand "/" -1) (("1" (expand "*" -1) (("1" (expand "-" -1) (("1" (lemma "deriv_exp_fun[posreal]" ("f" "LAMBDA (x: posreal): 1 / -x" "n" "j!1")) (("1" (assert) (("1" (flatten -1) (("1" (replace -3) (("1" (lemma "scal_derivable_fun[posreal]" ("f" "(LAMBDA (x: posreal): 1 / -x) ^ j!1" "b" "-factorial(j!1 - 1)")) (("1" (replace -2) (("1" (lemma "deriv_scal_fun[posreal]" ("ff" "(LAMBDA (x: posreal): 1 / -x) ^ j!1" "b" "-factorial(j!1 - 1)")) (("1" (replace -4) (("1" (lemma "extensionality" ("f" "-factorial(j!1 - 1) * (LAMBDA (x: posreal): 1 / -x) ^ j!1" "g" "LAMBDA (x: posreal): -factorial(j!1 - 1) / (-x) ^ j!1")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "extensionality" ("f" "-factorial(j!1 - 1) * (j!1 * (LAMBDA (x: posreal): 1 / -x) ^ (j!1 - 1) * (LAMBDA (x: posreal): --1 / (-x * -x)))" "g" "LAMBDA (x: posreal): -factorial(j!1) / (-x) ^ (1 + j!1)")) (("1" (split -1) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide-all-but (1 2)) (("2" (skosimp*) (("2" (expand "factorial" 1 2) (("2" (expand "*") (("2" (expand "^" 1 1) (("2" (rewrite "div_expt" 1) (("2" (lemma "expt_plus" ("n0x" "-x!1" "i" "j!1-1" "j" "2")) (("2" (replace -1) (("2" (case-replace "(-x!1) ^ 2 = -x!1 * -x!1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (skosimp*) (("2" (expand "*") (("2" (expand "^" 1 1) (("2" (rewrite "div_expt" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil) ("3" (assert) (("3" (lemma "deriv_domain_posreal") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (hide 2) (("4" (lemma "nderiv_ln") (("4" (inst?) nil nil)) nil)) nil)) nil)) nil) ((nderiv_derivable_aux formula-decl nil nth_derivatives "analysis/") (deriv_id_fun formula-decl nil derivatives "analysis/") (neg_derivable_fun formula-decl nil derivatives "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (inv_derivable_fun formula-decl nil derivatives "analysis/") (nzreal nonempty-type-eq-decl nil reals nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (deriv_exp_fun formula-decl nil derivatives "analysis/") (scal_derivable_fun formula-decl nil derivatives "analysis/") (^ const-decl "[T -> real]" real_fun_ops "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (deriv_scal_fun formula-decl nil derivatives "analysis/") (extensionality formula-decl nil functions nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (posint_exp application-judgement "posint" exponentiation nil) (div_expt formula-decl nil exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (minus_int_is_int application-judgement "int" integers nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (expt_1i formula-decl nil exponentiation nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (expt def-decl "real" exponentiation nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (expt_plus formula-decl nil exponentiation nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (nz_deriv_fun type-eq-decl nil derivatives "analysis/") (deriv_inv_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_neg_fun formula-decl nil derivatives "analysis/") (I const-decl "(bijective?[T, T])" identity nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (ln_derivable formula-decl nil ln_exp nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (expt_x1 formula-decl nil exponentiation nil) (factorial_0 formula-decl nil factorial "ints/") (minus_nzint_is_nzint application-judgement "nzint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nderiv_ln formula-decl nil ln_series nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (factorial def-decl "posnat" factorial "ints/") (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (- const-decl "[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) (IF const-decl "[boolean, T, T -> T]" if_def nil) (nderiv def-decl "[T -> real]" nth_derivatives "analysis/") (nderiv_fun type-eq-decl nil nth_derivatives "analysis/") (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (derivable_n_times? def-decl "bool" nth_derivatives "analysis/") (ln const-decl "real" ln_exp nil) (int_minus_int_is_int application-judgement "int" integers nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) nil) (ln_nderiv-2 nil 3302280610 ("" (induct "n") (("1" (expand "nderiv") (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (lemma "nderiv_ln" ("n" "j!1+1")) (("2" (lemma "nderiv_derivable_aux[posreal]" ("f" "ln" "n" "j!1")) (("2" (replace -2) (("2" (replace -1) (("2" (replace -3 1) (("2" (hide-all-but 1) (("2" (case-replace "j!1=0") (("1" (lemma "ln_derivable") (("1" (flatten -1) (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "deriv_id_fun[posreal]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "neg_derivable_fun" ("f" "LAMBDA (x: posreal): x")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_neg_fun" ("ff" "LAMBDA (x: posreal): x")) (("1" (replace -3) (("1" (expand "-" -1) (("1" (lemma "inv_derivable_fun" ("g" "LAMBDA (x_1: posreal): -x_1")) (("1" (replace -3) (("1" (expand "/") (("1" (lemma "deriv_inv_fun" ("gg" "LAMBDA (x_1: posreal): -x_1")) (("1" (replace -3) (("1" (expand "/" -1) (("1" (expand "*" -1) (("1" (expand "-" -1) (("1" (lemma "deriv_exp_fun[posreal]" ("f" "LAMBDA (x: posreal): 1 / -x" "n" "j!1")) (("1" (assert) (("1" (flatten -1) (("1" (replace -3) (("1" (lemma "scal_derivable_fun" ("f" "(LAMBDA (x: posreal): 1 / -x) ^ j!1" "b" "-factorial(j!1 - 1)")) (("1" (replace -2) (("1" (lemma "deriv_scal_fun" ("ff" "(LAMBDA (x: posreal): 1 / -x) ^ j!1" "b" "-factorial(j!1 - 1)")) (("1" (replace -4) (("1" (lemma "extensionality" ("f" "-factorial(j!1 - 1) * (LAMBDA (x: posreal): 1 / -x) ^ j!1" "g" "LAMBDA (x: posreal): -factorial(j!1 - 1) / (-x) ^ j!1")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "extensionality" ("f" "-factorial(j!1 - 1) * (j!1 * (LAMBDA (x: posreal): 1 / -x) ^ (j!1 - 1) * (LAMBDA (x: posreal): --1 / (-x * -x)))" "g" "LAMBDA (x: posreal): -factorial(j!1) / (-x) ^ (1 + j!1)")) (("1" (split -1) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide-all-but (1 2)) (("2" (skosimp*) (("2" (expand "factorial" 1 2) (("2" (expand "*") (("2" (expand "^" 1 1) (("2" (rewrite "div_expt" 1) (("2" (lemma "expt_plus" ("n0x" "-x!1" "i" "j!1-1" "j" "2")) (("2" (replace -1) (("2" (case-replace "(-x!1) ^ 2 = -x!1 * -x!1") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (skosimp*) (("2" (expand "*") (("2" (expand "^" 1 1) (("2" (rewrite "div_expt" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (hide 2) (("4" (lemma "nderiv_ln") (("4" (inst?) nil nil)) nil)) nil)) nil)) nil) ((deriv_id_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (deriv_neg_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (deriv_inv_fun formula-decl nil derivatives "analysis/") (nz_deriv_fun type-eq-decl nil derivatives "analysis/") (deriv_scal_fun formula-decl nil derivatives "analysis/") (scal_derivable_fun formula-decl nil derivatives "analysis/") (deriv_exp_fun formula-decl nil derivatives "analysis/") (inv_derivable_fun formula-decl nil derivatives "analysis/") (neg_derivable_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (ln_derivable formula-decl nil ln_exp nil) (ln const-decl "real" ln_exp nil)) nil) (ln_nderiv-1 nil 3302280550 ("" (induct "n") (("1" (expand "nderiv") (("1" (propax) nil))) ("2" (skosimp*) (("2" (lemma "ln_derivable_n_times" ("n" "j!1+1")) (("2" (lemma "nderiv_derivable_aux[posreal]" ("f" "ln" "n" "j!1")) (("2" (replace -2) (("2" (replace -1) (("2" (replace -3 1) (("2" (hide-all-but 1) (("2" (case-replace "j!1=0") (("1" (lemma "ln_derivable") (("1" (flatten -1) (("1" (replace -2) (("1" (assert) (("1" (expand "factorial") (("1" (lemma "extensionality" ("f" "(LAMBDA (t: posreal): 1 / t)" "g" "(LAMBDA (x: posreal): -1 / (-x) ^ 1)")) (("1" (split -1) (("1" (propax) nil) ("2" (hide-all-but (-3 1)) (("2" (skosimp*) (("2" (rewrite "expt_x1") (("2" (assert) nil))))))))))))))))))))) ("2" (assert) (("2" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "deriv_id_fun[posreal]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "neg_derivable_fun" ("f" "LAMBDA (x: posreal): x")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_neg_fun" ("ff" "LAMBDA (x: posreal): x")) (("1" (replace -3) (("1" (expand "-" -1) (("1" (lemma "inv_derivable_fun" ("g" "LAMBDA (x_1: posreal): -x_1")) (("1" (replace -3) (("1" (expand "/") (("1" (lemma "deriv_inv_fun" ("gg" "LAMBDA (x_1: posreal): -x_1")) (("1" (replace -3) (("1" (expand "/" -1) (("1" (expand "*" -1) (("1" (expand "-" -1) (("1" (lemma "deriv_exp_fun[posreal]" ("f" "LAMBDA (x: posreal): 1 / -x" "n" "j!1")) (("1" (assert) (("1" (flatten -1) (("1" (replace -3) (("1" (lemma "scal_derivable_fun" ("f" "(LAMBDA (x: posreal): 1 / -x) ^ j!1" "b" "-factorial(j!1 - 1)")) (("1" (replace -2) (("1" (lemma "deriv_scal_fun" ("ff" "(LAMBDA (x: posreal): 1 / -x) ^ j!1" "b" "-factorial(j!1 - 1)")) (("1" (replace -4) (("1" (lemma "extensionality" ("f" "-factorial(j!1 - 1) * (LAMBDA (x: posreal): 1 / -x) ^ j!1" "g" "LAMBDA (x: posreal): -factorial(j!1 - 1) / (-x) ^ j!1")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "extensionality" ("f" "-factorial(j!1 - 1) * (j!1 * (LAMBDA (x: posreal): 1 / -x) ^ (j!1 - 1) * (LAMBDA (x: posreal): --1 / (-x * -x)))" "g" "LAMBDA (x: posreal): -factorial(j!1) / (-x) ^ (1 + j!1)")) (("1" (split -1) (("1" (replace -1) (("1" (propax) nil))) ("2" (hide-all-but (1 2)) (("2" (skosimp*) (("2" (expand "factorial" 1 2) (("2" (expand "*") (("2" (expand "^" 1 1) (("2" (rewrite "div_expt" 1) (("2" (rewrite "expt_1i") (("2" (lemma "expt_plus" ("n0x" "-x!1" "i" "j!1-1" "j" "2")) (("2" (replace -1) (("2" (case-replace "(-x!1) ^ 2 = -x!1 * -x!1") (("1" (assert) nil) ("2" (hide-all-but 1) (("2" (grind) nil))))))))))))))))))))))))))))) ("2" (hide-all-but (1 2)) (("2" (skosimp*) (("2" (expand "*") (("2" (expand "^" 1 1) (("2" (rewrite "div_expt" 1) (("2" (rewrite "expt_1i") (("2" (assert) nil))))))))))))))))))) ("2" (propax) nil))))))))))))))))))))))) ("2" (propax) nil))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil))))) ("3" (skosimp*) (("3" (assert) nil))))))))))))))))))))))) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil))))) ("4" (lemma "ln_derivable_n_times") (("4" (propax) nil)))) nil) nil nil)) (IMP_taylor_series_TCC1 0 (IMP_taylor_series_TCC1-1 nil 3563622659 ("" (assert) nil nil) ((conn_abslt1 formula-decl nil ln_series nil)) nil)) (IMP_taylor_series_TCC2 0 (IMP_taylor_series_TCC2-1 nil 3563622659 ("" (assert) nil nil) ((noa_abslt1 formula-decl nil ln_series nil)) nil)) (IMP_taylor_series_TCC3 0 (IMP_taylor_series_TCC3-1 nil 3563622659 ("" (skeep) (("" (inst 1 "1-abs(x)") (("" (skeep) (("" (rewrite "abs_diff_commute") (("" (lemma "abs_diff") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) 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) (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) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (< const-decl "bool" reals nil) (abslt1 type-eq-decl nil ln_series nil) (abs_diff_commute formula-decl nil abs_lems "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_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) (abs_diff formula-decl nil abs_lems "reals/") (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (IMP_taylor_series_TCC4 0 (IMP_taylor_series_TCC4-1 nil 3563622659 ("" (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) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abslt1 type-eq-decl nil ln_series nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil)) nil)) (IMP_taylor_series_TCC5 0 (IMP_taylor_series_TCC5-1 nil 3563622659 ("" (inst 1 "0") (("" (grind) nil nil)) nil) ((abslt1 type-eq-decl nil ln_series nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil)) nil)) (ln_estimate_TCC1 0 (ln_estimate_TCC1-1 nil 3302450959 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (ln_estimate_TCC2 0 (ln_estimate_TCC2-1 nil 3320163563 ("" (subtype-tcc) nil nil) nil nil)) (ln_estimate_TCC3 0 (ln_estimate_TCC3-1 nil 3403261765 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil)) nil)) (ln_estimate_TCC4 0 (ln_estimate_TCC4-1 nil 3403261765 ("" (skosimp*) nil nil) nil nil)) (ln_taylors_TCC1 0 (ln_taylors_TCC1-1 nil 3302450959 ("" (skosimp*) (("" (assert) nil nil)) nil) ((conn_gt_m1 formula-decl nil ln_series nil)) shostak)) (ln_taylors_TCC2 0 (ln_taylors_TCC2-1 nil 3302450959 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil)) nil)) 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) (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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) shostak)) (ln_taylors_TCC3 0 (ln_taylors_TCC3-1 nil 3302450959 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (ln_taylors_TCC4 0 (ln_taylors_TCC4-1 nil 3563622659 ("" (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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Gt_m1 type-eq-decl nil ln_series nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (between type-eq-decl nil taylors "analysis/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (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_plus_real_is_real application-judgement "real" reals nil) (/= const-decl "boolean" notequal nil)) nil)) (ln_taylors_TCC5 0 (ln_taylors_TCC5-1 nil 3563622659 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil) (minus_real_is_real application-judgement "real" reals nil)) nil)) (ln_taylors 0 (ln_taylors-2 nil 3302450340 ("" (skosimp*) (("" (lemma "Taylors[posreal]" ("f" "ln" "n" "n!1" "bb" "xgm1!1+1" "aa" "1")) (("1" (lemma "nderiv_ln" ("n" "n!1+1")) (("1" (replace -1) (("1" (skosimp*) (("1" (inst + "c!1") (("1" (lemma "ln_nderiv" ("n" "n!1+1")) (("1" (simplify -1) (("1" (replace -1 -3) (("1" (simplify -3) (("1" (rewrite "div_expt" 1) (("1" (expand "ln_estimate" 1) (("1" (lemma "sigma_eq[nat]" ("low" "0" "high" "n!1" "F" "LAMBDA (nn:nat): IF nn > n!1 THEN 0 ELSIF nn = 0 THEN ln(1) ELSE nderiv(nn, ln)(1) * xgm1!1 ^ nn / factorial(nn) ENDIF" "G" "LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-xgm1!1) ^ nn / nn ENDIF")) (("1" (split -1) (("1" (replace -1 -4) (("1" (name-replace "K1" "sigma(0, n!1, LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-xgm1!1) ^ nn / nn ENDIF)") (("1" (replace -4 1) (("1" (hide-all-but 1) (("1" (typepred "c!1") (("1" (hide -1 -3 -4 -5) (("1" (expand "factorial" 1 2) (("1" (name-replace "K2" "factorial(n!1)") (("1" (lemma "div_cancel1" ("x" "((-1/ (-c!1) ^ (1 + n!1)) * xgm1!1 ^ (1 + n!1)) / (1+n!1)" "n0z" "K2")) (("1" (rewrite "div_div2" -1) (("1" (case "K2 * (((-1 / (-c!1) ^ (1 + n!1)) * xgm1!1 ^ (1 + n!1)) / (K2 + K2 * n!1)) = ((-K2 / (-c!1) ^ (1 + n!1)) * xgm (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (name-replace "K3" "K2 + K2 * n!1") (("2" (name-replace "K4" "xgm1!1 ^ (1 + n!1)") (("2" (name-replace "K5" "(-c!1) ^ (1 + n!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "n!2") (("2" (assert) (("2" (lift-if) (("2" (ground) (("2" (lemma "ln_nderiv") (("2" (inst?) (("2" (replace -1) (("2" (hide -1) (("2" (assert) (("2" (simplify 2) (("2" (lemma "cross_mult" ("x" "-factorial(n!2 - 1) / (-1) ^ n!2 * xgm1!1 ^ n!2" "n0x" "factorial(n!2)" "y" "-(-xgm1!1) ^ n!2" "n0y" "n!2")) (("2" (replace -1 2) (("2" (expand "factorial" 2 2) (("2" (case-replace "xgm1!1=0") (("1" (expand "^" 2 3) (("1" (expand "^" 2 1) (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (field 3) (("2" (flatten) (("2" (expand "^") (("2" (lemma "expt_of_mult") (("2" (inst - "n!2" "-xgm1!1" "-1") (("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" (hide-all-but 1) (("2" (skosimp*) nil nil)) nil) ("3" (skosimp*) (("3" (lemma "nderiv_ln") (("3" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (replace -1) (("2" (rewrite "ln_1") (("2" (expand "^" 1) (("2" (expand "expt" 1) (("2" (assert) (("2" (rewrite "zero_times1") (("2" (simplify 1) (("2" (expand "ln_estimate") (("2" (hide-all-but 1) (("2" (lemma "sigma_zero[nat]" ("low" "0" "high" "n!1")) (("2" (lemma "sigma_eq[nat]" ("low" "0" "high" "n!1" "F" "LAMBDA (i: nat): 0" "G" "LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-0) ^ nn / nn ENDIF")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (skosimp*) (("2" (case "n!2=0") (("1" (assert) nil nil) ("2" (assert) (("2" (expand "^") (("2" (expand "expt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2) (("2" (typepred "xgm1!1") (("2" (typepred "c!1") (("2" (replace -3) (("2" (replace -4) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (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) (>= 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) (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) (ln const-decl "real" ln_exp nil) (Gt_m1 type-eq-decl nil ln_series nil) (- const-decl "[numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (Taylors formula-decl nil taylors "analysis/") (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) (connected? const-decl "bool" deriv_domain_def "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (AND const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (xgm1!1 skolem-const-decl "Gt_m1" ln_series nil) (= const-decl "[T, T -> boolean]" equalities nil) (between type-eq-decl nil taylors "analysis/") (c!1 skolem-const-decl "between[posreal](1, 1 + xgm1!1)" ln_series 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) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (hat_02n formula-decl nil power_series "series/") (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (minus_int_is_int application-judgement "int" integers nil) (sigma_nat application-judgement "nat" sigma_nat "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (sigma_zero formula-decl nil sigma "reals/") (zero_times1 formula-decl nil real_props nil) (nat_exp application-judgement "nat" exponentiation nil) (ln_estimate const-decl "real" ln_series nil) (sigma def-decl "real" sigma "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (div_div2 formula-decl nil real_props nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (posint nonempty-type-eq-decl nil integers nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel1 formula-decl nil real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_expt application-judgement "int" exponentiation nil) (minus_even_is_even application-judgement "even_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (expt def-decl "real" exponentiation nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (both_sides_times1 formula-decl nil real_props nil) (div_cancel2 formula-decl nil real_props nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (both_sides_times2 formula-decl nil real_props nil) (expt_of_mult formula-decl nil exponentiation nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (cross_mult formula-decl nil real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (int_exp application-judgement "int" exponentiation nil) (subrange type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (factorial def-decl "posnat" factorial "ints/") (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (nderiv def-decl "[T -> real]" nth_derivatives "analysis/") (nderiv_fun type-eq-decl nil nth_derivatives "analysis/") (derivable_n_times? def-decl "bool" nth_derivatives "analysis/") (* 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) (IF const-decl "[boolean, T, T -> T]" if_def nil) (sigma_eq formula-decl nil sigma "reals/") (minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (ln_1 formula-decl nil ln_exp nil) (div_expt formula-decl nil exponentiation nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (int_minus_int_is_int application-judgement "int" integers nil) (ln_nderiv formula-decl nil ln_series nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (nderiv_ln formula-decl nil ln_series nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) nil) (ln_taylors-1 nil 3302449853 ("" (skosimp*) (("" (lemma "Taylors[posreal]" ("f" "ln" "n" "n!1" "bb" "xgm1!1+1" "aa" "1")) (("1" (lemma "ln_derivable_n_times" ("n" "n!1+1")) (("1" (replace -1) (("1" (skosimp*) (("1" (inst + "c!1") (("1" (lemma "ln_nderiv" ("n" "n!1+1")) (("1" (simplify -1) (("1" (replace -1 -3) (("1" (simplify -3) (("1" (rewrite "div_expt" 1) (("1" (expand "ln_series_n" 1) (("1" (lemma "sigma_eq[nat]" ("low" "0" "high" "n!1" "F" "LAMBDA (nn:nat): IF nn > n!1 THEN 0 ELSIF nn = 0 THEN ln(1) ELSE nderiv(nn, ln)(1) * xgm1!1 ^ nn / factorial(nn) ENDIF" "G" "LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-xgm1!1) ^ nn / nn ENDIF")) (("1" (split -1) (("1" (replace -1 -4) (("1" (name-replace "K1" "sigma(0, n!1, LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-xgm1!1) ^ nn / nn ENDIF)") (("1" (replace -4 1) (("1" (hide-all-but 1) (("1" (typepred "c!1") (("1" (hide -1 -3 -4 -5) (("1" (expand "factorial" 1 2) (("1" (name-replace "K2" "factorial(n!1)") (("1" (lemma "div_cancel1" ("x" "((-1/ (-c!1) ^ (1 + n!1)) * xgm1!1 ^ (1 + n!1)) / (1+n!1)" "n0z" "K2")) (("1" (rewrite "div_div2" -1) (("1" (case "K2 * (((-1 / (-c!1) ^ (1 + n!1)) * xgm1!1 ^ (1 + n!1)) / (K2 + K2 * n!1)) = ((-K2 / (-c!1) ^ (1 + n!1)) * xgm (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (assert) nil))))))) ("2" (hide 2) (("2" (name-replace "K3" "K2 + K2 * n!1") (("2" (name-replace "K4" "xgm1!1 ^ (1 + n!1)") (("2" (name-replace "K5" "(-c!1) ^ (1 + n!1)") (("2" (assert) nil))))))))))))))))))))))))))))))) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "n!2") (("2" (assert) (("2" (rewrite "ln_1") (("2" (case "n!2=0") (("1" (assert) nil) ("2" (assert) (("2" (lemma "ln_nderiv" ("n" "n!2")) (("2" (assert) (("2" (replace -1 2) (("2" (simplify 2) (("2" (hide -1) (("2" (lemma "cross_mult" ("x" "-factorial(n!2 - 1) / (-1) ^ n!2 * xgm1!1 ^ n!2" "n0x" "factorial(n!2)" "y" "-(-xgm1!1) ^ n!2" "n0y" "n!2")) (("2" (replace -1 2) (("2" (expand "factorial" 2 2) (("2" (case-replace "xgm1!1=0") (("1" (expand "^" 2 3) (("1" (expand "^" 2 1) (("1" (expand "expt") (("1" (assert) nil))))))) ("2" (lemma "div_expt" ("n0x" "xgm1!1" "n0y" "-1" "i" "n!2")) (("1" (assert) nil) ("2" (assert) nil))))))))))))))))))))))))))))))))))))) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (assert) (("2" (lemma "ln_derivable_n_times" ("n" "nn!1")) (("2" (propax) nil))))))))))))) ("2" (expand "/=" 1) (("2" (replace -1) (("2" (rewrite "ln_1") (("2" (expand "^" 1) (("2" (expand "expt" 1) (("2" (assert) (("2" (rewrite "zero_times1") (("2" (simplify 1) (("2" (expand "ln_series_n") (("2" (hide-all-but 1) (("2" (lemma "sigma_zero[nat]" ("low" "0" "high" "n!1")) (("2" (lemma "sigma_eq[nat]" ("low" "0" "high" "n!1" "F" "LAMBDA (i: nat): 0" "G" "LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-0) ^ nn / nn ENDIF")) (("2" (split -1) (("1" (assert) nil) ("2" (hide -1 2) (("2" (skosimp*) (("2" (case "n!2=0") (("1" (assert) nil) ("2" (assert) (("2" (expand "^") (("2" (expand "expt") (("2" (assert) nil))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (hide -1 -2) (("2" (typepred "xgm1!1") (("2" (typepred "c!1") (("2" (replace -3) (("2" (replace -4) (("2" (propax) nil))))))))))))))))))) ("2" (hide 2) (("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil))))))) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil)))))))) nil) nil nil)) (ln_estimate_error_bound_TCC1 0 (ln_estimate_error_bound_TCC1-1 nil 3558179379 ("" (subtype-tcc) nil nil) nil nil)) (ln_estimate_error_bound 0 (ln_estimate_error_bound-1 nil 3558179380 ("" (skeep) (("" (lemma "ln_taylors") (("" (inst?) (("" (skeep -1) (("" (case "abs((xp / -c) ^ (n + 1) / (n + 1)) < xp ^ (n + 1) / (n + 1)") (("1" (grind :exclude ("^" "ln" "ln_estimate")) nil nil) ("2" (hide-all-but 1) (("2" (typepred "c") (("2" (case "NOT c > 1") (("1" (assert) nil nil) ("2" (rewrite "abs_div") (("2" (case "abs(1+n) = 1+n") (("1" (replaces -1) (("1" (expand "^") (("1" (rewrite "abs_expt") (("1" (rewrite "abs_div") (("1" (rewrite "abs_neg") (("1" (lemma "div_expt") (("1" (inst - "1+n" _ _) (("1" (expand "^" -1) (("1" (rewrite -1) (("1" (expand "abs" +) (("1" (assert) (("1" (case "expt(c,1+n) > 1") (("1" (case "1/expt(c,1+n) < 1") (("1" (mult-by -1 "expt(xp,1+n)/(1+n)") (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) (("2" (case "FORALL (nn:nat): expt(c,1+nn) > 1") (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (induct "nn") (("1" (expand "expt" 1) (("1" (expand "expt" 1) (("1" (propax) nil nil)) nil)) nil) ("2" (skeep) (("2" (expand "expt" +) (("2" (mult-by -4 "expt(c,1+j)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (nn:nat): expt(c,1+nn) > 1") (("1" (inst?) nil nil) ("2" (induct "nn") (("1" (expand "expt" +) (("1" (expand "expt" +) (("1" (propax) nil nil)) nil)) nil) ("2" (skeep) (("2" (expand "expt" +) (("2" (mult-by -3 "expt(c,1+j)") (("2" (assert) 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) ((ln_taylors formula-decl nil ln_series nil) (div_expt formula-decl nil exponentiation nil) (expt def-decl "real" exponentiation nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (n skolem-const-decl "nat" ln_series nil) (c skolem-const-decl "between[{x: real | x > -1}](1, 1 + xp)" ln_series nil) (xp skolem-const-decl "posreal" ln_series nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (j skolem-const-decl "nat" ln_series nil) (both_sides_times_pos_gt1 formula-decl nil real_props nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (j skolem-const-decl "nat" ln_series nil) (nzreal nonempty-type-eq-decl nil reals nil) (nnreal_expt application-judgement "nnreal" exponentiation nil) (abs_neg formula-decl nil abs_lems "reals/") (posreal_expt application-judgement "posreal" exponentiation nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (abs_expt formula-decl nil exponent_props "reals/") (minus_nzint_is_nzint application-judgement "nzint" integers nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (abs_div formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_exp application-judgement "posreal" exponentiation nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (between type-eq-decl nil taylors "analysis/") (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (Gt_m1 type-eq-decl nil ln_series nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (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)) shostak)) (lnp1_TCC1 0 (lnp1_TCC1-1 nil 3321095836 ("" (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) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (abslt1 type-eq-decl nil ln_series 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) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (lnp1_TCC2 0 (lnp1_TCC2-1 nil 3321095836 ("" (skosimp*) (("" (lemma "one_over_x_cont[posreal]") (("" (assert) (("" (lemma "cont_Integrable?[posreal]") (("1" (inst?) (("1" (assert) nil nil) ("2" (typepred "x1!1") (("2" (expand "abs") (("2" (ground) nil nil)) nil)) nil)) nil) ("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) (("3" (expand "connected?") (("3" (skosimp*) (("3" (assert) nil nil)) nil)) 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) (>= 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) (one_over_x_cont formula-decl nil continuous_functions "analysis/") (cont_Integrable? formula-decl nil integral "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (abslt1 type-eq-decl nil ln_series nil) (x1!1 skolem-const-decl "abslt1" ln_series nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) nil)) (lnp1_TCC3 0 (lnp1_TCC3-1 nil 3563622659 ("" (assuming-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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types 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_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected? const-decl "bool" deriv_domain_def "analysis/")) nil)) (lnp1 0 (lnp1-2 nil 3321095882 ("" (skosimp*) (("" (expand "ln") (("" (propax) nil nil)) nil)) nil) ((ln const-decl "real" ln_exp nil)) nil) (lnp1-1 nil 3321095839 ("" (postpone) nil nil) nil shostak)) (ln_estimate_increasing_odd 0 (ln_estimate_increasing_odd-1 nil 3558194748 ("" (case "FORALL (m:nat): derivable?[real](LAMBDA (pr: real): ln_estimate(pr, m))") (("1" (label "derivtt" -1) (("1" (copy -1) (("1" (label "derivtt2" -1) (("1" (hide -1) (("1" (skeep) (("1" (lemma "nonneg_derivative[real]") (("1" (inst-cp -2 "2*n+1") (("1" (inst - "LAMBDA (pr:real): ln_estimate(pr,2*n+1)") (("1" (assert) (("1" (ground) (("1" (expand "increasing?") (("1" (inst - "px" "py") (("1" (assert) nil))))) ("2" (hide (2 3)) (("2" (case "FORALL (m:nat): FORALL (x: real): deriv(LAMBDA (pr: real): ln_estimate(pr, m), x) = sigma(0,m-1,(LAMBDA (nn:nat): (-x)^nn)) (("1" (inst - "2*n+1") (("1" (skeep) (("1" (inst - "x") (("1" (replaces -1) (("1" (assert) (("1" (case "x = 0 OR x = -1") (("1" (split -) (("1" (replaces -1) (("1" (rewrite "sigma_ge_0") (("1" (hide-all-but 1) (("1" (expand "^") (("1" (expand "expt") (("1" (grind) nil))))))))))) ("2" (replaces -1) (("2" (rewrite "sigma_ge_0") nil))))) ("2" (label "xtp" 1) (("2" (hide "xtp") (("2" (case "FORALL (kk:nat): sigma(0, kk - 1, LAMBDA (nn: nat): (-x) ^ nn) = (1-(-x)^kk)/(1+x)") (("1" (inst - "2*n+1") (("1" (assert) (("1" (replace -1) (("1" (lemma "mult_expt") (("1" (inst - "1+2*n" "-1" "x") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case "FORALL (m:nat): (-1)^(1+2*m) = -1") (("1" (inst?) (("1" (replaces -1) (("1" (assert) (("1" (cross-mult 1) (("1" (ground) (("1" (case "x>=0") (("1" (case "EXISTS (nnr:nnreal): x=nnr") (("1" (skeep -1) (("1" (replaces -1) (("1" (assert) nil))))) ("2" (inst + "x") nil))) ("2" (case "FORALL (kk:nat): abs(x^(kk+1))<1") (("1" (inst - "2*n") (("1" (hide-all-but (-1 +)) (("1" (grind :exclude "^") nil))))) ("2" (hide-all-but (-1 +)) (("2" (induct "kk") (("1" (hide 3) (("1" (grind) nil))) ("2" (skeep) (("2" (lemma "abs_expt") (("2" (expand "^") (("2" (rewrite -1) (("2" (rewrite -1) (("2" (expand "expt" +) (("2" (case "abs(x) < 1") (("1" (mult-by -1 "expt(abs(x),1+j)") (("1" (assert) nil))) ("2" (grind :exclude "^") nil))))))))))))))))))))))) ("2" (lemma "both_sides_expt_pos_ge_aux") (("2" (inst - "2*n" "-x" "1") (("2" (assert) (("2" (case "FORALL (nn:nat): expt(-x,1+2*nn) = - (x^(1+2*nn)) AND expt(1,1+2*nn) = 1") (("1" (inst - "n") (("1" (ground) nil))) ("2" (hide-all-but 1) (("2" (induct "nn") (("1" (grind) nil) ("2" (grind) nil) ("3" (skeep) (("3" (split) (("1" (expand "^") (("1" (expand "expt" +) (("1" (expand "expt" +) (("1" (assert) nil))))))) ("2" (assert) (("2" (expand "expt" +) (("2" (expand "expt" +) (("2" (propax) nil))))))))))))))))))))))))))))))))) ("2" (hide-all-but 1) (("2" (induct "m") (("1" (grind) nil) ("2" (skeep) (("2" (expand "^") (("2" (expand "expt" +) (("2" (expand "expt" +) (("2" (assert) nil))))))))))))))))))))) ("2" (assert) (("2" (flatten) (("2" (replaces -1) (("2" (assert) nil))))))))))))))))) ("2" (hide-all-but 1) (("2" (induct "kk") (("1" (grind) nil) ("2" (skeep) (("2" (assert) (("2" (expand "sigma" +) (("2" (replaces -1) (("2" (assert) (("2" (expand "^") (("2" (expand "expt" + 3) (("2" (assert) (("2" (name "yy" "expt(-x,j)") (("2" (replaces -1) (("2" (case "yy = (-(1-yy)+(1-(-x)*yy))/(1+x)") (("1" (assert) nil) ("2" (hide 2) (("2" (cross-mult 1) nil))))))))))))))))))))))))) ("3" (reveal "xtp") (("3" (ground) nil))) ("4" (hide 2) (("4" (skeep) (("4" (assert) nil))))))))) ("3" (reveal "xtp") (("3" (ground) nil))))))))))))))))))))) ("2" (induct "m") (("1" (hide 2) (("1" (skeep) (("1" (assert) (("1" (lemma "deriv_const[real]") (("1" (expand "ln_estimate" +) (("1" (expand "sigma" +) (("1" (expand "sigma" +) (("1" (expand "const_fun") (("1" (rewrite -1) nil))))))))))))))))) ("2" (hide 2) (("2" (skeep) (("2" (case "j = 0") (("1" (replaces -1) (("1" (assert) (("1" (skeep) (("1" (expand "ln_estimate" +) (("1" (expand "sigma" +) (("1" (expand "sigma" +) (("1" (expand "sigma" +) (("1" (expand "^") (("1" (expand "expt" +) (("1" (expand "expt" +) (("1" (assert) (("1" (lemma "deriv_identity[real]") (("1" (expand "I") (("1" (rewrite -1) nil))))))))))))))))))))))))))) ("2" (assert) (("2" (label "jpos" 1) (("2" (hide 1) (("2" (skeep) (("2" (inst - "x") (("2" (lemma "deriv_sum[real]") (("2" (inst - "LAMBDA (pr: real): ln_estimate(pr, j)" "LAMBDA (pr:real): -(-pr) ^ (1+j) / (1+j)" "x") (("2" (assert) (("2" (split -) (("1" (expand "sigma" +) (("1" (assert) (("1" (invoke (case "%1 = %2 AND %3 = %4 AND %5 = %6") (! -1 1) (! 1 1) (! -1 2 1) (! 1 2 2) (! -1 2 2) (! 1 2 1)) (("1" (flatten) (("1" (assert) nil))) ("2" (split) (("1" (invoke (case "%1 = %2") (! 1 1 1) (! 1 2 1)) (("1" (assert) nil) ("2" (hide (2 3)) (("2" (decompose-equality) (("2" (expand "ln_estimate" +) (("2" (expand "+" +) (("2" (expand "sigma" + 2) (("2" (propax) nil))))))))))))) ("2" (propax) nil) ("3" (lemma "deriv_neg[real]") (("3" (hide (-2 2)) (("3" (case "EXISTS (c:real): (c=1 OR c=-1) AND (-x)^j = -c*x^j AND (LAMBDA (pr: real): -(-pr) ^ (1 + j) / (1 + j (("1" (skeep -1) (("1" (replace -3) (("1" (replace -2) (("1" (lemma "deriv_scal[real]") (("1" (inst - "-c / (1+j)" "LAMBDA (pr: real): (pr) ^ (1 + j)" "x") (("1" (split -) (("1" (invoke (case "%1 = %2") (! -1 1 1) (! 1 1 1)) (("1" (replaces -1) (("1" (replaces -1) (("1" (lemma "deriv_x_n[real]") (("1" (inst - "LAMBDA (pr: real): (pr) ^ (1 + j)" "1+j") (("1" (assert) (("1" (flatten) (("1" (decompose-equality -2) (("1" (inst - "x") (("1" (expand "deriv" -1) (("1" (replaces -1) (("1" (cross-mult 1) nil))))))))))))))))))))) ("2" (hide-all-but 1) (("2" (decompose-equality) (("2" (expand "*") (("2" (assert) nil))))))))) ("2" (lemma "deriv_x_n[real]") (("2" (inst - "LAMBDA (pr: real): (pr) ^ (1 + j)" "1+j") (("2" (assert) (("2" (flatten) (("2" (expand "derivable?" -1) (("2" (inst - "x") nil))))))))))))))))))))))) ("2" (hide-all-but 1) (("2" (name "cc" "IF even?(j) THEN -1 ELSE 1 ENDIF") (("2" (inst + "cc") (("2" (split) (("1" (replaces -1 :dir rl) (("1" (grind) nil))) ("2" (lemma "mult_expt") (("2" (inst - "j" "-1" "x") (("1" (assert) (("1" (replace -1) (("1" (lemma "even_m1_pow") (("1" (inst - "j") (("1" (lemma "not_even_m1_pow") (("1" (inst - "j") (("1" (lift-if) (("1" (ground) nil))))))))))))))) ("2" (flatten) (("2" (replaces -1) (("2" (reveal "jpos") (("2" (expand "^") (("2" (expand "expt") (("2" (assert) nil))))))))))))))) ("3" (decompose-equality) (("3" (lemma "mult_expt") (("3" (inst - "1+j" "-1" "x!1") (("1" (replaces -1) (("1" (lemma "not_even_m1_pow") (("1" (inst - "1+j") (("1" (case "even?(1+j) IFF (NOT even?(j))") (("1" (replace -1) (("1" (assert) (("1" (lemma "even_m1_pow") (("1" (inst - "1+j") (("1" (replace -2) (("1" (lift-if) (("1" (ground) nil))))))))))))) ("2" (assert) (("2" (hide-all-but 1) (("2" (expand "even?") (("2" (ground) (("1" (skosimp*) (("1" (assert) (("1" (replace -2) (("1" (assert) (("1" (case "EXISTS (kk:nat): 1= 2*kk") (("1" (skosimp*) (("1" (assert) nil))) ("2" (inst + "j!1-j!2") (("2" (assert) nil))))))))))))) ("2" (lemma "even_or_odd") (("2" (inst - "j") (("2" (expand "even?") (("2" (expand "odd?") (("2" (ground) (("2" (skosimp*) (("2" (inst 3 "j!1+1") (("2" (assert) nil))))))))))))))))))))))))))))))) ("2" (flatten) (("2" (replaces -1) (("2" (reveal "jpos") (("2" (expand "^") (("2" (expand "expt") (("2" (assert) nil))))))))))))))))))))))))))))))))))))))) ("2" (inst -2 "j") (("2" (expand "derivable?" -2) (("2" (inst - "x") nil))))) ("3" (case "EXISTS (c:real): (c=1 OR c=-1) AND (-x)^j = -c*x^j AND (LAMBDA (pr: real): -(-pr) ^ (1 + j) / (1 + j (("1" (skeep -1) (("1" (replace -3) (("1" (lemma "derivable_scal[real]") (("1" (inst - "-c / (1+j)" "LAMBDA (pr: real): (pr) ^ (1 + j)") (("1" (expand "*" -1) (("1" (expand "derivable?" -1) (("1" (inst - "x") (("1" (assert) nil))))))) ("2" (lemma "deriv_x_n[real]") (("2" (inst - "LAMBDA (pr: real): (pr) ^ (1 + j)" "1+j") (("2" (assert) nil))))))))))))) ("2" (hide-all-but 1) (("2" (name "cc" "IF even?(j) THEN -1 ELSE 1 ENDIF") (("2" (inst + "cc") (("2" (split) (("1" (replaces -1 :dir rl) (("1" (grind) nil))) ("2" (lemma "mult_expt") (("2" (inst - "j" "-1" "x") (("1" (assert) (("1" (replace -1) (("1" (lemma "even_m1_pow") (("1" (inst - "j") (("1" (lemma "not_even_m1_pow") (("1" (inst - "j") (("1" (lift-if) (("1" (ground) nil))))))))))))))) ("2" (reveal "jpos") (("2" (flatten) (("2" (replaces -1) (("2" (expand "^") (("2" (expand "expt") (("2" (assert) nil))))))))))))))) ("3" (decompose-equality) (("3" (lemma "mult_expt") (("3" (inst - "1+j" "-1" "x!1") (("1" (replaces -1) (("1" (lemma "not_even_m1_pow") (("1" (inst - "1+j") (("1" (case "even?(1+j) IFF (NOT even?(j))") (("1" (replace -1) (("1" (assert) (("1" (lemma "even_m1_pow") (("1" (inst - "1+j") (("1" (replace -2) (("1" (lift-if) (("1" (ground) nil))))))))))))) ("2" (assert) (("2" (hide-all-but 1) (("2" (expand "even?") (("2" (ground) (("1" (skosimp*) (("1" (assert) (("1" (replace -2) (("1" (assert) (("1" (case "EXISTS (kk:nat): 1= 2*kk") (("1" (skosimp*) (("1" (assert) nil))) ("2" (inst + "j!1-j!2") (("2" (assert) nil))))))))))))) ("2" (lemma "even_or_odd") (("2" (inst - "j") (("2" (expand "even?") (("2" (expand "odd?") (("2" (ground) (("2" (skosimp*) (("2" (inst 3 "j!1+1") (("2" (assert) nil))))))))))))))))))))))))))))))) ("2" (flatten) (("2" (replaces -1) (("2" (assert) nil))))))))))))))))))))))))))))))))))))))))))))) ("3" (skosimp*) (("3" (assert) nil))) ("4" (reveal "derivtt2") (("4" (skeep) (("4" (inst - "m") (("4" (expand "derivable?" -1) (("4" (inst - "x") nil))))))))))) ("3" (skosimp*) (("3" (assert) nil))) ("4" (skeep) (("4" (inst - "m") (("4" (expand "derivable?" -1) (("4" (inst - "x") nil))))))))))))))) ("2" (inst - "1+2*n") nil))))) ("2" (lemma "connected_real") (("2" (propax) nil))))))))))))))) ("2" (hide 2) (("2" (induct "m") (("1" (expand "ln_estimate") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (lemma "derivable_const[real]") (("1" (inst - "0") (("1" (expand "const_fun") (("1" (propax) nil))))))))))))) ("2" (skeep) (("2" (case "j = 0") (("1" (replaces -1) (("1" (hide -) (("1" (expand "ln_estimate") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (lemma "identity_derivable[real]") (("1" (expand "derivable?" +) (("1" (skeep) (("1" (inst - "x") (("1" (expand "I") (("1" (assert) nil))))))))))))))))))))))))))))) ("2" (label "jpos" 1) (("2" (hide 1) (("2" (expand "ln_estimate") (("2" (expand "sigma" +) (("2" (lemma "derivable_sum[real]") (("2" (inst - "(LAMBDA (pr: real): ln_estimate(pr, j))" "LAMBDA (pr: real): -(-pr) ^ (1 + j) / (1 + j)") (("1" (invoke (case "%1 = %2") (! -1 1) (! 1 1)) (("1" (assert) nil) ("2" (hide 2) (("2" (decompose-equality +) (("1" (expand "+") (("1" (expand "ln_estimate") (("1" (propax) nil))))) ("2" (skosimp*) nil))))) ("3" (assert) (("3" (skosimp*) nil))))) ("2" (assert) (("2" (hide 2) (("2" (hide -1) (("2" (case "EXISTS (c:real): (LAMBDA (pr: real): -(-pr) ^ (1 + j) / (1 + j)) = (LAMBDA (pr: real): -c*(pr) ^ (1 (("1" (skeep -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "derivable_scal[real]") (("1" (inst - "-c / (1+j)" "LAMBDA (pr: real): (pr) ^ (1 + j)") (("1" (expand "*") (("1" (assert) nil))) ("2" (hide 2) (("2" (lemma "deriv_x_n[real]") (("2" (inst - "LAMBDA (pr: real): (pr) ^ (1 + j)" "1+j") (("2" (assert) nil))))))))))))))))) ("2" (hide-all-but 1) (("2" (name "cc" "IF even?(j) THEN -1 ELSE 1 ENDIF") (("2" (inst + "cc") (("2" (decompose-equality) (("2" (lemma "mult_expt") (("2" (inst - "1+j" "-1" "x!1") (("1" (replaces -1) (("1" (lemma "not_even_m1_pow") (("1" (inst - "1+j") (("1" (case "even?(1+j) IFF (NOT even?(j))") (("1" (replace -1) (("1" (assert) (("1" (lemma "even_m1_pow") (("1" (inst - "1+j") (("1" (replace -2) (("1" (lift-if) (("1" (ground) nil))))))))))))) ("2" (assert) (("2" (hide-all-but 1) (("2" (expand "even?") (("2" (ground) (("1" (skosimp*) (("1" (assert) (("1" (replace -2) (("1" (assert) (("1" (case "EXISTS (kk:nat): 1= 2*kk") (("1" (skosimp*) (("1" (assert) nil))) ("2" (inst + "j!1-j!2") (("2" (assert) nil))))))))))))) ("2" (lemma "even_or_odd") (("2" (inst - "j") (("2" (expand "even?") (("2" (expand "odd?") (("2" (ground) (("2" (skosimp*) (("2" (inst 3 "j!1+1") (("2" (assert) nil))))))))))))))))))))))))))))))) ("2" (flatten) (("2" (replaces -1) (("2" (expand "^") (("2" (expand "expt") (("2" (assert) nil))))))))))))))))))))))))))))) ("3" (expand "ln_estimate") (("3" (propax) nil)))))))))))))))))))))))) nil) ((derivable_sum judgement-tcc nil derivatives "analysis/") (x!1 skolem-const-decl "real" ln_series nil) (j skolem-const-decl "nat" ln_series nil) (identity_derivable formula-decl nil derivatives_def "analysis/") (derivable_const judgement-tcc nil derivatives "analysis/") (connected_real formula-decl nil deriv_domain "analysis/") (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (not_one_element_real formula-decl nil deriv_domain "analysis/") (deriv_domain_real formula-decl nil deriv_domain "analysis/") (deriv_const formula-decl nil derivatives_def "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (sigma_0_neg formula-decl nil sigma_nat "reals/") (x!1 skolem-const-decl "real" ln_series nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (int_plus_int_is_int application-judgement "int" integers nil) (even_or_odd formula-decl nil naturalnumbers nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (even_m1_pow formula-decl nil exponentiation nil) (not_even_m1_pow formula-decl nil exponentiation nil) (x skolem-const-decl "real" ln_series nil) (odd_int nonempty-type-eq-decl nil integers nil) (odd? const-decl "bool" integers nil) (even? const-decl "bool" integers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (div_cancel3 formula-decl nil real_props nil) (times_div2 formula-decl nil real_props nil) (deriv const-decl "[T -> real]" derivatives "analysis/") (deriv_x_n formula-decl nil derivatives "analysis/") (deriv_scal formula-decl nil derivatives_def "analysis/") (deriv_neg formula-decl nil derivatives_def "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (x!1 skolem-const-decl "real" ln_series nil) (minus_int_is_int application-judgement "int" integers nil) (nat_exp application-judgement "nat" exponentiation nil) (derivable_scal judgement-tcc nil derivatives "analysis/") (j skolem-const-decl "nat" ln_series nil) (deriv_sum formula-decl nil derivatives_def "analysis/") (I const-decl "(bijective?[T, T])" identity nil) (deriv_identity formula-decl nil derivatives_def "analysis/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (mult_expt formula-decl nil exponentiation nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (hat_02n formula-decl nil power_series "series/") (real_times_real_is_real application-judgement "real" reals nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (< const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (abs_expt formula-decl nil exponent_props "reals/") (nnreal_expt application-judgement "nnreal" exponentiation nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (j skolem-const-decl "nat" ln_series nil) (> const-decl "bool" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal type-eq-decl nil real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (posnat_expt application-judgement "posnat" exponentiation nil) (both_sides_expt_pos_ge_aux formula-decl nil exponentiation nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_neg_ge1 formula-decl nil extra_real_props nil) (nzreal nonempty-type-eq-decl nil reals nil) (x skolem-const-decl "real" ln_series nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (div_cancel4 formula-decl nil real_props nil) (sigma_ge_0 formula-decl nil sigma "reals/") (minus_even_is_even application-judgement "even_int" integers nil) (int_exp application-judgement "int" exponentiation nil) (int_expt application-judgement "int" exponentiation nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (expt def-decl "real" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (expt_1i formula-decl nil exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (deriv const-decl "real" derivatives_def "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (= const-decl "[T, T -> boolean]" equalities nil) (minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (increasing? const-decl "bool" real_fun_preds "reals/") (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (deriv_fun type-eq-decl nil derivatives "analysis/") (n skolem-const-decl "nat" ln_series 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) (connected? const-decl "bool" deriv_domain_def "analysis/") (nonneg_derivative formula-decl nil derivative_props "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (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) (derivable? const-decl "bool" derivatives "analysis/") (ln_estimate const-decl "real" ln_series nil)) nil)) (ln_estimate_increasing_even 0 (ln_estimate_increasing_even-1 nil 3558194834 ("" (induct "n") (("1" (assert) (("1" (skeep) (("1" (expand "ln_estimate") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (inst - "x1" "y1") (("2" (assert) (("2" (expand "ln_estimate") (("2" (expand "sigma" +) (("2" (expand "sigma" +) (("2" (case "-(-x1) ^ (1 + 2 * j) / (1 + 2 * j) + -(-x1) ^ (2 + 2 * j) / (2 + 2 * j) <= -(-y1) ^ (1 + 2 * j) / (1 + 2 * j) + -(-y1) ^ (2 + 2 * j) / (2 + 2 * j)") (("1" (assert) nil nil) ("2" (hide-all-but (-2 1)) (("2" (lemma "mult_expt") (("2" (case "FORALL (i: posnat, n0x, n0y: real): (n0x * n0y) ^ i = n0x ^ i * n0y ^ i") (("1" (hide -2) (("1" (inst-cp - "1+2*j" "-1" "x1") (("1" (inst-cp - "1+2*j" "-1" "y1") (("1" (inst-cp - "2+2*j" "-1" "x1") (("1" (inst - "2+2*j" "-1" "y1") (("1" (replaces -1) (("1" (replaces -1) (("1" (replaces -1) (("1" (replaces -1) (("1" (case "FORALL (jj:nat): (-1)^(1+2*jj) = -1 AND (-1)^(2+2*jj) = 1") (("1" (inst - "j") (("1" (flatten) (("1" (replaces -1) (("1" (replaces -1) (("1" (assert) (("1" (name "FF" "LAMBDA (xx:absle1): xx ^ (1 + 2 * j) / (1 + 2 * j) - xx ^ (2 + 2 * j) / (2 + 2 * j)") (("1" (case "derivable?[absle1](FF)") (("1" (lemma "nonneg_derivative[absle1]") (("1" (inst - "FF") (("1" (ground) (("1" (expand "FF" -1) (("1" (expand "increasing?") (("1" (inst - "x1" "y1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide (2 3)) (("2" (lemma "deriv_diff[absle1]") (("2" (skeep) (("2" (inst - "LAMBDA (xx:absle1): xx ^ (1 + 2 * j) / (1 + 2 * j)" "LAMBDA (xx:absle1): xx ^ (2 + 2 * j) / (2 + 2 * j)" "x") (("2" (split -) (("1" (assert) (("1" (invoke (case "%1 = FF") (! -1 1 1)) (("1" (replaces -1) (("1" (replaces -1) (("1" (name "aa" "2+2*j") (("1" (replace -1) (("1" (name "bb" "1+2*j") (("1" (replace -1) (("1" (lemma "deriv_scal[absle1]") (("1" (lemma "deriv_x_to_n[absle1]") (("1" (inst-cp - "bb" "1/bb") (("1" (inst - "aa" "1/aa") (("1" (assert) (("1" (flatten) (("1" (decompose-equality -2) (("1" (inst - "x") (("1" (expand "deriv" -1) (("1" (replace -1) (("1" (assert) (("1" (decompose-equality -4) (("1" (inst - "x") (("1" (expand "deriv" -1) (("1" (replace -1) (("1" (case "x^(2*j) >= x^(2*j+1)") (("1" (assert) (("1" (field) nil nil)) nil) ("2" (hide 2) (("2" (hide-all-but 1) (("2" (case "FORALL (jj:nat): x ^ (2 * jj) >= x ^ (2 * jj + 1)") (("1" (inst - "j") nil nil) ("2" (hide 2) (("2" (induct "jj") (("1" (typepred "x") (("1" (grind) nil nil)) nil) ("2" (skolem 1 "m") (("2" (flatten) (("2" (expand "^") (("2" (expand "expt" +) (("2" (expand "expt" +) (("2" (case "x*x>=0") (("1" (mult-by -2 "x*x") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst + "IF x!1 = 0 THEN 1 ELSE 0 ENDIF") (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand "deriv_domain?") (("3" (skosimp*) (("3" (case "x!1 < 0") (("1" (inst + "min(e!1,1)/2") (("1" (typepred "x!1") (("1" (grind) nil nil)) nil) ("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil) ("2" (inst + "-min(e!1,1)/2") (("1" (typepred "x!1") (("1" (grind) nil nil)) nil) ("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst + "IF x!1 = 0 THEN 1 ELSE 0 ENDIF") (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand "deriv_domain?") (("3" (skosimp*) (("3" (case "x!1 < 0") (("1" (inst + "min(e!1,1)/2") (("1" (typepred "x!1") (("1" (grind) nil nil)) nil) ("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil) ("2" (inst + "-min(e!1,1)/2") (("1" (typepred "x!1") (("1" (grind) nil nil)) nil) ("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2)) (("2" (decompose-equality) (("2" (decompose-equality -) (("2" (inst - "x!1") (("2" (expand "-") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "deriv_x_to_n[absle1]") (("2" (inst - "1+2*j" "1/(1+2*j)") (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (expand "derivable?" -1) (("2" (inst - "x") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "deriv_x_to_n[absle1]") (("3" (inst - "2+2*j" "1/(2+2*j)") (("3" (assert) (("3" (flatten) (("3" (expand "derivable?" -1) (("3" (inst - "x") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "connected?") (("2" (skosimp*) (("2" (typepred "x!1") (("2" (typepred "y!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "derivable_diff[absle1]") (("2" (inst - "LAMBDA (xx:absle1): xx ^ (1 + 2 * j) / (1 + 2 * j)" "LAMBDA (xx:absle1): xx ^ (2 + 2 * j) / (2 + 2 * j)") (("1" (expand "-") (("1" (expand "FF" +) (("1" (propax) nil nil)) nil)) nil) ("2" (lemma "deriv_x_to_n[absle1]") (("2" (inst - "2+2*j" "1/(2+2*j)") (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (lemma "deriv_x_to_n[absle1]") (("3" (inst - "1+2*j" "1/(1+2*j)") (("3" (assert) (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand "not_one_element?") (("3" (skosimp*) (("3" (inst + "IF x!1 = 0 THEN 1 ELSE 0 ENDIF") (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but 1) (("4" (expand "deriv_domain?") (("4" (skosimp*) (("4" (case "x!1 < 0") (("1" (inst + "min(e!1,1)/2") (("1" (typepred "x!1") (("1" (grind) nil nil)) nil) ("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil) ("2" (inst + "-min(e!1,1)/2") (("1" (typepred "x!1") (("1" (grind) nil nil)) nil) ("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (induct "jj") (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (skosimp*) (("3" (expand "^") (("3" (expand "expt" +) (("3" (expand "expt" +) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skeep) (("2" (case "n0x = 0 OR n0y = 0") (("1" (split -) (("1" (replaces -1) (("1" (assert) nil nil)) nil) ("2" (replaces -1) (("2" (assert) nil nil)) nil)) nil) ("2" (inst - "i" "n0x" "n0y") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((odd_plus_even_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" 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 "[T, T -> boolean]" equalities nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (int_exp application-judgement "int" exponentiation nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (e!1 skolem-const-decl "posreal" ln_series nil) (x!1 skolem-const-decl "absle1" ln_series nil) (x!1 skolem-const-decl "absle1" ln_series nil) (j skolem-const-decl "nat" ln_series nil) (derivable_diff judgement-tcc nil derivatives "analysis/") (nonneg_derivative formula-decl nil derivative_props "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (increasing? const-decl "bool" real_fun_preds "reals/") (deriv_diff formula-decl nil derivatives_def "analysis/") (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint nonempty-type-eq-decl nil integers nil) (deriv_scal formula-decl nil derivatives_def "analysis/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (deriv const-decl "[T -> real]" derivatives "analysis/") (int_minus_int_is_int application-judgement "int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_min application-judgement "{z: posreal | z <= x AND z <= y}" real_defs nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (posreal nonempty-type-eq-decl nil real_types nil) (e!1 skolem-const-decl "posreal" ln_series nil) (x!1 skolem-const-decl "absle1" ln_series nil) (nzreal nonempty-type-eq-decl nil reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (< const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (x!1 skolem-const-decl "absle1" ln_series nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (expt def-decl "real" exponentiation nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (times_div1 formula-decl nil real_props nil) (div_cancel2 formula-decl nil real_props nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (x!1 skolem-const-decl "absle1" ln_series nil) (x!1 skolem-const-decl "absle1" ln_series nil) (e!1 skolem-const-decl "posreal" ln_series nil) (deriv_x_to_n formula-decl nil derivatives "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (deriv_fun type-eq-decl nil derivatives "analysis/") (FF skolem-const-decl "[absle1 -> real]" ln_series nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (nzreal_expt application-judgement "nzreal" exponentiation nil) (int_expt application-judgement "int" exponentiation nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (n0x skolem-const-decl "real" ln_series nil) (n0y skolem-const-decl "real" ln_series nil) (hat_02n formula-decl nil power_series "series/") (nat_exp application-judgement "nat" exponentiation nil) (mult_expt formula-decl nil exponentiation 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) (^ const-decl "real" exponentiation 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) (/= const-decl "boolean" notequal nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (even_plus_even_is_even application-judgement "even_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (minus_real_is_real application-judgement "real" reals nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma def-decl "real" sigma "reals/") (nat_induction formula-decl nil naturalnumbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (ln_estimate const-decl "real" ln_series nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (absle1 type-eq-decl nil ln_series nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (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)) nil)) (lnp1_prep_TCC1 0 (lnp1_prep_TCC1-1 nil 3319985090 ("" (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) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (abslt1 type-eq-decl nil ln_series 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) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (lnp1_prep_TCC2 0 (lnp1_prep_TCC2-1 nil 3319985090 ("" (subtype-tcc) nil nil) nil nil)) (lnp1_prep 0 (lnp1_prep-2 nil 3321032085 ("" (skosimp*) (("" (prop) (("1" (lemma "inv_fun_continuous[{x: real | x > -1}]") (("1" (inst - "(LAMBDA (x: {x: real | x > -1}): x+1)") (("1" (expand "/") (("1" (lemma "continuous_Integrable?[{x: real | x > -1}]") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (expand "continuous?" -1) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (inst 1 "0") nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "linear_fun_cont[{x: real | x > -1}]") (("2" (inst - "1" "1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "Int_chg_var[posreal,{x:real | x > -1}]") (("1" (inst - "0" "x1!1" "(LAMBDA (t: posreal): 1 / t)" "(LAMBDA (t: {x:real | x > -1}): 1+t)") (("1" (assert) (("1" (typepred "x1!1") (("1" (rewrite "abs_lt") (("1" (flatten) (("1" (assert) (("1" (lemma "deriv_linear_fun[{x: real | x > -1}]") (("1" (inst - "1" "1") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (hide 2) (("1" (replace -2) (("1" (lemma "const_fun_continuous[{x: real | x > -1}]") (("1" (inst - "1") (("1" (expand "const_fun") (("1" (assert) (("1" (lemma "one_over_x_cont[posreal]") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "0") nil nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (continuous? const-decl "bool" continuous_functions "analysis/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (nz_continuous_fun type-eq-decl nil continuous_functions "analysis/") (continuous_Integrable? formula-decl nil integral "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (TRUE const-decl "bool" booleans nil) (Closed_interval type-eq-decl nil intervals_real "reals/") (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (Gt_m1 type-eq-decl nil ln_series nil) (abslt1 type-eq-decl nil ln_series nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (linear_fun_cont formula-decl nil continuous_functions "analysis/") (inv_fun_continuous formula-decl nil continuous_functions "analysis/") (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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (deriv_linear_fun formula-decl nil derivatives "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (one_over_x_cont formula-decl nil continuous_functions "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (const_fun_continuous judgement-tcc nil continuous_functions "analysis/") (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) (abs_lt formula-decl nil abs_lems "reals/") (Int_chg_var formula-decl nil integral_chg_var "analysis/") (posreal nonempty-type-eq-decl nil real_types nil)) nil) (lnp1_prep-1 nil 3319985192 ("" (skosimp*) (("" (lemma "Int_chg_var[posreal,{x:real | x > -1}]") (("1" (inst - "0" "x1!1" "(LAMBDA (t: posreal): 1 / t)" "(LAMBDA (t: {x:real | x > -1}): 1+t)") (("1" (assert) (("1" (typepred "x1!1") (("1" (rewrite "abs_lt") (("1" (flatten) (("1" (assert) (("1" (lemma "deriv_linear_fun[{x: real | x > -1}]") (("1" (inst - "1" "1") (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (hide 2) (("1" (replace -2) (("1" (lemma "const_fun_continuous[{x: real | x > -1}]") (("1" (inst - "1") (("1" (expand "const_fun") (("1" (assert) (("1" (lemma "one_over_x_cont[posreal]") (("1" (lemma "one_over_x_cont[posreal]") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "0") nil nil) ("3" (skosimp*) (("3" (inst + "x!1+1") (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (inst + "x!1+1") (("5" (assert) nil nil)) nil)) nil) ("6" (skosimp*) (("6" (assert) nil nil)) nil)) nil)) nil) ((deriv_linear_fun formula-decl nil derivatives "analysis/") (one_over_x_cont formula-decl nil continuous_functions "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (const_fun_continuous judgement-tcc nil continuous_functions "analysis/") (Int_chg_var formula-decl nil integral_chg_var "analysis/")) shostak)) (geom_neg_TCC1 0 (geom_neg_TCC1-1 nil 3320162826 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (geom_neg_TCC2 0 (geom_neg_TCC2-1 nil 3320162826 ("" (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) (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) (^ const-decl "real" exponentiation nil) (series const-decl "sequence[real]" series "series/") (convergence const-decl "bool" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (/= const-decl "boolean" notequal nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (geom_neg_TCC3 0 (geom_neg_TCC3-1 nil 3320162826 ("" (skosimp*) (("" (lemma "geometric_series") (("" (expand "conv_series?") (("" (expand "convergent?") (("" (inst - "-x!1") (("" (rewrite "abs_lt") (("" (assert) (("" (rewrite "abs_lt") (("" (assert) (("" (expand "geometric") (("" (inst + "1 / (1 + x!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((geometric_series formula-decl nil series "series/") (conv_series? const-decl "bool" series "series/")) nil)) (geom_neg 0 (geom_neg-1 nil 3320162843 ("" (skosimp*) (("" (prop) (("1" (lemma "geometric_series") (("1" (inst - "-x!1") (("1" (rewrite "abs_neg") (("1" (assert) (("1" (expand "convergent?") (("1" (inst + "1/(1+x!1)") (("1" (expand "geometric") (("1" (assert) nil nil)) nil) ("2" (hide -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "geometric_sum") (("2" (inst - "-x!1") (("2" (assert) (("2" (rewrite "abs_neg") (("2" (assert) (("2" (expand "geometric") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals 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) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals 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) (geometric const-decl "sequence[real]" series "series/") (convergent? const-decl "bool" convergence_sequences "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (abs_neg formula-decl nil abs_lems "reals/") (geometric_series formula-decl nil series "series/") (geometric_sum formula-decl nil series "series/")) shostak)) (lnp1_conv 0 (lnp1_conv-1 nil 3321113124 ("" (expand "lnp1_seq") (("" (lemma "conv_integseq[abslt1]") (("1" (expand "integseq") (("1" (inst - "(LAMBDA (n: nat): (-1)^n)") (("1" (split -1) (("1" (case-replace "(LAMBDA (k: nat): IF k = 0 THEN 0 ELSE ((-1) ^ (k - 1)) / k ENDIF) = (LAMBDA (n): IF n = 0 THEN 0 ELSE ((-1 (("1" (hide -1 2) (("1" (apply-extensionality 1 :hide? t) (("1" (lift-if) (("1" (ground) (("1" (mult-by 2 "x!1") (("1" (expand "^") (("1" (expand "expt" 2 2) (("1" (expand "expt" 2 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "m1_conv") (("2" (expand "conv_powerseries?") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide 2) (("2" (typepred "x!1") (("2" (rewrite "abs_neg") nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (inst + "IF x!1 >= 0 THEN (1-x!1)/2 ELSE abs(x!1+1)/2 ENDIF") (("1" (skosimp*) (("1" (typepred "x!1") (("1" (grind) nil nil)) nil)) nil) ("2" (flatten) (("2" (cross-mult 2) (("2" (assert) (("2" (typepred "x!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (flatten) (("3" (case-replace "(1 - x!1) / 2 > 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (cross-mult 1) (("2" (assert) (("2" (typepred "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (hide 2) (("4" (inst-cp + "0") (("1" (inst + "1/2") (("1" (assert) nil nil) ("2" (grind) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil) ("5" (skosimp*) (("5" (assert) (("5" (hide 2) (("5" (typepred "x!1") (("5" (typepred "y!1") (("5" (expand "abs") (("5" (lift-if) (("5" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((abslt1 type-eq-decl nil ln_series nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (conv_integseq formula-decl nil power_series_integ "series/") (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (connected? const-decl "bool" deriv_domain_def "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (sequence type-eq-decl nil sequences 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) (conv_powerseries? const-decl "bool" power_series_conv "series/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (m1_conv formula-decl nil power_series_conv "series/") (NOT const-decl "[bool -> bool]" booleans 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) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_exp application-judgement "int" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (rat_exp application-judgement "rat" exponentiation nil) (int_expt application-judgement "int" exponentiation nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (expt def-decl "real" exponentiation nil) (div_cancel2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (both_sides_times1 formula-decl nil real_props nil) (integseq const-decl "sequence[real]" power_series_integ "series/") (abs_neg formula-decl nil abs_lems "reals/") (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (x!1 skolem-const-decl "abslt1" ln_series nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types 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) (lnp1_seq const-decl "real" ln_series nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil)) shostak)) (int_geo_prep_TCC1 0 (int_geo_prep_TCC1-1 nil 3321108060 ("" (subtype-tcc) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil)) nil)) (int_geo_prep_TCC2 0 (int_geo_prep_TCC2-1 nil 3321108060 ("" (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) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (abslt1 type-eq-decl nil ln_series 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) (/= const-decl "boolean" notequal nil)) nil)) (int_geo_prep 0 (int_geo_prep-1 nil 3321108102 ("" (skosimp*) (("" (lemma "inv_fun_continuous[abslt1]") (("" (inst - "(LAMBDA (x: abslt1): x+1)") (("1" (expand "/") (("1" (lemma "continuous_Integrable?[abslt1]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (skosimp*) (("1" (expand "continuous?" -1) (("1" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "u!1") (("2" (hide -3 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (assert) (("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst-cp + "1/2") (("1" (inst + "1/4") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (grind) nil nil)) nil) ("2" (ground) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (hide -3 2) (("3" (expand "connected?") (("3" (skosimp*) (("3" (hide -3) (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "linear_fun_cont[abslt1]") (("2" (inst - "1" "1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) (("3" (hide 1) (("3" (typepred "x!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((abslt1 type-eq-decl nil ln_series nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (inv_fun_continuous formula-decl nil continuous_functions "analysis/") (minus_real_is_real application-judgement "real" reals nil) (linear_fun_cont formula-decl nil continuous_functions "analysis/") (/ const-decl "[T -> real]" real_fun_ops "reals/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (Closed_interval type-eq-decl nil intervals_real "reals/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (continuous_Integrable? formula-decl nil integral "analysis/") (nz_continuous_fun type-eq-decl nil continuous_functions "analysis/") (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (continuous? const-decl "bool" continuous_functions "analysis/") (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (int_geo_neg_TCC1 0 (int_geo_neg_TCC1-1 nil 3321103125 ("" (skosimp*) (("" (lemma "lnp1_prep") (("" (inst?) (("" (flatten) nil nil)) nil)) nil)) nil) ((lnp1_prep formula-decl nil ln_series nil) (abslt1 type-eq-decl nil ln_series nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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)) nil)) (int_geo_neg 0 (int_geo_neg-2 nil 3352452469 ("" (skosimp*) (("" (case-replace "Integral(0, x1!1, (LAMBDA (u: {x: real | x > -1}): 1 / (u + 1))) = Integral(0, x1!1, (LAMBDA (u: abslt1): 1 / (u + 1)))") (("1" (hide -1) (("1" (lemma "geom_neg") (("1" (case-replace "(LAMBDA (u: abslt1): 1 / (1 + u)) = (LAMBDA (x: abslt1): inf_sum(LAMBDA n: (-x) ^ n))") (("1" (hide -1 -2) (("1" (rewrite "lnp1_conv") (("1" (lemma "integral_powerseries[abslt1]") (("1" (expand "inf_sum") (("1" (expand "Inf_sum") (("1" (expand "powerseries") (("1" (rewrite "apow_rew") (("1" (expand "apowerseq") (("1" (expand "powerseq") (("1" (inst - "(LAMBDA (n: nat): (-1)^n)" "x1!1") (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (case "FORALL (x: abslt1): convergent?(series(LAMBDA (k: nat): (-1) ^ k * x ^ k ))") (("1" (case-replace "(LAMBDA (x: abslt1): limit(series(LAMBDA (k: nat): (-1) ^ k * x ^ k))) = (LAMBDA (x: abslt1): limit(series(LAMBDA n: (("1" (replace -4) (("1" (expand "integ_powerseq") (("1" (expand "lnp1_seq") (("1" (hide -1 -3 -4) (("1" (lemma "limit_series_shift") (("1" (inst - "(LAMBDA (k: nat): IF k = 0 THEN 0 ELSE ((-1) ^ (1 + k)) / k * x1!1 ^ k ENDIF)" "1") (("1" (assert) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (case-replace "(LAMBDA (k: nat): ((-1) ^ k * x1!1 ^ (1 + k)) / (1 + k)) = (LAMBDA n: (((-1) ^ (2 + n)) / (1 + n)) * x1!1 ^ (1 + n))") (("1" (hide 2) (("1" (apply-extensionality 1 :hide? t) (("1" (name-replace "XP" "x1!1 ^ (1 + x!1)") (("1" (field 1) (("1" (cancel-terms 1) (("1" (expand "^") (("1" (expand "expt" 1 2) (("1" (expand "expt" 1 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "lnp1_conv") (("2" (expand "lnp1_seq") (("2" (expand "conv_powerseries?") (("2" (expand "powerseries") (("2" (assert) (("2" (expand "powerseq") (("2" (inst - "x1!1") (("2" (case-replace "(LAMBDA (k: nat): IF k = 0 THEN 0 ELSE ((-1) ^ (1 + k)) / k ENDIF * x1!1 ^ k) = (LAMBDA (k: nat): IF k = 0 THEN 0 ELSE ((-1) ^ (1 + k)) / k * x1!1 ^ k ENDIF) ") (("1" (hide -1 -2 2) (("1" (apply-extensionality 1 :hide? t) (("1" (lift-if) (("1" (ground) nil nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("1" (hide -1 -2) (("1" (case-replace "(LAMBDA (k: nat): (-1) ^ k * x!1 ^ k) = (LAMBDA n: (-x!1) ^ n)") (("1" (hide 2) (("1" (apply-extensionality 1 :hide? t) (("1" (rewrite "mult_expt" :dir rl) (("1" (assert) nil nil) ("2" (ground) (("2" (replace -1) (("2" (assert) (("2" (hide -2) (("2" (case-replace "0 ^ x!2 = 0") (("1" (assert) nil nil) ("2" (case-replace "x!2 = 0") (("1" (assert) nil nil) ("2" (rewrite "hat_02n") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2) (("2" (skosimp*) (("2" (lemma "geom_neg") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skeep) (("3" (inst? -) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide -) (("3" (skosimp*) (("3" (lemma "geom_neg") (("3" (inst - "x!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (skeep) (("4" (inst? -) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (hide 2) (("2" (skosimp*) (("2" (hide -1) (("2" (lemma "geom_neg") (("2" (inst -1 "x!1") (("2" (assert) (("2" (flatten) (("2" (case-replace "(LAMBDA (k: nat): IF k = 0 THEN 1 ELSE (-1) ^ k * x!1 ^ k ENDIF) = (LAMBDA n: (-x!1) ^ n)") (("1" (hide -1 2) (("1" (case-replace "(LAMBDA (k: nat): (-1) ^ k * x!1 ^ k) = (LAMBDA n: (-x!1) ^ n)") (("1" (apply-extensionality 1 :hide? t) (("1" (hide-all-but 1) (("1" (rewrite "mult_expt" :dir rl) (("1" (assert) nil nil) ("2" (flatten) (("2" (replace -1) (("2" (assert) (("2" (rewrite "hat_02n") (("1" (assert) nil nil) ("2" (case-replace "x!2 = 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality :hide? t) (("2" (lift-if) (("2" (ground) (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide 3) (("2" (hide -1 -2) (("2" (rewrite "mult_expt" :dir rl) (("1" (assert) nil nil) ("2" (flatten) (("2" (replace -1) (("2" (rewrite "hat_02n") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "abs_0") (("2" (assert) nil nil)) nil) ("3" (hide 2) (("3" (expand "conv_powerseries?") (("3" (skosimp*) (("3" (typepred "x!1") (("3" (rewrite "m1_conv") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (rewrite "abs_neg") nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (inst + "IF x!1 >= 0 THEN (1-x!1)/2 ELSE abs(x!1+1)/2 ENDIF") (("1" (skosimp*) (("1" (grind) nil nil)) nil) ("2" (flatten) (("2" (grind) nil nil)) nil) ("3" (flatten) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (expand "conv_series?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (typepred "u!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 2) (("3" (inst?) (("3" (assert) (("3" (expand "conv_series?") (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (hide 1) (("4" (hide -2) (("4" (typepred "u!1") (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "Int_diff_dom[abslt1,Gt_m1]") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (rewrite "abs_0") (("1" (assert) (("1" (lemma "lnp1_prep") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (lemma "int_geo_prep") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (typepred "u!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst + "0") nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (rewrite "int_geo_prep") nil nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (typepred "u!1") (("4" (grind) nil nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (lemma "inv_fun_continuous[{x: real | x > -1}]") (("5" (inst - "(LAMBDA (x: {x: real | x > -1}): x+1)") (("1" (expand "/") (("1" (lemma "continuous_Integrable?[abslt1]") (("1" (inst?) (("1" (assert) (("1" (expand "continuous?" -1) (("1" (rewrite "abs_0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "abs_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "linear_fun_cont[{x: real | x > -1}]") (("2" (inst?) (("2" (inst - "1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (lemma "lnp1_prep") (("6" (inst?) (("6" (flatten) (("6" (assert) nil nil)) nil)) nil)) nil)) nil) ("7" (assert) (("7" (hide 2) (("7" (typepred "x1!1") (("7" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types 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) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (Integrable? const-decl "bool" integral_def "analysis/") (Integrable_funs type-eq-decl nil integral_def "analysis/") (Integral const-decl "real" integral_def "analysis/") (< const-decl "bool" reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (abslt1 type-eq-decl nil ln_series 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) (geom_neg formula-decl nil ln_series nil) (integral_powerseries formula-decl nil power_series_integ "series/") (connected? const-decl "bool" deriv_domain_def "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (Inf_sum const-decl "real" power_series_conv "series/") (lnp1_seq const-decl "real" ln_series nil) (apow_rew formula-decl nil power_series "series/") (powerseq const-decl "sequence[real]" power_series "series/") (nzreal_exp application-judgement "nzreal" exponentiation nil) (int_exp application-judgement "int" exponentiation nil) (m1_conv formula-decl nil power_series_conv "series/") (abs_0 formula-decl nil abs_lems "reals/") (int_times_even_is_even application-judgement "even_int" integers nil) (limit const-decl "real" convergence_sequences "analysis/") (integ_powerseq const-decl "sequence[real]" power_series_integ "series/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (expt def-decl "real" exponentiation nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (int_expt application-judgement "int" exponentiation nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (div_cancel2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (both_sides_times1 formula-decl nil real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (posint nonempty-type-eq-decl nil integers nil) (sigma def-decl "real" sigma "reals/") (conv_powerseries? const-decl "bool" power_series_conv "series/") (real_div_nzreal_is_real application-judgement "real" reals nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (limit_series_shift formula-decl nil series "series/") (minus_even_is_even application-judgement "even_int" integers nil) (nat_exp application-judgement "nat" exponentiation nil) (hat_02n formula-decl nil power_series "series/") (expt_x0 formula-decl nil exponentiation nil) (mult_expt formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (series const-decl "sequence[real]" series "series/") (convergent? const-decl "bool" convergence_sequences "analysis/") (real_times_real_is_real application-judgement "real" reals nil) (apowerseq const-decl "sequence[real]" power_series "series/") (powerseries const-decl "sequence[real]" power_series "series/") (abs_neg formula-decl nil abs_lems "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (x!1 skolem-const-decl "abslt1" ln_series nil) (lnp1_conv formula-decl nil ln_series nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" 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) (sequence type-eq-decl nil sequences nil) (conv_series? const-decl "bool" series "series/") (inf_sum const-decl "real" series "series/") (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (Int_diff_dom formula-decl nil integral_diff_doms "analysis/") (Gt_m1 type-eq-decl nil ln_series nil) (int_geo_prep formula-decl nil ln_series nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (lnp1_prep formula-decl nil ln_series nil) (inv_fun_continuous formula-decl nil continuous_functions "analysis/") (linear_fun_cont formula-decl nil continuous_functions "analysis/") (/ const-decl "[T -> real]" real_fun_ops "reals/") (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (continuous? const-decl "bool" continuous_functions "analysis/") (continuous_Integrable? formula-decl nil integral "analysis/") (nz_continuous_fun type-eq-decl nil continuous_functions "analysis/") (continuous? const-decl "bool" continuous_functions "analysis/")) nil) (int_geo_neg-1 nil 3320164561 ("" (skosimp*) (("" (case-replace "Integral(0, x1!1, (LAMBDA (u: {x: real | x > -1}): 1 / (u + 1))) = Integral(0, x1!1, (LAMBDA (u: abslt1): 1 / (u + 1)))") (("1" (hide -1) (("1" (lemma "geom_neg") (("1" (case-replace "(LAMBDA (u: abslt1): 1 / (1 + u)) = (LAMBDA (x: abslt1): inf_sum(LAMBDA n: (-x) ^ n))") (("1" (hide -1 -2) (("1" (rewrite "lnp1_conv") (("1" (lemma "integral_powerseries[abslt1]") (("1" (expand "inf_sum") (("1" (expand "Inf_sum") (("1" (expand "powerseries") (("1" (expand "powerseq") (("1" (inst - "(LAMBDA (n: nat): (-1)^n)" "x1!1") (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (case "FORALL (x: abslt1): convergent?(series(LAMBDA (k: nat): IF k = 0 THEN 1 ELSE (-1) ^ k * x ^ k ENDIF))") (("1" (case-replace "(LAMBDA (x: abslt1): limit(series(LAMBDA (k: nat): IF k = 0 THEN 1 ELSE (-1) ^ k * x ^ k ENDIF))) = (LAMBDA (x: abslt1): limit(series(LAMBDA n: (-x) ^ n)))") (("1" (replace -4) (("1" (expand "integ_powerseq") (("1" (expand "lnp1_seq") (("1" (hide -1 -3 -4) (("1" (lemma "limit_series_shift") (("1" (inst - "(LAMBDA (k: nat): IF k = 0 THEN 0 ELSE ((-1) ^ (1 + k)) / k * x1!1 ^ k ENDIF)" "1") (("1" (assert) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (expand "sigma") (("1" (case-replace "(LAMBDA (k: nat): ((-1) ^ k * x1!1 ^ (1 + k)) / (1 + k)) = (LAMBDA n: (((-1) ^ (2 + n)) / (1 + n)) * x1!1 ^ (1 + n))") (("1" (hide 2) (("1" (apply-extensionality 1 :hide? t) (("1" (name-replace "XP" "x1!1 ^ (1 + x!1)") (("1" (field 1) (("1" (cancel-terms 1) (("1" (expand "^") (("1" (expand "expt" 1 2) (("1" (expand "expt" 1 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "lnp1_conv") (("2" (expand "lnp1_seq") (("2" (expand "conv_powerseries?") (("2" (expand "powerseries") (("2" (assert) (("2" (expand "powerseq") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("1" (hide -1 -2) (("1" (case-replace "(LAMBDA (k: nat): IF k = 0 THEN 1 ELSE (-1) ^ k * x!1 ^ k ENDIF) = (LAMBDA n: (-x!1) ^ n)") (("1" (hide 2) (("1" (apply-extensionality 1 :hide? t) (("1" (rewrite "mult_expt" :dir rl) (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (replace -1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lift-if) (("2" (ground) (("1" (replace -1) (("1" (grind) nil nil)) nil) ("2" (replace -1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2) (("2" (skosimp*) (("2" (lemma "geom_neg") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide -) (("3" (skosimp*) (("3" (lemma "geom_neg") (("3" (inst - "x!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (hide 2) (("2" (skosimp*) (("2" (hide -1) (("2" (lemma "geom_neg") (("2" (inst -1 "x!1") (("2" (assert) (("2" (flatten) (("2" (case-replace "(LAMBDA (k: nat): IF k = 0 THEN 1 ELSE (-1) ^ k * x!1 ^ k ENDIF) = (LAMBDA n: (-x!1) ^ n)") (("2" (hide -1 2) (("2" (apply-extensionality 1 :hide? t) (("2" (lift-if) (("2" (ground) (("1" (replace -1) (("1" (expand "^") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (hide -1 3) (("2" (lemma "mult_expt") (("2" (inst?) (("1" (assert) nil nil) ("2" (assert) (("2" (flatten) (("2" (replace -1) (("2" (assert) (("2" (expand "^") (("2" (expand "expt") (("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) ("2" (hide 2) (("2" (grind) nil nil)) nil) ("3" (hide 2) (("3" (expand "conv_powerseries?") (("3" (skosimp*) (("3" (typepred "x!1") (("3" (rewrite "m1_conv") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (rewrite "abs_neg") nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (typepred "x!1") (("3" (inst + "IF x!1 >= 0 THEN (1-x!1)/2 ELSE abs(x!1+1)/2 ENDIF") (("1" (skosimp*) (("1" (grind) nil nil)) nil) ("2" (flatten) (("2" (grind) nil nil)) nil) ("3" (flatten) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (hide 2) (("4" (case "x!1 = 0") (("1" (inst + "1/2") (("1" (assert) nil nil) ("2" (grind) nil nil)) nil) ("2" (inst + "0") (("1" (assert) nil nil) ("2" (rewrite "abs_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("5" (skosimp*) (("5" (hide 2) (("5" (typepred "x!1") (("5" (typepred "y!1") (("5" (expand "abs") (("5" (lift-if) (("5" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("1" (inst?) (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (expand "conv_series?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (typepred "u!1") (("3" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 2) (("3" (inst?) (("3" (assert) (("3" (expand "conv_series?") (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (hide 1) (("4" (hide -2) (("4" (typepred "u!1") (("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "Int_diff_dom[abslt1,Gt_m1]") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (rewrite "abs_0") (("1" (assert) (("1" (lemma "lnp1_prep") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (prop) (("1" (hide -) (("1" (typepred "x1!1") (("1" (grind) nil nil)) nil)) nil) ("2" (hide -2) (("2" (lemma "int_geo_prep") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "u!1") (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst + "0") nil nil)) nil) ("3" (skosimp*) (("3" (hide 2) (("3" (inst + "x!1+1") (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil) ("5" (skosimp*) (("5" (hide 2) (("5" (inst-cp + "1/2") (("1" (inst-cp + "0") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (rewrite "abs_0") (("2" (assert) nil nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil) ("6" (skosimp*) (("6" (assert) (("6" (hide 2) (("6" (typepred "y!1") (("6" (typepred "x!1") (("6" (expand "abs") (("6" (lift-if) (("6" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (rewrite "int_geo_prep") nil nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (typepred "u!1") (("4" (grind) nil nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (lemma "inv_fun_continuous[{x: real | x > -1}]") (("5" (inst - "(LAMBDA (x: {x: real | x > -1}): x+1)") (("1" (expand "/") (("1" (lemma "continuous_Integrable?[abslt1]") (("1" (inst?) (("1" (assert) (("1" (expand "continuous?" -1) (("1" (rewrite "abs_0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "abs_0") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (hide -1 2) (("2" (inst-cp + "1/2") (("1" (inst + "0") (("1" (assert) nil nil) ("2" (rewrite "abs_0") (("2" (assert) nil nil)) nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (hide -3 2) (("3" (typepred "x!1") (("3" (typepred "y!1") (("3" (expand "abs") (("3" (lift-if) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "linear_fun_cont[{x: real | x > -1}]") (("2" (inst?) (("2" (inst - "1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (hide 2) (("6" (lemma "lnp1_prep") (("6" (inst?) (("6" (flatten) (("6" (assert) nil nil)) nil)) nil)) nil)) nil) ("7" (assert) (("7" (hide 2) (("7" (typepred "x1!1") (("7" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((nz_continuous_fun type-eq-decl nil continuous_functions "analysis/") (continuous_Integrable? formula-decl nil integral "analysis/") (linear_fun_cont formula-decl nil continuous_functions "analysis/") (inv_fun_continuous formula-decl nil continuous_functions "analysis/") (Int_diff_dom formula-decl nil integral_diff_doms "analysis/") (limit_series_shift formula-decl nil series "series/") (sigma def-decl "real" sigma "reals/") (integ_powerseq const-decl "sequence[real]" power_series_integ "series/") (limit const-decl "real" convergence_sequences "analysis/") (m1_conv formula-decl nil power_series_conv "series/") (powerseq const-decl "sequence[real]" power_series "series/") (integral_powerseries formula-decl nil power_series_integ "series/") (convergence const-decl "bool" convergence_sequences "analysis/") (Integral const-decl "real" integral_def "analysis/") (Integrable_funs type-eq-decl nil integral_def "analysis/") (Integrable? const-decl "bool" integral_def "analysis/")) shostak)))
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.859Bemerkung: (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-01) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26