Impressum exp_series.prf
Sprache: Lisp
(exp_seriesnil 3568830993 ("" (assuming-tcc) nil nil )"bool" deriv_domain_def "analysis/" )) nil ))nil 3568830993 ("" (assert ) nil nil )nil deriv_domain "analysis/" ))nil ))nil 3568830993 ("" (assuming-tcc) nil nil )nil nil ))nil 3568830993 ("" (assuming-tcc) nil nil )nil nil ))nil 3563622656"" (lemma "deriv_domain_real" ) (("" (propax) nil nil )) nil )nil deriv_domain "analysis/" ))nil ))nil 3298644142"" (induct "n" )"1" (lemma "exp_deriv" )"1" (flatten)"1" (expand "derivable_n_times?" )"1" (assert )"1" (expand "derivable_n_times?" )"1" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "nderiv" 1)"2" (expand "nderiv" )"2" (lemma "exp_deriv" ) (("2" (flatten) nil nil )) nil )) nil ))nil )"3" (skosimp*)"3" (lemma "exp_deriv" )"3" (flatten)"3" (prop)"1" (expand "derivable_n_times?" 1)"1" (assert ) nil nil )) nil )"2" (expand "nderiv" 1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"4" (skosimp*) nil nil ) ("5" (skosimp*) nil nil ))nil )nil ln_exp nil )nil naturalnumbers nil )"[T -> real]" nth_derivatives "analysis/" )nil nth_derivatives "analysis/" )"{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 )"bool" nth_derivatives "analysis/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil defined_types 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 3298647578"" (expand "inf_deriv_fun?" )"" (induct "n" )"1" (lemma "nderiv_exp" )"1" (inst?) (("1" (flatten) nil nil )) nil )) nil )"2" (skosimp*)"2" (expand "derivable_n_times?" 1)"2" (lemma "exp_deriv" )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil defined_types nil )"bool" nth_derivatives "analysis/" )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )nil naturalnumbers nil )nil exp_series nil )nil ln_exp nil )"bool" taylors "analysis/" ))nil 3298643720"" (skosimp*)"" (assert )"" (lemma "nderiv_exp" )"" (inst?) (("" (flatten) nil nil )) nil )) nil ))nil ))nil )"posint" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil exp_series nil ))nil 3298643720"" (rewrite "exp_inf_deriv" ) nil nil )nil exp_series nil )) shostak))nil 3298638694"" (skosimp*)"" (lemma "squeezing_abs_0" )"" (inst?)"1" (assert )"1" case "EXISTS (M: posreal): (FORALL (t: between[real](0,x!1)): exp(t) <= M)" )"1" (skosimp*)"1" "(LAMBDA n: M!1*abs(x!1)^(n+1)/factorial(n+1))" )"1" (assert )"1" (hide 2)"1" (prop)"1" (lemma "conv_x_to_n_div_fact" )"1" (inst - "abs(x!1)" )"1" (lemma "convergence_shift" )"1" (inst?)"1" "1" )"1" assert )"1" "cnv_seq_scal" )"1" "1" "M!1" )"1" assert )"1" expand "*" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (expand "Taylor_rem" )"2" (rewrite "abs_div" )"2" (expand "abs" 1 2)"2" "2" assert )"2" "C" "GET_C(exp, x!1, n!1)" )"2" "2" "2" "C" )"2" rewrite "abs_hat" )"1" expand "abs" 1 1)"1" assert )"1" "nderiv_exp" )"1" "n!1+1" )"1" "1" replace -2)"1" assert )"1" "1" expand "abs" "1" "abs(x!1) ^ (1 + n!1)" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "x!1 = 0" )"1" expand "^" )"1" expand "expt" )"1" expand "abs" )"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 ))nil )"2" (hide 2)"2" (hide -1)"2" (inst + "exp(abs(x!1))" )"2" (skosimp*)"2" (lemma "exp_increasing" )"2" (expand "increasing?" )"2" (inst?)"2" (assert )"2" (hide 2)"2" "x!1" )"2" "t!1" )"2" expand "abs" )"2" "2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "exp_inf_deriv" ) nil nil )"3" (skosimp*)"3" (lemma "exp_inf_deriv" )"3" (expand "inf_deriv_fun?" ) (("3" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil convergence_ops "analysis/" )nil exp_series nil )nil ln_exp nil )"real" reals nil )"bool" real_fun_preds "reals/" )"nnreal" nil )"nnreal" exponentiation nil )"posint" nil )"[T -> real]" real_fun_ops "reals/" )nil convergence_ops "analysis/" )nil convergence_ops "analysis/" )nil convergence_special nil )"real" reals nil )"real" reals nil )nil real_types nil )nil real_props nil )nil reals nil )nil exponent_props "reals/" )"int" integers nil )nil extra_real_propsnil )nil exp_series nil )"nat" exponentiation nil )"real" exponentiation nil )"nat" exponentiation nil )nil real_props nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )nil real_props nil )nil real_props nil )nil real_props nil )"{j: posint | j >= i}" nil )nil real_props nil )nil reals nil )"[T -> real]" nth_derivatives "analysis/" )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil integers nil )nil integers nil )"posnat" factorial "ints/" )"posint" nil )"nnreal" nil )"bool" reals nil )"{c: between[T](0, x) | " taylor_series " series/") "[numfield, numfield -> numfield]" number_fields nil )"real" taylor_series "series/" )"sequence[real]" power_series "series/" )"real" taylors "analysis/" )nil taylors "analysis/" )"bool" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil nth_derivatives "analysis/" )nil sequences nil )"bool" taylors "analysis/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )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" nth_derivatives "analysis/" )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil )nil 3298638280"" (skosimp*)"" (lemma "squeezing_abs_0" )"" (inst?)"1" (assert )"1" case "EXISTS (M: posreal): FORALL t: 0 <= t IMPLIES exp(t) <= M" )"1" (skosimp*)"1" "(LAMBDA n: M!1*abs(x!1)^(n+1)/factorial(n+1))" )"1" (assert )"1" (prop)"1" (hide 2) (("1" (postpone) nil nil )) nil )"2" (skosimp*)"2" (hide 2)"2" (expand "Taylor_rem" )"2" (rewrite "nderiv_exp" )"2" (rewrite "abs_div" )"1" expand "abs" 1 2)"1" "1" assert )"1" "C" "GET_C(exp, x!1, n!1)" )"1" "1" (postpone) nil nil ))nil )"2" "2" "x!2+1" )"2" (assert ) nil nil ))nil ))nil )"3" (postpone) nil nil ))nil ))nil )"2" "2" "x!2+1" )"2" (assert ) nil nil ))nil ))nil )"3" (postpone) nil nil ))nil ))nil )"2" "2" "x!2+1" )"2" (assert ) nil nil ))nil ))nil )"3" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )"2" (skosimp*)"2" (inst + "x!2+1" ) (("2" (assert ) nil nil )) nil )) nil )"3" (postpone) nil nil ) ("4" (postpone) nil nil ))nil ))nil ))nil )nil nil )nil 3298633339"" (skosimp*)"" (lemma "squeezing_abs_0" )"" (inst?)"1" (assert )"1" case "EXISTS (M: posreal): FORALL t: 0 <= x!1 IMPLIES exp(t) <= M" )"1" (skosimp*)"1" "(LAMBDA n: M!1*abs(x!1)^(n+1)/factorial(n+1))" )"1" (assert )"1" (prop)"1" (hide 2) (("1" (postpone) nil nil )) nil )"2" (skosimp*)"2" (hide 2)"2" (expand "Taylor_rem" )"2" (rewrite "nderiv_exp" )"2" (rewrite "abs_div" )"1" expand "abs" 1 2)"1" "1" assert )"1" "C" "GET_C(exp, x!1, n!1)" )"1" "1" "C" )"1" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil )"3" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil )"3" (postpone) nil nil ))nil ))nil )"2" "2" "x!2+1" )"2" (assert ) nil nil ))nil ))nil )"3" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )"2" (skosimp*)"2" (inst + "x!2+1" ) (("2" (assert ) nil nil )) nil )) nil )"3" (postpone) nil nil )"4" (skosimp*) (("4" (postpone) nil nil )) nil ))nil ))nil ))nil )nil shostak))nil 3445687755"" (lemma "is_taylor_prep" )"" (inst - "exp" )"" (assert )"" (case-replace "Taylor_seq[real](exp) = exp_seq" )"1" (assert )"1" (rewrite "exp_inf_deriv" )"1" (skosimp*)"1" (lemma "exp_series_prep" )"1" (inst?)"1" (expand "convergent?" )"1" (inst + "0" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (expand "Taylor_seq" )"2" (expand "exp_seq" )"2" (apply-extensionality 1 :hide? t)"1" (lemma "nderiv_exp" )"1" (inst?)"1" (flatten)"1" (replace -2)"1" (rewrite "exp_0" ) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "nderiv_exp" )"2" (inst?) (("2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (rewrite "exp_inf_deriv" ) nil nil ))nil ))nil ))nil ))nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" taylors "analysis/" )"real" taylor_series "series/" )"real" exp_series nil )nil exp_series nil )nil exp_series nil )"bool" convergence_sequences "analysis/" )nil number_fields nil )"posnat" factorial "ints/" )nil integers nil )nil integers nil )"[T -> real]" nth_derivatives "analysis/" )nil nth_derivatives "analysis/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" nth_derivatives "analysis/" )"real" reals nil )"posrat" nil )nil ln_exp nil )nil exp_series nil )nil taylor_series "series/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil )nil 3298646416"" (lemma "is_taylor_prep" )"" (inst - "exp" )"" (assert )"" (case-replace "Taylor_seq[real](exp) = exp_seq" )"1" (assert )"1" (rewrite "exp_inf_deriv" )"1" (skosimp*)"1" (lemma "exp_series_prep" )"1" (inst?)"1" (expand "convergent" )"1" (inst + "0" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2)"2" (expand "Taylor_seq" )"2" (expand "exp_seq" )"2" (apply-extensionality 1 :hide? t)"1" (lemma "nderiv_exp" )"1" (inst?)"1" (flatten)"1" (replace -2)"1" (rewrite "exp_0" ) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "nderiv_exp" )"2" (inst?) (("2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (rewrite "exp_inf_deriv" ) nil nil ))nil ))nil ))nil ))nil )nil taylor_series "series/" )nil ln_exp nil )"real" taylor_series "series/" )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil ))nil 3298643720 ("" (rewrite "conv_exp" ) nil nil )nil exp_series nil )) shostak))nil 3298643739"" (lemma "is_taylor[real]" )"" (inst?)"" (assert )"" (split -1)"1" (replace -1)"1" (case-replace "Taylor_seq[real](exp) = exp_seq" )"1" (hide 2)"1" (expand "Taylor_seq" )"1" (expand "exp_seq" )"1" (apply-extensionality 1 :hide? t)"1" (lemma "nderiv_exp" )"1" (inst - "x!1" )"1" (flatten)"1" (assert )"1" replace -2)"1" (rewrite "exp_0" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "nderiv_exp" )"2" (inst?) (("2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "exp_inf_deriv" ) nil nil )"3" (skosimp*) (("3" (rewrite "exp_series_prep" ) nil nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[T, T -> boolean]" equalities nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"bool" taylors "analysis/" )"real" taylor_series "series/" )"real" exp_series nil )nil number_fields nil )"posnat" factorial "ints/" )nil integers nil )nil integers nil )"[T -> real]" nth_derivatives "analysis/" )nil nth_derivatives "analysis/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" nth_derivatives "analysis/" )"real" reals nil )"posrat" nil )nil ln_exp nil )nil exp_series nil )nil exp_series nil )nil exp_series nil )nil taylor_series "series/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil 3302449689"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil ))nil 3403261760"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil ))nil ))nil 3403261760"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil ))nil ))nil 3302449689"" (skosimp*) (("" (assert ) nil nil )) nil )"posint" nil )"(total_order?[real])" nil ))nil 3352447184"" (skosimp*)"" "Taylors[real]" ("f" "exp" "n" "n!1" "aa" "0" "bb" "x!1" ))"" "sigma_eq[nat]" "low" "1" "high" "n!1" "F" "LAMBDA (nn:nat): IF nn > n!1 THEN 0" " G" "LAMBDA (nn: nat): x!1 ^ nn / factorial(nn)" ))"1" (assert )"1" (expand "exp_estimate" )"1" (split -1)"1" (rewrite "sigma_first" -2)"1" (replace -1)"1" (hide -1)"1" (lemma "nderiv_exp" ("n" "n!1+1" ))"1" (flatten) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (case-replace "n!1 = 0" )"1" (assert )"1" (expand "sigma" )"1" (split -3)"1" (lemma "nderiv_exp" )"1" (inst?)"1" (flatten)"1" replace -2)"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (lemma "nderiv_exp" )"2" (inst?) (("2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (skosimp*)"2" (hide 2)"2" (hide -1)"2" (lemma "nderiv_exp" )"2" (inst?)"2" (flatten)"2" (replace -2) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (assert )"2" (hide - 4)"2" (lemma "nderiv_exp" )"2" (inst?) (("2" (flatten) nil nil )) nil )) nil ))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 naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals 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 )"bool" reals nil )nil booleans nil )nil taylors "analysis/" )"posint" nil )"real" reals nil )nil ln_exp nil )nil exp_series nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )nil sigma "reals/" )nil integers nil )"real" exp_series nil )"real" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )nil sigma "reals/" )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" nth_derivatives "analysis/" )nil nth_derivatives "analysis/" )"[T -> real]" nth_derivatives "analysis/" )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )nil integers nil )"posnat" factorial "ints/" )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" ))nil )nil 3302448557"" (skosimp*)"" (lemma "Taylors" ("f" "exp" "n" "n!1" "aa" "0" "bb" "x!1" ))"" "sigma_eq[nat]" "low" "1" "high" "n!1" "F" "LAMBDA (nn:nat): IF nn > n!1 THEN 0" " G" "LAMBDA (nn: nat): x!1 ^ nn / factorial(nn)" ))"1" (assert )"1" (expand "exp_estimate" )"1" (split -1)"1" (rewrite "sigma_first" -2)"1" (replace -1)"1" (hide -1)"1" (lemma "nderiv_exp" ("n" "n!1+1" ))"1" (flatten) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (case-replace "n!1 = 0" )"1" (assert )"1" (expand "sigma" )"1" (split -3)"1" (lemma "nderiv_exp" )"1" (inst?)"1" (flatten)"1" replace -2)"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (lemma "nderiv_exp" )"2" (inst?) (("2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (skosimp*)"2" (hide 2)"2" (hide -1)"2" (lemma "nderiv_exp" )"2" (inst?)"2" (flatten)"2" (replace -2) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (assert )"2" (hide - 4)"2" (lemma "nderiv_exp" )"2" (inst?) (("2" (flatten) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )nil ln_exp nil )"real" ln_exp nil )"{py | x = ln(py)}" ln_exp nil ))nil ))nil 3302449689"" (skosimp*) (("" (assert ) nil nil )) nil )"posint" nil )"(total_order?[real])" nil ))nil 3302449661"" (skosimp*)"" (lemma "exp_taylors" ("x" "x!1" "n" "n!1" ))"" (skosimp*)"" (typepred "c!1" )"" (lemma "trichotomy" ("x" "x!1" ))"" case "exp(x!1) - exp_estimate(x!1, n!1) = exp(c!1) * x!1 ^ (n!1 + 1) / factorial(n!1 + 1)" )"1" (replace -1)"1" (rewrite "abs_div" 1)"1" (expand "abs" 1 2)"1" "both_sides_div_pos_le1" "x" "abs(exp(c!1) * x!1 ^ (1 + n!1))" "y" "max(exp(x!1),1) * x!1 ^ (1 + n!1)" "pz" "factorial(1 + n!1)" ))"1" (hide -1 -2 -7)"1" (rewrite "abs_mult" )"1" (expand "abs" 1 1)"1" (case "exp(c!1)<=max(exp(x!1),1)" )"1" "1" "expt_pos" "px" "x!1" "i" "1+n!1" ))"1" expand "abs" 1)"1" "exp_strict_increasing" )"1" expand "strict_increasing?" )"1" "0" "c!1" )"1" "c!1" "x!1" )"1" rewrite "exp_0" )"1" assert )"1" "1" expand "max" )"1" assert )"1" "both_sides_times_pos_lt1" "x" "exp(c!1)" "y" "exp(x!1)" "pz" "x!1^(1+n!1)" ))"1" assert )"1" "both_sides_div_pos_lt1" "x" "exp(c!1) * x!1 ^ (1 + n!1)" "y" "exp(x!1) * x!1 ^ (1 + n!1)" "pz" "factorial(1+n!1)" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" replace -1)"2" replace -5)"2" rewrite "exp_0" )"2" expand "max" )"2" expand "^" )"2" expand "expt" )"2" expand "abs" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "exp_strict_increasing" )"3" expand "strict_increasing?" )"3" assert )"3" "3" "3" "x!1" "c!1" )"3" "c!1" "0" )"3" rewrite "exp_0" )"3" expand "max" )"3" assert )"3" "exp(c!1)" )"3" "3" case "abs(x!1 ^ (1 + n!1)) = abs(x!1) ^ (1 + n!1)" )"1" "posreal_div_posreal_is_posreal" "px" "abs(x!1) ^ (1 + n!1)" "py" "factorial(1 + n!1)" ))"1" "both_sides_times_pos_le1" "x" "exp(c!1)" "y" "1" "pz" "abs(x!1) ^ (1 + n!1) / factorial(1 + n!1)" ))"1" assert )nil nil )"2" nil nil ))nil )"2" "2" "expt_pos" "px" "abs(x!1)" "i" "1+n!1" ))"1" nil nil )"2" "2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "FORALL (n:nat): abs(x!1^n) = abs(x!1)^n" )"1" "1+n!1" )nil nil )"2" "2" "n" )"1" rewrite "expt_x0" )"1" rewrite "expt_x0" )"1" expand "abs" )"1" nil nil ))nil ))nil ))nil )"2" "2" expand "^" )"2" expand "expt" "2" rewrite "abs_mult" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "max" )"2" "exp_strict_increasing" )"2" expand "strict_increasing?" )"2" "1" assert )"1" "1" "0" "c!1" )"1" "c!1" "x!1" )"1" rewrite "exp_0" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace -1)"2" replace -3)"2" rewrite "exp_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" "x!1" "c!1" )"3" "c!1" "0" )"3" rewrite "exp_0" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))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_series nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )nil taylors "analysis/" )"posnat" factorial "ints/" )nil integers nil )nil integers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"real" exp_series nil )"{py | x = ln(py)}" ln_exp nil )"real" ln_exp nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"posint" nil )"real" reals nil )nil reals nil )nil real_props nil )"{j: posint | j >= i}" nil )"nnreal" nil )"posint" nil )nil real_props nil )"[numfield -> numfield]" number_fields nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil real_props nil )"{y: posreal | y >= x}" nil )"bool" reals nil )nil real_props nil )nil real_types nil )nil defined_types nil )nil naturalnumbers nil )nil exponentiation nil )"nnreal" exponentiation nil )"nat" exponentiation nil )"nat" exponentiation nil )"nonneg_rat" nil )"real" exponentiation nil )"{j: nonneg_int | j >= i}" nil )nil exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil ln_exp nil )nil ln_exp nil )nil real_props nil )nil real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" real_fun_preds "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"nnreal" nil )"nnreal" exponentiation nil )"{z: posreal | z >= x AND z >= y}" real_defs nil )"real" reals nil )"odd_int" integers nil )"real" reals nil )nil real_axioms nil )"real" reals nil ))nil )nil 3302449625"" (skosimp*)"" (lemma "exp_taylors" ("x" "x!1" "n" "n!1" ))"" (skosimp*)"" (typepred "c!1" )"" (lemma "trichotomy" ("x" "x!1" ))"" case "exp(x!1) - exp_series_n(x!1, n!1) = exp(c!1) * x!1 ^ (n!1 + 1) / factorial(n!1 + 1)" )"1" (replace -1)"1" (rewrite "abs_div" 1)"1" (expand "abs" 1 2)"1" "both_sides_div_pos_le1" "x" "abs(exp(c!1) * x!1 ^ (1 + n!1))" "y" "max(exp(x!1),1) * x!1 ^ (1 + n!1)" "pz" "factorial(1 + n!1)" ))"1" (hide -1 -2 -7)"1" (rewrite "abs_mult" )"1" (expand "abs" 1 1)"1" (case "exp(c!1)<=max(exp(x!1),1)" )"1" "1" "expt_pos" "px" "x!1" "i" "1+n!1" ))"1" expand "abs" 1)"1" "exp_strict_increasing" )"1" expand "strict_increasing?" )"1" "0" "c!1" )"1" "c!1" "x!1" )"1" rewrite "exp_0" )"1" assert )"1" "1" expand "max" )"1" assert )"1" "both_sides_times_pos_lt1" "x" "exp(c!1)" "y" "exp(x!1)" "pz" "x!1^(1+n!1)" ))"1" assert )"1" "both_sides_div_pos_lt1" "x" "exp(c!1) * x!1 ^ (1 + n!1)" "y" "exp(x!1) * x!1 ^ (1 + n!1)" "pz" "factorial(1+n!1)" ))"1" assert )nil )))))))))))))))))))))))))))"2" (assert ) nil )))"2" replace -1)"2" replace -5)"2" rewrite "exp_0" )"2" expand "max" )"2" expand "^" )"2" expand "expt" )"2" expand "abs" )"2" assert )nil )))))))))))))))"3" "exp_strict_increasing" )"3" expand "strict_increasing?" )"3" assert )"3" "3" "3" "x!1" "c!1" )"3" "c!1" "0" )"3" rewrite "exp_0" )"3" expand "max" )"3" assert )"3" "exp(c!1)" )"3" "3" case "abs(x!1 ^ (1 + n!1)) = abs(x!1) ^ (1 + n!1)" )"1" "posreal_div_posreal_is_posreal" "px" "abs(x!1) ^ (1 + n!1)" "py" "factorial(1 + n!1)" ))"1" "both_sides_times_pos_le1" "x" "exp(c!1)" "y" "1" "pz" "abs(x!1) ^ (1 + n!1) / factorial(1 + n!1)" ))"1" assert )"1" replace "1" assert )nil )))))"2" nil )))"2" "2" "expt_pos" "px" "abs(x!1)" "i" "1+n!1" ))"1" nil )"2" "2" expand "abs" )"2" assert )nil )))))))))))"2" "2" case "FORALL (n:nat): abs(x!1^n) = abs(x!1)^n" )"1" "1+n!1" )nil )"2" "2" "n" )"1" rewrite "expt_x0" )"1" rewrite "expt_x0" )"1" expand "abs" )"1" nil )))))))"2" "2" expand "^" )"2" expand "expt" "2" rewrite "abs_mult" "2" assert )nil )))))))))))))))))))))))))))))))))))))))))))))"2" "2" expand "max" )"2" "exp_strict_increasing" )"2" expand "strict_increasing?" )"2" "1" assert )"1" "1" "0" "c!1" )"1" "c!1" "x!1" )"1" rewrite "exp_0" )"1" assert )nil )))))))))))"2" assert )"2" replace -1)"2" replace -3)"2" rewrite "exp_0" )"2" assert )nil )))))))))"3" assert )"3" "3" "x!1" "c!1" )"3" "c!1" "0" )"3" rewrite "exp_0" )"3" assert )nil )))))))))))))))))))))))))))))))))))))"2" (assert ) nil ))))))))))))nil )nil nil ))nil 3559669148"" (name "TT" "LAMBDA (x:real): -1<=x" )"" case "FORALL (n:nat): FORALL (m:nat): m<=n IMPLIES increasing?(LAMBDA (x:(TT)): exp_estimate(x,m)) AND exp_estimate(-1,m)>=0" )"1" (skeep)"1" (inst - "n" )"1" (inst - "n" )"1" (assert )"1" (flatten)"1" (expand "increasing?" )"1" (inst - "x" "y" )"1" (assert ) nil nil )"2" (expand "TT" ) (("2" (assert ) nil nil )) nil )"3" (expand "TT" ) (("3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "n" )"1" (skeep)"1" (case "m = 0" )"1" (replace -1)"1" (assert ) (("1" (grind) nil nil )) nil )) nil )"2" (assert ) nil nil ))nil ))nil )"2" (skeep)"2" (skeep)"2" (case "NOT j = m-1" )"1" (inst - "m" ) (("1" (assert ) nil nil )) nil )"2" (replace -1)"2" (assert )"2" (hide -3)"2" (hide -1)"2" (case "NOT exp_estimate(-1,m)>=0" )"1" (hide 2)"1" (lemma "even_or_odd" )"1" "m" )"1" "1" expand "even?" )"1" "1" "1" "2*j!1-1" )"1" assert )"1" "1" "1" expand "exp_estimate" )"1" expand "sigma" +)"1" assert )"1" case "j!1 = 0" )"1" "1" assert )nil nil ))nil )"2" assert )"2" case "1 > 2*j!1" )"1" assert )nil nil )"2" assert )"2" case "(-1) ^ (2 * j!1) / factorial(2 * j!1) >= 0" )"1" assert )nil nil )"2" "2" "2" "even_m1_pow" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "NOT j!1 = 0" )"1" case "j!1 >= 1" )"1" (assert ) nil nil )"2" assert )"2" expand "exp_estimate" )"2" expand "sigma" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" replace -1)"2" assert )"2" expand "exp_estimate" )"2" expand "sigma" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "m-2" )"1" assert )"1" "1" "1" expand "odd?" )"1" "1" case "NOT j!1 >= 0" )"1" (assert ) nil nil )"2" assert )"2" "2" assert )"2" expand "exp_estimate" )"2" expand "sigma" "2" expand "sigma" "2" assert )"2" case "j!1 = 0" )"1" assert )"1" "1" assert )nil nil ))nil ))nil )"2" assert )"2" case "-((-1) ^ (1 + 2 * j!1)) / factorial(1 + 2 * j!1) ") "1" assert )nil nil )"2" "2" "2" "even_m1_pow" )"2" "2*j!1" )"2" assert )"2" "2" "not_even_m1_pow" )"2" "1+2*j!1" )"2" assert )"2" "2" assert )"2" "2" "factorial(2*j!1)" )"2" "2*j!1" )"2" expand "factorial" "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 )"2" assert )"2" case "m = 0" )"1" "1" "1" (grind) nil nil ))nil ))nil )"2" case "m = 1" )"1" "1" "1" (grind) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (lemma "poly_increasing" )"2" expand "increasing?" )"2" "2" "exp_seq" "m" "x!1" "y!1" )"2" assert )"2" case "polynomial(exp_seq,m) = LAMBDA (gg:real): exp_estimate(gg,m)" )"1" replace -1)"1" assert )"1" "1" "1" "m-1" )"1" assert )"1" "1" "-1" "c!1" )"1" assert )"1" "x!1" )"1" expand "TT" )"1" assert )"1" case "polynomial(poly_deriv(exp_seq),m-1) = LAMBDA (gg:real): exp_estimate(gg,m-1)" )"1" replace "1" assert )nil nil ))nil )"2" "2" "2" expand "exp_estimate" )"2" expand "polynomial" )"2" "sigma_split" )"2" "2" "0" )"2" assert )"2" replace "2" "2" case "FORALL (a1,a2,b1,b2:real): a1=b1 AND a2=b2 IMPLIEs a1+a2 = b1+b2" )"1" rewrite "1" "1" nil nil ))nil )"2" "2" rewrite "sigma_eq" )"2" "2" "2" expand "exp_seq" )"2" expand "poly_deriv" )"2" case "(1+n!1)/factorial(1+n!1) = 1/factorial(n!1)" )"1" assert )nil nil )"2" "2" expand "factorial" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))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 ))nil ))nil )"2" expand "TT" )"2" assert )"2" "x!1" )"2" expand "TT" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" expand "TT" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "polynomial" )"2" "sigma_split" )"2" "2" "0" )"2" assert )"2" "2" expand "exp_estimate" )"2" case "FORALL (a1,a2,b1,b2:real): a1=b1 AND a2=b2 IMPLIEs a1+a2 = b1+b2" )"1" rewrite "1" "1" nil nil ))nil )"2" "2" rewrite "sigma_eq" )"2" "2" "2" expand "exp_seq" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" exp_series nil )"bool" real_fun_preds "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" exp_series nil )"real" exp_series nil )"[real -> bool]" exp_series nil )nil defined_types nil )nil naturalnumbers nil )"real" exponentiation nil )"real" sigma "reals/" )"(strict_total_order?[real])" real_props nil )"nzrat" rationalsnil )"real" reals nil )nil naturalnumbers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"odd_int" integersnil )"[numfield, numfield -> numfield]" number_fields nil )"int" exp_series nil )"int" exponentiation nil )"nzreal" exponentiation nil )nil exponentiation nil )nil real_types nil )nil real_types nil )nil real_props nil )"posnat" factorial "ints/" )nil integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"bool" reals nil )"nonneg_int" nil )"rat" exponentiation nil )"bool" integers nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" exponentiation nil )"even_int" integersnil )"odd_int" integersnil )nil exponentiation nil )"posrat" nil )"even_int" integersnil )nil real_props nil )"nzint" integersnil )nil real_props nil )nil reals nil )nil real_props nil )"posint" nil )nil real_props nil )"nzrat" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )nil exponentiation nil )nil factorial "ints/" )"rat" rationals nil )"posint" nil )"odd_int" integers nil )"bool" integers nil )"nat" exp_series nil )nil polynomials "reals/" )"real" polynomials "reals/" )"real" reals nil )nil sigma "reals/" )nil sigma "reals/" )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"nonneg_rat" nil )"posrat" nil )"posrat" nil )nil sigma "reals/" )nil integers nil )"rat" rationals nil )nil sigma "reals/" )"real" exp_series nil )"[real -> real]" polynomials "reals/" )nil sequences nil )"real" exp_series nil )"int" integers nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )"odd_int" integers 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 )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil ))nil 3568453550"" (case "FORALL (m:posnat): exp_estimate(-1,m)>=0" )"1" case "FORALL (m:posnat): m>1 IMPLIES exp_estimate(-1,m) > 0" )"1" (skeep)"1" (inst - "n" )"1" (assert )"1" (lemma "exp_estimate_increasing" )"1" (inst - "n" "-1" "x" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (copy -1)"2" (skeep)"2" (inst - "m" )"2" (case "NOT exp_estimate(-1,m) = 0" )"1" (assert ) nil nil )"2" (hide (-2 1))"2" (lemma "even_or_odd" )"2" (inst - "m" )"2" (ground)"1" (expand "even?" )"1" (skeep -1)"1" (replaces -1)"1" assert )"1" "2*j-1" )"1" assert )"1" expand "exp_estimate" )"1" expand "sigma" - 1)"1" case "(-1) ^ (2 * j) / factorial(2 * j) > 0" )"1" assert )"1" "rd" "1 + sigma(1, 2 * j - 1, LAMBDA (nn: nat): (-1) ^ nn / factorial(nn))" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "even_m1_pow" )"2" "2*j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "odd?" )"2" (skeep -1)"2" (case "NOT j >= 1" )"1" case "j = 1" )"1" "1" "1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "m-2" )"1" expand "exp_estimate" )"1" expand "sigma" - 1)"1" expand "sigma" - 1)"1" "aa" "1 + sigma(1, m - 2, LAMBDA (nn: nat): (-1) ^ nn / factorial(nn))" )"1" "1" case "((-1) ^ (m - 1)) / factorial(m - 1) > (-(-1) ^ m) / factorial(m)" )"1" (assert ) nil nil )"2" "even_m1_pow" )"2" "2" assert )"2" "2*j" )"2" assert )"2" "2" assert )"2" "not_even_m1_pow" )"2" "1+2*j" )"2" assert )"2" "2" assert )"2" "2" "factorial(2*j)" )"2" expand "factorial" "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 )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" case "FORALL (mm: nat): FORALL (kk:nat): kk<=mm IMPLIES exp_estimate(-1, kk) >= 0" )"1" (skeep)"1" (inst - "m" )"1" (inst - "m" ) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (hide 2)"2" (induct "mm" )"1" (grind) nil nil )"2" (skeep)"2" (skeep)"2" (case "NOT kk = j+1" )"1" (inst - "kk" ) (("1" (assert ) nil nil )) nil )"2" (hide -3)"2" (assert )"2" (assert )"2" (replaces -1)"2" (case "j = 0" )"1" (replaces -1)"1" "1" (grind) nil nil ))nil ))nil )"2" (lemma "even_or_odd" )"2" "1+j" )"2" "1" expand "even?" )"1" "1" "2*j!1-1" )"1" assert )"1" "1" expand "exp_estimate" )"1" expand "sigma" +)"1" assert )"1" case "(-1) ^ (2 * j!1) / factorial(2 * j!1) >= 0" )"1" assert )nil nil )"2" "2" "even_m1_pow" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" expand "odd?" )"2" "2" "j-1" )"2" "2" assert )"2" expand "exp_estimate" )"2" expand "sigma" +)"2" case "1> 1+2*j!1" )"1" assert )nil nil )"2" assert )"2" expand "sigma" "2" assert )"2" case "-((-1) ^ (1 + 2 * j!1)) / factorial(1 + 2 * j!1) ") "1" assert )nil nil )"2" "2" "even_m1_pow" )"2" "2*j!1" )"2" assert )"2" "2" "not_even_m1_pow" )"2" "2" assert )"2" "2" "2" case "1+2*j!1 > 1" )"1" "factorial(2*j!1)" )"1" expand "factorial" "1" assert )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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" nil )nil real_props nil )"int" exp_series nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_props nil )"real" exponentiation nil )"posint" nil )"nzreal" exponentiation nil )"int" exponentiation nil )nil naturalnumbers nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"nat" exp_series nil )nil exp_series nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"bool" integers nil )"odd_int" integers nil )"nzrat" rationals nil )"posrat" nil )"nzint" integersnil )nil real_props nil )nil reals nil )nil extra_real_props nil )"posint" nil )"int" integers nil )nil real_props nil )nil exponentiation nil )"nzint" integers nil )"posnat" exp_series nil )"bool" integers nil )"odd_int" integersnil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" exponentiation nil )"nzreal" exponentiation nil )"nzrat" rationalsnil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"posnat" factorial "ints/" )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"rat" rationals nil )"even_int" integersnil )"int" integers nil )"real" reals nil )"rat" rationals nil )"real" reals nil )nil exponentiation nil )"nonneg_int" nil )nil real_types nil )nil real_types nil )nil extra_real_props nil )"real" sigma "reals/" )"rat" exponentiation nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"odd_int" integers nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )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 integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"real" exp_series nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil ))nil 3568629731"" (induct "n" )"1" (grind) nil nil )"2" (skeep)"2" (expand "exp_estimate" )"2" (expand "sigma" +) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil )"nnreal" nil )"posint" nil )nil power_series "series/" )"nat" exponentiation nil )"real" exponentiation nil )"real" sigma "reals/" )"(strict_total_order?[real])" real_props nil )"nonneg_rat" nil )"nnreal" sigma_nat "reals/" )"posreal" nil )nil naturalnumbers nil )"real" exp_series nil )"[T, T -> boolean]" equalities nil )nil defined_types 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 ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.263Angebot
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-29)
¤ *Eine klare Vorstellung vom Zielzustand
2026-05-26
