Quelle log.prf
Sprache: Lisp
(log (cauchy_ln_small_TCC1 0nil 3394161634"" (expand "cauchy_ln_small?" )"" (inst + "0" ) (("" (rewrite "int_lemma" ) nil nil )) nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"[numfield -> numfield]" number_fields nil )nil log nil )nil int nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" log nil )"odd_int" integersnil ))nil ))nil 3394109924"" (skosimp)"" (typepred "x!1" )"" (expand "cauchy_ln_small?" )"" (skosimp)"" (expand "cauchy_real?" )"" (inst + "x!2" ) nil nil )) nil ))nil ))nil ))nil ))nil )nil log nil )"bool" log 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 )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" cauchy nil )"odd_int" integersnil ))nil ))nil 3394161634"" (expand "cauchy_ln_med?" )"" (inst + "1" ) (("" (rewrite "int_lemma" ) nil nil )) nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil log nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil int nil )"bool" log nil ))nil ))nil 3394127143"" (skosimp)"" (typepred "x!1" )"" (expand "cauchy_ln_med?" )"" (expand "cauchy_posreal?" )"" (skosimp) (("" (inst + "x!2" ) nil nil )) nil )) nil ))nil ))nil ))nil )nil log nil )"bool" log 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 )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil log nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil ))nil ))nil 3394175254"" (expand "cauchy_gt_quarter?" )"" (inst + "1" ) (("" (rewrite "int_lemma" ) nil nil )) nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil log nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil int nil )"bool" log nil ))nil ))nil 3394161634"" (skosimp)"" (typepred "x!1" )"" (expand "cauchy_gt_quarter?" )"" (skosimp)"" (expand "cauchy_posreal?" )"" (inst + "x!2" ) nil nil )) nil ))nil ))nil ))nil ))nil )nil log nil )"bool" log 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 )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil log nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" cauchy nil ))nil ))nil 3394113740"" (skosimp)"" (expand "cauchy_nzreal?" )"" (inst + "n!1" )"1" (rewrite "int_lemma" ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil )"bool" cauchy nil )nil int nil )nil reals nil )nil numbers nil )nil booleans nil )"boolean" notequal 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 )"nat" log nil ))nil ))nil 3394113740"" (skosimp)"" (expand "cauchy_nzreal?" )"" (inst + "n!1" )"1" (rewrite "int_lemma" ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil )"bool" cauchy nil )nil int nil )nil reals nil )nil numbers nil )nil booleans nil )"boolean" notequal 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 )"nat" log nil ))nil ))nil 3394113740"" (skosimp) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil ))nil ))nil 3394113751"" (skosimp)"" (expand "cauchy_ln_series" )"" (typepred "n!1" )"" (expand ">=" )"" (expand "<=" )"" (split -1)"1" (assert )"1" (expand "lnT" )"1" (case "even?(n!1)" )"1" (assert )"1" (expand "even?" )"1" (skosimp)"1" replace -1)"1" rewrite "expt_times" )"1" rewrite "expt_x2" )"1" rewrite "expt_1i" )"1" replace -1 * rl)"1" "1" "div_lemma" "x" "-1" "nzy" "n!1" "cx" "cauchy_int(-1)" "nzcy" "cauchy_int(n!1)" ))"1" rewrite "int_lemma" )"1" rewrite "int_lemma" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (rewrite "even_iff_not_odd" )"2" (expand "odd?" )"2" "2" replace -1)"2" rewrite "expt_plus" )"2" rewrite "expt_times" )"2" rewrite "expt_x2" )"2" rewrite "expt_1i" )"2" replace -1 * rl)"2" "2" "div_lemma" "x" "1" "nzy" "n!1" "cx" "cauchy_int(1)" "nzcy" "cauchy_int(n!1)" ))"2" rewrite "int_lemma" )"2" rewrite "int_lemma" )"2" rewrite "expt_x1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1 * rl)"2" (lemma "unique_cauchy_zero" ("x" "0" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"cauchy_real" log nil )"real_gtm1_le1" ln_exp_series_alt "lnexp_fnd/" )"(divides(m))" dividesnil )"bool" integers nil )nil exponentiation nil )"nzint" nil )"nzrat" nil )"odd_int" integersnil )nil exponentiation nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil naturalnumbers nil )"odd_int" integers nil )"nzreal" exponentiation nil )"int" exponentiation nil )"nzint" integersnil )"nzrat" nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )nil exponentiation nil )"nzrat" rationalsnil )"int" integers nil )"even_int" nil )"(divides(n))" dividesnil )"rat" exponentiation nil )nil exponentiation nil )nil int nil )nil reals nil )nil cauchy nil )"bool" cauchy nil )"cauchy_real" int nil )nil cauchy nil )"bool" cauchy nil )nil div nil )"odd_int" integersnil )nil inv nil )"bool" integers nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )nil cauchy nil )"bool" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[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 )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil ))nil 3394115362"" (skosimp)"" (expand "cauchys_real?" )"" (lemma "ln_series_lemma" )"" "lambda n:IF n = 0 THEN 0 ELSE lnT(1)(n - 1) ENDIF" )"1" (expand "cauchys_prop" ) (("1" (propax) nil nil ))nil )"2" (skosimp) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" sum nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans 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 )IF const-decl "[boolean, T, T -> T]" if_def nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )nil ln_exp_series_alt"lnexp_fnd/" )"real_gtm1_le1" ln_exp_series_alt "lnexp_fnd/" )"bool" sum nil )"(total_order?[real])" nil )nil log nil )"odd_int" integersnil ))nil ))nil 3394115371"" (skosimp)"" (expand "ln_estimate" )"" "powerseries_lemma" "x" "ssx!1" "cx" "cssx!1" "xs" "LAMBDA n: IF n = 0 THEN 0 ELSE lnT(1)(n-1) ENDIF" "cxs" "cauchy_ln_series" "m" "n!1" ))"1" (expand "powerseries" )"1" (replace -2)"1" (lemma "ln_series_lemma" )"1" (replace -1)"1" (hide -1)"1" "CPS" "cauchy_powerseries(cssx!1, cauchy_ln_series, n!1)" )"1" (expand "lnT" )"1" "(LAMBDA (i:nat): IF i = 0 THEN 0LAMBDA (nn: nat):IF nn = 0 THEN 0 ELSE -(-ssx!1) ^ nn / nn ENDIF)") "1" (hide-all-but 1)"1" "1" "x!1=0" )"1" assert )"1" "(-ssx!1) ^ x!1 = (-1) ^ x!1* ssx!1 ^ x!1" )"1" (assert ) nil nil )"2" "2" "ssx!1=0" )"1" expand "^" )"1" expand "expt" )"1" (assert ) nil nil ))nil ))nil )"2" "mult_expt" "n0x" "-1" "n0y" "ssx!1" "i" "x!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp) nil nil ))nil ))nil )"2" (skosimp) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"real" ln_exp_series_alt "lnexp_fnd/" )"(total_order?[real])" nil )"real" powerseries nil )nil log nil )"real" exponentiation nil )"int" integers nil )"even_int" nil )"(divides(n))" dividesnil )"(divides(m))" dividesnil )"even_int" integersnil )"int" exponentiation nil )nil reals nil )nil exponentiation nil )"int" exponentiation nil )"nzreal" exponentiation nil )"nzint" integersnil )"nzrat" nil )"real" realsnil )"real" realsnil )"real" reals nil )"[numfield, numfield -> numfield]" number_fieldsnil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"bool" sum nil )nil sum nil )"cauchy_real" powerseries nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers 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" log nil )nil log nil )"cauchy_real" log nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"[numfield -> numfield]" number_fields nil )nil log nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil ln_exp_series_alt"lnexp_fnd/" )"real_gtm1_le1" ln_exp_series_alt "lnexp_fnd/" )"[numfield, numfield -> numfield]" number_fieldsnil )"odd_int" integersnil ))nil 3394115362"" (lemma "ln_series_lemma" )"" (expand "cauchys_real?" )"" "lambda n:IF n = 0 THEN 0 ELSE lnT(1)(n - 1) ENDIF" )"1" (expand "cauchys_prop" ) (("1" (propax) nil nil )) nil )"2" (skosimp) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"bool" sum nil )"(total_order?[real])" nil )"bool" sum nil )"real_gtm1_le1" ln_exp_series_alt "lnexp_fnd/" )nil ln_exp_series_alt"lnexp_fnd/" )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def 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, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )"int" integers nil )nil log nil ))nil ))nil 3394113740 ("" (subtype-tcc) nil nil )"real" exponentiation nil )"bool" cauchy nil )"posnat" exponentiation nil )"odd_int" integersnil ))nil ))nil 3508599150"" (skosimp)"" "ln_estimate_lemma" ("ssx" "ssx!1" "cssx" "cssx!1" ))"" (expand "cauchy_ln_drx" )"" (expand "cauchy_prop" 1)"" (skosimp)"" (inst - "2+p!1" )"" (assert )"" "ln_estimate_bnd" "z" "ssx!1" "n" "2+p!1" ))"" (name-replace "LOG_" "ln(1 + ssx!1)" )"" "CPS" "cauchy_powerseries(cssx!1, cauchy_ln_series, 2 + p!1)" )"" "EST" "ln_estimate(ssx!1, 2 + p!1)" )"" (expand "round" )"" "floor(1 / 2 + CPS(2 + p!1) / 4)" )"" "RR" "floor(1 / 2 + CPS(2 + p!1) / 4)" )"" "" expand "cauchy_prop" )"" "2+p!1" )"" "" case "abs(LOG_ - EST)*2^p!1 < 1/4" )"1" "1" case "abs(LOG_* 2 ^ p!1 - CPS(2 + p!1)/4) < 1/2" )"1" "1" "P2" "2 ^ p!1" )"1" nil nil ))nil ))nil )"2" "2" "abs_mult" "x" "LOG_-EST" "y" "2^p!1" ))"2" expand "abs" "2" replace "2" "2" rewrite "expt_plus" )"2" rewrite "expt_x2" )"2" "P2" "2^p!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "ABS" "abs(LOG_ - EST)" )"2" "ssx!1" )"2" case "abs(ssx!1) ^ (2 + p!1 + 1) <= 1/2^(3+p!1)" )"1" case "1 <= IF ssx!1 < 0 THEN 1 + ssx!1 ELSE 1 ENDIF * (2 + p!1 + 1)" )"1" "le_div_le_pos" "nnx" "abs(ssx!1) ^ (2 + p!1 + 1)" "y" "1 / 2 ^ (3 + p!1)" "pz" "1" "w" "IF ssx!1 < 0 THEN 1 + ssx!1 ELSE 1 ENDIF * (2 + p!1 + 1)" ))"1" replace -3)"1" replace "1" "RHS" "abs(ssx!1) ^ (2 + p!1 + 1) / IF ssx!1 < 0 THEN 1 + ssx!1 ELSE 1 ENDIF * (2 + p!1 + 1))") "1" rewrite "div_div2" )"1" "both_sides_expt_gt1_lt" "gt1x" "2" "i" "2+p!1" "j" "3+p!1" ))"1" assert )"1" "1" "div_mult_pos_lt2" "py" "2^p!1" "x" "ABS" "z" "1/4" ))"1" replace "1" "1" rewrite "div_div2" )"1" "both_sides_div_pos_lt2" "pz" "1" "px" "2 ^ (3 + p!1)" "py" "2 ^ (2 + p!1)" ))"1" assert )"1" "expt_plus" "n0x" "2" "i" "2" "j" "p!1" ))"1" rewrite "expt_x2" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "ssx!1<0" )"1" "both_sides_times_pos_le1" "pz" "3+p!1" "x" "-1/2" "y" "ssx!1" ))"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "ssx!1=0" )"1" expand "^" "1" expand "expt" "1" expand "abs" )"1" assert )nil nil ))nil ))nil ))nil )"2" "both_sides_expt_pos_le" "px" "abs(ssx!1)" "py" "1/2" "pm" "3+p!1" ))"1" "1" "1" "1" rewrite "inv_expt" )"1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil log nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil log nil )"bool" log 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 log nil )"posint" exponentiation nil )"bool" cauchy nil )"posint" nil )"[numfield, numfield -> numfield]" number_fieldsnil )"real" realsnil )nil ln_exp_series_alt"lnexp_fnd/" )"bool" reals nil )nil ln_exp_series_alt"lnexp_fnd/" )"(total_order?[real])" nil )"cauchy_real" log nil )"cauchy_real" powerseries nil )nil sum nil )"bool" sum nil )nil cauchy nil )"bool" cauchy nil )"int" prelude_aux nil )"posrat" nil )nil exponentiation nil )nil integers nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )"nonneg_int" nil )"nat" exponentiation nil )"real" exponentiation nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" realsnil )nil exponentiation nil )nil real_props nil )nil real_props nil )"nzrat" nil )nil real_props nil )nil reals nil )nil real_props nil )"nnreal" exponentiation nil )"rat" rationalsnil )"nzrat" nil )nil real_props nil )nil inv nil )"even_int" nil )"int" integers nil )"posint" nil )"(divides(n))" dividesnil )"(divides(m))" dividesnil )nil exponentiation nil )nil reals nil )nil real_props nil )"int" integers nil )"real" reals nil )nil integers nil )nil integers nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fieldsnil )"{n: nonneg_real | n >= m AND n >= -m}" nil )"[numfield, numfield -> numfield]" number_fieldsnil )"nnreal" nil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil integers nil )NOT const-decl "[bool -> bool]" booleans nil )"rat" rationals nil )"real" ln_exp_series_alt "lnexp_fnd/" )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" ln_exp "lnexp_fnd/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"rat" rationalsnil )"real" realsnil )"real" reals nil )"int" log nil )"odd_int" integersnil ))nil )nil 3394116656"" (skosimp)"" "ln_estimate_lemma" ("ssx" "ssx!1" "cssx" "cssx!1" ))"" (expand "cauchy_ln_drx" )"" (expand "cauchy_prop" 1)"" (skosimp)"" (inst - "2+p!1" )"" (assert )"" "ln_estimate_bnd" "z" "ssx!1" "n" "2+p!1" ))"" (name-replace "LOG" "ln(1 + ssx!1)" )"" "CPS" "cauchy_powerseries(cssx!1, cauchy_ln_series, 2 + p!1)" )"" "EST" "ln_estimate(ssx!1, 2 + p!1)" )"" (expand "round" )"" "floor(1 / 2 + CPS(2 + p!1) / 4)" )"" "RR" "floor(1 / 2 + CPS(2 + p!1) / 4)" )"" "" expand "cauchy_prop" )"" "2+p!1" )"" "" case "abs(LOG - EST)*2^p!1 < 1/4" )"1" "1" case "abs(LOG* 2 ^ p!1 - CPS(2 + p!1)/4) < 1/2" )"1" "1" "P2" "2 ^ p!1" )"1" nil nil ))nil ))nil )"2" "2" "abs_mult" "x" "LOG-EST" "y" "2^p!1" ))"2" expand "abs" "2" replace "2" "2" rewrite "expt_plus" )"2" rewrite "expt_x2" )"2" "P2" "2^p!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "ABS" "abs(LOG - EST)" )"2" "ssx!1" )"2" case "abs(ssx!1) ^ (2 + p!1 + 1) <= 1/2^(3+p!1)" )"1" case "1 <= IF ssx!1 < 0 THEN 1 + ssx!1 ELSE 1 ENDIF * (2 + p!1 + 1)" )"1" "le_div_le_pos" "nnx" "abs(ssx!1) ^ (2 + p!1 + 1)" "y" "1 / 2 ^ (3 + p!1)" "pz" "1" "w" "IF ssx!1 < 0 THEN 1 + ssx!1 ELSE 1 ENDIF * (2 + p!1 + 1)" ))"1" replace -3)"1" replace "1" "RHS" "abs(ssx!1) ^ (2 + p!1 + 1) / IF ssx!1 < 0 THEN 1 + ssx!1 ELSE 1 ENDIF * (2 + p!1 + 1))") "1" rewrite "div_div2" )"1" "both_sides_expt_gt1_lt" "gt1x" "2" "i" "2+p!1" "j" "3+p!1" ))"1" assert )"1" "1" "div_mult_pos_lt2" "py" "2^p!1" "x" "ABS" "z" "1/4" ))"1" replace "1" "1" rewrite "div_div2" )"1" "both_sides_div_pos_lt2" "pz" "1" "px" "2 ^ (3 + p!1)" "py" "2 ^ (2 + p!1)" ))"1" assert )"1" "expt_plus" "n0x" "2" "i" "2" "j" "p!1" ))"1" rewrite "expt_x2" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "ssx!1<0" )"1" "both_sides_times_pos_le1" "pz" "3+p!1" "x" "-1/2" "y" "ssx!1" ))"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" "ssx!1=0" )"1" expand "^" "1" expand "expt" "1" expand "abs" )"1" assert )nil nil ))nil ))nil ))nil )"2" "both_sides_expt_pos_le" "px" "abs(ssx!1)" "py" "1/2" "pm" "3+p!1" ))"1" "1" "1" "1" rewrite "inv_expt" )"1" assert )nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" cauchy nil )nil ln_exp_series_alt"lnexp_fnd/" )nil ln_exp_series_alt"lnexp_fnd/" )"cauchy_real" powerseries nil )nil sum nil )"bool" sum nil )nil cauchy nil )"bool" cauchy nil )"int" prelude_aux nil )nil inv nil )"real" ln_exp_series_alt "lnexp_fnd/" )"real" ln_exp "lnexp_fnd/" ))nil 3394115362"" (skosimp)"" (typepred "cssx!1" )"" (expand "cauchy_ln_small?" )"" (skosimp)"" (lemma "ln_drx_lemma" ("ssx" "x!1" "cssx" "cssx!1" ))"" (assert )"" (expand "cauchy_real?" )"" (inst + "ln(1+x!1)" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil log nil )"bool" log 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 )"real" reals nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fieldsnil )"real" ln_exp "lnexp_fnd/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" cauchy nil )nil log nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"[numfield -> numfield]" number_fields nil )nil log nil )"odd_int" integersnil ))nil ))nil 3394163248"" (lemma "lemma_div2n" ("x" "1" "cx" "cauchy_int(1)" "n" "1" ))"" (rewrite "int_lemma" )"" "neg_lemma" "x" "div2n(1, 1)" "cx" "cauchy_div2n(cauchy_int(1), 1)" ))"" (assert )"" (expand "div2n" )"" (rewrite "expt_x1" )"" (expand "cauchy_ln_small?" )"" (inst + "-(1/2)" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil int nil )"real" reals nil )nil exponentiation nil )"posint" exponentiation nil )"posrat" nil )"nzrat" rationalsnil )nil log nil )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" log nil )"odd_int" integers nil )nil neg nil )"cauchy_real" shift nil )"real" shift nil )nil shift 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 )"cauchy_real" int nil ))nil ))nil 3394163248"" (lemma "lemma_div2n" ("x" "1" "cx" "cauchy_int(1)" "n" "1" ))"" (rewrite "int_lemma" )"" (expand "div2n" )"" (rewrite "expt_x1" )"" "neg_lemma" "x" "1/2" "cx" "cauchy_div2n(cauchy_int(1), 1)" ))"" (assert )"" "ln_drx_lemma" "ssx" "-(1/2)" "cssx" "cauchy_neg(cauchy_div2n(cauchy_int(1), 1))" ))"" (assert )"" (assert )"" (lemma "ln_strict_increasing" )"" (expand "strict_increasing?" )"" (inst - "1/2" "1" )"" assert )"" expand "cauchy_negreal?" )"" "ln(1/2)" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil int nil )nil exponentiation nil )"posint" exponentiation nil )"nzrat" rationalsnil )nil application-judgement "cauchy_real" log nil )nil ln_exp "lnexp_fnd/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" cauchy nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" ln_exp "lnexp_fnd/" )"(total_order?[real])" nil )nil ln_exp "lnexp_fnd/" )"(strict_total_order?[real])" real_props nil )"bool" real_fun_preds "reals/" )nil log nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"cauchy_real" neg nil )nil log nil )"bool" log nil )nil log nil )"posrat" nil )nil neg nil )"cauchy_real" shift nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"real" shift nil )nil shift 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 )"cauchy_real" int nil ))nil ))nil 3394163580"" (expand "cauchy_ln_half" )"" "lemma_div2n" ("x" "1" "cx" "cauchy_int(1)" "n" "1" ))"" (rewrite "int_lemma" )"" (expand "div2n" )"" (rewrite "expt_x1" )"" "neg_lemma" "x" "1/2" "cx" "cauchy_div2n(cauchy_int(1), 1)" ))"" (assert )"" "ln_drx_lemma" "ssx" "-(1/2)" "cssx" "cauchy_neg(cauchy_div2n(cauchy_int(1), 1))" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"cauchy_real" int 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 shift nil )"real" shift nil )"posrat" nil )nil neg nil )"cauchy_real" shift nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil log nil )"bool" log nil )nil log nil )"cauchy_real" neg nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil log nil )nil application-judgement "cauchy_real" log nil )"nzrat" rationalsnil )"posint" exponentiation nil )nil exponentiation nil )nil int nil )"cauchy_negreal" log nil ))nil 3394116128"" (lemma "cauchy_ln_half_lemma" )"" (lemma "ln_div" ("px" "1" "py" "2" ))"" (replace -1)"" (expand "cauchy_ln2" )"" "neg_lemma" "x" "-ln(2)" "cx" "cauchy_ln_half" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil ln_exp "lnexp_fnd/" )"cauchy_posreal" log nil )nil ln_exp "lnexp_fnd/" )"cauchy_posreal" neg nil )"real" realsnil )"posrat" nil )"real" reals nil )nil neg nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" cauchy nil )nil cauchy nil )"bool" cauchy nil )nil cauchy nil )"cauchy_negreal" log nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"real" ln_exp "lnexp_fnd/" )nil log nil ))nil 3394115362"" (typepred "cauchy_ln2" )"" (expand "cauchy_posreal?" )"" (skosimp)"" (typepred "x!1" )"" "lemma_div2n" "x" "x!1" "cx" "cauchy_ln2" "n" "1" ))"" (assert )"" (expand "div2n" )"" (rewrite "expt_x1" )"" (inst + "x!1/2" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil exponentiation nil )"posint" exponentiation nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"posreal" nil )"real" shift nil )nil shift nil )"bool" cauchy nil )nil cauchy nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers 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 )"bool" reals nil )nil naturalnumbers nil )"bool" cauchy nil )nil cauchy nil )"cauchy_posreal" log nil ))nil ))nil 3394118462"" (lemma "cauchy_ln2_lemma" )"" (expand "cauchy_ln_sqrt2" )"" "lemma_div2n" "x" "ln(2)" "cx" "cauchy_ln2" "n" "1" ))"" (assert )"" (expand "div2n" )"" (rewrite "expt_x1" )"" (lemma "ln_expt" ("px" "sqrt(2)" "i" "2" ))"" (rewrite "expt_x2" )"" (rewrite "sq_rew" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"cauchy_posreal" log nil )"posreal" sqrt "reals/" )nil exponentiation nil )"posint" exponentiation nil )nil inv nil )"posreal" real_types nil )"real" realsnil )"real" realsnil )nil sqrt "reals/" )"posreal" sq "reals/" )"(total_order?[real])" nil )nil sq "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil real_types nil )nil integers nil )nil ln_exp "lnexp_fnd/" )"real" shift nil )nil shift 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_posreal" log nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" ln_exp "lnexp_fnd/" )nil log nil ))nil 3394127143"" (skosimp)"" (typepred "cmx!1" )"" (expand "cauchy_ln_med?" )"" (skosimp)"" (typepred "x!1" )"" "sub_lemma" "x" "x!1" "cx" "cmx!1" "y" "1" "cy" "cauchy_int(1)" ))"" (rewrite "int_lemma" )"" (assert )"" (expand "cauchy_prop" -4)"" (inst - "2" )"" (flatten)"" (rewrite "expt_x2" )"" case "1/2<x!1&x!1<3/2" )"1" "1" expand "cauchy_ln_small?" )"1" "x!1 - 1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil log nil )"bool" log 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 )"cauchy_real" int nil )nil cauchy nil )"bool" cauchy nil )nil sub nil )"(total_order?[real])" nil )nil inv nil )"(divides(n))" dividesnil )"even_int" nil )"posint" nil )"int" integers nil )"real" realsnil )"[numfield, numfield -> numfield]" number_fieldsnil )nil log nil )"[numfield -> numfield]" number_fields nil )"ln_medreal" log nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" realsnil )"int" integers nil )"bool" log nil )"odd_int" integers nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )"posrat" nil )"bool" cauchy nil )"posint" exponentiation nil )nil int nil )nil log nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ))nil ))nil 3394127143"" (skosimp*)"" (typepred "cmx!1" )"" (expand "cauchy_ln_med?" )"" (skosimp)"" (lemma "sqrt_lemma" ("nnx" "x!1" "nncx" "cmx!1" ))"" (assert )"" (typepred "x!1" )"" "sub_lemma" "x" "sqrt(x!1)" "cx" "cauchy_sqrt(cmx!1)" "y" "1" "cy" "cauchy_int(1)" ))"" (rewrite "int_lemma" )"" (assert )"" "sqrt_le" "nny" "sq(1/2)" "nnz" "x!1" ))"" "sqrt_le" "nnz" "sq(3/2)" "nny" "x!1" ))"" expand "sq" -1 2)"" expand "sq" -2 2)"" assert )"" expand "cauchy_ln_small?" )"" "sqrt(x!1) - 1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil log nil )"bool" log 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 )"(total_order?[real])" nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"cauchy_real" int nil )"cauchy_nnreal" sqrtx nil )nil cauchy nil )"bool" cauchy nil )nil sub nil )"odd_int" integers nil )"bool" log nil )"[numfield -> numfield]" number_fields nil )nil log nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil sqrt "reals/" )"posreal" sqrt "reals/" )"posreal" sq "reals/" )"(strict_total_order?[real])" real_props nil )"real" realsnil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )"nonneg_real" sq "reals/" )nil sqrt "reals/" )"posrat" nil )nil int nil )"(total_order?[real])" nil )nil sqrtx nil )"bool" cauchy nil )nil cauchy nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil log nil ))nil ))nil 3394127143 ("" (subtype-tcc) nil nil )"real" exponentiation nil )"bool" cauchy nil )"posnat" exponentiationnil ))nil ))nil 3394127185"" (skosimp)"" (expand "cauchy_ln_dr" )"" (case-replace "3 <= cmx!1(2) AND cmx!1(2) <= 5" )"1" (flatten)"1" "sub_lemma" "x" "mx!1" "cx" "cmx!1" "y" "1" "cy" "cauchy_int(1)" ))"1" (rewrite "int_lemma" )"1" (assert )"1" (expand "cauchy_prop" -4)"1" (inst - "2" )"1" (rewrite "expt_x2" )"1" (flatten)"1" (case "1/2<mx!1&mx!1<3/2" )"1" "1" "ln_drx_lemma" "ssx" "mx!1 - 1" "cssx" "cauchy_sub(cmx!1, cauchy_int(1))" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace 1 2)"2" (hide 1)"2" "sqrt_lemma" ("nnx" "mx!1" "nncx" "cmx!1" ))"2" (assert )"2" "sub_lemma" "x" "sqrt(mx!1)" "cx" "cauchy_sqrt(cmx!1)" "y" "1" "cy" "cauchy_int(1)" ))"2" (rewrite "int_lemma" )"2" (assert )"2" (typepred "mx!1" )"2" "sqrt_le" "nny" "sq(1/2)" "nnz" "mx!1" ))"2" "sqrt_le" "nnz" "sq(3/2)" "nny" "mx!1" ))"2" expand "sq" -1 2)"2" expand "sq" -2 2)"2" assert )"2" "ln_drx_lemma" "ssx" "sqrt(mx!1) - 1" "cssx" "cauchy_sub(cauchy_sqrt(cmx!1), cauchy_int(1))" ))"2" assert )"2" "lemma_mul2n" "x" "ln(sqrt(mx!1))" "cx" "cauchy_ln_drx(cauchy_sub(cauchy_sqrt(cmx!1),cauchy_int(1)))" "n" "1" ))"2" assert )"2" expand "mul2n" )"2" rewrite "expt_x1" )"2" "ln_expt" "px" "sqrt(mx!1)" "i" "2" ))"2" rewrite "expt_x2" )"2" rewrite "sq_rew" )"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 )"cauchy_real" log nil )nil real_types nil )nil cauchy nil )"bool" cauchy nil )nil sqrtx nil )"(total_order?[real])" nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt"reals/" )"[numfield, numfield -> numfield]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil real_types nil )"cauchy_nnreal" sqrtx nil )nil sqrt "reals/" )"nonneg_real" sq "reals/" )"posreal" sq "reals/" )"posreal" sqrt "reals/" )nil sqrt "reals/" )nil exponentiation nil )"nnreal" nil )nil sqrt "reals/" )nil sq "reals/" )nil integers nil )nil ln_exp "lnexp_fnd/" )"real" shift nil )"real" ln_exp "lnexp_fnd/" )nil real_types nil )"bool" reals nil )"int" log nil )nil shift nil )NOT const-decl "[bool -> bool]" booleans nil )nil int nil )"posint" exponentiation nil )"bool" cauchy nil )nil inv nil )"(divides(n))" dividesnil )"even_int" nil )"posint" nil )"int" integers nil )"posrat" nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"real" realsnil )nil log nil )"bool" log nil )nil log nil )"cauchy_real" sub nil )"[numfield -> numfield]" number_fields nil )nil log nil )"[numfield, numfield -> numfield]" number_fieldsnil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" realsnil )"int" integers nil )"(total_order?[real])" nil )nil application-judgement "cauchy_real" log nil )nil sub nil )"bool" cauchy nil )nil cauchy nil )"cauchy_real" int nil )nil log nil )nil log nil )"bool" log nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil numbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3394113740"" (skosimp)"" (typepred "cgt!1" )"" (expand "cauchy_gt_quarter?" )"" (skosimp)"" (expand "cauchy_ln_med?" )"" (inst + "x!1" )"" (expand "cauchy_prop" )"" (inst - "2" )"" (rewrite "expt_x2" )"" (flatten) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil log nil )"bool" log 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 )"(total_order?[real])" nil )nil log nil )"bool" reals nil )nil log nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal_gt_quarter" log nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"real" realsnil )"int" integers nil )"int" integers nil )"posint" nil )"even_int" nil )"(divides(n))" dividesnil )nil inv nil )"bool" cauchy nil )"posint" exponentiation nil )"bool" log nil ))nil ))nil 3394113740 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers 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 )"bool" reals nil )nil naturalnumbers nil )"bool" log nil )nil log nil )"posnat" exponentiation nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" cauchy nil )"real" exponentiation nil ))nil ))nil 3394113740"" (skosimp*)"" (case "8<=t!1" )"1" (hide 1)"1" (rewrite "floor_log2_def" )"1" (case "3<=log2(t!1)" )"1" "floor_plus_int" ("i" "3" "x" "log2(t!1)-3" ))"1" "nonneg_floor_is_nat" ("x" "log2(t!1) - 3" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil )"2" (hide-all-but (-1 1))"2" (lemma "ln_strict_increasing" )"2" (expand "<=" -2)"2" (split -2)"1" (expand "strict_increasing?" )"1" (inst-cp - "2^3" "t!1" )"1" (rewrite "ln_expt" )"1" expand "log2" )"1" rewrite "expt_x3" )"1" assert )"1" rewrite "div_mult_pos_le2" )"1" "1" "2" )"1" assert )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (expand "log2" )"2" (case-replace "t!1=2^3" )"1" (rewrite "ln_expt" )"1" (assert ) nil nil )) nil )"2" (rewrite "expt_x3" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil )nil appendix nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"(total_order?[real])" nil )"[T, T -> boolean]" equalities nil )"bool" real_fun_preds "reals/" )nil ln_exp "lnexp_fnd/" )"real" realsnil )nil exponentiation nil )"(divides(m))" dividesnil )"(divides(n))" dividesnil )"even_int" nil )"posint" nil )"int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"real" ln_exp "lnexp_fnd/" )nil real_props nil )nil ln_exp "lnexp_fnd/" )"(strict_total_order?[real])" real_props nil )"real" realsnil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"int" log nil )"posint" exponentiation nil )nil ln_exp "lnexp_fnd/" )"real" realsnil )nil floor_ceil nil )nil integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil )"int" integers nil )"int" integers nil )"real" reals nil )nil floor_ceil nil )"real" prelude_aux nil )nil real_types nil )nil real_types nil ))nil ))nil 3394127143"" (skosimp*)"" (case "9<=cgt!1(2)" )"1" (hide 1)"1" (typepred "cgt!1" )"1" (expand "cauchy_gt_quarter?" )"1" (skosimp)"1" (typepred "floor_log2(t!1)" )"1" "lemma_A3" "i" "floor_log2(t!1)" "px" "t!1" ))"1" (rewrite "floor_log2_def" )"1" (flatten)"1" (case "n!1>=2" )"1" "floor(log2(t!1))=n!1+1" )"1" "1" assert )"1" "1" "lemma_div2n" "x" "x!1" "cx" "cgt!1" "n" "n!1" ))"1" assert )"1" expand "div2n" )"1" case "1/4<=x!1 / 2 ^ n!1&x!1 / 2 ^ n!1<=9/4" )"1" "1" expand "cauchy_ln_med?" )"1" "x!1 / 2 ^ n!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "cauchy_prop" )"2" "2" )"2" rewrite "expt_x2" )"2" "2" case "2^(n!1-2)<=x!1&x!1<=9*2^(n!1-2)" )"1" "1" "expt_plus" "n0x" "2" "i" "n!1" "j" "-2" ))"1" rewrite "expt_inverse" )"1" rewrite "expt_x2" )"1" replace "1" "1" "1" rewrite "div_mult_pos_le2" "1" assert )nil nil ))nil )"2" rewrite "div_mult_pos_le1" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" "2" case "2 ^ n!1 <= 4*x!1 & 4*x!1 <= 9 * 2 ^ n!1" )"1" "1" "expt_plus" "n0x" "2" "i" "n!1" "j" "-2" ))"1" rewrite "expt_inverse" )"1" rewrite "expt_x2" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "X4" "4 * x!1" )"2" case "2^n!1<=t!1-1&t!1+1<=9*2^n!1" )"1" "1" assert )nil nil ))nil )"2" "2" rewrite "expt_plus" )"2" rewrite "expt_plus" )"2" rewrite "expt_x1" )"2" rewrite "expt_x2" )"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 )"2" (assert ) nil nil ))nil )"2" (case-replace "n!1=-1" )"1" assert )"1" assert )"1" (grind) nil nil ))nil ))nil )"2" "n!1=0" )"1" assert )"1" "floor(log2(t!1)) =1" )"1" rewrite "expt_x2" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" "n!1=1" )"1" assert )"1" "floor(log2(t!1))=2" )"1" rewrite "expt_x3" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )nil log nil )"bool" log nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil appendix nil )nil real_types nil )nil real_types nil )"odd_int" integers nil )"cauchy_real" shift nil )"real" exponentiation nil )"real" ln_exp "lnexp_fnd/" )"real" integral_def "analysis/" )"posreal" nil )"posnat" exponentiation nil )"int" integers nil )"(divides(m))" dividesnil )nil exponentiation nil )"real" prelude_aux nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[T, T -> boolean]" equalities nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"(total_order?[real])" nil )nil shift nil )"bool" cauchy nil )nil cauchy nil )nil log nil )"real" shift nil )nil exponentiation nil )"odd_int" integersnil )"real" realsnil )nil exponentiation nil )nil real_props nil )nil real_props nil )nil reals nil )"[numfield -> numfield]" number_fields nil )nil exponentiation nil )"even_int" integersnil )"nzint" integersnil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"posrat" nil )"int" integers nil )"int" integers nil )"posint" nil )"even_int" nil )"(divides(n))" dividesnil )nil inv nil )"bool" cauchy nil )"posint" exponentiation nil )nil log nil )"posreal_gt_quarter" log nil )"int" log nil )"bool" log nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )"real" realsnil )"posrat" nil )nil appendix nil )"(total_order?[real])" nil )nil integers nil )"bool" reals nil )nil integers nil )"nat" appendix nil ))nil ))nil 3394109924"" (skosimp) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil ))nil ))nil 3394172288"" (skosimp)"" (expand "cauchy_lnx" )"" (case-replace "cgt!1(2) <= 8" )"1" (lemma "ln_dr_lemma" ("mx" "gt!1" "cmx" "cgt!1" ))"1" (assert ) nil nil )"2" (hide 2)"2" (expand "cauchy_prop" )"2" (inst - "2" )"2" (rewrite "expt_x2" )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (case "9<=cgt!1(2)" )"1" (hide 1)"1" (rewrite "floor_log2_def" )"1" "lemma_A3" "i" "floor(log2(cgt!1(2)))" "px" "cgt!1(2)" ))"1" (assert )"1" (flatten)"1" (typepred "floor_log2(cgt!1(2))" )"1" (rewrite "floor_log2_def" )"1" "N" "floor(log2(cgt!1(2)))" )"1" case "N>=2" )"1" "lemma_div2n" "x" "gt!1" "cx" "cgt!1" "n" "N-1" ))"1" assert )"1" expand "cauchy_prop" -7)"1" "2" )"1" rewrite "expt_x2" )"1" "1" expand "div2n" )"1" case "1/4<=gt!1 / 2 ^ (N - 1)>!1 / 2 ^ (N - 1)<=9/4" )"1" "1" "ln_dr_lemma" "mx" "gt!1 / 2 ^ (N - 1)" "cmx" "cauchy_div2n(cgt!1, N - 1)" ))"1" assert )"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" "add_lemma" "x" "ln(gt!1 / 2 ^ (N - 1))" "cx" "cauchy_ln_dr(cauchy_div2n(cgt!1, N - 1))" "y" "(N - 1) * ln(2)" "cy" "cauchy_mul(cauchy_int(N - 1), cauchy_ln2)" ))"1" assert )"1" "ln(gt!1 / 2 ^ (N - 1)) + ln(2) * N - ln(2)=ln(gt!1)" )"1" "1" rewrite "ln_div" )"1" rewrite "ln_expt" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" case "2^(N-3)<=gt!1>!1<9*2^(N-3)" )"1" "1" "expt_plus" "n0x" "2" "i" "N" "j" "-1" ))"1" "expt_plus" "n0x" "2" "i" "N" "j" "-2" ))"1" "expt_plus" "n0x" "2" "i" "N" "j" "-3" ))"1" rewrite "expt_inverse" )"1" rewrite "expt_inverse" )"1" rewrite "expt_inverse" )"1" rewrite "expt_x1" )"1" rewrite "expt_x2" )"1" rewrite "expt_x3" )"1" replace "1" replace "1" "1" assert )"1" "1" rewrite "div_mult_pos_le2" nil nil )"2" rewrite "div_mult_pos_le1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" case "cgt!1(2)/4 - 1/4 <gt!1>!1 < 1/4 + cgt!1(2)/4" )"1" "1" "1" case "2 ^ (N - 3) <= (2 ^ N-1)/4 & (2^(1+N)+1)/4 <=9 * 2 ^ (N - 3)" )"1" "1" assert )nil nil ))nil )"2" "2" rewrite "expt_plus" )"2" "expt_plus" "n0x" "2" "i" "N" "j" "-3" ))"2" rewrite "expt_inverse" )"2" rewrite "expt_x1" )"2" rewrite "expt_x3" )"2" replace "2" assert )"2" "both_sides_expt_gt1_le" "gt1x" "2" "i" "2" "j" "N" ))"2" rewrite "expt_x2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "2" "N=0" )"1" rewrite "expt_x1" )"1" (assert ) nil nil ))nil )"2" "N=1" )"1" rewrite "expt_x2" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"[nat -> int]" log nil )"real" prelude_aux nil )nil real_types nil )nil real_types nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )nil integers nil )nil appendix nil )"posrat" nil )"real" realsnil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"cauchy_real" shift nil )nil mul nil )"cauchy_real" int nil )"bool" cauchy nil )nil cauchy nil )"cauchy_posreal" log nil )"real" ln_exp "lnexp_fnd/" )nil log nil )"real" reals nil )nil ln_exp "lnexp_fnd/" )nil ln_exp "lnexp_fnd/" )"odd_int" integers nil )"real" realsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"cauchy_real" mul nil )"cauchy_real" log nil )nil add nil )nil int nil )"posrat" nil )nil exponentiation nil )"[numfield -> numfield]" number_fields nil )nil reals nil )nil exponentiation nil )nil exponentiation nil )"(divides(m))" dividesnil )nil real_props nil )nil real_props nil )nil exponentiation nil )"even_int" integersnil )"nzint" integersnil )"rat" rationalsnil )"posrat" nil )nil exponentiation nil )"rat" rationals nil )"rat" rationalsnil )"real" shift nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil cauchy nil )"bool" cauchy nil )nil shift nil )"[T, T -> boolean]" equalities nil )"nat" appendix nil )NOT const-decl "[bool -> bool]" booleans nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )nil integers nil )"bool" reals nil )nil integers nil )nil appendix nil )"(total_order?[real])" nil )nil log nil )"bool" reals nil )nil log nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil log nil )"bool" log nil )nil log nil )"(total_order?[real])" nil )"posint" exponentiation nil )"bool" cauchy nil )nil inv nil )"(divides(n))" dividesnil )"even_int" nil )"posint" nil )"int" integers nil )"int" integers nil )"real" realsnil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil log nil )"bool" log nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))nil 3394172287"" (skosimp)"" (typepred "cgt!1" )"" (expand "cauchy_gt_quarter?" )"" (skosimp)"" "ln_lemma_x" ("cgt_14" "cgt!1" "gt_14" "x!1" ))"" (expand "cauchy_real?" )"" (inst + "ln(x!1)" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil log nil )"bool" log 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 )"real" ln_exp "lnexp_fnd/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil log nil )"bool" reals nil )nil log nil ))nil ))nil 3394109924"" (skosimp)"" (typepred "pcx!1" )"" (expand "cauchy_posreal?" )"" (skosimp)"" (lemma "inv_lemma" ("nzx" "x!1" "nzcx" "pcx!1" ))"" (assert )"" (expand "cauchy_gt_quarter?" )"" (inst + "1/x!1" )"" (hide -1)"" (expand "cauchy_prop" )"" (inst - "2" )"" (rewrite "expt_x2" )"" "" assert )"" case "0<x!1&x!1<3/4" )"1" "1" "both_sides_div_pos_lt2" "pz" "1" "py" "x!1" "px" "3/4" ))"1" rewrite "div_div1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil 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 )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )nil number_fields nil )nil log nil )"bool" reals nil )"posreal" log nil )"posint" exponentiation nil )"bool" cauchy nil )nil inv nil )"(divides(n))" dividesnil )"even_int" nil )"posint" nil )"int" integers nil )"int" integers nil )"posreal" real_types nil )"int" integers nil )nil reals nil )nil real_props nil )"even_int" nil )nil real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posrat" nil )"bool" log nil )nil inv nil )"bool" cauchy nil )nil cauchy nil )"boolean" notequal nil )nil reals nil )nil real_types nil )"bool" reals nil )nil real_types nil ))nil ))nil 3394109924"" (skosimp)"" (case "3<=pcx!1(2)" )"1" (hide 1)"1" (typepred "pcx!1" )"1" (expand "cauchy_posreal?" )"1" (skosimp)"1" (expand "cauchy_gt_quarter?" )"1" (inst + "x!1" )"1" (expand "cauchy_prop" )"1" (inst - "2" )"1" (rewrite "expt_x2" )"1" (flatten) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) 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 )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil log nil )"bool" reals nil )"posreal" log nil )"int" integers nil )"posreal" real_types nil )"int" integers nil )"(total_order?[real])" nil )"int" integers nil )"posint" nil )"even_int" nil )"(divides(n))" dividesnil )nil inv nil )"bool" cauchy nil )"posint" exponentiation nil )"bool" log nil ))nil ))nil 3394110574"" (skosimp)"" (expand "cauchy_ln" )"" (case-replace "pcx!1(2) <= 2" )"1" (lemma "inv_lemma" ("nzx" "px!1" "nzcx" "pcx!1" ))"1" (assert )"1" (expand "cauchy_prop" -3)"1" (inst - "2" )"1" (rewrite "expt_x2" )"1" (flatten)"1" (case "0<px!1&px!1<3/4" )"1" (flatten)"1" "both_sides_div_pos_lt2" "pz" "1" "px" "3/4" "py" "px!1" ))"1" rewrite "div_div1" )"1" assert )"1" "ln_lemma_x" "gt_14" "1/px!1" "cgt_14" "cauchy_inv(pcx!1)" ))"1" assert )"1" "neg_lemma" "x" "ln(1 / px!1)" "cx" "cauchy_lnx(cauchy_inv(pcx!1))" ))"1" assert )"1" "ln_div" "px" "1" "py" "px!1" ))"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "3<=pcx!1(2)" )"1" (assert )"1" (hide 1)"1" "ln_lemma_x" "gt_14" "px!1" "cgt_14" "pcx!1" ))"1" (assert ) nil nil )"2" (hide 2)"2" (expand "cauchy_prop" )"2" (inst - "2" )"2" (rewrite "expt_x2" )"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"cauchy_real" log nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil reals nil )"boolean" notequal nil )nil cauchy nil )"bool" cauchy nil )nil inv nil )"posint" exponentiation nil )"bool" cauchy nil )nil inv nil )"(divides(n))" dividesnil )"even_int" nil )"posint" nil )"int" integers nil )"posrat" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil real_props nil )"int" integers nil )"posreal" real_types nil )"int" integers nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil ln_exp "lnexp_fnd/" )"real" realsnil )nil ln_exp "lnexp_fnd/" )"real" ln_exp "lnexp_fnd/" )"[nat -> int]" log nil )nil cauchy nil )"bool" cauchy nil )nil neg nil )nil log nil )"cauchy_nzreal" inv nil )nil log nil )"bool" log nil )nil log nil )"even_int" nil )nil real_props nil )nil reals nil )"(total_order?[real])" nil )nil application-judgement "cauchy_real" log 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 )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.303Bemerkung:
(vorverarbeitet am 2026-04-26)
¤ *© Formatika GbR, Deutschland
2026-05-26
