Quellcode-Bibliothek exp_approx.prf
Sprache: Lisp
(exp_approxnil 3307800311"" (expand "exp_neg_le1_lb" )"" (expand "exp_neg_le1_ub" )"" (skosimp)"" (case "FORALL (n:nat): 0 < x!1^(2*n) & x!1^(2*n) <= 1" )"1" case "FORALL (n:nat): -1 <= x!1^(2*n+1) & x!1^(2*n+1) < 0" )"1" (case "max(exp(x!1), 1) = 1" )"1" case "FORALL (n,m:posnat): n < m => abs(x!1)^m/factorial(m) < abs(x!1)^n/factorial(n)" )"1" "FORALL (n: nat, x: real): LAMBDA (nn: nat):IF nn = 0 THEN 1 ELSE x ^ nn / factorial(nn) ENDIF)") "1" (hide -1)"1" "exp_estimate(x!1, 1 + 2 * n!1) < exp(x!1)" )"1" "exp_taylors_err" "x" "x!1" "n" "1+2*n!1" ))"1" (reveal -1)"1" (copy -1)"1" (inst?)"1" replace -1)"1" "1" "1" replace -1)"1" "1" expand "abs" -1 1)"1" assert )"1" replace -4)"1" "1" expand "sigma" -1 1)"1" "RHS" "sigma(0, 2 * n!1, LAMBDA (nn: nat):IF nn = 0 THEN 1 ELSE x!1 ^ nn / factorial(nn) ENDIF)") "1" case "(x!1^(1+2*n!1))/factorial(1+2*n!1) + abs(x!1)^(2+2*n!1)/factorial(2+2*n!1) < 0" )"1" assert )nil nil )"2" "1+2*n!1" "2+2*n!1" )"2" assert )"2" "abs(x!1) ^ (1 + 2 * n!1) = -(x!1^(1+2*n!1))" )"1" assert )nil nil )"2" "2" "2" rewrite "expt_plus" )"2" rewrite "expt_plus" )"2" rewrite "expt_times" )"2" rewrite "expt_times" )"2" expand "abs" )"2" "(-x!1) ^ 2=x!1 ^ 2" )"1" assert )"1" "1" nil nil ))nil ))nil )"2" "2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "exp_taylors_err" "x" "x!1" "n" "2+2*n!1" ))"2" (reveal -1)"2" (inst?)"2" replace -1)"2" "2" "2" "2" replace -1)"2" "2" replace -3)"2" expand "abs" -1 1)"2" expand "sigma" -1)"2" "LB" "sigma(0, 1 + 2 * n!1, LAMBDA (nn: nat):IF nn = 0 THEN 1 ELSE x!1 ^ nn / factorial(nn) ENDIF)") "2" "exp(x!1) - LB - (x!1 ^ (2 + 2 * n!1)) / factorial(2 + 2 * n!1) < 0" )"1" "1" case "x!1^(2+2*n!1) / factorial(2+2*n!1) - abs(x!1)^(3+2*n!1)/factorial(3+2*n!1) > 0" )"1" assert )nil nil )"2" "2" "2+2*n!1" "3+2*n!1" )"2" assert )"2" "abs(x!1) ^ (2 + 2 * n!1) = x!1 ^ (2 + 2 * n!1)" )"1" assert )nil nil )"2" "2" "expt_times" "i" "2" "j" "1+n!1" ))"2" "abs(x!1)" )"2" "x!1" )"2" "abs(x!1)^2 = x!1^2" )"1" assert )nil nil )"2" "2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "(x!1 ^ (2 + 2 * n!1)) / factorial(2 + 2 * n!1) > 0" )"1" assert )nil nil )"2" "2" "1+n!1" )"2" "2" "posreal_div_posreal_is_posreal" "px" "x!1 ^ (2 + 2 * n!1)" "py" "factorial(2 + 2 * n!1)" ))"1" nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skosimp*)"2" (expand "exp_estimate" )"2" (lemma "sigma_first" )"2" "LAMBDA (nn: nat): IF nn = 0 THEN 1 ELSE x!2 ^ nn / factorial(nn) ENDIF" "n!2" "0" )"2" (case-replace "n!2 > 0 " )"1" assert )"1" replace -2)"1" assert )"1" "1" rewrite "sigma_restrict_eq" )"1" "1" expand "restrict" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "n!2 = 0" )"1" assert )"1" "1" expand "sigma" )"1" expand "sigma" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-4 -5 1))"2" (skosimp)"2" case "forall (n,m:posnat): factorial(n) < factorial(n+m)" )"1" (case "abs(x!1) ^ m!1 <= abs(x!1) ^ n!2" )"1" "lt_div_lt_pos1" "px" "abs(x!1) ^ m!1" "w" "factorial(m!1)" "y" "abs(x!1) ^ n!2" "pz" "factorial(n!2)" ))"1" (split -1)"1" (propax) nil nil )"2" (propax) nil nil )"3" (inst - "n!2" "m!1-n!2" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil )"2" "expt_pos" "px" "abs(x!1)" "i" "m!1" ))"1" (propax) nil nil )"2" (expand "abs" )"2" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2 -1)"2" (case-replace "abs(x!1)=1" )"1" (rewrite "expt_1i" )"1" rewrite "expt_1i" )"1" (assert ) nil nil ))nil ))nil )"2" (case "abs(x!1)<1" )"1" "both_sides_expt_lt1_lt" "lt1x" "abs(x!1)" "i" "m!1" "j" "n!2" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" expand "abs" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2 -3 2)"2" (hide -1)"2" (induct "m" )"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (skosimp*)"3" "j!1=0" )"1" expand "factorial" 1 2)"1" "both_sides_times_pos_lt1" "pz" "factorial(n!3)" "x" "1" "y" "1+n!3" ))"1" (assert ) nil nil ))nil ))nil )"2" assert )"2" "n!3" )"2" expand "factorial" 2 2)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-4 1))"2" (expand "max" )"2" (lemma "exp_strict_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "x!1" "0" )"2" (rewrite "exp_0" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (inst - "n!2" )"2" (flatten)"2" (rewrite "expt_plus" 1)"2" "both_sides_times_neg_lt1" "nz" "x!1" "y" "0" "x" "x!1^(2*n!2)" ))"1" "both_sides_times_neg_le1" "nz" "x!1" "x" "1" "y" "x!1^(2*n!2)" ))"1" (assert )"1" (name-replace "AA" "x!1 ^ (2 * n!2)" )"1" (grind) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (rewrite "expt_times" 1)"2" (case "0 < x!1^2 & x!1^2<=1" )"1" (flatten)"1" (lemma "expt_pos" ("i" "n!2" "px" "x!1^2" ))"1" (expand "<=" -3)"1" (split -3)"1" (case-replace "n!2=0" )"1" (rewrite "expt_x0" )"1" (assert ) nil nil )) nil )"2" "both_sides_expt_pos_lt" "px" "x!1^2" "py" "1" "pm" "n!2" ))"1" rewrite "expt_1i" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (replace -1)"2" (rewrite "expt_1i" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" "negreal_times_negreal_is_posreal" "nx" "x!1" "ny" "x!1" ))"1" (lemma "le_times_le_neg" )"1" (inst - "x!1" "x!1" "-1" "-1" )"1" (expand "^" )"1" (expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" exp_approx nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )AND const-decl "[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]" number_fieldsnil )nil booleans nil )nil numbers nil )"[bool, bool -> bool]" booleans nil )nil real_props nil )nil real_types nil )nil real_types nil )nil real_props nil )"{z: posreal | z >= x AND z >= y}" real_defs nil )"[T, T -> boolean]" equalities nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil real_types nil )"bool" reals nil )nil real_types nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )nil exponentiation nil )nil exponentiation nil )nil real_props nil )"int" integers nil )"posnat" exp_approx nil )"posnat" exp_approx nil )"int" integers nil )nil exponentiation nil )nil real_props nil )nil naturalnumbers nil )nil defined_types nil )NOT const-decl "[bool -> bool]" booleans nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"real" exp_series nil )"real" reals nil )"odd_int" integers nil )"posint" nil )"nnreal" exponentiation nil )"real" reals nil )nil reals nil )nil exponentiation nil )nil exponentiation nil )"real" exponentiation nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"even_int" integersnil )"nnreal" nil )nil exp_series nil )"real" reals nil )nil real_types nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )"[T -> real]" sigma "reals/" )nil sigma "reals/" )"posnat" factorial "ints/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil integers nil )nil integers nil )"nnreal" nil )"bool" real_fun_preds "reals/" )nil ln_exp nil )nil ln_exp nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"odd_int" integers nil )"posint" nil )"odd_int" integers nil )nil exponentiation nil )nil exponentiation nil )nil real_types nil )"real" exp_approx nil )nil real_props nil )"real" exp_approx nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil ))nil )nil 3307367265"" (expand "exp_neg_le1_lb" )"" (expand "exp_neg_le1_ub" )"" (skosimp)"" (case "FORALL (n:nat): 0 < x!1^(2*n) & x!1^(2*n) <= 1" )"1" case "FORALL (n:nat): -1 <= x!1^(2*n+1) & x!1^(2*n+1) < 0" )"1" (case "max(exp(x!1), 1) = 1" )"1" case "FORALL (n,m:posnat): n < m => abs(x!1)^m/factorial(m) < abs(x!1)^n/factorial(n)" )"1" "exp_estimate(x!1, 1 + 2 * n!1) < exp(x!1)" )"1" (lemma "exp_series" ("x" "x!1" "n" "1+2*n!1" ))"1" (expand "abs" -1 1)"1" (assert )"1" (replace -4)"1" (hide -2)"1" (expand "exp_estimate" )"1" expand "sigma" -1 1)"1" "RHS" "sigma(0, 2 * n!1, LAMBDA (nn: nat):IF nn = 0 THEN 1 ELSE x!1 ^ nn / factorial(nn) ENDIF)") "1" case "(x!1^(1+2*n!1))/factorial(1+2*n!1) + abs(x!1)^(2+2*n!1)/factorial(2+2*n!1) < 0" )"1" (assert ) nil )"2" "1+2*n!1" "2+2*n!1" )"2" assert )"2" "abs(x!1) ^ (1 + 2 * n!1) = -(x!1^(1+2*n!1))" )"1" (assert ) nil )"2" "2" "2" rewrite "expt_plus" )"1" rewrite "expt_plus" )"1" rewrite "expt_x1" )"1" rewrite "expt_x1" )"1" rewrite "expt_times" )"1" rewrite "expt_times" )"1" expand "abs" )"1" "(-x!1) ^ 2=x!1 ^ 2" )"1" assert )nil )"2" "2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" assert )nil )))))))))))))))))"2" expand "abs" )"2" assert )nil )))))))))))"2" expand "abs" )"2" assert )nil )))))))))))))))))))))))))))))))))"2" (hide 2)"2" "exp_series" ("x" "x!1" "n" "2+2*n!1" ))"2" (replace -3)"2" (expand "abs" -1 1)"2" (expand "exp_estimate" )"2" (expand "sigma" -1)"2" "LB" "sigma(0, 1 + 2 * n!1, LAMBDA (nn: nat):IF nn = 0 THEN 1 ELSE x!1 ^ nn / factorial(nn) ENDIF)") "2" "exp(x!1) - LB - (x!1 ^ (2 + 2 * n!1)) / factorial(2 + 2 * n!1) < 0" )"1" "1" case "x!1^(2+2*n!1) / factorial(2+2*n!1) - abs(x!1)^(3+2*n!1)/factorial(3+2*n!1) > 0" )"1" (assert ) nil )"2" "2" "2+2*n!1" "3+2*n!1" )"2" assert )"2" "abs(x!1) ^ (2 + 2 * n!1) = x!1 ^ (2 + 2 * n!1)" )"1" (assert ) nil )"2" "2" "expt_times" "i" "2" "j" "1+n!1" ))"2" "abs(x!1)" )"1" "x!1" )"1" "abs(x!1)^2 = x!1^2" )"1" assert )nil )"2" "2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" expand "abs" )"2" assert )nil )))))))))))))))))"2" expand "abs" )"2" assert )nil )))))))))))))))))))))"2" "2" case "(x!1 ^ (2 + 2 * n!1)) / factorial(2 + 2 * n!1) > 0" )"1" (assert ) nil )"2" "2" "1+n!1" )"2" "2" "posreal_div_posreal_is_posreal" "px" "x!1 ^ (2 + 2 * n!1)" "py" "factorial(2 + 2 * n!1)" ))"1" (propax) nil )"2" assert )nil )))))))))))))))))))))))))))))))"2" (hide-all-but (-4 -5 1))"2" (skosimp)"2" case "forall (n,m:posnat): factorial(n) < factorial(n+m)" )"1" (case "abs(x!1) ^ m!1 <= abs(x!1) ^ n!2" )"1" "lt_div_lt_pos1" "px" "abs(x!1) ^ m!1" "w" "factorial(m!1)" "y" "abs(x!1) ^ n!2" "pz" "factorial(n!2)" ))"1" (split -1)"1" (propax) nil ) ("2" (propax) nil )"3" (inst - "n!2" "m!1-n!2" )"1" (assert ) nil )"2" (assert ) nil )))))"2" "expt_pos" "px" "abs(x!1)" "i" "m!1" ))"1" (propax) nil )"2" (expand "abs" )"2" (assert ) nil )))))))"2" (hide 2 -1)"2" (case-replace "abs(x!1)=1" )"1" (rewrite "expt_1i" )"1" rewrite "expt_1i" )"1" (assert ) nil )))))"2" (case "abs(x!1)<1" )"1" "both_sides_expt_lt1_lt" "lt1x" "abs(x!1)" "i" "m!1" "j" "n!2" ))"1" (assert ) nil )"2" assert )"2" expand "abs" )"2" (assert ) nil )))))))"2" expand "abs" )"2" (assert ) nil )))))))))))"2" (hide -2 -3 2)"2" (hide -1)"2" (induct "m" )"1" (assert ) nil ) ("2" (assert ) nil )"3" (skosimp*)"3" "j!1=0" )"1" expand "factorial" 1 2)"1" "both_sides_times_pos_lt1" "pz" "factorial(n!3)" "x" "1" "y" "1+n!3" ))"1" (assert ) nil )))))"2" assert )"2" "n!3" )"2" expand "factorial" 2 2)"2" assert )nil )))))))))))))))))))))))))"2" (hide-all-but (-4 1))"2" (expand "max" )"2" (lemma "exp_strict_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "x!1" "0" )"2" (rewrite "exp_0" )"2" (assert ) nil )))))))))))))))"2" (hide 2)"2" (skosimp)"2" (inst - "n!2" )"2" (flatten)"2" (rewrite "expt_plus" 1)"2" (rewrite "expt_x1" 1)"2" "both_sides_times_neg_lt1" "nz" "x!1" "y" "0" "x" "x!1^(2*n!2)" ))"1" "both_sides_times_neg_le1" "nz" "x!1" "x" "1" "y" "x!1^(2*n!2)" ))"1" (assert ) nil )))"2" (assert ) nil )))))))))))))))))"2" (hide 2)"2" (skosimp)"2" (rewrite "expt_times" 1)"2" (case "0 < x!1^2 & x!1^2<=1" )"1" (flatten)"1" (lemma "expt_pos" ("i" "n!2" "px" "x!1^2" ))"1" (expand "<=" -3)"1" (split -3)"1" (case-replace "n!2=0" )"1" (rewrite "expt_x0" )"1" (assert ) nil )))"2" "both_sides_expt_pos_lt" "px" "x!1^2" "py" "1" "pm" "n!2" ))"1" rewrite "expt_1i" )"1" (assert ) nil )))"2" (assert ) nil )))))"2" (replace -1)"2" (rewrite "expt_1i" )"2" (assert ) nil )))))))))"2" (assert ) nil )))))"2" (hide 2)"2" "negreal_times_negreal_is_posreal" "nx" "x!1" "ny" "x!1" ))"1" (lemma "le_times_le_neg" )"1" (inst - "x!1" "x!1" "-1" "-1" )"1" (expand "^" )"1" (expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" (assert ) nil )))))))))"2" (assert ) nil )))))"2" (assert ) nil ))))))))))))))))))))nil )nil nil )nil 3295528895"" (expand "exp_neg_le1_lb" )"" (expand "exp_neg_le1_ub" )"" (skosimp)"" (case "FORALL (n:nat): 0 < x!1^(2*n) & x!1^(2*n) <= 1" )"1" case "FORALL (n:nat): -1 <= x!1^(2*n+1) & x!1^(2*n+1) < 0" )"1" (case "max(exp(x!1), 1) = 1" )"1" case "FORALL (n,m:posnat): n < m => abs(x!1)^m/factorial(m) < abs(x!1)^n/factorial(n)" )"1" "exp_series_n(x!1, 1 + 2 * n!1) < exp(x!1)" )"1" (lemma "exp_series" ("x" "x!1" "n" "1+2*n!1" ))"1" (expand "abs" -1 1)"1" (assert )"1" (replace -4)"1" (hide -2)"1" (expand "exp_series_n" )"1" expand "sigma" -1 1)"1" "RHS" "sigma(0, 2 * n!1, LAMBDA (nn: nat):IF nn = 0 THEN 1 ELSE x!1 ^ nn / factorial(nn) ENDIF)") "1" case "(x!1^(1+2*n!1))/factorial(1+2*n!1) + abs(x!1)^(2+2*n!1)/factorial(2+2*n!1) < 0" )"1" (assert ) nil nil )"2" "1+2*n!1" "2+2*n!1" )"2" assert )"2" "abs(x!1) ^ (1 + 2 * n!1) = -(x!1^(1+2*n!1))" )"1" (assert ) nil nil )"2" "2" "2" rewrite "expt_plus" )"1" rewrite "expt_plus" )"1" rewrite "expt_x1" )"1" rewrite "expt_x1" )"1" rewrite "expt_times" )"1" rewrite "expt_times" )"1" expand "abs" )"1" "(-x!1) ^ 2=x!1 ^ 2" )"1" assert )nil nil )"2" "2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "exp_series" ("x" "x!1" "n" "2+2*n!1" ))"2" (replace -3)"2" (expand "abs" -1 1)"2" (expand "exp_series_n" )"2" (expand "sigma" -1)"2" "LB" "sigma(0, 1 + 2 * n!1, LAMBDA (nn: nat):IF nn = 0 THEN 1 ELSE x!1 ^ nn / factorial(nn) ENDIF)") "2" "exp(x!1) - LB - (x!1 ^ (2 + 2 * n!1)) / factorial(2 + 2 * n!1) < 0" )"1" "1" case "x!1^(2+2*n!1) / factorial(2+2*n!1) - abs(x!1)^(3+2*n!1)/factorial(3+2*n!1) > 0" )"1" (assert ) nil nil )"2" "2" "2+2*n!1" "3+2*n!1" )"2" assert )"2" "abs(x!1) ^ (2 + 2 * n!1) = x!1 ^ (2 + 2 * n!1)" )"1" (assert ) nil nil )"2" "2" "expt_times" "i" "2" "j" "1+n!1" ))"2" "abs(x!1)" )"1" "x!1" )"1" "abs(x!1)^2 = x!1^2" )"1" assert )nil nil )"2" "2" expand "^" )"2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "(x!1 ^ (2 + 2 * n!1)) / factorial(2 + 2 * n!1) > 0" )"1" (assert ) nil nil )"2" "2" "1+n!1" )"2" "2" "posreal_div_posreal_is_posreal" "px" "x!1 ^ (2 + 2 * n!1)" "py" "factorial(2 + 2 * n!1)" ))"1" (propax) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-4 -5 1))"2" (skosimp)"2" case "forall (n,m:posnat): factorial(n) < factorial(n+m)" )"1" (case "abs(x!1) ^ m!1 <= abs(x!1) ^ n!2" )"1" "lt_div_lt_pos1" "px" "abs(x!1) ^ m!1" "w" "factorial(m!1)" "y" "abs(x!1) ^ n!2" "pz" "factorial(n!2)" ))"1" (split -1)"1" (propax) nil nil )"2" (propax) nil nil )"3" (inst - "n!2" "m!1-n!2" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil )"2" "expt_pos" "px" "abs(x!1)" "i" "m!1" ))"1" (propax) nil nil )"2" (expand "abs" )"2" (assert ) nil nil )) nil ))nil ))nil )"2" (hide 2 -1)"2" (case-replace "abs(x!1)=1" )"1" (rewrite "expt_1i" )"1" rewrite "expt_1i" )"1" (assert ) nil nil ))nil ))nil )"2" (case "abs(x!1)<1" )"1" "both_sides_expt_lt1_lt" "lt1x" "abs(x!1)" "i" "m!1" "j" "n!2" ))"1" (assert ) nil nil )"2" assert )"2" expand "abs" )"2" (assert ) nil nil ))nil ))nil ))nil )"2" expand "abs" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2 -3 2)"2" (hide -1)"2" (induct "m" )"1" (assert ) nil nil )"2" (assert ) nil nil )"3" (skosimp*)"3" "j!1=0" )"1" expand "factorial" 1 2)"1" "both_sides_times_pos_lt1" "pz" "factorial(n!3)" "x" "1" "y" "1+n!3" ))"1" (assert ) nil nil ))nil ))nil )"2" assert )"2" "n!3" )"2" expand "factorial" 2 2)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but (-4 1))"2" (expand "max" )"2" (lemma "exp_strict_increasing" )"2" (expand "strict_increasing?" )"2" (inst - "x!1" "0" )"2" (rewrite "exp_0" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (inst - "n!2" )"2" (flatten)"2" (rewrite "expt_plus" 1)"2" (rewrite "expt_x1" 1)"2" "both_sides_times_neg_lt1" "nz" "x!1" "y" "0" "x" "x!1^(2*n!2)" ))"1" "both_sides_times_neg_le1" "nz" "x!1" "x" "1" "y" "x!1^(2*n!2)" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (rewrite "expt_times" 1)"2" (case "0 < x!1^2 & x!1^2<=1" )"1" (flatten)"1" (lemma "expt_pos" ("i" "n!2" "px" "x!1^2" ))"1" (expand "<=" -3)"1" (split -3)"1" (case-replace "n!2=0" )"1" (rewrite "expt_x0" )"1" (assert ) nil nil )) nil )"2" "both_sides_expt_pos_lt" "px" "x!1^2" "py" "1" "pm" "n!2" ))"1" rewrite "expt_1i" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (replace -1)"2" (rewrite "expt_1i" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" "negreal_times_negreal_is_posreal" "nx" "x!1" "ny" "x!1" ))"1" (lemma "le_times_le_neg" )"1" (inst - "x!1" "x!1" "-1" "-1" )"1" (expand "^" )"1" (expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )"real" sigma "reals/" )"bool" real_fun_preds "reals/" )nil ln_exp nil )nil ln_exp nil ))nil 3307800357"" (expand "strict_decreasing?" )"" (expand "exp_neg_le1_ub" )"" (skosimp*)"" case "FORALL (i:nat,j:posnat): exp_estimate(x!1, 2 * (i+j)) < exp_estimate(x!1, 2 * i)" )"1" (inst - "x!2" "y!1-x!2" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (hide -3 2)"2" (skolem 1 ("m" "_" ))"2" (induct "j" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (skolem 1 ("n" ))"3" (flatten)"3" (expand "exp_estimate" )"3" (expand "sigma" 1 1)"3" (expand "sigma" 1 1)"3" case "(x!1 ^ (1 + 2 * m + 2 * n)) / factorial(1 + 2 * m + 2 * n) ") "1" (case-replace "n=0" )"1" assert )"1" "1" "1" "m = 0" )"1" assert )"1" expand "sigma" )"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide 2 -1)"2" "2" "both_sides_div_pos_lt1" "x" "x!1 ^ (1 + 2 * m + 2 * n)" "y" "0" "pz" "factorial(1 + 2 * m + 2 * n)" ))"2" "expt_plus" "n0x" "x!1" "i" "1" "j" "2*m+2*n" ))"1" rewrite "expt_x1" )"1" "expt_times" "n0x" "x!1" "i" "2" "j" "m+n" ))"1" "expt_pos" "px" "x!1^2" "i" "m+n" ))"1" "both_sides_times_pos_lt1" "x" "x!1" "y" "0" "pz" "x!1 ^ (2 * m + 2 * n)" ))"1" assert )"1" "both_sides_times_neg_lt1" "nz" "x!1 ^ (1 + 2 * m + 2 * n) / factorial(1 + 2 * m + 2 * n)" "y" "-1*(x!1/(2+2*m+2*n))" "x" "1" ))"1" "div_mult_pos_lt1" "py" "2+2*n+2*m" "z" "-1*x!1" "x" "1" ))"1" replace -1 -2)"1" "1" assert )"1" rewrite "div_times" "1" expand "factorial" "1" "expt_plus" "n0x" "x!1" "i" "1" "j" "1+2*n+2*m" ))"1" rewrite "expt_x1" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "2" "negreal_times_negreal_is_posreal" "nx" "x!1" "ny" "x!1" ))"1" expand "^" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" exp_approx nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" exp_series nil )"bool" reals nil )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 )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nonneg_int" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"odd_int" integers nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"nat" exp_approx nil )"nat" exp_approx nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"even_int" integersnil )nil real_props nil )nil real_types nil )nil real_types nil )nil exponentiation nil )nil exponentiation nil )"nonneg_rat" nil )"real" reals nil )nil real_props nil )nil reals nil )nil real_props nil )"even_int" integersnil )"even_int" integersnil )"[numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_props nil )nil real_props nil )nil real_types nil )"real" exponentiation nil )nil exponentiation nil )nil reals nil )nil exponentiation nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"posint" nil )"odd_int" integers nil )"nonneg_int" nil )"posnat" factorial "ints/" )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"real" reals nil )"real" sigma "reals/" )"odd_int" integers nil )nil naturalnumbers nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"bool" real_fun_preds "reals/" ))nil )nil 3295616436"" (expand "strict_decreasing?" )"" (expand "exp_neg_le1_ub" )"" (skosimp*)"" case "FORALL (i:nat,j:posnat): exp_series_n(x!1, 2 * (i+j)) < exp_series_n(x!1, 2 * i)" )"1" (inst - "x!2" "y!1-x!2" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (hide -3 2)"2" (skolem 1 ("m" "_" ))"2" (induct "j" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (skolem 1 ("n" ))"3" (flatten)"3" (expand "exp_series_n" )"3" (expand "sigma" 1 1)"3" (expand "sigma" 1 1)"3" case "(x!1 ^ (1 + 2 * m + 2 * n)) / factorial(1 + 2 * m + 2 * n) ") "1" (case-replace "n=0" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" (hide 2 -1)"2" "2" "both_sides_div_pos_lt1" "x" "x!1 ^ (1 + 2 * m + 2 * n)" "y" "0" "pz" "factorial(1 + 2 * m + 2 * n)" ))"2" "expt_plus" "n0x" "x!1" "i" "1" "j" "2*m+2*n" ))"1" rewrite "expt_x1" )"1" "expt_times" "n0x" "x!1" "i" "2" "j" "m+n" ))"1" "expt_pos" "px" "x!1^2" "i" "m+n" ))"1" "both_sides_times_pos_lt1" "x" "x!1" "y" "0" "pz" "x!1 ^ (2 * m + 2 * n)" ))"1" assert )"1" "both_sides_times_neg_lt1" "nz" "x!1 ^ (1 + 2 * m + 2 * n) / factorial(1 + 2 * m + 2 * n)" "y" "-1*(x!1/(2+2*m+2*n))" "x" "1" ))"1" "div_mult_pos_lt1" "py" "2+2*n+2*m" "z" "-1*x!1" "x" "1" ))"1" replace -1 -2)"1" "1" assert )"1" rewrite "div_times" "1" expand "factorial" "1" "expt_plus" "n0x" "x!1" "i" "1" "j" "1+2*n+2*m" ))"1" rewrite "expt_x1" )"1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "2" "negreal_times_negreal_is_posreal" "nx" "x!1" "ny" "x!1" ))"1" expand "^" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" sigma "reals/" )"bool" real_fun_preds "reals/" ))nil 3307800385"" (expand "strict_increasing?" )"" (expand "exp_neg_le1_lb" )"" (skosimp*)"" case "FORALL (i:nat,j:posnat): exp_estimate(x!1, 1 + 2*i) < exp_estimate(x!1, 1+2*(j+i))" )"1" (inst - "x!2" "y!1-x!2" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (hide -3 2)"2" (skolem 1 ("n" "_" ))"2" (induct "j" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (skolem 1 ("m" ))"3" (flatten)"3" (expand "exp_estimate" )"3" (expand "sigma" 1 2)"3" (expand "sigma" 1 2)"3" case "(x!1 ^ (2 + 2 * m + 2 * n)) / factorial(2 + 2 * m + 2 * n) ") "1" (case-replace "m=0" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" (hide -1 2)"2" "posreal_div_posreal_is_posreal" "px" "x!1 ^ (2 + 2 * m + 2 * n)" "py" "factorial(2 + 2 * m + 2 * n)" ))"1" "both_sides_times_pos_lt1" "pz" "x!1 ^ (2 + 2 * m + 2 * n) / factorial(2 + 2 * m + 2 * n)" "x" "-1*(x!1/(3 + 2 * m + 2 * n))" "y" "1" ))"1" "div_mult_pos_lt1" "py" "3 + 2 * m + 2 * n" "z" "-1*x!1" "x" "1" ))"1" assert )"1" rewrite "div_times" -2)"1" "expt_plus" "n0x" "x!1" "i" "1" "j" "2+2*m+2*n" ))"1" rewrite "expt_x1" )"1" replace -1 -3 rl)"1" expand "factorial" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "2" "expt_times" "n0x" "x!1" "i" "2" "j" "1+m+n" ))"1" "expt_pos" "px" "x!1^2" "i" "1+m+n" ))"1" (assert ) nil nil )"2" "2" "negreal_times_negreal_is_posreal" "nx" "x!1" "ny" "x!1" ))"1" (grind) nil nil )"2" (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 ))nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" exp_approx nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" exp_series nil )"bool" reals nil )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 )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"odd_int" integers nil )"posint" nil )"odd_int" integers nil )"(total_order?[real])" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"nat" exp_approx nil )"nat" exp_approx nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_types nil )"real" exponentiation nil )nil exponentiation nil )"real" reals nil )nil real_props nil )"[numfield -> numfield]" number_fields nil )"odd_int" integers nil )"posint" nil )nil exponentiation nil )nil reals nil )nil exponentiation nil )nil real_props nil )nil reals nil )nil real_props nil )nil real_types nil )nil real_types nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"posint" nil )"odd_int" integers nil )"posnat" factorial "ints/" )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"real" reals nil )"real" sigma "reals/" )"even_int" integersnil )nil naturalnumbers nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"bool" real_fun_preds "reals/" ))nil )nil 3295619040"" (expand "strict_increasing?" )"" (expand "exp_neg_le1_lb" )"" (skosimp*)"" case "FORALL (i:nat,j:posnat): exp_series_n(x!1, 1 + 2*i) < exp_series_n(x!1, 1+2*(j+i))" )"1" (inst - "x!2" "y!1-x!2" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil )"2" (hide -3 2)"2" (skolem 1 ("n" "_" ))"2" (induct "j" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (skolem 1 ("m" ))"3" (flatten)"3" (expand "exp_series_n" )"3" (expand "sigma" 1 2)"3" (expand "sigma" 1 2)"3" case "(x!1 ^ (2 + 2 * m + 2 * n)) / factorial(2 + 2 * m + 2 * n) ") "1" (case-replace "m=0" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil )"2" (hide -1 2)"2" "posreal_div_posreal_is_posreal" "px" "x!1 ^ (2 + 2 * m + 2 * n)" "py" "factorial(2 + 2 * m + 2 * n)" ))"1" "both_sides_times_pos_lt1" "pz" "x!1 ^ (2 + 2 * m + 2 * n) / factorial(2 + 2 * m + 2 * n)" "x" "-1*(x!1/(3 + 2 * m + 2 * n))" "y" "1" ))"1" "div_mult_pos_lt1" "py" "3 + 2 * m + 2 * n" "z" "-1*x!1" "x" "1" ))"1" assert )"1" rewrite "div_times" -2)"1" "expt_plus" "n0x" "x!1" "i" "1" "j" "2+2*m+2*n" ))"1" rewrite "expt_x1" )"1" replace -1 -3 rl)"1" expand "factorial" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "2" "expt_times" "n0x" "x!1" "i" "2" "j" "1+m+n" ))"1" "expt_pos" "px" "x!1^2" "i" "1+m+n" ))"1" (assert ) nil nil )"2" "2" "negreal_times_negreal_is_posreal" "nx" "x!1" "ny" "x!1" ))"1" (grind) nil nil )"2" (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 ))nil )"real" sigma "reals/" )"bool" real_fun_preds "reals/" ))nil 3307800417"" (skosimp*)"" (case "exp_neg_le1_lb(1, x!1) > 0" )"1" (lemma "exp_neg_le1_lb_strict_increasing_n" ("x" "x!1" ))"1" (expand "strict_increasing?" )"1" (assert )"1" (case-replace "pn!1=1" )"1" (inst - "1" "pn!1" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "exp_neg_le1_lb" )"2" (expand "exp_estimate" )"2" (expand "sigma" )"2" (expand "sigma" )"2" (expand "sigma" )"2" (expand "factorial" )"2" (expand "factorial" )"2" (expand "factorial" )"2" (expand "factorial" )"2" (lemma "quad_min_val" )"2" (inst - "1/2" "1" "1" "x!1" )"2" assert )"2" "(4 * (1 / 2) - 1) / (4 * (1 / 2)) = 1/2" )"1" expand "quadratic" )"1" "x!1 ^ 2 = sq(x!1)" )"1" case "x!1 ^ 3 / 6 >= -1/6" )"1" assert )"1" (grind) nil nil ))nil )"2" "2" "sq_le" "nna" "-x!1" "nnb" "1" ))"2" assert )"2" rewrite "sq_neg" )"2" expand "^" )"2" expand "expt" 1)"2" replace -2 1)"2" "sq_nz_pos" )"2" "-x!1" )"2" rewrite "sq_neg" )"2" "2" "le_times_le_pos" "nnx" "sq(x!1)/6" "y" "1/6" "nnz" "-x!1" "w" "1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" exp_approx 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]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" real_fun_preds "reals/" )nil integers nil )nil integers nil )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )nil exp_approxnil )"real" sigma "reals/" )"int" integers nil )"posrat" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil reals nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posrat" nil )"rat" rationals nil )"rat" rationals nil )"nonneg_real" sq "reals/" )nil real_types nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"posreal" nil )"nnreal" nil )"posreal" sq "reals/" )nil reals nil )nil real_props nil )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" )"real" reals nil )"nnreal" nil )"real" reals nil )"real" exponentiation nil )"[numfield -> numfield]" number_fields nil )"real" quadratic "reals/" )nil sq "reals/" )"nzrat" rationalsnil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )nil quad_minmax "reals/" )"nonneg_int" nil )"posnat" factorial "ints/" )"even_int" integersnil )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" nil )"real" exp_series nil ))nil )nil 3295554734"" (skosimp*)"" (case "exp_neg_le1_lb(1, x!1) > 0" )"1" (lemma "exp_neg_le1_lb_strict_increasing_n" ("x" "x!1" ))"1" (expand "strict_increasing?" )"1" (assert )"1" (case-replace "pn!1=1" )"1" (inst - "1" "pn!1" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "exp_neg_le1_lb" )"2" (expand "exp_series_n" )"2" (expand "sigma" )"2" (expand "sigma" )"2" (expand "sigma" )"2" (expand "sigma" )"2" (expand "factorial" )"2" (expand "factorial" )"2" (expand "factorial" )"2" (expand "factorial" )"2" "quadratic_min_val" "a" "1/2" "b" "1" "c" "1" "x" "x!1" "f" "quadratic(1/2,1,1)" "minpt" "-1" ))"2" assert )"2" "(4 * (1 / 2) - 1) / (4 * (1 / 2)) = 1/2" )"1" expand "quadratic" )"1" "x!1 ^ 2 = sq(x!1)" )"1" case "x!1 ^ 3 / 6 >= -1/6" )"1" rewrite "expt_x1" )"1" (assert ) nil nil ))nil )"2" "2" "sq_le" "nna" "-x!1" "nnb" "1" ))"2" assert )"2" rewrite "sq_neg" )"2" expand "^" )"2" expand "expt" 1)"2" replace -2 1)"2" "sq_nz_pos" )"2" "-x!1" )"2" rewrite "sq_neg" )"2" "2" "le_times_le_pos" "nnx" "sq(x!1)/6" "y" "1/6" "nnz" "-x!1" "w" "1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_fun_preds "reals/" )"real" sigma "reals/" )"real" quadratic "reals/" )"nonneg_real" sq "reals/" )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" ))nil 3295622180"" (skosimp)"" (typepred "floor(nx!1)" )"" (typepred "nx!1" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil real_types nil )nil real_types nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans 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]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"int" integers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil 3295622180"" (skosimp)"" (lemma "exp_neg_ub_TCC1" ("nx" "nx!1" ))"" (assert ) 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil exp_approx nil )"int" integers nil )"posint" nil )"nzreal" nil )"(total_order?[real])" nil ))nil 3374415239"" (skosimp*)"" (assert )"" (lemma "exp_neg_ub_TCC1" ("nx" "nx!1" ))"" (typepred "floor(nx!1)" )"" (name-replace "F" "floor(nx!1)" )"" (name "P" "-F" )"" (replace -1)"" "both_sides_div_pos_lt1" "x" "nx!1" "y" "0" "pz" "P" ))"1" (assert )"1" "div_mult_pos_le2" "py" "P" "z" "nx!1" "x" "-1" ))"1" (assert )"1" "exp_neg_le1_bounds" "x" "nx!1/P" "n" "1+n!1" ))"1" (assert )"1" (flatten)"1" "exp(nx!1 / P)" )"1" "expt_pos" "px" "exp_neg_le1_ub(1 + n!1, nx!1 / P)" "i" "P" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nzreal" nil )"posint" nil )"(total_order?[real])" nil )"int" integers nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )NOT const-decl "[bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )nil integers nil )nil real_props nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )nil real_props nil )nil exp_approx nil )nil naturalnumbers nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil exponentiation nil )"real" exp_approx nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"rat" rationals nil )"posint" nil )"[T, T -> boolean]" equalities nil )nil exp_approx nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil ))nil )nil 3295622180"" (skosimp) (("" (assert ) nil nil )) nil ) nil shostak))nil 3295622181"" (skosimp) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"nzreal" nil )"posint" nil )"int" integers nil ))nil 3295622181"" (skosimp*)"" (assert )"" (typepred "floor(nx!1)" )"" (name-replace "F" "floor(nx!1)" )"" (typepred "nx!1" )"" (name "P" "-F" )"" (replace -1)"" "both_sides_div_pos_lt1" "x" "nx!1" "y" "0" "pz" "P" ))"1" (assert )"1" "div_mult_pos_le2" "py" "P" "z" "nx!1" "x" "-1" ))"1" (assert )"1" "exp_neg_le1_lb_pos" "x" "nx!1/P" "pn" "1+n!1" ))"1" (assert )"1" "expt_pos" "px" "exp_neg_le1_lb(1 + n!1, nx!1 / P)" "i" "P" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nzreal" nil )"posint" nil )"(total_order?[real])" nil )"int" integers nil )"[T, T -> boolean]" equalities nil )"[numfield -> numfield]" number_fields nil )nil integers nil )nil real_props nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )nil real_props nil )nil exp_approx nil )nil integers nil )nil integers nil )nil naturalnumbers nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil exponentiation nil )"real" exp_approx nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"rat" rationals nil )"posint" nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )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 )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil real_types nil )nil real_types nil ))nil 3295363258"" (skosimp)"" (expand "exp_neg_lb" )"" (expand "exp_neg_ub" )"" (typepred "floor(nx!1)" )"" (typepred "nx!1" )"" (name-replace "F" "floor(nx!1)" )"" (name "P" "-F" )"" (replace -1)"" "both_sides_div_pos_lt1" "pz" "P" "x" "nx!1" "y" "0" ))"1" "div_mult_pos_le2" "py" "P" "z" "nx!1" "x" "-1" ))"1" (assert )"1" (lemma "exp_scal" ("i" "P" "x" "nx!1/P" ))"1" (rewrite "div_cancel1" -1)"1" (replace -1)"1" "exp_neg_le1_bounds" "x" "nx!1/P" "n" "1+n!1" ))"1" "exp_neg_le1_lb_pos" "x" "nx!1/P" "pn" "1+n!1" ))"1" "exp(nx!1 / P)" )"1" assert )"1" "1" "both_sides_expt_pos_lt" "pm" "P" ))"1" "exp_neg_le1_lb(1 + n!1, nx!1 / P)" "exp(nx!1 / P)" )"1" "exp(nx!1 / P)" "exp_neg_le1_ub(1 + n!1, nx!1 / P)" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"int" integers nil )"posreal" exp_approx nil )nil real_types nil )nil real_types nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans 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]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"odd_int" integers nil )nil real_props nil )nil ln_exp nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil exp_approx nil )nil integers nil )nil integers nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )nil exponentiation nil )"real" exp_approx nil )"nat" exp_approx nil )"negreal" exp_approx nil )"int" exp_approx nil )"real" exp_approx nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )nil naturalnumbers nil )nil exp_approx nil )nil real_props nil )nil reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"nzreal" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"rat" rationals nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_props nil )nil integers nil )"[numfield -> numfield]" number_fields nil )"posreal" exp_approx nil ))nil 3295528481"" (skosimp) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3295622181"" (skosimp) (("" (assert ) nil nil )) nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3295623866"" (skosimp)"" (lemma "trichotomy" ("x" "x!1" ))"" (split -1)"1" (expand "exp_lb" )"1" (expand "exp_ub" )"1" (assert )"1" (lemma "exp_neg_bounds" ("n" "n!1" "nx" "-x!1" ))"1" (flatten)"1" (lemma "exp_diff" ("x" "0" "y" "x!1" ))"1" (rewrite "exp_0" )"1" (replace -1)"1" (rewrite "div_mult_pos_lt1" )"1" (rewrite "div_mult_pos_lt2" )"1" (rewrite "div_mult_pos_le1" )"1" rewrite "div_mult_pos_le2" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "exp_ub" )"2" (expand "exp_lb" )"2" (replace -1)"2" (rewrite "exp_0" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"3" (lemma "exp_neg_bounds" ("n" "n!1" "nx" "x!1" ))"1" (flatten)"1" (expand "exp_lb" )"1" (expand "exp_ub" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_axioms nil )"posreal" exp_approx nil )"real" reals nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil ln_exp nil )"odd_int" integers nil )"posreal" exp_approx nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )"[T, T -> boolean]" equalities nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_props nil )"posreal" nil )nil real_props nil )"real" reals nil )nil real_props nil )nil real_props nil )"posreal" exp_approx nil )nil ln_exp nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil exp_approx 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" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"posreal" exp_approx nil ))nil 3295625003"" (skosimp)"" (expand "e" )"" (expand "e_lb" )"" (expand "e_ub" ) (("" (rewrite "exp_bounds" ) nil nil ))nil ))nil ))nil ))nil )"posreal" ln_exp nil )"posreal" exp_approx 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]" number_fieldsnil )nil booleans nil )nil numbers nil )nil exp_approx nil )"posreal" exp_approx nil ))nil 3307355846"" case "1000000000/2718281829 < 1/e & 1/e <1000000000/2718281828" )"1" (flatten)"1" (assert )"1" (rewrite "div_mult_pos_lt2" -1)"1" (rewrite "div_mult_pos_lt1" -2)"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "exp_diff" ("x" "0" "y" "1" ))"2" (rewrite "exp_0" )"2" (expand "e" )"2" (replace -1 1 rl)"2" (hide -1)"2" (lemma "exp_neg_le1_bounds" ("x" "-1" "n" "10" ))"2" (assert )"2" (flatten)"2" case "1000000000 / 2718281829 < exp_neg_le1_lb(10, -1)" )"1" case "exp_neg_le1_ub(10, -1) < 1000000000 / 2718281828" )"1" (assert ) nil nil )"2" (hide-all-but 1)"2" (grind) nil nil )) nil ))nil )"2" (hide-all-but 1) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil ln_exp nil )"odd_int" integers nil )nil exp_approx nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"[numfield -> numfield]" number_fields nil )"real" exp_approx nil )"real" exponentiation nil )"real" exponentiation nil )"posnat" factorial "ints/" )"real" sigma "reals/" )"real" exp_series nil )"even_int" integersnil )"posint" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )"nzreal" exponentiation nil )"int" exponentiation nil )"(strict_total_order?[real])" real_props nil )"nzrat" rationalsnil )"real" reals nil )"real" exp_approx nil )"(total_order?[real])" nil )"odd_int" integersnil )nil ln_exp nil )nil real_props nil )"posreal" nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"posrat" nil )"posreal" nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" ln_exp nil ))nil ))nil 3307358139"" (lemma "e_bounds2" )"" (expand "e_lb" )"" (expand "e_ub" ) (("" (flatten) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"posreal" exp_approx nil )"(strict_total_order?[real])" real_props nil )"posrat" nil )"posreal" exp_approx nil )nil exp_approx nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.135Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-26)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
