| 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 1 MB |
|
SSL ln_exp_series_alt.prfSprache: Lisp |
|||||||||||||||
|
(ln_exp_series_alt (noa_posreal 0 (noa_posreal-1 nil 3477844115 ("" (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)) (conn_posreal 0 (conn_posreal-1 nil 3477844124 ("" (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)) (noa_gt_m1 0 (noa_gt_m1-1 nil 3477844134 ("" (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 3477844144 ("" (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)) (deriv_domain_gtm1 0 (deriv_domain_gtm1-1 nil 3477844153 ("" (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 3279382887 ("" (lemma "deriv_domain_posreal") (("" (propax) nil nil)) nil) ((deriv_domain_posreal formula-decl nil deriv_domain "analysis/")) shostak)) (nderiv_ln_TCC2 0 (nderiv_ln_TCC2-1 nil 3279382887 ("" (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)) (nderiv_ln 0 (nderiv_ln-2 nil 3445353631 ("" (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)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "ln_derivable") (("2" (flatten -1) (("2" (lemma "identity_derivable_fun[posreal]") (("2" (lemma "const_derivable_fun[posreal]" ("b" "-factorial(j!1)")) (("2" (lemma "deriv_id_fun[posreal]") (("2" (lemma "deriv_const_fun[posreal]" ("b" "-factorial(j!1)")) (("2" (expand "I") (("2" (expand "const_fun") (("2" (lemma "neg_derivable_fun[posreal]" ("f" "LAMBDA (x: posreal): x")) (("2" (assert) (("2" (expand "-") (("2" (lemma "deriv_neg_fun[posreal]" ("ff" "LAMBDA (x: posreal): x")) (("2" (replace -4) (("2" (expand "-" -1) (("2" (lemma "inv_derivable_fun[posreal]" ("g" "LAMBDA (x_1: posreal): -x_1")) (("2" (assert) (("2" (expand "/") (("2" (lemma "deriv_inv_fun[posreal]" ("gg" "LAMBDA (x_1: posreal): -x_1")) (("2" (replace -3) (("2" (expand "/") (("2" (expand "*") (("2" (expand "-" -1) (("2" (lemma "extensionality" ("f" "LAMBDA (x: posreal): --1 / (-x * -x)" "g" "LAMBDA (x: posreal): 1 / (x * x)")) (("2" (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" (rewrite "expt_1i") (("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)) nil) ("2" (hide 3) (("2" (skosimp*) (("2" (expand "*" 1) (("2" (expand "^" 1 1) (("2" (rewrite "div_expt" 1) (("2" (rewrite "expt_1i" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (expt_1i formula-decl nil exponentiation nil) (expt_plus formula-decl nil exponentiation nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (expt def-decl "real" exponentiation nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (odd_minus_odd_is_even application-judgement "even_int" integers 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/") (expt_x1 formula-decl nil exponentiation nil) (factorial_1 formula-decl nil factorial "ints/") (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 3270048547 ("" (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) (("1" (expand "factorial" -1) (("1" (assert) nil nil)) 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" (rewrite "expt_1i") (("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)) nil) ("2" (hide 3) (("2" (skosimp*) (("2" (expand "*" 1) (("2" (expand "^" 1 1) (("2" (rewrite "div_expt" 1) (("2" (rewrite "expt_1i" 1) (("2" (assert) nil 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/") (factorial_1 formula-decl nil factorial "ints/") (factorial_0 formula-decl nil factorial "ints/") (ln const-decl "real" ln_exp nil) (nderiv_fun type-eq-decl nil nth_derivatives "analysis/") (nderiv def-decl "[T -> real]" nth_derivatives "analysis/") (factorial def-decl "posnat" factorial "ints/")) shostak)) (ln_nderiv_TCC1 0 (ln_nderiv_TCC1-1 nil 3270048004 ("" (lemma "nderiv_ln") (("" (propax) nil nil)) nil) ((nderiv_ln formula-decl nil ln_exp_series_alt nil)) shostak)) (ln_nderiv_TCC2 0 (ln_nderiv_TCC2-1 nil 3270047982 ("" (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 3270056481 ("" (skosimp*) (("" (assert) nil nil)) nil) ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (ln_nderiv 0 (ln_nderiv-2 nil 3352447560 ("" (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) (("1" (lemma "extensionality" ("f" "(LAMBDA (t: posreal): 1 / t)" "g" "(LAMBDA (x: posreal): -1 / (-x) ^ 1)")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but (-3 1)) (("2" (skosimp*) (("2" (rewrite "expt_x1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "identity_derivable_fun[posreal]") (("2" (lemma "deriv_id_fun[posreal]") (("2" (expand "I") (("2" (lemma "neg_derivable_fun[posreal]" ("f" "LAMBDA (x: posreal): x")) (("2" (assert) (("2" (expand "-") (("2" (lemma "deriv_neg_fun[posreal]" ("ff" "LAMBDA (x: posreal): x")) (("2" (replace -3) (("2" (expand "-" -1) (("2" (lemma "inv_derivable_fun[posreal]" ("g" "LAMBDA (x_1: posreal): -x_1")) (("2" (replace -3) (("2" (expand "/") (("2" (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" (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 nil) ("2" (hide-all-but 1) (("2" (grind) nil 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" (rewrite "expt_1i") (("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" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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" (lemma "nderiv_ln") (("4" (propax) 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/") (* 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_plus formula-decl nil exponentiation nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (expt def-decl "real" exponentiation nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (expt_1i formula-decl nil exponentiation nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" 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) (identity_derivable_fun formula-decl nil derivatives "analysis/") (ln_derivable formula-decl nil ln_exp nil) (extensionality formula-decl nil functions nil) (expt_x1 formula-decl nil exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (factorial_0 formula-decl nil factorial "ints/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nderiv_ln formula-decl nil ln_exp_series_alt 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-1 nil 3270056529 ("" (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) (("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 nil) ("2" (hide-all-but (-3 1)) (("2" (skosimp*) (("2" (rewrite "expt_x1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) 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" (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 nil) ("2" (hide-all-but 1) (("2" (grind) nil 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" (rewrite "expt_1i") (("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)) 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" (lemma "nderiv_ln") (("4" (propax) 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)) shostak)) (ln_estimate_TCC1 0 (ln_estimate_TCC1-1 nil 3270048045 ("" (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 3270048058 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (ln_estimate_TCC3 0 (ln_estimate_TCC3-1 nil 3374506918 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (ln_estimate_TCC4 0 (ln_estimate_TCC4-1 nil 3374506918 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (/= const-decl "boolean" notequal nil)) nil)) (ln_estimate_scaf1_TCC1 0 (ln_estimate_scaf1_TCC1-1 nil 3309536146 ("" (skosimp) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (ln_estimate_scaf1 0 (ln_estimate_scaf1-2 nil 3352449073 ("" (skosimp) (("" (lemma "id_fun_continuous[posreal]") (("" (expand "I") (("" (lemma "const_fun_continuous[posreal]" ("u" "1")) (("" (expand "const_fun") (("" (lemma "diff_fun_continuous[posreal]" ("h1" "LAMBDA (x: posreal): 1" "h2" "LAMBDA (x: posreal): x")) (("1" (expand "-") (("1" (case "forall (n:nat): continuous?(LAMBDA (t: posreal): (1 - t) ^ n)") (("1" (inst - "n!1") (("1" (lemma "div_fun_continuous[posreal]" ("h" "LAMBDA (t: posreal): (1 - t) ^ n!1" "h3" "LAMBDA (x: posreal): x")) (("1" (expand "/") (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (hide -3 2) (("2" (induct "n") (("1" (hide -1) (("1" (lemma "extensionality" ("f" "LAMBDA (x: posreal): 1" "g" "LAMBDA (t: posreal): (1 - t) ^ 0")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "^") (("2" (expand "expt") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "prod_fun_continuous[posreal]" ("h1" "LAMBDA (t: posreal): (1 - t) ^ j!1" "h2" "LAMBDA (t: posreal): (1 - t)")) (("1" (expand "*") (("1" (lemma "extensionality" ("f" "LAMBDA (x: posreal): (1 - x) ^ j!1 - x * (1 - x) ^ j!1" "g" "LAMBDA (t: posreal): (1 - t) ^ (j!1 + 1)")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "^") (("2" (expand "expt" 1 3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) 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) (id_fun_continuous judgement-tcc nil continuous_functions "analysis/") (const_fun_continuous judgement-tcc nil continuous_functions "analysis/") (diff_fun_continuous judgement-tcc nil continuous_functions "analysis/") (continuous? const-decl "bool" continuous_functions "analysis/") (continuous_fun nonempty-type-eq-decl nil continuous_functions "analysis/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (real_minus_real_is_real application-judgement "real" reals nil) (div_fun_continuous judgement-tcc nil continuous_functions "analysis/") (nzreal nonempty-type-eq-decl nil reals nil) (nz_continuous_fun type-eq-decl nil continuous_functions "analysis/") (/ const-decl "[T -> real]" real_fun_ops "reals/") (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (extensionality formula-decl nil functions nil) (expt def-decl "real" exponentiation nil) (prod_fun_continuous judgement-tcc nil continuous_functions "analysis/") (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) (* const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (I const-decl "(bijective?[T, T])" identity nil)) nil) (ln_estimate_scaf1-1 nil 3309536222 ("" (skosimp) (("" (lemma "id_fun_continuous[posreal]") (("" (expand "I") (("" (lemma "const_fun_continuous[posreal]" ("u" "1")) (("" (expand "const_fun") (("" (lemma "diff_fun_continuous" ("h1" "LAMBDA (x: posreal): 1" "h2" "LAMBDA (x: posreal): x")) (("1" (expand "-") (("1" (case "forall (n:nat): continuous?(LAMBDA (t: posreal): (1 - t) ^ n)") (("1" (inst - "n!1") (("1" (lemma "div_fun_continuous" ("h" "LAMBDA (t: posreal): (1 - t) ^ n!1" "h3" "LAMBDA (x: posreal): x")) (("1" (expand "/") (("1" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (hide -3 2) (("2" (induct "n") (("1" (hide -1) (("1" (lemma "extensionality" ("f" "LAMBDA (x: posreal): 1" "g" "LAMBDA (t: posreal): (1 - t) ^ 0")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "^") (("2" (expand "expt") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "prod_fun_continuous" ("h1" "LAMBDA (t: posreal): (1 - t) ^ j!1" "h2" "LAMBDA (t: posreal): (1 - t)")) (("1" (expand "*") (("1" (lemma "extensionality" ("f" "LAMBDA (x: posreal): (1 - x) ^ j!1 - x * (1 - x) ^ j!1" "g" "LAMBDA (t: posreal): (1 - t) ^ (j!1 + 1)")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "^") (("2" (expand "expt" 1 3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((id_fun_continuous judgement-tcc nil continuous_functions "analysis/") (const_fun_continuous judgement-tcc nil continuous_functions "analysis/") (diff_fun_continuous judgement-tcc nil continuous_functions "analysis/") (continuous_fun nonempty-type-eq-decl nil continuous_functions "analysis/") (div_fun_continuous judgement-tcc nil continuous_functions "analysis/") (nz_continuous_fun type-eq-decl nil continuous_functions "analysis/") (prod_fun_continuous judgement-tcc nil continuous_functions "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/")) shostak)) (ln_estimate_scaf2_TCC1 0 (ln_estimate_scaf2_TCC1-1 nil 3471688910 ("" (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/")) nil)) (ln_estimate_scaf2 0 (ln_estimate_scaf2-1 nil 3309539006 ("" (skosimp) (("" (lemma "continuous_Integrable?[posreal]") (("1" (inst?) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (lemma "ln_estimate_scaf1" ("n" "n!1")) (("2" (expand "continuous?" -1) (("2" (inst - "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst + "x!2+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (expand "connected?") (("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) (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/") (continuous? const-decl "bool" continuous_functions "analysis/") (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (Closed_interval type-eq-decl nil intervals_real "reals/") (ln_estimate_scaf1 formula-decl nil ln_exp_series_alt nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" 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) (/ 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) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) shostak)) (ln_estimate_scaf3_TCC1 0 (ln_estimate_scaf3_TCC1-1 nil 3309546558 ("" (skosimp) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (ln_estimate_scaf3_TCC2 0 (ln_estimate_scaf3_TCC2-1 nil 3309546568 ("" (lemma "ln_estimate_scaf2" ("n" "0")) (("" (propax) nil nil)) nil) ((ln_estimate_scaf2 formula-decl nil ln_exp_series_alt 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_estimate_scaf3 0 (ln_estimate_scaf3-1 nil 3309540591 ("" (skosimp) (("" (expand "ln") (("" (lemma "extensionality" ("f" "LAMBDA (t: posreal): (1 - t) ^ 0 / t" "g" "LAMBDA (t: posreal): 1 / t")) (("" (split -1) (("1" (assert) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "^") (("2" (expand "expt") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ln const-decl "real" ln_exp nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (expt def-decl "real" exponentiation nil) (real_minus_real_is_real application-judgement "real" reals nil) (extensionality formula-decl nil functions nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation 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) (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)) shostak)) (ln_estimate_scaf4_TCC1 0 (ln_estimate_scaf4_TCC1-1 nil 3309547516 ("" (skosimp) (("" (assert) nil nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (ln_estimate_scaf4_TCC2 0 (ln_estimate_scaf4_TCC2-1 nil 3309547523 ("" (skosimp) (("" (assert) nil nil)) nil) nil shostak)) (ln_estimate_scaf4_TCC3 0 (ln_estimate_scaf4_TCC3-1 nil 3309547541 ("" (skosimp) (("" (assert) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (ln_estimate_scaf4 0 (ln_estimate_scaf4-1 nil 3309546853 ("" (skosimp) (("" (name "SS" "sigma(0, n!1, LAMBDA (i: nat): x!1 ^ i)") (("" (replace -1) (("" (lemma "add_div" ("x" "SS" "n0x" "1" "y" "x!1^(n!1+1)" "n0y" "1-x!1")) (("1" (replace -1 2) (("1" (lemma "both_sides_div1" ("x" "1" "y" "SS * (1 - x!1) + x!1 ^ (n!1 + 1)" "n0z" "1-x!1")) (("1" (replace -1 2) (("1" (hide -1 -2) (("1" (case "forall (n:nat): 1 = sigma(0, n, LAMBDA (i: nat): x!1 ^ i) *(1-x!1) + x!1 ^ (n+1)") (("1" (inst - "n!1") (("1" (assert) nil nil)) nil) ("2" (hide-all-but (1 2)) (("2" (induct "n") (("1" (expand "sigma") (("1" (assert) (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (name-replace "DRL101" "sigma(0, j!1, LAMBDA (i: nat): x!1 ^ i)") (("2" (case-replace "(x!1 ^ (1 + j!1)) * x!1 = x!1 ^ (2 + j!1)") (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (expand "^") (("2" (expand "expt" 1 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (add_div formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (both_sides_div1 formula-decl nil real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (expt def-decl "real" exponentiation nil) (sigma_0_neg formula-decl nil sigma_nat "reals/") (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals 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) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (ln_estimate_scaf5_TCC1 0 (ln_estimate_scaf5_TCC1-1 nil 3309550054 ("" (skosimp) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (ln_estimate_scaf5_TCC2 0 (ln_estimate_scaf5_TCC2-1 nil 3309550054 ("" (skosimp) (("" (assert) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (ln_estimate_scaf5 0 (ln_estimate_scaf5-1 nil 3309548279 ("" (skosimp) (("" (lemma "ln_estimate_scaf4" ("x" "1-nzx!1" "n" "n!1")) (("" (assert) nil nil)) nil)) nil) ((nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (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) (ln_estimate_scaf4 formula-decl nil ln_exp_series_alt nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals 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) (real_div_nzreal_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (ln_estimate_scaf6 0 (ln_estimate_scaf6-2 nil 3352449131 ("" (induct "n") (("1" (expand "ln_estimate") (("1" (expand "sigma") (("1" (assert) (("1" (lemma "const_derivable_fun[posreal]" ("b" "0")) (("1" (expand "const_fun") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "ln_estimate") (("2" (expand "sigma" 1) (("2" (name "F" "(LAMBDA px: sigma(0, j!1, LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-(px - 1)) ^ nn / nn ENDIF))") (("1" (lemma "extensionality" ("f" "(LAMBDA px: sigma(0, j!1, LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-(px - 1)) ^ nn / nn ENDIF) + -(-(px - 1)) ^ (1 + j!1) / (1 + j!1))" "g" "F-(LAMBDA px: (1-px)^(1+j!1)/(1+j!1))")) (("1" (split -1) (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (lemma "identity_derivable_fun[posreal]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[posreal]" ("b" "1")) (("1" (lemma "diff_derivable_fun[posreal]" ("f1" "LAMBDA (x: posreal): 1" "f2" "LAMBDA (x: posreal): x")) (("1" (expand "const_fun") (("1" (assert) (("1" (expand "-" -1) (("1" (lemma "deriv_exp_fun[posreal]" ("f" "LAMBDA (x:posreal): 1-x" "n" "1+j!1")) (("1" (assert) (("1" (flatten) (("1" (hide -2) (("1" (expand "^" -1) (("1" (lemma "scal_derivable_fun[posreal]" ("b" "1/(1+j!1)" "f" "LAMBDA (t: posreal): (1 - t) ^ (1 + j!1)")) (("1" (assert) (("1" (lemma "extensionality" ("f" "1 / (1 + j!1) * (LAMBDA (t: posreal): (1 - t) ^ (1 + j!1))" "g" "(LAMBDA px: (1 - px) ^ (1 + j!1) / (1 + j!1))")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "diff_derivable_fun[posreal]" ("f1" "F" "f2" "(LAMBDA px: (1 - px) ^ (1 + j!1) / (1 + j!1))")) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "*") (("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) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "F") (("2" (expand "-") (("2" (case-replace "-(x!1 - 1) = 1-x!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (extensionality formula-decl nil functions nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (F skolem-const-decl "[posreal -> real]" ln_exp_series_alt nil) (I const-decl "(bijective?[T, T])" identity nil) (diff_derivable_fun formula-decl nil derivatives "analysis/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (scal_derivable_fun formula-decl nil derivatives "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (^ const-decl "[T -> real]" real_fun_ops "reals/") (deriv_exp_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (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) (^ const-decl "real" exponentiation nil) (sigma_0_neg formula-decl nil sigma_nat "reals/") (const_derivable_fun formula-decl nil derivatives "analysis/") (sigma def-decl "real" sigma "reals/") (nat_induction formula-decl nil naturalnumbers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (ln_estimate const-decl "real" ln_exp_series_alt nil) (derivable? const-decl "bool" derivatives "analysis/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil) (ln_estimate_scaf6-1 nil 3309551069 ("" (induct "n") (("1" (expand "ln_estimate") (("1" (expand "sigma") (("1" (lemma "const_derivable_fun[posreal]" ("b" "0")) (("1" (expand "const_fun") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "ln_estimate") (("2" (expand "sigma" 1) (("2" (name "F" "(LAMBDA px: sigma(0, j!1, LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-(px - 1)) ^ nn / nn ENDIF))") (("1" (lemma "extensionality" ("f" "(LAMBDA px: sigma(0, j!1, LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-(px - 1)) ^ nn / nn ENDIF) + -(-(px - 1)) ^ (1 + j!1) / (1 + j!1))" "g" "F-(LAMBDA px: (1-px)^(1+j!1)/(1+j!1))")) (("1" (split -1) (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (lemma "identity_derivable_fun[posreal]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[posreal]" ("b" "1")) (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: posreal): 1" "f2" "LAMBDA (x: posreal): x")) (("1" (expand "const_fun") (("1" (assert) (("1" (expand "-" -1) (("1" (lemma "deriv_exp_fun" ("f" "LAMBDA (x:posreal): 1-x" "n" "1+j!1")) (("1" (assert) (("1" (flatten) (("1" (hide -2) (("1" (expand "^" -1) (("1" (lemma "scal_derivable_fun" ("b" "1/(1+j!1)" "f" "LAMBDA (t: posreal): (1 - t) ^ (1 + j!1)")) (("1" (assert) (("1" (lemma "extensionality" ("f" "1 / (1 + j!1) * (LAMBDA (t: posreal): (1 - t) ^ (1 + j!1))" "g" "(LAMBDA px: (1 - px) ^ (1 + j!1) / (1 + j!1))")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "diff_derivable_fun" ("f1" "F" "f2" "(LAMBDA px: (1 - px) ^ (1 + j!1) / (1 + j!1))")) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "*") (("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) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "F") (("2" (expand "-") (("2" (case-replace "-(x!1 - 1) = 1-x!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil) ((diff_derivable_fun formula-decl nil derivatives "analysis/") (deriv_exp_fun formula-decl nil derivatives "analysis/") (scal_derivable_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (const_derivable_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (sigma def-decl "real" sigma "reals/")) shostak)) (ln_estimate_scaf7_TCC1 0 (ln_estimate_scaf7_TCC1-1 nil 3309557879 ("" (lemma "ln_estimate_scaf6") (("" (skosimp) (("" (inst - "n!1+1") nil nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (ln_estimate_scaf6 formula-decl nil ln_exp_series_alt nil)) shostak)) (ln_estimate_scaf7 0 (ln_estimate_scaf7-2 nil 3352449229 ("" (induct "n") (("1" (expand "ln_estimate") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "deriv_id_fun[posreal]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[posreal]" ("b" "1")) (("1" (lemma "deriv_const_fun[posreal]" ("b" "1")) (("1" (expand "const_fun") (("1" (lemma "diff_derivable_fun[posreal]" ("f1" "LAMBDA (x: posreal): x" "f2" "LAMBDA (x: posreal): 1")) (("1" (assert) (("1" (lemma "deriv_diff_fun[posreal]" ("ff1" "LAMBDA (x: posreal): x" "ff2" "LAMBDA (x: posreal): 1")) (("1" (replace -3) (("1" (replace -5) (("1" (expand "-") (("1" (lemma "extensionality" ("f" "LAMBDA px: -(-(px - 1)) ^ 1 / 1" "g" "lambda px: px-1")) (("1" (split -1) (("1" (replace -1) (("1" (replace -2) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "^" 1) (("1" (expand "expt" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "^") (("2" (expand "expt") (("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) ("2" (skosimp*) (("2" (expand "ln_estimate") (("2" (expand "sigma" 1) (("2" (name "F" "(LAMBDA px: -sigma(0, 1 + j!1, LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-(1 - px)) ^ nn / nn ENDIF))") (("1" (lemma "extensionality" ("f" "F+ (lambda px: (px-1) ^ (2 + j!1) / (2 + j!1))" "g" "(LAMBDA px: -(sigma(0, 1 + j!1, LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-(1 - px)) ^ nn / nn ENDIF) + -(-(1 - px)) ^ (2 + j!1) / (2 + j!1)))")) (("1" (split -1) (("1" (hide -1 -2) (("1" (name "FF" "(LAMBDA px: sigma(0, 1 + j!1, LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-(px - 1)) ^ nn / nn ENDIF))") (("1" (replace -1) (("1" (lemma "extensionality" ("f" "(LAMBDA px: sigma(0, 1 + j!1, LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-(px - 1)) ^ nn / nn ENDIF) + -(-(px - 1)) ^ (2 + j!1) / (2 + j!1))" "g" "FF-(lambda px: (1-px)^(2+j!1)/(2+j!1))")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "ln_estimate_scaf6" ("n" "1+j!1")) (("1" (expand "ln_estimate") (("1" (replace -3) (("1" (hide -2 -3) (("1" (name "GG" "(LAMBDA px: sigma(0, j!1, (LAMBDA (i: nat): (1 - px) ^ i)))") (("1" (lemma "extensionality" ("f" "(LAMBDA px: (1 - px) ^ (1 + j!1) + sigma(0, j!1, (LAMBDA (i: nat): (1 - px) ^ i)))" "g" "GG+(LAMBDA px: (1 - px) ^ (1 + j!1))")) (("1" (split -1) (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "deriv_id_fun[posreal]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[posreal]" ("b" "1")) (("1" (lemma "deriv_const_fun[posreal]" ("b" "1")) (("1" (expand "const_fun") (("1" (lemma "diff_derivable_fun[posreal]" ("f1" "LAMBDA (x: posreal): 1" "f2" "LAMBDA (x: posreal): x")) (("1" (assert) (("1" (lemma "deriv_diff_fun[posreal]" ("ff1" "LAMBDA (x: posreal): 1" "ff2" "LAMBDA (x: posreal): x")) (("1" (replace -3) (("1" (replace -5) (("1" (expand "-") (("1" (lemma "deriv_exp_fun[posreal]" ("f" "LAMBDA (x:posreal): 1-x" "n" "2+j!1")) (("1" (assert) (("1" (flatten) (("1" (expand "^" (-1 -2)) (("1" (replace -3) (("1" (lemma "scal_derivable_fun[posreal]" ("b" "1/(2+j!1)" "f" "LAMBDA (t: posreal): (1 - t) ^ (2 + j!1)")) (("1" (assert) (("1" (lemma "deriv_scal_fun[posreal]" ("b" "1/(2+j!1)" "ff" "LAMBDA (t: posreal): (1 - t) ^ (2 + j!1)")) (("1" (replace -4) (("1" (lemma "extensionality" ("f" "1 / (2 + j!1) * (((2 + j!1) * (LAMBDA (t: posreal): (1 - t) ^ (1 + j!1))) * (LAMBDA (x_1: posreal): -1))" "g" "LAMBDA (t: posreal): - ((1 - t) ^ (1 + j!1))")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "extensionality" ("f" "(1 / (2 + j!1) * (LAMBDA (t: posreal): (1 - t) ^ (2 + j!1)))" "g" "(LAMBDA (t: posreal): (1 - t) ^ (2 + j!1)/(2+j!1))")) (("1" (split -1) (("1" (replace -1) (("1" (hide -1 -2 -5 -6 -7 -8 -9 -10 -11 -12) (("1" (lemma "diff_derivable_fun[posreal]" ("f1" "FF" "f2" "(LAMBDA (t: posreal): (1 - t) ^ (2 + j!1) / (2 + j!1))")) (("1" (assert) (("1" (lemma "deriv_diff_fun[posreal]" ("ff1" "FF" "ff2" "(LAMBDA (t: posreal): (1 - t) ^ (2 + j!1) / (2 + j!1))")) (("1" (replace -6) (("1" (replace -3) (("1" (expand "-" -1) (("1" (replace -1) (("1" (hide-all-but 1) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "+") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (expand "*") (("2" (assert) (("2" (name-replace "DRL106" "(1 - x!1) ^ (1 + j!1)") (("2" (assert) (("2" (lemma "div_cancel3") (("2" (inst - "2+j!1" "(-2-j!1)*DRL106" "-DRL106") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "GG") (("2" (expand "+") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "FF") (("2" (expand "-") (("2" (lemma "both_sides_div1") (("2" (inst - "2+j!1" "-(-(x!1 - 1)) ^ (2 + j!1)" "-1 * ((1 - x!1) ^ (2 + j!1))") (("2" (replace -1 1) (("2" (hide -1) (("2" (case-replace "-(x!1 - 1) = 1-x!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "F") (("2" (expand "+") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (lemma "ln_estimate_scaf6" ("n" "1+n!2")) (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (F skolem-const-decl "[posreal -> real]" ln_exp_series_alt nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (ln_estimate_scaf6 formula-decl nil ln_exp_series_alt nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (^ const-decl "[T -> real]" real_fun_ops "reals/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (scal_derivable_fun formula-decl nil derivatives "analysis/") (deriv_scal_fun formula-decl nil derivatives "analysis/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (div_cancel3 formula-decl nil real_props nil) (minus_even_is_even application-judgement "even_int" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (deriv_exp_fun formula-decl nil derivatives "analysis/") (GG skolem-const-decl "[posreal -> real]" ln_exp_series_alt nil) (both_sides_div1 formula-decl nil real_props nil) (FF skolem-const-decl "[posreal -> real]" ln_exp_series_alt nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (deriv_id_fun formula-decl nil derivatives "analysis/") (const_derivable_fun formula-decl nil derivatives "analysis/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (extensionality formula-decl nil functions 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) (real_div_nzreal_is_real application-judgement "real" reals nil) (expt def-decl "real" exponentiation nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (sigma_0_neg formula-decl nil sigma_nat "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (deriv_const_fun formula-decl nil derivatives "analysis/") (I const-decl "(bijective?[T, T])" identity nil) (identity_derivable_fun formula-decl nil derivatives "analysis/") (minus_real_is_real application-judgement "real" reals nil) (nat_induction formula-decl nil naturalnumbers nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal 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 "[T -> real]" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (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? const-decl "bool" derivatives "analysis/") (ln_estimate const-decl "real" ln_exp_series_alt nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil) (ln_estimate_scaf7-1 nil 3309557976 ("" (induct "n") (("1" (expand "ln_estimate") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "deriv_id_fun[posreal]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[posreal]" ("b" "1")) (("1" (lemma "deriv_const_fun[posreal]" ("b" "1")) (("1" (expand "const_fun") (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: posreal): x" "f2" "LAMBDA (x: posreal): 1")) (("1" (assert) (("1" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x: posreal): x" "ff2" "LAMBDA (x: posreal): 1")) (("1" (replace -3) (("1" (replace -5) (("1" (expand "-") (("1" (lemma "extensionality" ("f" "LAMBDA px: -(-(px - 1)) ^ 1 / 1" "g" "lambda px: px-1")) (("1" (split -1) (("1" (replace -1) (("1" (replace -2) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "^" 1) (("1" (expand "expt" 1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "^") (("2" (expand "expt") (("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) ("2" (skosimp*) (("2" (expand "ln_estimate") (("2" (expand "sigma" 1) (("2" (name "F" "(LAMBDA px: -sigma(0, 1 + j!1, LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-(1 - px)) ^ nn / nn ENDIF))") (("1" (lemma "extensionality" ("f" "F+ (lambda px: (px-1) ^ (2 + j!1) / (2 + j!1))" "g" "(LAMBDA px: -(sigma(0, 1 + j!1, LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-(1 - px)) ^ nn / nn ENDIF) + -(-(1 - px)) ^ (2 + j!1) / (2 + j!1)))")) (("1" (split -1) (("1" (hide -1 -2) (("1" (name "FF" "(LAMBDA px: sigma(0, 1 + j!1, LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-(px - 1)) ^ nn / nn ENDIF))") (("1" (replace -1) (("1" (lemma "extensionality" ("f" "(LAMBDA px: sigma(0, 1 + j!1, LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-(px - 1)) ^ nn / nn ENDIF) + -(-(px - 1)) ^ (2 + j!1) / (2 + j!1))" "g" "FF-(lambda px: (1-px)^(2+j!1)/(2+j!1))")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "ln_estimate_scaf6" ("n" "1+j!1")) (("1" (expand "ln_estimate") (("1" (replace -3) (("1" (hide -2 -3) (("1" (name "GG" "(LAMBDA px: sigma(0, j!1, (LAMBDA (i: nat): (1 - px) ^ i)))") (("1" (lemma "extensionality" ("f" "(LAMBDA px: (1 - px) ^ (1 + j!1) + sigma(0, j!1, (LAMBDA (i: nat): (1 - px) ^ i)))" "g" "GG+(LAMBDA px: (1 - px) ^ (1 + j!1))")) (("1" (split -1) (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "deriv_id_fun[posreal]") (("1" (expand "I") (("1" (lemma "const_derivable_fun[posreal]" ("b" "1")) (("1" (lemma "deriv_const_fun[posreal]" ("b" "1")) (("1" (expand "const_fun") (("1" (lemma "diff_derivable_fun" ("f1" "LAMBDA (x: posreal): 1" "f2" "LAMBDA (x: posreal): x")) (("1" (assert) (("1" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x: posreal): 1" "ff2" "LAMBDA (x: posreal): x")) (("1" (replace -3) (("1" (replace -5) (("1" (expand "-") (("1" (lemma "deriv_exp_fun" ("f" "LAMBDA (x:posreal): 1-x" "n" "2+j!1")) (("1" (assert) (("1" (flatten) (("1" (expand "^" (-1 -2)) (("1" (replace -3) (("1" (lemma "scal_derivable_fun" ("b" "1/(2+j!1)" "f" "LAMBDA (t: posreal): (1 - t) ^ (2 + j!1)")) (("1" (assert) (("1" (lemma "deriv_scal_fun" ("b" "1/(2+j!1)" "ff" "LAMBDA (t: posreal): (1 - t) ^ (2 + j!1)")) (("1" (replace -4) (("1" (lemma "extensionality" ("f" "1 / (2 + j!1) * (((2 + j!1) * (LAMBDA (t: posreal): (1 - t) ^ (1 + j!1))) * (LAMBDA (x_1: posreal): -1))" "g" "LAMBDA (t: posreal): - ((1 - t) ^ (1 + j!1))")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "extensionality" ("f" "(1 / (2 + j!1) * (LAMBDA (t: posreal): (1 - t) ^ (2 + j!1)))" "g" "(LAMBDA (t: posreal): (1 - t) ^ (2 + j!1)/(2+j!1))")) (("1" (split -1) (("1" (replace -1) (("1" (hide -1 -2 -5 -6 -7 -8 -9 -10 -11 -12) (("1" (lemma "diff_derivable_fun" ("f1" "FF" "f2" "(LAMBDA (t: posreal): (1 - t) ^ (2 + j!1) / (2 + j!1))")) (("1" (assert) (("1" (lemma "deriv_diff_fun" ("ff1" "FF" "ff2" "(LAMBDA (t: posreal): (1 - t) ^ (2 + j!1) / (2 + j!1))")) (("1" (replace -6) (("1" (replace -3) (("1" (expand "-" -1) (("1" (replace -1) (("1" (hide-all-but 1) (("1" (apply-extensionality 1 :hide? t) (("1" (expand "+") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (expand "*") (("2" (assert) (("2" (name-replace "DRL106" "(1 - x!1) ^ (1 + j!1)") (("2" (assert) (("2" (lemma "div_cancel3") (("2" (inst - "2+j!1" "(-2-j!1)*DRL106" "-DRL106") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "GG") (("2" (expand "+") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "FF") (("2" (expand "-") (("2" (lemma "both_sides_div1") (("2" (inst - "2+j!1" "-(-(x!1 - 1)) ^ (2 + j!1)" "-1 * ((1 - x!1) ^ (2 + j!1))") (("2" (replace -1 1) (("2" (hide -1) (("2" (case-replace "-(x!1 - 1) = 1-x!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "F") (("2" (expand "+") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (lemma "ln_estimate_scaf6" ("n" "1+n!2")) (("3" (propax) nil nil)) nil)) nil)) nil)) nil) ((+ const-decl "[T -> real]" real_fun_ops "reals/") (deriv_exp_fun formula-decl nil derivatives "analysis/") (deriv_scal_fun formula-decl nil derivatives "analysis/") (scal_derivable_fun formula-decl nil derivatives "analysis/") (deriv_id_fun formula-decl nil derivatives "analysis/") (const_derivable_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (deriv_const_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (sigma def-decl "real" sigma "reals/") (deriv const-decl "[T -> real]" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/")) shostak)) (ln_estimate_scaf8_TCC1 0 (ln_estimate_scaf8_TCC1-1 nil 3309557879 ("" (skosimp) (("" (assert) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (ln_estimate_scaf8_TCC2 0 (ln_estimate_scaf8_TCC2-1 nil 3309557879 ("" (skosimp) (("" (lemma "ln_estimate_scaf2" ("x" "px!1" "n" "n!1+1")) (("" (propax) 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 "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (ln_estimate_scaf2 formula-decl nil ln_exp_series_alt nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil)) shostak)) (ln_estimate_scaf8 0 (ln_estimate_scaf8-2 nil 3352449313 ("" (skolem 1 ("n" "_")) (("" (lemma "extensionality_postulate" ("f" "ln" "g" "lambda px: ln_estimate(px - 1, n + 1) + (-1) ^ (n + 1) * Integral(1, px, LAMBDA (t: posreal): (1 - t) ^ (n + 1) / t)")) (("1" (hide -1) (("1" (rewrite "extensionality_postulate") (("1" (name "L" "LAMBDA (px: posreal): ln_estimate(px - 1, 1 + n)") (("1" (name "II" "LAMBDA (px: posreal): Integral(1, px, LAMBDA (t: posreal): ((1 - t) ^ (1 + n)) / t)") (("1" (lemma "extensionality" ("f" "(LAMBDA (px: posreal): ln_estimate(px - 1, 1 + n) + Integral(1, px, LAMBDA (t: posreal): ((1 - t) ^ (1 + n)) / t))" "g" "L+II")) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "derivs_eq[posreal]" ("F" "ln" "G" "L+II")) (("1" (lemma "ln_derivable") (("1" (flatten) (("1" (lemma "ln_estimate_scaf6" ("n" "1+n")) (("1" (lemma "ln_estimate_scaf7" ("n" "n")) (("1" (replace -7) (("1" (hide -7) (("1" (lemma "fundamental[posreal]" ("f" "LAMBDA (t: posreal): ((1 - t) ^ (1 + n)) / t" "F" "II" "a" "1")) (("1" (lemma "ln_estimate_scaf1" ("n" "1+n")) (("1" (replace -1) (("1" (expand "II" -2 1) (("1" (flatten) (("1" (hide -1) (("1" (lemma "sum_derivable_fun[posreal]" ("f1" "L" "f2" "II")) (("1" (assert) (("1" (lemma "deriv_sum_fun[posreal]" ("ff1" "L" "ff2" "II")) (("1" (replace -4) (("1" (replace -5) (("1" (split -9) (("1" (expand "const_fun") (("1" (skosimp) (("1" (case-replace "c!1=0") (("1" (replace -2 1) (("1" (apply-extensionality 1 :hide? t) (("1" (hide-all-but 1) (("1" (expand "+") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (rewrite "extensionality_postulate" -1 :dir rl) (("2" (inst - "1") (("2" (rewrite "ln_1") (("2" (expand "+") (("2" (expand "II") (("2" (lemma "Integral_a_to_a[posreal]" ("a" "1" "f" "LAMBDA (t: posreal): ((1 - t) ^ (1 + n)) / t")) (("2" (replace -1) (("2" (hide -1) (("2" (expand "L") (("2" (case "forall (n:nat): ln_estimate(0, n) = 0") (("1" (inst - "1+n") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (expand "ln_estimate") (("2" (induct "n") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (replace -1) (("2" (hide -1) (("2" (expand "^") (("2" (expand "expt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (replace -8) (("2" (hide-all-but 1) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "+") (("2" (lemma "ln_estimate_scaf5" ("nzx" "x!1" "n" "n")) (("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-all-but 1) (("2" (assert) (("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (assert) (("3" (expand "connected?") (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "II") (("2" (expand "L") (("2" (expand "+") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "ln_estimate_scaf2" ("n" "1+n")) (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (lemma "ln_estimate_scaf2" ("n" "1+n")) (("2" (propax) nil nil)) nil)) nil)) 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) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (Integral const-decl "real" integral_def "analysis/") (Integrable_funs type-eq-decl nil integral_def "analysis/") (Integrable? const-decl "bool" integral_def "analysis/") (- const-decl "[numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (ln_estimate const-decl "real" ln_exp_series_alt nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (ln const-decl "real" ln_exp nil) (extensionality_postulate formula-decl nil functions nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (ln_derivable formula-decl nil ln_exp nil) (ln_estimate_scaf6 formula-decl nil ln_exp_series_alt nil) (int_minus_int_is_int application-judgement "int" integers nil) (fundamental formula-decl nil fundamental_theorem "analysis/") (sum_derivable_fun formula-decl nil derivatives "analysis/") (deriv_sum_fun formula-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal nonempty-type-eq-decl nil reals nil) (ln_estimate_scaf5 formula-decl nil ln_exp_series_alt nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (ln_1 formula-decl nil ln_exp nil) (L skolem-const-decl "[posreal -> real]" ln_exp_series_alt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (minus_even_is_even application-judgement "even_int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def 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) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (int_exp application-judgement "int" exponentiation nil) (minus_int_is_int application-judgement "int" integers nil) (expt def-decl "real" exponentiation 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) (int_expt application-judgement "int" exponentiation nil) (Integral_a_to_a formula-decl nil integral "analysis/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (II skolem-const-decl "[posreal -> real]" ln_exp_series_alt nil) (ln_estimate_scaf1 formula-decl nil ln_exp_series_alt nil) (ln_estimate_scaf7 formula-decl nil ln_exp_series_alt nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (derivs_eq formula-decl nil indefinite_integral "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (extensionality formula-decl nil functions nil) (= const-decl "[T, T -> boolean]" equalities nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (ln_estimate_scaf2 formula-decl nil ln_exp_series_alt nil)) nil) (ln_estimate_scaf8-1 nil 3309589315 ("" (skolem 1 ("n" "_")) (("" (lemma "extensionality_postulate" ("f" "ln" "g" "lambda px: ln_estimate(px - 1, n + 1) + (-1) ^ (n + 1) * Integral(1, px, LAMBDA (t: posreal): (1 - t) ^ (n + 1) / t)")) (("1" (hide -1) (("1" (rewrite "extensionality_postulate") (("1" (name "L" "LAMBDA (px: posreal): ln_estimate(px - 1, 1 + n)") (("1" (name "II" "LAMBDA (px: posreal): Integral(1, px, LAMBDA (t: posreal): ((1 - t) ^ (1 + n)) / t)") (("1" (lemma "extensionality" ("f" "(LAMBDA (px: posreal): ln_estimate(px - 1, 1 + n) + Integral(1, px, LAMBDA (t: posreal): ((1 - t) ^ (1 + n)) / t))" "g" "L+II")) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "derivs_eq" ("F" "ln" "G" "L+II")) (("1" (lemma "ln_derivable") (("1" (flatten) (("1" (lemma "ln_estimate_scaf6" ("n" "1+n")) (("1" (lemma "ln_estimate_scaf7" ("n" "n")) (("1" (replace -7) (("1" (hide -7) (("1" (lemma "fundamental[posreal]" ("f" "LAMBDA (t: posreal): ((1 - t) ^ (1 + n)) / t" "F" "II" "a" "1")) (("1" (lemma "ln_estimate_scaf1" ("n" "1+n")) (("1" (replace -1) (("1" (expand "II" -2 1) (("1" (flatten) (("1" (hide -1) (("1" (lemma "sum_derivable_fun" ("f1" "L" "f2" "II")) (("1" (assert) (("1" (lemma "deriv_sum_fun" ("ff1" "L" "ff2" "II")) (("1" (replace -4) (("1" (replace -5) (("1" (split -9) (("1" (expand "const_fun") (("1" (skosimp) (("1" (case-replace "c!1=0") (("1" (replace -2 1) (("1" (apply-extensionality 1 :hide? t) (("1" (hide-all-but 1) (("1" (expand "+") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (rewrite "extensionality_postulate" -1 :dir rl) (("2" (inst - "1") (("2" (rewrite "ln_1") (("2" (expand "+") (("2" (expand "II") (("2" (lemma "Integral_a_to_a" ("a" "1" "f" "LAMBDA (t: posreal): ((1 - t) ^ (1 + n)) / t")) (("2" (replace -1) (("2" (hide -1) (("2" (expand "L") (("2" (case "forall (n:nat): ln_estimate(0, n) = 0") (("1" (inst - "1+n") (("1" (assert) nil nil)) nil) ("2" (hide-all-but 1) (("2" (expand "ln_estimate") (("2" (induct "n") (("1" (expand "sigma") (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (replace -1) (("2" (hide -1) (("2" (expand "^") (("2" (expand "expt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (replace -8) (("2" (hide-all-but 1) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "+") (("2" (lemma "ln_estimate_scaf5" ("nzx" "x!1" "n" "n")) (("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" (skosimp) (("2" (inst + "x!1*2") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "II") (("2" (expand "L") (("2" (expand "+") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "ln_estimate_scaf2" ("n" "1+n")) (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (lemma "ln_estimate_scaf2" ("n" "1+n")) (("2" (propax) nil nil)) nil)) nil)) nil) ((Integral const-decl "real" integral_def "analysis/") (Integrable_funs type-eq-decl nil integral_def "analysis/") (Integrable? const-decl "bool" integral_def "analysis/") (ln const-decl "real" ln_exp nil) (ln_derivable formula-decl nil ln_exp nil) (fundamental formula-decl nil fundamental_theorem "analysis/") (sum_derivable_fun formula-decl nil derivatives "analysis/") (deriv_sum_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (ln_1 formula-decl nil ln_exp nil) (sigma def-decl "real" sigma "reals/") (Integral_a_to_a formula-decl nil integral "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/")) shostak)) (ln_estimate_scaf9_TCC1 0 (ln_estimate_scaf9_TCC1-1 nil 3309627736 ("" (lemma "ln_estimate_scaf2") (("" (propax) nil nil)) nil) ((ln_estimate_scaf2 formula-decl nil ln_exp_series_alt nil)) shostak)) (ln_estimate_scaf9 0 (ln_estimate_scaf9-1 nil 3309629369 ("" (skosimp) (("" (case-replace "n!1=0") (("1" (expand "ln_estimate") (("1" (expand "sigma") (("1" (expand "ln") (("1" (lemma "extensionality" ("f" "LAMBDA (t: posreal): (1 - t) ^ 0 / t" "g" "LAMBDA (t: posreal): 1 / t")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (skosimp) (("2" (expand "^") (("2" (expand "expt") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "ln_estimate_scaf8" ("px" "px!1" "n" "n!1-1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (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) (sigma def-decl "real" sigma "reals/") (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 "[numfield, numfield -> numfield]" number_fields 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) (extensionality formula-decl nil functions nil) (real_minus_real_is_real application-judgement "real" reals nil) (expt def-decl "real" exponentiation nil) (sigma_0_neg formula-decl nil sigma_nat "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (ln const-decl "real" ln_exp nil) (ln_estimate const-decl "real" ln_exp_series_alt nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (ln_estimate_scaf8 formula-decl nil ln_exp_series_alt nil)) shostak)) (ln_estimate_scaf10_TCC1 0 (ln_estimate_scaf10_TCC1-1 nil 3309628050 ("" (skosimp) (("" (assert) nil nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (ln_estimate_scaf10 0 (ln_estimate_scaf10-6 nil 3445353682 ("" (stop-rewrite "abs_nat") (("" (case "forall (n:nat): continuous?[posreal](LAMBDA (t: posreal): (1 - t) ^ n)") (("1" (skosimp) (("1" (inst - "n!1") (("1" (lemma "continuous_Integrable?[posreal]" ("a" "1" "b" "px!1" "f" "LAMBDA (t: posreal): (1 - t) ^ n!1")) (("1" (split -1) (("1" (lemma "const_derivable_fun[posreal]" ("b" "1")) (("1" (lemma "deriv_const_fun[posreal]" ("b" "1")) (("1" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "deriv_id_fun[posreal]") (("1" (expand "I") (("1" (lemma "diff_derivable_fun[posreal]" ("f1" "LAMBDA (x: posreal): 1" "f2" "LAMBDA (x: posreal): x")) (("1" (assert) (("1" (lemma "deriv_diff_fun[posreal]" ("ff1" "LAMBDA (x: posreal): 1" "ff2" "LAMBDA (x: posreal): x")) (("1" (replace -3) (("1" (replace -5) (("1" (expand "-") (("1" (lemma "deriv_exp_fun[posreal]" ("n" "1+n!1" "f" "LAMBDA (x_1: posreal): 1 - x_1")) (("1" (assert) (("1" (expand "^" -1) (("1" (flatten) (("1" (replace -3) (("1" (hide -3 -4 -5 -6 -7 -8) (("1" (lemma "scal_derivable_fun[posreal]" ("b" "-1/(1+n!1)" "f" "LAMBDA (t: posreal): (1 - t) ^ (1 + n!1)")) (("1" (assert) (("1" (lemma "deriv_scal_fun[posreal]" ("b" "-1/(1+n!1)" "ff" "LAMBDA (t: posreal): (1 - t) ^ (1 + n!1)")) (("1" (expand "*") (("1" (replace -4 -1) (("1" (assert) (("1" (lemma "extensionality" ("f" "(LAMBDA (x: posreal): -1 * ((1 - x) ^ n!1 * (-1 / (1 + n!1))) - (1 - x) ^ n!1 * (-1 / (1 + n!1)) * n!1)" "g" "LAMBDA (t: posreal): (1 - t) ^ n!1")) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "fundamental3[posreal]" ("f" "LAMBDA (t: posreal): (1 - t) ^ n!1" "F" "LAMBDA (x: posreal): -1 / (1 + n!1) * (1 - x) ^ (1 + n!1)" "a" "1" "b" "px!1")) (("1" (replace -2 -1) (("1" (replace -3 -1) (("1" (replace -7 -1) (("1" (simplify -1) (("1" (expand "^" -1 3) (("1" (expand "expt" -1) (("1" (case "abs(Integral(1, px!1, LAMBDA (t: posreal): (1 - t) ^ n!1 / t)) <= abs(Integral(1, px!1, LAMBDA ( (("1" (replace -2 -1) (("1" (name-replace "DRL100" "abs(Integral(1, px!1, LAMBDA (t: posreal): (1 - t) ^ n!1 / t))") (("1" (hide-all-but (-1 -9 -10 1)) (("1" (rewrite "abs_mult" -1) (("1" (rewrite "abs_div" -1) (("1" (expand "abs" -1 1) (("1" (expand "abs" -1 1) (("1" (expand "<=" -2) (("1" (split -2) (("1" (rewrite "abs_expt" -2 :dir rl) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (expand "^") (("2" (expand "expt") (("2" (rewrite "zero_times1") (("2" (expand "abs") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -2 -3 -4 -5) (("2" (hide -1) (("2" (expand "<=" -3) (("2" (split -3) (("1" (lemma "ln_estimate_scaf2" ("x" "px!1" "n" "n!1")) (("1" (name-replace "F" "LAMBDA (t: posreal): (1 - t) ^ n!1 / t") (("1" (name-replace "G" "LAMBDA (t: posreal): (1 - t) ^ n!1") (("1" (case "even?(n!1)") (("1" (lemma "Integral_ge_0_open[posreal]" ("a" "1" "b" "px!1" "f" "F")) (("1" (lemma "Integral_ge_0_open[posreal]" ("a" "1" "b" "px!1" "f" "G")) (("1" (assert) (("1" (split -1) (("1" (split -2) (("1" (expand "abs") (("1" (assert) (("1" (lemma "Integral_diff[posreal]" ("a" "1" "b" "px!1" "f" "G" "g" "F")) (("1" (assert) (("1" (flatten) (("1" (lemma "Integral_ge_0_open[posreal]" ("a" "1" "b" "px!1" "f" "LAMBDA (x: posreal): G(x) - F(x)")) (("1" (assert) (("1" (hide-all-but (1 -7 -5 -10)) (("1" (expand "even?") (("1" (skosimp*) (("1" (expand "F") (("1" (expand "G") (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "(1 - x!1) ^ n!1" "py" "1-1/x!1")) (("1" (assert) nil nil) ("2" (assert) (("2" (hide 2) (("2" (typepred "x!1") (("2" (lemma "div_mult_pos_lt1" ("py" "x!1" "x" "1" "z" "1")) (("2" (assert) (("2" (flatten) (("2" (typepred "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (replace -1) (("3" (rewrite "expt_times" 1) (("1" (lemma "sq_nz_pos" ("nz" "1-x!1")) (("1" (expand "sq") (("1" (expand "^" 1 1) (("1" (expand "^" 1 2) (("1" (expand "expt") (("1" (expand "expt") (("1" (expand "expt") (("1" (lemma "expt_pos" ("px" "1 - 2 * x!1 + x!1 * x!1" "i" "j!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "x!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "x!1") (("2" (assert) 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" (skosimp) (("2" (expand "F" 1) (("2" (typepred "x!1") (("2" (rewrite "div_mult_pos_ge1" 1) (("2" (expand "even?") (("2" (skosimp) (("2" (replace -5 1) (("2" (rewrite "expt_times" 1) (("2" (lemma "sq_nz_pos" ("nz" "1-x!1")) (("1" (expand "sq") (("1" (expand "^" 1 1) (("1" (expand "expt" 1) (("1" (expand "expt" 1) (("1" (expand "expt" 1) (("1" (lemma "expt_pos" ("px" "1 - 2 * x!1 + x!1 * x!1" "i" "j!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "even?") (("2" (skosimp*) (("2" (expand "G") (("2" (hide -2 -4 -5) (("2" (replace -1) (("2" (rewrite "expt_times" 1) (("1" (lemma "sq_nz_pos" ("nz" "1-x!1")) (("1" (expand "sq") (("1" (expand "^" 1 1) (("1" (expand "expt" 1) (("1" (expand "expt" 1) (("1" (expand "expt" 1) (("1" (lemma "expt_pos" ("px" "1 - 2 * x!1 + x!1 * x!1" "i" "j!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "x!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "even_or_odd") (("2" (case "forall (x:posreal): 1 < x & x <= px!1 => G(x) < 0") (("1" (case "forall (x:posreal): 1 < x & x <= px!1 => F(x) < 0") (("1" (case "forall (x:posreal): 1 < x & x <= px!1 => G(x) < F(x)") (("1" (lemma "Integral_ge_0_open[posreal]" ("a" "1" "b" "px!1" "f" "-F")) (("1" (lemma "Integral_ge_0_open[posreal]" ("a" "1" "b" "px!1" "f" "-G")) (("1" (lemma "Integral_neg[posreal]" ("a" "1" "b" "px!1" "f" "F")) (("1" (lemma "Integral_neg[posreal]" ("a" "1" "b" "px!1" "f" "G")) (("1" (assert) (("1" (flatten) (("1" (assert) (("1" (split -5) (("1" (split -6) (("1" (expand ">=" (-1 -2)) (("1" (expand "<=" (-1 -2)) (("1" (split -1) (("1" (expand "abs" 1) (("1" (assert) (("1" (split -2) (("1" (assert) (("1" (lemma "Integral_diff[posreal]" ("a" "1" "b" "px!1" "f" "-G" "g" "-F")) (("1" (assert) (("1" (flatten) (("1" (lemma "Integral_ge_0_open[posreal]" ("a" "1" "b" "px!1" "f" "LAMBDA (x: posreal): (-G)(x) - (-F)(x)")) (("1" (replace -2) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide 2) (("2" (assert) nil nil)) nil) ("3" (skosimp) (("3" (expand "-" 1) (("3" (inst -9 "x!1") (("3" (assert) (("3" (typepred "x!1") (("3" (assert) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (assert) (("2" (case-replace "Integral(1, px!1, G) = 0") (("1" (lemma "Integral_diff[posreal]" ("a" "1" "b" "px!1" "f" "-G" "g" "-F")) (("1" (assert) (("1" (replace -3 -1 rl) (("1" (flatten) (("1" (lemma "Integral_ge_0_open[posreal]" ("a" "1" "b" "px!1" "f" "LAMBDA (x: posreal): (-G)(x) - (-F)(x)")) (("1" (replace -2) (("1" (split -1) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (skosimp) (("3" (expand "-" 1) (("3" (inst -10 "x!1") (("3" (assert) (("3" (typepred "x!1") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "-" 1) (("2" (inst -7 "x!1") (("2" (assert) (("2" (typepred "x!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "-" 1) (("2" (inst -8 "x!1") (("2" (assert) (("2" (typepred "x!1") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "odd?") (("2" (skosimp*) (("2" (expand "G") (("2" (expand "F") (("2" (rewrite "div_mult_pos_lt2" 1) (("2" (lemma "both_sides_times_neg_lt1" ("nz" "(1 - x!1) ^ n!1" "y" "1" "x" "x!1")) (("1" (assert) nil nil) ("2" (hide-all-but (-1 -2 -7 -10 1 -5)) (("2" (replace -3) (("2" (rewrite "expt_plus" 1) (("2" (rewrite "expt_x1") (("2" (lemma "both_sides_times_pos_lt1" ("pz" "(1 - x!1) ^ (2 * j!1)" "x" "1-x!1" "y" "0")) (("1" (assert) nil nil) ("2" (hide 2) (("2" (rewrite "expt_times") (("2" (lemma "sq_nz_pos" ("nz" "1-x!1")) (("1" (lemma "expt_pos" ("px" "sq(1 - x!1)" "i" "j!1")) (("1" (expand "sq") (("1" (expand "^" 1 1) (("1" (expand "^" 1 2) (("1" (expand "expt") (("1" (expand "expt") (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -3 -5 -6) (("2" (skosimp) (("2" (inst - "x!1") (("2" (assert) (("2" (expand "F") (("2" (expand "G") (("2" (rewrite "div_mult_pos_lt1" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -4 -5 2) (("2" (expand "odd?") (("2" (skosimp*) (("2" (expand "G") (("2" (replace -3) (("2" (rewrite "expt_plus") (("2" (rewrite "expt_x1") (("2" (rewrite "expt_times") (("2" (lemma "sq_nz_pos" ("nz" "1-x!1")) (("1" (expand "sq") (("1" (expand "^" 1 1) (("1" (expand "expt" 1) (("1" (expand "expt" 1) (("1" (expand "expt" 1) (("1" (lemma "expt_pos" ("px" "1 - 2 * x!1 + x!1 * x!1" "i" "j!1")) (("1" (lemma "both_sides_times_pos_lt1" ("pz" "(1 - 2 * x!1 + x!1 * x!1) ^ j!1" "x" "1-x!1" "y" "0")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (lemma "Integral_a_to_a[posreal]" ("a" "1" "f" "LAMBDA (t: posreal): (1 - t) ^ n!1")) (("2" (replace -1) (("2" (lemma "Integral_a_to_a[posreal]" ("a" "1" "f" "LAMBDA (t: posreal): (1 - t) ^ n!1/t")) (("2" (replace -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "ln_estimate_scaf2" ("x" "px!1" "n" "n!1")) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (lemma "div_cancel1" ("x" "(1 - x!1) ^ n!1" "n0z" "-1-n!1")) (("2" (case-replace "-1 / (1 + n!1) = 1/(-1-n!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (expand "continuous?" -1) (("2" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (expand "connected?") (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "const_fun_continuous[posreal]" ("u" "1")) (("2" (lemma "id_fun_continuous[posreal]") (("2" (expand "I") (("2" (expand "const_fun") (("2" (lemma "diff_fun_continuous[posreal]" ("h1" "LAMBDA (x: posreal): 1" "h2" "LAMBDA (x: posreal): x")) (("1" (expand "-") (("1" (induct "n") (("1" (lemma "extensionality" ("f" "LAMBDA (t: posreal): (1 - t) ^ 0" "g" "LAMBDA (x: posreal): 1")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "^") (("2" (expand "expt") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "prod_fun_continuous[posreal]" ("h1" "LAMBDA (x_1: posreal): 1 - x_1" "h2" "LAMBDA (t: posreal): (1 - t) ^ j!1")) (("1" (lemma "extensionality" ("f" "((LAMBDA (x_1: posreal): 1 - x_1) * (LAMBDA (t: posreal): (1 - t) ^ j!1))" "g" "(LAMBDA (t: posreal): (1 - t) ^ (j!1 + 1))")) (("1" (split -1) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "*") (("2" (expand "^") (("2" (expand "expt" 1 3) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (continuous? const-decl "bool" continuous_functions "analysis/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (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_minus_real_is_real application-judgement "real" reals nil) (deriv_const_fun formula-decl nil derivatives "analysis/") (deriv_id_fun formula-decl nil derivatives "analysis/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (deriv_exp_fun formula-decl nil derivatives "analysis/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "[T -> real]" real_fun_ops "reals/") (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (scal_derivable_fun formula-decl nil derivatives "analysis/") (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (deriv_scal_fun formula-decl nil derivatives "analysis/") (extensionality formula-decl nil functions nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (div_cancel1 formula-decl nil real_props nil) (fundamental3 formula-decl nil fundamental_theorem "analysis/") (nat_exp application-judgement "nat" exponentiation nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (expt def-decl "real" exponentiation nil) (even? const-decl "bool" integers nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (Integral_diff formula-decl nil integral "analysis/") (F skolem-const-decl "[posreal -> real]" ln_exp_series_alt nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (Open_interval type-eq-decl nil intervals_real "reals/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (sq_nz_pos judgement-tcc nil sq "reals/") (expt_pos formula-decl nil exponentiation nil) (real_plus_real_is_real application-judgement "real" reals nil) (sq const-decl "nonneg_real" sq "reals/") (expt_times formula-decl nil exponentiation nil) (G skolem-const-decl "[posreal -> real]" ln_exp_series_alt nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (Integral_ge_0_open formula-decl nil integral "analysis/") (minus_even_is_even application-judgement "even_int" integers nil) (Integral_neg formula-decl nil integral "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (both_sides_times_neg_lt1 formula-decl nil real_props nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (expt_x1 formula-decl nil exponentiation nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (expt_plus formula-decl nil exponentiation nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (odd? const-decl "bool" integers nil) (even_or_odd formula-decl nil naturalnumbers nil) (ln_estimate_scaf2 formula-decl nil ln_exp_series_alt nil) (Integral_a_to_a formula-decl nil integral "analysis/") (abs_0 formula-decl nil abs_lems "reals/") (nonzero_real nonempty-type-eq-decl nil reals nil) (abs_div formula-decl nil real_props nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (minus_real_is_real application-judgement "real" reals nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (abs_expt formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (zero_times1 formula-decl nil real_props nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs 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) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (abs_mult formula-decl nil real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (Integral const-decl "real" integral_def "analysis/") (Integrable_funs type-eq-decl nil integral_def "analysis/") (Integrable? const-decl "bool" integral_def "analysis/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (nat_expt application-judgement "nat" exponentiation nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (I const-decl "(bijective?[T, T])" identity nil) (identity_derivable_fun formula-decl nil derivatives "analysis/") (const_derivable_fun formula-decl nil derivatives "analysis/") (Closed_interval type-eq-decl nil intervals_real "reals/") (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/") (const_fun_continuous judgement-tcc nil continuous_functions "analysis/") (diff_fun_continuous judgement-tcc nil continuous_functions "analysis/") (continuous_fun nonempty-type-eq-decl nil continuous_functions "analysis/") (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (prod_fun_continuous judgement-tcc nil continuous_functions "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (id_fun_continuous judgement-tcc nil continuous_functions "analysis/")) nil) (ln_estimate_scaf10-5 nil 3413217110 ("" (stop-rewrite "abs_nat") (("" (case "forall (n:nat): continuous[posreal](LAMBDA (t: posreal): (1 - t) ^ n)") (("1" (skosimp) (("1" (inst - "n!1") (("1" (lemma "continuous_Integrable?[posreal]" ("a" "1" "b" "px!1" "f" "LAMBDA (t: posreal): (1 - t) ^ n!1")) (("1" (split -1) (("1" (lemma "const_derivable_fun[posreal]" ("b" "1")) (("1" (lemma "deriv_const_fun[posreal]" ("b" "1")) (("1" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "deriv_id_fun[posreal]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "diff_derivable_fun[posreal]" ("f1" "LAMBDA (x: posreal): 1" "f2" "LAMBDA (x: posreal): x")) (("1" (assert) (("1" (lemma "deriv_diff_fun[posreal]" ("ff1" "LAMBDA (x: posreal): 1" "ff2" "LAMBDA (x: posreal): x")) (("1" (replace -3) (("1" (replace -5) (("1" (expand "-") (("1" (lemma "deriv_exp_fun[posreal]" ("n" "1+n!1" "f" "LAMBDA (x_1: posreal): 1 - x_1")) (("1" (assert) (("1" (expand "^" -1) (("1" (flatten) (("1" (replace -3) (("1" (hide -3 -4 -5 -6 -7 -8) (("1" (lemma "scal_derivable_fun[posreal]" ("b" "-1/(1+n!1)" "f" "LAMBDA (t: posreal): (1 - t) ^ (1 + n!1)")) (("1" (assert) (("1" (lemma "deriv_scal_fun[posreal]" ("b" "-1/(1+n!1)" "ff" "LAMBDA (t: posreal): (1 - t) ^ (1 + n!1)")) (("1" (expand "*") (("1" (replace -4 -1) (("1" (assert) (("1" (lemma "extensionality" ("f" "(LAMBDA (x: posreal): -1 * ((1 - x) ^ n!1 * (-1 / (1 + n!1))) - (1 - x) ^ n!1 * (-1 / (1 + n!1)) * n!1)" "g" "LAMBDA (t: posreal): (1 - t) ^ n!1")) (("1" (split -1) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "fundamental3[posreal]" ("f" "LAMBDA (t: posreal): (1 - t) ^ n!1" "F" "LAMBDA (x: posreal): -1 / (1 + n!1) * (1 - x) ^ (1 + n!1)" "a" "1" "b" "px!1")) (("1" (replace -2 -1) (("1" (replace -3 -1) (("1" (replace -7 -1) (("1" (simplify -1) (("1" (expand "^" -1 3) (("1" (expand "expt" -1) (("1" (case "abs(Integral(1, px!1, LAMBDA (t: posreal): (1 - t) ^ n!1 / t)) <= abs(Integral(1, px!1, LAMBDA ( (("1" (replace -2 -1) (("1" (name-replace "DRL100" "abs(Integral(1, px!1, LAMBDA (t: posreal): (1 - t) ^ n!1 / t))") (("1" (hide-all-but (-1 -9 -10 1)) (("1" (rewrite "abs_mult" -1) (("1" (rewrite "abs_div" -1) (("1" (expand "abs" -1 1) (("1" (expand "abs" -1 1) (("1" (expand "<=" -2) (("1" (split -2) (("1" (rewrite "abs_expt" -2 :dir rl) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (expand "^") (("2" (expand "expt") (("2" (rewrite "zero_times1") (("2" (expand "abs") (("2" (propax) nil nil)) --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.657 Sekunden (vorverarbeitet am 2026-04-30) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26