Impressum exp.prf
Sprache: Lisp
(exp (cauchy_exp_series_TCC1 0nil 3394181533"" (skosimp*)"" (expand "cauchy_nzreal?" )"" (inst + "factorial(n!1)" )"" (rewrite "int_lemma" ) nil nil )) nil ))nil ))nil )"bool" cauchy nil )nil int nil )"posnat" factorial "ints/" )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil ))nil 3394181533"" (skosimp*)"" "inv_lemma" "nzx" "factorial(n!1)" "nzcx" "cauchy_int(factorial(n!1))" ))"" (rewrite "int_lemma" )"" (expand "cauchy_nnreal?" )"" (inst + "1 / factorial(n!1)" ) nil nil )) nil ))nil ))nil ))nil )nil reals nil )"boolean" notequal nil )"posnat" factorial "ints/" )nil integers nil )"bool" reals nil )nil integers nil )"cauchy_real" int nil )nil cauchy nil )"bool" cauchy nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil inv nil )"bool" cauchy nil )nil real_types nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"posrat" nil )nil int nil ))nil ))nil 3394181733"" (skosimp)"" (expand "cauchy_exp_series" )"" (expand "expT" )"" (case-replace "n!1=0" )"1" (expand "factorial" )"1" "inv_lemma" "nzx" "1" "nzcx" "cauchy_int(1)" ))"1" (rewrite "int_lemma" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert )"2" (rewrite "expt_1i" )"2" "inv_lemma" "nzx" "factorial(n!1)" "nzcx" "cauchy_int(factorial(n!1))" ))"2" (rewrite "int_lemma" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"cauchy_nnreal" exp nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil reals nil )"boolean" notequal nil )"cauchy_real" int nil )nil cauchy nil )"bool" cauchy nil )nil cauchy nil )"bool" cauchy nil )nil inv nil )nil int nil )"posnat" factorial "ints/" )nil integers nil )"bool" reals nil )nil integers nil )nil exponentiation nil )"posrat" nil )"posint" exponentiation nil )"real" ln_exp_series_alt "lnexp_fnd/" ))nil 3394181533"" (skosimp)"" (expand "cauchys_real?" )"" (lemma "exp_series_lemma" )"" (inst + "expT(1)" )"" (expand "cauchys_prop" ) (("" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" sum nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"real" ln_exp_series_alt "lnexp_fnd/" )"bool" sum nil )nil exp nil ))nil ))nil 3394181952"" (skosimp)"" (expand "exp_estimate" )"" "powerseries_lemma" "x" "x!1" "xs" "expT(1)" "cx" "cx!1" "cxs" "cauchy_exp_series" "m" "n!1" ))"" (replace -2)"" (lemma "exp_series_lemma" )"" (replace -1)"" (expand "powerseries" )"" "(LAMBDA (i:nat): IF i = 0 THEN expT(1)(i)") "" (hide-all-but 1)"" (apply-extensionality :hide? t)"" (expand "expT" )"" (case-replace "x!2=0" )"" assert )"" rewrite "expt_1i" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" ln_exp_series_alt "lnexp_fnd/" )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fieldsnil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"real" realsnil )"posrat" nil )"posint" exponentiation nil )"real" realsnil )nil exponentiation nil )"real" powerseries nil )nil exp nil )nil powerseries nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" cauchy nil )nil cauchy nil )"bool" cauchy nil )nil cauchy nil )"cauchy_nnreal" exp nil )"real" ln_exp_series_alt "lnexp_fnd/" ))nil 3394183332"" (lemma "exp_series_lemma" )"" (expand "cauchys_real?" )"" (inst + "expT(1)" )"" (expand "cauchys_prop" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil )"bool" sum nil )"bool" sum nil )"real" ln_exp_series_alt "lnexp_fnd/" )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil exp nil ))nil ))nil 3508599234"" (skosimp)"" (expand "cauchy_prop" 1)"" (skosimp)"" "exp_estimate_lemma" "x" "sx!1" "cx" "csx!1" "n" "p!1+3" ))"" (assert )"" (expand "cauchy_exp_dr" )"" (expand "cauchy_prop" -1)"" (inst - "2+p!1" )"" "CPS" "cauchy_powerseries(csx!1, cauchy_exp_series, 3 + p!1)(2 + p!1)" )"" (flatten)"" case "abs(exp_estimate(sx!1,3+p!1)*2^p!1-CPS/4)<1/4" )"1" (hide -2 -3)"1" "lemma_A2" "r" "round(CPS / 4)" "p" "CPS" "q" "4" ))"1" assert )"1" "1" case "abs(CPS/4-round(CPS / 4))<=1/2" )"1" "1" case "abs(exp_estimate(sx!1, 3 + p!1) * 2 ^ p!1 - round(CPS / 4)) < 3 / 4" )"1" "1" "RR" "round(CPS / 4)" )"1" "exp_estimate_bnd" "x" "sx!1" "n" "3+p!1" ))"1" case "abs((exp(sx!1) - exp_estimate(sx!1, 3 + p!1))*2^p!1) <= 1/4" )"1" "1" "EXP_" "exp(sx!1)" )"1" assert )nil nil ))nil ))nil )"2" "2" "abs_mult" "x" "exp(sx!1) - exp_estimate(sx!1, 3 + p!1)" "y" "2 ^ p!1" ))"2" replace -1)"2" expand "abs" "2" "2" case "max(exp(sx!1), 1) * abs(sx!1) ^ (3 + p!1 + 1) / ") "1" "LHS" "abs(exp(sx!1) - exp_estimate(sx!1, 3 + p!1))" )"1" "RHS" "max(exp(sx!1), 1) * abs(sx!1) ^ (3 + p!1 + 1) / ") "1" rewrite "div_mult_pos_le2" "1" rewrite "div_mult_pos_le2" "1" "both_sides_times_pos_le1" "pz" "4 * 2 ^ p!1" "x" "LHS" "y" "RHS" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "max(exp(sx!1), 1) * abs(sx!1) ^ (3 + p!1 + 1)<exp(1)" )"1" case "12 * 2 ^ p!1 <= factorial(4 + p!1)" )"1" case "exp(1)<3" )"1" "sx!1=0" )"1" expand "abs" )"1" expand "^" "1" expand "expt" )"1" assert )nil nil ))nil ))nil ))nil )"2" "lt_div_lt_pos2" "nnx" "max(exp(sx!1), 1) * abs(sx!1) ^ (3 + p!1 + 1)" "y" "3" "pz" "12 * 2 ^ p!1" "w" "factorial(4 + p!1)" ))"2" assert )nil nil ))nil ))nil )"2" "2" "exp_strict_increasing" )"2" expand "strict_increasing?" )"2" "1" "ln(3)" )"2" rewrite "exp_ln" )"2" "1" nil nil )"2" "2" "ln_bounds" "px" "3" "n" "4" ))"2" "LN3" "ln(3)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "forall (m:nat): 12*2^m<factorial(4+m)" )"1" "p!1" )"1" assert )nil nil ))nil )"2" "2" "m" )"1" nil nil )"2" "2" rewrite "expt_plus" )"2" expand "factorial" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sx!1=0" )"1" rewrite "exp_0" )"1" expand "max" )"1" expand "abs" )"1" expand "^" )"1" expand "expt" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "exp_strict_increasing" )"2" expand "strict_increasing?" )"2" "sx!1" "1" )"2" assert )"2" "both_sides_expt_pos_lt" "px" "abs(sx!1)" "py" "1" "pm" "4+p!1" ))"2" rewrite "expt_1i" )"2" "2" "2" "1" "both_sides_times_pos_lt1" "pz" "max(exp(sx!1), 1)" "x" "abs(sx!1) ^ (4 + p!1)" "y" "1" ))"1" assert )"1" case "max(exp(sx!1), 1)<=e" )"1" assert )nil nil )"2" "2" "EXP_" "exp(sx!1)" )"2" expand "max" )"2" "EXP_ < 1" )"1" "exp_strict_increasing" )"1" expand "strict_increasing?" )"1" "0" "1" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" 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" "2" "RR" "round(CPS / 4)" )"2" "P2" "2^p!1" )"2" "EST" "exp_estimate(sx!1, 3 + p!1)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "RR" "round(CPS / 4)" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3 2)"2" rewrite "expt_plus" )"2" rewrite "expt_x2" )"2" "EST" "exp_estimate(sx!1, 3 + p!1)" )"2" "P2" "2^p!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" exponentiation nil )"bool" cauchy nil )nil prelude_aux nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )nil cauchy nil )"bool" cauchy nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil exp nil )"posint" nil )"int" exp nil )"posint" nil )nil inv nil )"int" integers nil )"rat" rationals nil )"(divides(m))" dividesnil )"(divides(n))" dividesnil )"even_int" nil )"int" integers nil )"rat" rationalsnil )"rat" rationalsnil )"(total_order?[real])" nil )"bool" reals nil )nil real_types nil )"real" ln_exp "lnexp_fnd/" )"{py | x = ln(py)}" ln_exp "lnexp_fnd/" )"odd_int" integers nil )nil real_props nil )"nnreal" nil )"posint" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"posnat" factorial "ints/" )nil real_types nil )nil real_props nil )nil real_props nil )"nonneg_int" nil )nil exponentiation nil )nil exponentiation nil )nil reals nil )"even_int" nil )"(total_order?[real])" nil )"posnat" exponentiation nil )nil naturalnumbers nil )nil defined_types nil )nil real_props nil )"real" exponentiation nil )"nat" exponentiation nil )"nonneg_rat" nil )nil power_series "series/" )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil ln_approx "lnexp_fnd/" )"real" reals nil )"nzrat" nil )"(strict_total_order?[real])" real_props nil )"nzint" integersnil )"nzint" nil )"int" exponentiation nil )"nzreal" exponentiation nil )"nzrat" rationalsnil )"nzrat" nil )"rat" exponentiation nil )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_series "lnexp_fnd/" )"real" sigma "reals/" )"[n: nat, {y | y < p AND x = p ^ n * y}]" "reals/" )nil ln_exp "lnexp_fnd/" )"bool" real_fun_preds "reals/" )nil exponentiation nil )nil real_props nil )"posreal" ln_exp "lnexp_fnd/" )nil exponentiation nil )"nnreal" nil )"nnreal" exponentiation nil )"{z: posreal | z >= x AND z >= y}" real_defs nil )nil ln_exp_series_alt"lnexp_fnd/" )"real" reals nil )"{r: nonneg_rat | r >= q}" real_defs nil )"rat" rationals nil )nil integers nil )"even_int" nil )"int" prelude_aux nil )nil integers nil )"bool" reals nil )nil integers nil )nil appendix nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" ln_exp_series_alt "lnexp_fnd/" )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"{n: nonneg_real | n >= m AND n >= -m}" nil )nil real_types nil )"posrat" nil )"real" realsnil )"real" realsnil )"rat" rationalsnil )"[T, T -> boolean]" equalities nil )"bool" sum nil )nil sum nil )"cauchy_real" powerseries nil )"bool" cauchy nil )nil cauchy nil )"cauchy_nnreal" exp nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"posreal" real_types nil ))nil )nil 3394186556"" (skosimp)"" (expand "cauchy_prop" 1)"" (skosimp)"" "exp_estimate_lemma" "x" "sx!1" "cx" "csx!1" "n" "p!1+3" ))"" (assert )"" (expand "cauchy_exp_dr" )"" (expand "cauchy_prop" -1)"" (inst - "2+p!1" )"" "CPS" "cauchy_powerseries(csx!1, cauchy_exp_series, 3 + p!1)(2 + p!1)" )"" (flatten)"" case "abs(exp_estimate(sx!1,3+p!1)*2^p!1-CPS/4)<1/4" )"1" (hide -2 -3)"1" "lemma_A2" "r" "round(CPS / 4)" "p" "CPS" "q" "4" ))"1" assert )"1" "1" case "abs(CPS/4-round(CPS / 4))<=1/2" )"1" "1" case "abs(exp_estimate(sx!1, 3 + p!1) * 2 ^ p!1 - round(CPS / 4)) < 3 / 4" )"1" "1" "RR" "round(CPS / 4)" )"1" "exp_estimate_bnd" "x" "sx!1" "n" "3+p!1" ))"1" case "abs((exp(sx!1) - exp_estimate(sx!1, 3 + p!1))*2^p!1) <= 1/4" )"1" "1" "EXP" "exp(sx!1)" )"1" assert )nil nil ))nil ))nil )"2" "2" "abs_mult" "x" "exp(sx!1) - exp_estimate(sx!1, 3 + p!1)" "y" "2 ^ p!1" ))"2" replace -1)"2" expand "abs" "2" "2" case "max(exp(sx!1), 1) * abs(sx!1) ^ (3 + p!1 + 1) / ") "1" "LHS" "abs(exp(sx!1) - exp_estimate(sx!1, 3 + p!1))" )"1" "RHS" "max(exp(sx!1), 1) * abs(sx!1) ^ (3 + p!1 + 1) / ") "1" rewrite "div_mult_pos_le2" "1" rewrite "div_mult_pos_le2" "1" "both_sides_times_pos_le1" "pz" "4 * 2 ^ p!1" "x" "LHS" "y" "RHS" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "max(exp(sx!1), 1) * abs(sx!1) ^ (3 + p!1 + 1)<exp(1)" )"1" case "12 * 2 ^ p!1 <= factorial(4 + p!1)" )"1" case "exp(1)<3" )"1" "sx!1=0" )"1" expand "abs" )"1" expand "^" "1" expand "expt" )"1" assert )nil nil ))nil ))nil ))nil )"2" "lt_div_lt_pos2" "nnx" "max(exp(sx!1), 1) * abs(sx!1) ^ (3 + p!1 + 1)" "y" "3" "pz" "12 * 2 ^ p!1" "w" "factorial(4 + p!1)" ))"2" assert )nil nil ))nil ))nil )"2" "2" "exp_strict_increasing" )"2" expand "strict_increasing?" )"2" "1" "ln(3)" )"2" rewrite "exp_ln" )"2" "1" nil nil )"2" "2" "ln_bounds" "px" "3" "n" "4" ))"2" "LN3" "ln(3)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "forall (m:nat): 12*2^m<factorial(4+m)" )"1" "p!1" )"1" assert )nil nil ))nil )"2" "2" "m" )"1" nil nil )"2" "2" rewrite "expt_plus" )"2" expand "factorial" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "sx!1=0" )"1" rewrite "exp_0" )"1" expand "max" )"1" expand "abs" )"1" expand "^" )"1" expand "expt" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "exp_strict_increasing" )"2" expand "strict_increasing?" )"2" "sx!1" "1" )"2" assert )"2" "both_sides_expt_pos_lt" "px" "abs(sx!1)" "py" "1" "pm" "4+p!1" ))"2" rewrite "expt_1i" )"2" "2" "2" "1" "both_sides_times_pos_lt1" "pz" "max(exp(sx!1), 1)" "x" "abs(sx!1) ^ (4 + p!1)" "y" "1" ))"1" assert )"1" case "max(exp(sx!1), 1)<=e" )"1" assert )nil nil )"2" "2" "EXP" "exp(sx!1)" )"2" expand "max" )"2" "EXP < 1" )"1" "exp_strict_increasing" )"1" expand "strict_increasing?" )"1" "0" "1" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" 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" "2" "RR" "round(CPS / 4)" )"2" "P2" "2^p!1" )"2" "EST" "exp_estimate(sx!1, 3 + p!1)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "RR" "round(CPS / 4)" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3 2)"2" rewrite "expt_plus" )"2" rewrite "expt_x2" )"2" "EST" "exp_estimate(sx!1, 3 + p!1)" )"2" "P2" "2^p!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cauchy nil )"bool" cauchy nil )"cauchy_real" powerseries nil )nil sum nil )"bool" sum nil )"real" ln_exp_series_alt "lnexp_fnd/" )nil appendix nil )"int" prelude_aux nil )nil ln_exp_series_alt"lnexp_fnd/" )"posreal" ln_exp "lnexp_fnd/" )"bool" real_fun_preds "reals/" )nil ln_exp "lnexp_fnd/" )"[n: nat, {y | y < p AND x = p ^ n * y}]" "reals/" )"real" sigma "reals/" )"real" ln_series "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )nil ln_approx "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil power_series "series/" )"{py | x = ln(py)}" ln_exp "lnexp_fnd/" )"real" ln_exp "lnexp_fnd/" )nil inv nil )"bool" cauchy nil )nil cauchy nil )"bool" cauchy nil )nil cauchy nil )nil prelude_aux nil )"bool" cauchy nil ))nil 3394183332"" (skosimp)"" (typepred "csx!1" )"" (expand "cauchy_smallreal?" )"" (skosimp)"" (lemma "exp_dr_lemma" ("csx" "csx!1" "sx" "sx!1" ))"" (expand "cauchy_posreal?" )"" (inst + "exp(sx!1)" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" cauchy nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"real" ln_exp "lnexp_fnd/" )"{py | x = ln(py)}" ln_exp "lnexp_fnd/" )nil exp nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil prelude_aux nil ))nil ))nil 3394183332"" (skosimp*)"" (typepred "cx!1" )"" (expand "cauchy_real?" )"" (skosimp)"" "div_lemma" "x" "x!1" "cx" "cx!1" "nzy" "ln(2)" "nzcy" "cauchy_ln2" ))"1" (rewrite "cauchy_ln2_lemma" )"1" (assert )"1" (expand "cauchy_prop" -1)"1" (inst - "0" )"1" (replace -3 * rl)"1" (rewrite "expt_x0" )"1" (flatten)"1" "mul_lemma" "x" "n!1" "cx" "cauchy_int(n!1)" "y" "ln(2)" "cy" "cauchy_ln2" ))"1" rewrite "int_lemma" )"1" rewrite "cauchy_ln2_lemma" )"1" "sub_lemma" "x" "x!1" "cx" "cx!1" "y" "n!1 * ln(2)" "cy" "cauchy_mul(cauchy_int(n!1), cauchy_ln2)" ))"1" assert )"1" replace -8 * rl)"1" rewrite "div_mult_pos_lt2" "1" rewrite "div_mult_pos_lt1" "1" case "ln(2)<1" )"1" expand "cauchy_smallreal?" )"1" "x!1 - n!1 * ln(2)" )"1" assert )nil nil ))nil ))nil )"2" "2" "ln_bounds" "px" "2" "n" "2" ))"2" "2" "2" "LN2" "ln(2)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ln_strict_increasing" )"2" expand "strict_increasing?" )"2" "1" "2" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "ln_strict_increasing" )"2" expand "strict_increasing?" )"2" "1" "2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "ln_strict_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "1" "2" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil log nil )"real" realsnil )"posint" exponentiation nil )"bool" cauchy nil )nil int nil )"real" realsnil )nil sub nil )"cauchy_real" mul nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )nil real_props nil )"[T, T -> boolean]" equalities nil )"(total_order?[real])" nil )"posint" nil )"nzrat" nil )"nzint" integersnil )"int" integers nil )"nzint" nil )"(divides(n))" dividesnil )"int" exponentiation nil )"nzreal" exponentiation nil )"(divides(m))" dividesnil )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_series "lnexp_fnd/" )"real" sigma "reals/" )"real" exponentiation nil )"real" exponentiation nil )"[n: nat, {y | y < p AND x = p ^ n * y}]" "reals/" )nil ln_approx "lnexp_fnd/" )"bool" cauchy nil )"real" reals nil )"int" exp nil )"real" exp nil )"[numfield -> numfield]" number_fields nil )nil prelude_aux nil )"bool" reals nil )"bool" real_fun_preds "reals/" )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )"real" realsnil )nil real_props nil )"[numfield, numfield -> numfield]" number_fieldsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"int" integers nil )"int" integers nil )"cauchy_real" int nil )nil mul nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )nil div nil )"bool" cauchy nil )nil cauchy nil )"bool" cauchy nil )nil cauchy nil )"cauchy_posreal" log nil )"boolean" notequal nil )nil reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" ln_exp "lnexp_fnd/" ))nil ))nil 3394183332"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3394183332"" (skosimp*)"" (hide 1)"" (case "0<ln(2)&ln(2)<1" )"1" (flatten)"1" (typepred "cx!1" )"1" (expand "cauchy_real?" )"1" (skosimp)"1" "div_lemma" "x" "x!1" "cx" "cx!1" "nzy" "ln(2)" "nzcy" "cauchy_ln2" ))"1" (rewrite "cauchy_ln2_lemma" )"1" (assert )"1" (expand "cauchy_prop" -1)"1" (inst - "0" )"1" rewrite "expt_x0" )"1" replace -5 * rl)"1" "1" assert )"1" rewrite "div_mult_pos_lt2" -1)"1" rewrite "div_mult_pos_lt1" "1" "mul_lemma" "x" "n!1" "cx" "cauchy_int(n!1)" "y" "ln(2)" "cy" "cauchy_ln2" ))"1" rewrite "int_lemma" )"1" rewrite "cauchy_ln2_lemma" )"1" "sub_lemma" "x" "x!1" "cx" "cx!1" "y" "n!1 * ln(2)" "cy" "cauchy_mul(cauchy_int(n!1), cauchy_ln2)" ))"1" assert )"1" replace "1" expand "cauchy_smallreal?" )"1" "x!1 - n!1 * ln(2)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (lemma "ln_bounds" ("px" "2" "n" "1" ))"2" (name-replace "LN2" "ln(2)" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"[T, T -> boolean]" equalities nil )"[n: nat, {y | y < p AND x = p ^ n * y}]" "reals/" )"real" exponentiation nil )"real" exponentiation nil )"real" sigma "reals/" )"real" ln_series "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"(divides(m))" dividesnil )"nzreal" exponentiation nil )"int" exponentiation nil )"(divides(n))" dividesnil )"nzint" nil )"int" integers nil )"nzint" integersnil )"nzrat" nil )"posint" nil )"(total_order?[real])" nil )nil ln_approx "lnexp_fnd/" )nil reals nil )"boolean" notequal nil )"cauchy_posreal" log nil )nil cauchy nil )"bool" cauchy nil )nil cauchy nil )"bool" cauchy nil )nil div nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" realsnil )"int" integers nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil real_props nil )nil int nil )nil sub nil )"cauchy_real" mul nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil prelude_aux nil )"[numfield -> numfield]" number_fields nil )"bool" cauchy nil )"real" realsnil )"real" reals nil )"cauchy_real" int nil )nil mul nil )nil real_props nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )"(total_order?[real])" nil )nil exponentiation nil )"bool" cauchy nil )"posint" exponentiation nil )"real" realsnil )nil log nil )NOT const-decl "[bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" cauchy nil )nil cauchy nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" ln_exp "lnexp_fnd/" ))nil ))nil 3394183332"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3394183332"" (skosimp*)"" (case-replace "n!1=0" )"1" (hide -1 1 2)"1" "mul_lemma" "x" "0" "cx" "cauchy_int(0)" "y" "ln(2)" "cy" "cauchy_ln2" ))"1" (rewrite "int_lemma" )"1" (rewrite "cauchy_ln2_lemma" )"1" "unique_cauchy_zero3" "cx" "cauchy_mul(cauchy_int(0), cauchy_ln2)" ))"1" (assert )"1" (replace -1)"1" (typepred "cx!1" )"1" (expand "cauchy_real?" )"1" (skosimp)"1" "sub_lemma" "x" "x!1" "cx" "cx!1" "y" "0" "cy" "cauchy_zero" ))"1" "unique_cauchy_zero" "x" "0" ))"1" assert )"1" "1" replace -6 * rl)"1" "1" "div_lemma" "x" "x!1" "cx" "cx!1" "nzy" "ln(2)" "nzcy" "cauchy_ln2" ))"1" rewrite "cauchy_ln2_lemma" )"1" assert )"1" expand "cauchy_prop" "1" "0" )"1" rewrite "expt_x0" )"1" replace "1" "1" assert )"1" rewrite "div_mult_pos_lt2" "1" rewrite "div_mult_pos_lt1" "1" case "ln(2)<1" )"1" expand "cauchy_smallreal?" )"1" "x!1" )"1" assert )nil nil ))nil ))nil )"2" "2" "ln_bounds" "px" "2" "n" "1" ))"2" "LN2" "ln(2)" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "ln_strict_increasing" )"2" expand "strict_increasing?" )"2" "1" "2" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "ln_strict_increasing" )"2" expand "strict_increasing?" )"2" "1" "2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ln_strict_increasing" )"2" expand "strict_increasing?" )"2" "1" "2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"real" ln_exp "lnexp_fnd/" )nil real_types nil )"bool" reals nil )nil real_types nil )"cauchy_posreal" log nil )nil cauchy nil )"bool" cauchy nil )"cauchy_real" int nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil mul nil )nil log nil )"real" realsnil )NOT const-decl "[bool -> bool]" booleans nil )nil cauchy nil )"real" realsnil )"posint" exponentiation nil )"bool" cauchy nil )nil exponentiation nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_props nil )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )"bool" real_fun_preds "reals/" )"bool" reals nil )nil prelude_aux nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"real" exp nil )"bool" cauchy nil )nil ln_approx "lnexp_fnd/" )"(total_order?[real])" nil )"real" reals nil )"posint" nil )"nzrat" nil )"nzint" integersnil )"int" integers nil )"nzint" nil )"(divides(n))" dividesnil )"int" exponentiation nil )"nzreal" exponentiation nil )"(divides(m))" dividesnil )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_series "lnexp_fnd/" )"real" sigma "reals/" )"real" exponentiation nil )"real" exponentiation nil )"[n: nat, {y | y < p AND x = p ^ n * y}]" "reals/" )nil real_props nil )"(strict_total_order?[real])" real_props nil )"odd_int" integersnil )"posint" nil )"odd_int" integersnil )nil reals nil )"boolean" notequal nil )nil cauchy nil )"bool" cauchy nil )nil div nil )"cauchy_nnreal" cauchy nil )nil cauchy nil )"bool" cauchy nil )nil sub nil )"cauchy_real" mul nil )nil cauchy nil )nil int nil ))nil ))nil 3508599271"" (skosimp)"" (expand "cauchy_exp" )"" (name "N" "cauchy_div(cx!1, cauchy_ln2)(0)" )"" (replace -1)"" "mul_lemma" "x" "N" "cx" "cauchy_int(N)" "y" "ln(2)" "cy" "cauchy_ln2" ))"" (rewrite "int_lemma" )"" (rewrite "cauchy_ln2_lemma" )"" "sub_lemma" "x" "x!1" "cx" "cx!1" "y" "N * ln(2)" "cy" "cauchy_mul(cauchy_int(N), cauchy_ln2)" ))"" (assert )"" (case "0<ln(2)&ln(2)<1" )"1" (flatten)"1" "div_lemma" "x" "x!1" "cx" "cx!1" "nzy" "ln(2)" "nzcy" "cauchy_ln2" ))"1" rewrite "cauchy_ln2_lemma" )"1" assert )"1" expand "cauchy_prop" -1)"1" "0" )"1" rewrite "expt_x0" )"1" replace -6)"1" "1" assert )"1" rewrite "div_mult_pos_lt1" )"1" rewrite "div_mult_pos_lt2" )"1" "exp_dr_lemma" "sx" "x!1 - N * ln(2)" "csx" "cauchy_sub(cx!1, cauchy_mul(cauchy_int(N), cauchy_ln2))" ))"1" assert )"1" "EXP_" "cauchy_exp_dr(cauchy_sub(cx!1, ") "1" "trichotomy" "x" "N" ))"1" "1" assert )"1" "lemma_mul2n" "x" "exp(x!1 - N * ln(2))" "cx" "EXP_" "n" "N" ))"1" assert )"1" expand "mul2n" )"1" rewrite "exp_diff" "1" rewrite "exp_scal" "1" assert )"1" rewrite "exp_ln" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )"3" "lemma_div2n" "x" "exp(x!1 - N * ln(2))" "cx" "EXP_" "n" "-N" ))"3" assert )"3" expand "div2n" )"3" rewrite "exp_diff" )"3" rewrite "exp_scal" )"3" rewrite "exp_ln" )"3" rewrite "div_div2" )"3" "expt_plus" "n0x" "2" "i" "N" "j" "-N" ))"3" rewrite "expt_x0" )"3" replace "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" expand "cauchy_smallreal?" )"3" "x!1 - N * ln(2)" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide-all-but 1)"2" "ln_bounds" ("px" "2" "n" "2" ))"2" "LN2" "ln(2)" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[nat -> int]" exp nil )nil int nil )"real" realsnil )nil sub nil )"cauchy_real" mul nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil div nil )"boolean" notequal nil )nil reals nil )"real" realsnil )"int" integers nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil real_props nil )"int" exp nil )"real" exp nil )"real" reals nil )nil real_axioms nil )"int" integers nil )nil exponentiation nil )nil reals nil )"posrat" nil )nil real_props nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"real" shift nil )nil shift nil )nil ln_exp "lnexp_fnd/" )"nnrat" exponentiation nil )"posrat" exponentiation nil )"odd_int" integers nil )"posreal" nil )"posreal" real_types nil )nil ln_exp "lnexp_fnd/" )"nzreal" exponentiation nil )"posreal" exponentiationnil )nil ln_exp "lnexp_fnd/" )nil integers nil )"real" shift nil )"{py | x = ln(py)}" ln_exp "lnexp_fnd/" )nil shift nil )nil application-judgement "cauchy_posreal" exp nil )"int" exp nil )nil prelude_aux nil )"[numfield -> numfield]" number_fields nil )"cauchy_real" sub nil )nil cauchy nil )"bool" cauchy nil )nil exp nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fieldsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )"bool" cauchy nil )"posint" exponentiation nil )"real" realsnil )nil ln_approx "lnexp_fnd/" )"(total_order?[real])" nil )"posint" nil )"nzrat" nil )"nzint" integersnil )"int" integers nil )"nzint" nil )"(divides(n))" dividesnil )"int" exponentiation nil )"nzreal" exponentiation nil )"(divides(m))" dividesnil )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_series "lnexp_fnd/" )"real" sigma "reals/" )"real" exponentiation nil )"[n: nat, {y | y < p AND x = p ^ n * y}]" "reals/" )"(strict_total_order?[real])" real_props nil )nil log nil )nil mul nil )"cauchy_real" int nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" ln_exp "lnexp_fnd/" )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" cauchy nil )nil cauchy nil )"bool" cauchy nil )nil cauchy nil )"cauchy_real" div nil )"bool" cauchy nil )nil cauchy nil )"cauchy_posreal" log nil ))nil )nil 3394193300"" (skosimp)"" (expand "cauchy_exp" )"" (name "N" "cauchy_div(cx!1, cauchy_ln2)(0)" )"" (replace -1)"" "mul_lemma" "x" "N" "cx" "cauchy_int(N)" "y" "ln(2)" "cy" "cauchy_ln2" ))"" (rewrite "int_lemma" )"" (rewrite "cauchy_ln2_lemma" )"" "sub_lemma" "x" "x!1" "cx" "cx!1" "y" "N * ln(2)" "cy" "cauchy_mul(cauchy_int(N), cauchy_ln2)" ))"" (assert )"" (case "0<ln(2)&ln(2)<1" )"1" (flatten)"1" "div_lemma" "x" "x!1" "cx" "cx!1" "nzy" "ln(2)" "nzcy" "cauchy_ln2" ))"1" rewrite "cauchy_ln2_lemma" )"1" assert )"1" expand "cauchy_prop" -1)"1" "0" )"1" rewrite "expt_x0" )"1" replace -6)"1" "1" assert )"1" rewrite "div_mult_pos_lt1" )"1" rewrite "div_mult_pos_lt2" )"1" "exp_dr_lemma" "sx" "x!1 - N * ln(2)" "csx" "cauchy_sub(cx!1, cauchy_mul(cauchy_int(N), cauchy_ln2))" ))"1" assert )"1" "EXP" "cauchy_exp_dr(cauchy_sub(cx!1, ") "1" "trichotomy" "x" "N" ))"1" "1" assert )"1" "lemma_mul2n" "x" "exp(x!1 - N * ln(2))" "cx" "EXP" "n" "N" ))"1" assert )"1" expand "mul2n" )"1" rewrite "exp_diff" "1" rewrite "exp_scal" "1" assert )"1" rewrite "exp_ln" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )"3" "lemma_div2n" "x" "exp(x!1 - N * ln(2))" "cx" "EXP" "n" "-N" ))"3" assert )"3" expand "div2n" )"3" rewrite "exp_diff" )"3" rewrite "exp_scal" )"3" rewrite "exp_ln" )"3" rewrite "div_div2" )"3" "expt_plus" "n0x" "2" "i" "N" "j" "-N" ))"3" rewrite "expt_x0" )"3" replace "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" expand "cauchy_smallreal?" )"3" "x!1 - N * ln(2)" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide-all-but 1)"2" "ln_bounds" ("px" "2" "n" "2" ))"2" "LN2" "ln(2)" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil int nil )nil sub nil )"cauchy_real" mul nil )nil div nil )"real" shift nil )nil shift nil )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )"real" shift nil )"{py | x = ln(py)}" ln_exp "lnexp_fnd/" )nil shift nil )"bool" cauchy nil )nil cauchy nil )"cauchy_real" sub nil )nil prelude_aux nil )"bool" cauchy nil )nil ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_approx "lnexp_fnd/" )"real" ln_series "lnexp_fnd/" )"real" sigma "reals/" )"[n: nat, {y | y < p AND x = p ^ n * y}]" "reals/" )nil log nil )nil mul nil )"cauchy_real" int nil )"real" ln_exp "lnexp_fnd/" )"bool" cauchy nil )nil cauchy nil )"bool" cauchy nil )nil cauchy nil )"cauchy_real" div nil )"bool" cauchy nil )nil cauchy nil )"cauchy_posreal" log nil ))nil 3394186422"" (skosimp)"" (typepred "cx!1" )"" (expand "cauchy_real?" )"" (skosimp)"" (lemma "exp_lemma" ("x" "x!1" "cx" "cx!1" ))"" (assert )"" (expand "cauchy_posreal?" )"" (inst + "exp(x!1)" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"{py | x = ln(py)}" ln_exp "lnexp_fnd/" )"real" ln_exp "lnexp_fnd/" )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" cauchy nil )nil exp nil ))nil )))
Messung V0.5 in Prozent C=98 H=100 G=98
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.133Bemerkung:
(vorverarbeitet am 2026-04-28)
¤ *Bot Zugriff
2026-05-26
