Impressum exp_approx.prf

Sprache: Lisp

(exp_approx
(exp_neg_le1_bounds 0
 (exp_neg_le1_bounds-3 nil 3307800311
 ("" (skosimp)
 (("" (case "exp(x!1) < exp_neg_le1_ub(n!1, x!1)")
 (("1" (assert)
 (("1" (expand "exp_neg_le1_ub")
 (("1" (expand "exp_neg_le1_lb")
 (("1" (lemma "exp_taylors_err")
 (("1" (inst - "2*n!1" "x!1")
 (("1" (expand "abs")
 (("1" (assert)
 (("1"
 (case "(max(exp(x!1), 1) * (-x!1) ^ (1 + 2 * n!1)) <= 1")
 (("1" (mult-by -1 "1/factorial(1+2*n!1)")
 (("1" (assert) nil nil)) nil)
 ("2" (assert)
 (("2"
 (case "FORALL (aa,bb:nnreal): aa<=1 AND bb<=1 IMPLIES aa*bb <= 1")
 (("1" (rewrite -1)
 (("1" (expand "max" 1)
 (("1"
 (lift-if)
 (("1"
 (ground)
 (("1"
 (lemma "exp_increasing")
 (("1"
 (expand "increasing?")
 (("1"
 (inst - "x!1" "0")
 (("1" (assert) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (lemma "both_sides_expt_pos_le")
 (("2"
 (inst - "1+2*n!1" "-x!1" "1")
 (("2" (assert) nil nil))
 nil))
 nil)
 ("3" (assert)
 (("3"
 (lemma "nnreal_expt")
 (("3"
 (expand "^")
 (("3" (inst?) nil nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (hide-all-but 1)
 (("2" (skeep)
 (("2"
 (mult-ineq -1 -2)
 (("2" (assert) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (hide 2)
 (("2" (expand "exp_neg_le1_ub")
 (("2"
 (name "FF" "LAMBDA (nn:nat): exp_estimate(x!1, 2 * nn)")
 (("2"
 (comment "this part of the proof changed 1/30/2013 by Anthony")
 (("2" (case "FORALL (nn:nat): FF(nn+1) < FF(nn)")
 (("1"
 (case "FORALL (epsil:posreal): EXISTS (M:nat): FORALL (nn:nat): nn>=M IMPLIES abs(exp(x!1)-exp_estimate(x!1,nn)) < epsil")
 (("1"
 (case "FORALL (nn,mm:nat): mm>nn IMPLIES FF(mm) < FF(nn)")
 (("1" (hide -3)
 (("1" (inst-cp - "n!1" "n!1+1")
 (("1" (assert)
 (("1" (case "NOT exp(x!1)>=FF(n!1)")
 (("1" (expand "FF" 1)
 (("1" (assert) nil nil)) nil)
 ("2" (inst -4 "(exp(x!1) - FF(1+n!1))/2")
 (("1"
 (skeep -4)
 (("1"
 (case
 "EXISTS (KK:posnat): 2*KK > M AND KK > 1+n!1")
 (("1"
 (skeep -1)
 (("1"
 (inst -6 "2*KK")
 (("1"
 (assert)
 (("1"
 (inst - "1+n!1" "KK")
 (("1"
 (assert)
 (("1"
 (expand "FF")
 (("1" (assert) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (hide-all-but 1)
 (("2"
 (inst + "max(M+1,2+n!1)")
 (("2" (grind) nil nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (assert) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (hide 2)
 (("2" (hide -1)
 (("2"
 (case "FORALL (nn,mm:nat): FF(nn+1+mm) <= FF(nn+1)")
 (("1" (skeep)
 (("1" (case "mm = nn+1")
 (("1"
 (inst -4 "nn")
 (("1" (assert) nil nil))
 nil)
 ("2"
 (assert)
 (("2"
 (inst - "nn" "mm-1-nn")
 (("2"
 (assert)
 (("2"
 (inst - "nn")
 (("2" (assert) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (hide 2)
 (("2" (induct "mm")
 (("1" (assert) nil nil)
 ("2"
 (skeep)
 (("2"
 (skeep)
 (("2"
 (assert)
 (("2"
 (inst - "nn")
 (("2"
 (assert)
 (("2"
 (inst - "(1+j+nn)")
 (("2" (assert) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (hide (-1 -2 2))
 (("2" (lemma "exp_taylors_err")
 (("2" (lemma "archimedean")
 (("2" (skeep)
 (("2" (inst - "epsil")
 (("2" (skosimp*)
 (("2"
 (inst + "n!2 + 2")
 (("2"
 (skeep)
 (("2"
 (inst - "nn" "x!1")
 (("2"
 (case
 "(max(exp(x!1), 1) * abs(x!1) ^ (1 + nn)) <= 1")
 (("1"
 (mult-by
 -1
 "1/factorial(1+nn)")
 (("1"
 (assert)
 (("1"
 (case
 "1/factorial(1+nn) < 1/n!2")
 (("1" (assert) nil nil)
 ("2"
 (cross-mult 1)
 (("2"
 (case
 "FORALL (kkr:nat): factorial(1+kkr)>=kkr")
 (("1"
 (assert)
 (("1"
 (inst - "nn")
 (("1"
 (assert)
 nil
 nil))
 nil))
 nil)
 ("2"
 (hide-all-but 1)
 (("2"
 (induct "kkr")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (skeep)
 (("2"
 (assert)
 (("2"
 (expand
 "factorial"
 +)
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (case
 "FORALL (aa,bb:nnreal): aa<=1 AND bb<=1 IMPLIES aa*bb <= 1")
 (("1"
 (rewrite -1)
 (("1"
 (expand "max" 1)
 (("1"
 (lift-if)
 (("1"
 (ground)
 (("1"
 (lemma
 "exp_increasing")
 (("1"
 (expand
 "increasing?")
 (("1"
 (inst
 -
 "x!1"
 "0")
 (("1"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (lemma
 "both_sides_expt_pos_le")
 (("2"
 (inst
 -
 "1+nn"
 "abs(x!1)"
 "1")
 (("2"
 (assert)
 (("2"
 (expand "abs" 1)
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (hide-all-but 1)
 (("2"
 (skeep)
 (("2"
 (mult-ineq -1 -2)
 (("2" (assert) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (hide (-1 2))
 (("2" (skeep)
 (("2" (expand "FF")
 (("2" (expand "exp_estimate")
 (("2" (expand "sigma" + 1)
 (("2" (expand "sigma" + 1)
 (("2"
 (case "-(x!1 ^ (1 + 2 * nn)) / factorial(1 + 2 * nn)
 > (x!1 ^ (2 + 2 * nn)) / factorial(2 + 2 * nn)")
 (("1" (assert) nil nil)
 ("2"
 (hide 2)
 (("2"
 (case
 "-(x!1 ^ (1 + 2 * nn)) >=
 (x!1 ^ (2 + 2 * nn))")
 (("1"
 (cross-mult 1)
 (("1"
 (mult-by -1 "factorial(1+2*nn)")
 (("1"
 (case "2+2*nn > 1")
 (("1"
 (mult-by
 -1
 "-(x!1 ^ (1 + 2 * nn)) * factorial(1 + 2 * nn)")
 (("1"
 (assert)
 (("1"
 (expand "factorial" + 1)
 (("1" (assert) nil nil))
 nil))
 nil)
 ("2"
 (hide 2)
 (("2"
 (case
 "FORALL (aa:real): aa > 0 IMPLIES (aa>=0 AND aa>0)")
 (("1"
 (rewrite -1)
 (("1"
 (hide 2)
 (("1"
 (lemma
 "posreal_exp")
 (("1"
 (inst
 -
 "(1+2*nn)"
 "-x!1")
 (("1"
 (assert)
 (("1"
 (lemma
 "mult_expt")
 (("1"
 (inst
 -
 "1+2*nn"
 "-1"
 "x!1")
 (("1"
 (replaces
 -1)
 (("1"
 (lemma
 "not_even_m1_pow")
 (("1"
 (inst?)
 (("1"
 (split
 -)
 (("1"
 (replaces
 -1)
 (("1"
 (mult-by
 -1
 "factorial(1+2*nn)")
 (("1"
 (assert)
 nil
 nil))
 nil))
 nil)
 ("2"
 (lemma
 "even_or_odd")
 (("2"
 (inst?)
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (hide-all-but 1)
 (("2" (grind) nil nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (assert) nil nil))
 nil))
 nil))
 nil)
 ("2"
 (hide 2)
 (("2"
 (mult-by
 -1
 "-(x!1 ^ (1 + 2 * nn))")
 (("1"
 (assert)
 (("1"
 (expand "^")
 (("1"
 (expand "expt" + 2)
 (("1" (assert) nil nil))
 nil))
 nil))
 nil)
 ("2"
 (hide 2)
 (("2"
 (lemma "mult_expt")
 (("2"
 (inst
 -
 "1+2*nn"
 "-1"
 "x!1")
 (("2"
 (lemma "posreal_exp")
 (("2"
 (inst
 -
 "1+2*nn"
 "-x!1")
 (("2"
 (replaces -2)
 (("2"
 (lemma
 "not_even_m1_pow")
 (("2"
 (inst?)
 (("2"
 (split -)
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (lemma
 "even_or_odd")
 (("2"
 (inst?)
 (("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))
 ";;; this part of the proof changed 1/30/2013 by Anthony"))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ((exp_neg_le1_ub const-decl "real" exp_approx nil)
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (int nonempty-type-eq-decl nil integers nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (exp const-decl "{py | x = ln(py)}" ln_exp nil)
 (ln const-decl "real" ln_exp nil)
 (= const-decl "[T, T -> boolean]" equalities nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (> const-decl "bool" reals nil)
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (real nonempty-type-from-decl nil reals nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (boolean nonempty-type-decl nil booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (exp_taylors_err formula-decl nil exp_series nil)
 (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
 nil)
 (<= const-decl "bool" reals nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
 (OR const-decl "[bool, bool -> bool]" booleans nil)
 (/= const-decl "boolean" notequal nil)
 (^ const-decl "real" exponentiation nil)
 (- const-decl "[numfield -> numfield]" number_fields nil)
 (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (posrat_times_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (factorial def-decl "posnat" factorial "ints/")
 (posnat nonempty-type-eq-decl nil integers nil)
 (nonneg_int nonempty-type-eq-decl nil integers nil)
 (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
 (nznum nonempty-type-eq-decl nil number_fields nil)
 (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
 nil)
 (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
 real_types nil)
 (nnreal type-eq-decl nil real_types nil)
 (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
 (nnreal_expt judgement-tcc nil exponentiation nil)
 (both_sides_expt_pos_le formula-decl nil exponentiation nil)
 (expt_1i formula-decl nil exponentiation nil)
 (posint_exp application-judgement "posint" exponentiation nil)
 (real_gt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (increasing? const-decl "bool" real_fun_preds "reals/")
 (exp_0 formula-decl nil ln_exp nil)
 (exp_increasing formula-decl nil ln_exp nil)
 (n!1 skolem-const-decl "nat" exp_approx nil)
 (x!1 skolem-const-decl "real" exp_approx nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (le_times_le_any1 formula-decl nil extra_real_props nil)
 (posint_times_posint_is_posint application-judgement "posint"
 integers nil)
 (odd_times_odd_is_odd application-judgement "odd_int" integers nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
 (minus_real_is_real application-judgement "real" reals nil)
 (real_div_nzreal_is_real application-judgement "real" reals nil)
 (real_times_real_is_real application-judgement "real" reals nil)
 (posreal_max application-judgement
 "{z: posreal | z >= x AND z >= y}" real_defs nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (real_minus_real_is_real application-judgement "real" reals nil)
 (exp_neg_le1_lb const-decl "real" exp_approx nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (even_times_int_is_even application-judgement "even_int" integers
 nil)
 (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
 integers nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (minus_odd_is_odd application-judgement "odd_int" integers nil)
 (sigma def-decl "real" sigma "reals/")
 (real_plus_real_is_real application-judgement "real" reals nil)
 (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
 nil)
 (both_sides_times_pos_gt1 formula-decl nil real_props nil)
 (nn skolem-const-decl "nat" exp_approx nil)
 (mult_expt formula-decl nil exponentiation nil)
 (even_or_odd formula-decl nil naturalnumbers nil)
 (nzreal_exp application-judgement "nzreal" exponentiation nil)
 (int_exp application-judgement "int" exponentiation nil)
 (not_even_m1_pow formula-decl nil exponentiation nil)
 (nzreal nonempty-type-eq-decl nil reals nil)
 (posreal_exp judgement-tcc nil exponentiation nil)
 (div_mult_pos_gt2 formula-decl nil extra_real_props nil)
 (div_mult_pos_gt1 formula-decl nil extra_real_props nil)
 (expt def-decl "real" exponentiation nil)
 (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (int_minus_int_is_int application-judgement "int" integers nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (pred type-eq-decl nil defined_types nil)
 (nat_induction formula-decl nil naturalnumbers nil)
 (even_plus_even_is_even application-judgement "even_int" integers
 nil)
 (posrat_max application-judgement "{s: posrat | s >= q AND s >= r}"
 real_defs nil)
 (posint_max application-judgement "{k: posint | i <= k AND j <= k}"
 real_defs nil)
 (FF skolem-const-decl "[nat -> real]" exp_approx nil)
 (NOT const-decl "[bool -> bool]" booleans nil)
 (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
 real_types nil)
 (nnreal_exp application-judgement "nnreal" exponentiation nil)
 (div_mult_pos_lt1 formula-decl nil real_props nil)
 (times_div2 formula-decl nil real_props nil)
 (nonzero_real nonempty-type-eq-decl nil reals nil)
 (div_mult_pos_lt2 formula-decl nil real_props nil)
 (factorial_1 formula-decl nil factorial "ints/")
 (archimedean formula-decl nil real_props nil)
 (nnint_plus_posint_is_posint application-judgement "posint"
 integers nil)
 (exp_estimate const-decl "real" exp_series nil))
 nil)
 (exp_neg_le1_bounds-2 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"
 (case-replace
 "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"
 (name-replace
 "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"
 (inst -2 "1+2*n!1" "2+2*n!1")
 (("2"
 (assert)
 (("2"
 (case-replace
 "abs(x!1) ^ (1 + 2 * n!1) = -(x!1^(1+2*n!1))")
 (("1" (assert) nil)
 ("2"
 (hide 2 3 -1 -3)
 (("2"
 (hide -1 -2 -3)
 (("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"
 (case-replace
 "(-x!1) ^ 2=x!1 ^ 2")
 (("1"
 (assert)
 nil)
 ("2"
 (hide
 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"
 (lemma "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"
 (name-replace
 "LB"
 "sigma(0, 1 + 2 * n!1,
 LAMBDA (nn: nat):
 IF nn = 0 THEN 1 ELSE x!1 ^ nn / factorial(nn) ENDIF)")
 (("2"
 (case-replace
 "exp(x!1) - LB - (x!1 ^ (2 + 2 * n!1)) / factorial(2 + 2 * n!1) < 0")
 (("1"
 (hide -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"
 (hide -1 2)
 (("2"
 (inst - "2+2*n!1" "3+2*n!1")
 (("2"
 (assert)
 (("2"
 (case-replace
 "abs(x!1) ^ (2 + 2 * n!1) = x!1 ^ (2 + 2 * n!1)")
 (("1" (assert) nil)
 ("2"
 (hide -1 2)
 (("2"
 (lemma
 "expt_times"
 ("i"
 "2"
 "j"
 "1+n!1"))
 (("2"
 (inst-cp
 -
 "abs(x!1)")
 (("1"
 (inst - "x!1")
 (("1"
 (case-replace
 "abs(x!1)^2 = x!1^2")
 (("1"
 (assert)
 nil)
 ("2"
 (hide-all-but
 (-7 1))
 (("2"
 (expand
 "^")
 (("2"
 (expand
 "expt")
 (("2"
 (expand
 "expt")
 (("2"
 (expand
 "expt")
 (("2"
 (expand
 "abs")
 (("2"
 (assert)
 nil)))))))))))))))))
 ("2"
 (expand "abs")
 (("2"
 (assert)
 nil)))))))))))))))))))))
 ("2"
 (hide -1)
 (("2"
 (case
 "(x!1 ^ (2 + 2 * n!1)) / factorial(2 + 2 * n!1) > 0")
 (("1" (assert) nil)
 ("2"
 (hide 2 3)
 (("2"
 (inst -4 "1+n!1")
 (("2"
 (flatten)
 (("2"
 (lemma
 "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"
 (lemma "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"
 (lemma "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"
 (lemma
 "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"
 (case-replace "j!1=0")
 (("1"
 (expand "factorial" 1 2)
 (("1"
 (lemma
 "both_sides_times_pos_lt1"
 ("pz"
 "factorial(n!3)"
 "x"
 "1"
 "y"
 "1+n!3"))
 (("1" (assert) nil)))))
 ("2"
 (assert)
 (("2"
 (inst - "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"
 (lemma "both_sides_times_neg_lt1"
 ("nz" "x!1" "y" "0" "x" "x!1^(2*n!2)"))
 (("1"
 (lemma "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"
 (lemma "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"
 (lemma "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)
 (exp_neg_le1_bounds-1 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"
 (case-replace
 "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"
 (name-replace
 "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"
 (inst -2 "1+2*n!1" "2+2*n!1")
 (("2"
 (assert)
 (("2"
 (case-replace
 "abs(x!1) ^ (1 + 2 * n!1) = -(x!1^(1+2*n!1))")
 (("1" (assert) nil nil)
 ("2"
 (hide 2 3 -1 -3)
 (("2"
 (hide -1 -2 -3)
 (("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"
 (case-replace
 "(-x!1) ^ 2=x!1 ^ 2")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (hide
 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"
 (lemma "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"
 (name-replace
 "LB"
 "sigma(0, 1 + 2 * n!1,
 LAMBDA (nn: nat):
 IF nn = 0 THEN 1 ELSE x!1 ^ nn / factorial(nn) ENDIF)")
 (("2"
 (case-replace
 "exp(x!1) - LB - (x!1 ^ (2 + 2 * n!1)) / factorial(2 + 2 * n!1) < 0")
 (("1"
 (hide -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"
 (hide -1 2)
 (("2"
 (inst - "2+2*n!1" "3+2*n!1")
 (("2"
 (assert)
 (("2"
 (case-replace
 "abs(x!1) ^ (2 + 2 * n!1) = x!1 ^ (2 + 2 * n!1)")
 (("1" (assert) nil nil)
 ("2"
 (hide -1 2)
 (("2"
 (lemma
 "expt_times"
 ("i"
 "2"
 "j"
 "1+n!1"))
 (("2"
 (inst-cp
 -
 "abs(x!1)")
 (("1"
 (inst - "x!1")
 (("1"
 (case-replace
 "abs(x!1)^2 = x!1^2")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (hide-all-but
 (-7 1))
 (("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"
 (hide -1)
 (("2"
 (case
 "(x!1 ^ (2 + 2 * n!1)) / factorial(2 + 2 * n!1) > 0")
 (("1" (assert) nil nil)
 ("2"
 (hide 2 3)
 (("2"
 (inst -4 "1+n!1")
 (("2"
 (flatten)
 (("2"
 (lemma
 "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"
 (lemma "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"
 (lemma "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"
 (lemma
 "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"
 (case-replace "j!1=0")
 (("1"
 (expand "factorial" 1 2)
 (("1"
 (lemma
 "both_sides_times_pos_lt1"
 ("pz"
 "factorial(n!3)"
 "x"
 "1"
 "y"
 "1+n!3"))
 (("1" (assert) nil nil))
 nil))
 nil)
 ("2"
 (assert)
 (("2"
 (inst - "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"
 (lemma "both_sides_times_neg_lt1"
 ("nz" "x!1" "y" "0" "x" "x!1^(2*n!2)"))
 (("1"
 (lemma "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"
 (lemma "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"
 (lemma "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)
 ((max const-decl
 "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}"
 finite_sets_minmax "finite_sets/")
 (ln const-decl "real" ln_exp nil)
 (exp const-decl "{py | x = ln(py)}" ln_exp nil)
 (sigma def-decl "real" sigma "reals/")
 (strict_increasing? const-decl "bool" real_fun_preds "reals/")
 (exp_0 formula-decl nil ln_exp nil)
 (exp_strict_increasing formula-decl nil ln_exp nil))
 shostak))
(exp_neg_le1_ub_strict_decreasing_n 0
 (exp_neg_le1_ub_strict_decreasing_n-2 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)
 + (x!1 ^ (2 + 2 * m + 2 * n)) / factorial(2 + 2 * m + 2 * n) < 0")
 (("1" (case-replace "n=0")
 (("1"
 (assert)
 (("1"
 (lift-if)
 (("1"
 (ground)
 (("1"
 (case-replace "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"
 (hide -1)
 (("2"
 (lemma
 "both_sides_div_pos_lt1"
 ("x"
 "x!1 ^ (1 + 2 * m + 2 * n)"
 "y"
 "0"
 "pz"
 "factorial(1 + 2 * m + 2 * n)"))
 (("2"
 (lemma
 "expt_plus"
 ("n0x"
 "x!1"
 "i"
 "1"
 "j"
 "2*m+2*n"))
 (("1"
 (rewrite "expt_x1")
 (("1"
 (lemma
 "expt_times"
 ("n0x"
 "x!1"
 "i"
 "2"
 "j"
 "m+n"))
 (("1"
 (lemma
 "expt_pos"
 ("px" "x!1^2" "i" "m+n"))
 (("1"
 (lemma
 "both_sides_times_pos_lt1"
 ("x"
 "x!1"
 "y"
 "0"
 "pz"
 "x!1 ^ (2 * m + 2 * n)"))
 (("1"
 (assert)
 (("1"
 (lemma
 "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"
 (lemma
 "div_mult_pos_lt1"
 ("py"
 "2+2*n+2*m"
 "z"
 "-1*x!1"
 "x"
 "1"))
 (("1"
 (replace -1 -2)
 (("1"
 (hide -1)
 (("1"
 (assert)
 (("1"
 (rewrite
 "div_times"
 -1)
 (("1"
 (expand
 "factorial"
 1
 2)
 (("1"
 (lemma
 "expt_plus"
 ("n0x"
 "x!1"
 "i"
 "1"
 "j"
 "1+2*n+2*m"))
 (("1"
 (rewrite
 "expt_x1")
 (("1"
 (replace
 -1
 1)
 (("1"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (assert) nil nil))
 nil)
 ("2"
 (hide-all-but (-5 1))
 (("2"
 (lemma
 "negreal_times_negreal_is_posreal"
 ("nx" "x!1" "ny" "x!1"))
 (("1"
 (expand "^")
 (("1"
 (expand "expt")
 (("1"
 (expand "expt")
 (("1"
 (expand "expt")
 (("1"
 (propax)
 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)
 ((exp_neg_le1_ub const-decl "real" exp_approx nil)
 (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (exp_estimate const-decl "real" exp_series nil)
 (< const-decl "bool" reals nil)
 (posnat nonempty-type-eq-decl nil integers nil)
 (> const-decl "bool" reals nil)
 (nonneg_int nonempty-type-eq-decl nil integers nil)
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (>= const-decl "bool" reals nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (int nonempty-type-eq-decl nil integers nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (real nonempty-type-from-decl nil reals nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (boolean nonempty-type-decl nil booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
 integers nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (even_times_int_is_even application-judgement "even_int" integers
 nil)
 (posint_times_posint_is_posint application-judgement "posint"
 integers nil)
 (minus_odd_is_odd application-judgement "odd_int" integers nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (x!2 skolem-const-decl "nat" exp_approx nil)
 (y!1 skolem-const-decl "nat" exp_approx nil)
 (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (int_minus_int_is_int application-judgement "int" integers nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (real_gt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (even_plus_even_is_even application-judgement "even_int" integers
 nil)
 (both_sides_div_pos_lt1 formula-decl nil real_props nil)
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (expt_x1 formula-decl nil exponentiation nil)
 (expt_pos formula-decl nil exponentiation nil)
 (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat"
 rationals nil)
 (real_times_real_is_real application-judgement "real" reals nil)
 (div_mult_pos_lt1 formula-decl nil real_props nil)
 (nonzero_real nonempty-type-eq-decl nil reals nil)
 (div_times formula-decl nil real_props nil)
 (odd_plus_odd_is_even application-judgement "even_int" integers
 nil)
 (int_times_even_is_even application-judgement "even_int" integers
 nil)
 (- const-decl "[numfield -> numfield]" number_fields nil)
 (negreal nonempty-type-eq-decl nil real_types nil)
 (nonpos_real nonempty-type-eq-decl nil real_types nil)
 (<= const-decl "bool" reals nil)
 (both_sides_times_neg_lt1 formula-decl nil real_props nil)
 (both_sides_times_pos_lt1 formula-decl nil real_props nil)
 (negreal_times_negreal_is_posreal judgement-tcc nil real_types nil)
 (expt def-decl "real" exponentiation nil)
 (expt_times formula-decl nil exponentiation nil)
 (nzreal nonempty-type-eq-decl nil reals nil)
 (expt_plus formula-decl nil exponentiation nil)
 (= const-decl "[T, T -> boolean]" equalities nil)
 (real_div_nzreal_is_real application-judgement "real" reals nil)
 (nnint_plus_posint_is_posint application-judgement "posint"
 integers nil)
 (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
 (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
 integers nil)
 (factorial def-decl "posnat" factorial "ints/")
 (^ const-decl "real" exponentiation nil)
 (OR const-decl "[bool, bool -> bool]" booleans nil)
 (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
 (nznum nonempty-type-eq-decl nil number_fields nil)
 (/= const-decl "boolean" notequal nil)
 (real_plus_real_is_real application-judgement "real" reals nil)
 (sigma def-decl "real" sigma "reals/")
 (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
 (nat_induction formula-decl nil naturalnumbers nil)
 (pred type-eq-decl nil defined_types nil)
 (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
 (strict_decreasing? const-decl "bool" real_fun_preds "reals/"))
 nil)
 (exp_neg_le1_ub_strict_decreasing_n-1 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)
 + (x!1 ^ (2 + 2 * m + 2 * n)) / factorial(2 + 2 * m + 2 * n) < 0")
 (("1" (case-replace "n=0")
 (("1" (assert) nil nil)
 ("2" (assert) nil nil))
 nil)
 ("2" (hide 2 -1)
 (("2"
 (hide -1)
 (("2"
 (lemma
 "both_sides_div_pos_lt1"
 ("x"
 "x!1 ^ (1 + 2 * m + 2 * n)"
 "y"
 "0"
 "pz"
 "factorial(1 + 2 * m + 2 * n)"))
 (("2"
 (lemma
 "expt_plus"
 ("n0x"
 "x!1"
 "i"
 "1"
 "j"
 "2*m+2*n"))
 (("1"
 (rewrite "expt_x1")
 (("1"
 (lemma
 "expt_times"
 ("n0x"
 "x!1"
 "i"
 "2"
 "j"
 "m+n"))
 (("1"
 (lemma
 "expt_pos"
 ("px" "x!1^2" "i" "m+n"))
 (("1"
 (lemma
 "both_sides_times_pos_lt1"
 ("x"
 "x!1"
 "y"
 "0"
 "pz"
 "x!1 ^ (2 * m + 2 * n)"))
 (("1"
 (assert)
 (("1"
 (lemma
 "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"
 (lemma
 "div_mult_pos_lt1"
 ("py"
 "2+2*n+2*m"
 "z"
 "-1*x!1"
 "x"
 "1"))
 (("1"
 (replace -1 -2)
 (("1"
 (hide -1)
 (("1"
 (assert)
 (("1"
 (rewrite
 "div_times"
 -1)
 (("1"
 (expand
 "factorial"
 1
 2)
 (("1"
 (lemma
 "expt_plus"
 ("n0x"
 "x!1"
 "i"
 "1"
 "j"
 "1+2*n+2*m"))
 (("1"
 (rewrite
 "expt_x1")
 (("1"
 (replace
 -1
 1)
 (("1"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (assert) nil nil))
 nil)
 ("2"
 (hide-all-but (-5 1))
 (("2"
 (lemma
 "negreal_times_negreal_is_posreal"
 ("nx" "x!1" "ny" "x!1"))
 (("1"
 (expand "^")
 (("1"
 (expand "expt")
 (("1"
 (expand "expt")
 (("1"
 (expand "expt")
 (("1"
 (propax)
 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)
 ((sigma def-decl "real" sigma "reals/")
 (strict_decreasing? const-decl "bool" real_fun_preds "reals/"))
 shostak))
(exp_neg_le1_lb_pos 0
 (exp_neg_le1_lb_pos-2 nil 3307800417
 ("" (skeep)
 (("" (lemma "exp_neg_le1_bounds")
 (("" (inst?)
 (("" (assert)
 (("" (flatten)
 (("" (expand "exp_neg_le1_lb")
 (("" (expand "exp_neg_le1_ub")
 (("" (assert)
 ((""
 (case "1000001/1000000 / factorial(1 + 2 * pn) < exp(x)")
 (("1" (assert) nil nil)
 ("2" (lemma "exp_increasing")
 (("2" (expand "increasing?")
 (("2" (inst - "-1" "x")
 (("2" (assert)
 (("2"
 (case "1000001/1000000 / factorial(1 + 2 * pn) < exp(-1)")
 (("1" (assert) nil nil)
 ("2"
 (hide-all-but 1)
 (("2"
 (lemma "e_bnds")
 (("2"
 (rewrite "exp_int")
 (("2"
 (expand "^")
 (("2"
 (expand "expt")
 (("2"
 (expand "expt")
 (("2"
 (cross-mult 1)
 (("2"
 (case
 "FORALL (kk:posnat): factorial(1+2*kk) > 4*1000001/1000000")
 (("1"
 (inst?)
 (("1"
 (ground)
 nil
 nil))
 nil)
 ("2"
 (hide-all-but 1)
 (("2"
 (induct "kk")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (assert)
 nil
 nil)
 ("3"
 (skeep)
 (("3"
 (assert)
 (("3"
 (case "j = 0")
 (("1"
 (assert)
 (("1"
 (replaces
 -1)
 (("1"
 (hide -)
 (("1"
 (grind)
 nil
 nil))
 nil))
 nil))
 nil)
 ("2"
 (assert)
 (("2"
 (expand
 "factorial"
 +)
 (("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)
 ((exp_neg_le1_bounds formula-decl nil exp_approx nil)
 (real_gt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (minus_odd_is_odd application-judgement "odd_int" integers nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (posint_times_posint_is_posint application-judgement "posint"
 integers nil)
 (even_times_int_is_even application-judgement "even_int" integers
 nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (exp_neg_le1_lb const-decl "real" exp_approx nil)
 (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (real_minus_real_is_real application-judgement "real" reals nil)
 (exp_increasing formula-decl nil ln_exp nil)
 (- const-decl "[numfield -> numfield]" number_fields nil)
 (e_bnds formula-decl nil ln_exp nil)
 (^ const-decl "real" exponentiation nil)
 (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
 (pred type-eq-decl nil defined_types nil)
 (nat_induction formula-decl nil naturalnumbers nil)
 (factorial_1 formula-decl nil factorial "ints/")
 (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
 integers nil)
 (nnint_plus_posint_is_posint application-judgement "posint"
 integers nil)
 (even_plus_even_is_even application-judgement "even_int" integers
 nil)
 (div_mult_pos_lt2 formula-decl nil real_props nil)
 (posreal_times_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (int_times_even_is_even application-judgement "even_int" integers
 nil)
 (nonzero_real nonempty-type-eq-decl nil reals nil)
 (times_div2 formula-decl nil real_props nil)
 (posreal_div_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (e const-decl "posreal" ln_exp nil)
 (div_mult_pos_lt1 formula-decl nil real_props nil)
 (expt def-decl "real" exponentiation nil)
 (nzreal_exp application-judgement "nzreal" exponentiation nil)
 (posreal_exp application-judgement "posreal" exponentiation nil)
 (exp_int formula-decl nil ln_exp nil)
 (integer nonempty-type-from-decl nil integers nil)
 (increasing? const-decl "bool" real_fun_preds "reals/")
 (exp const-decl "{py | x = ln(py)}" ln_exp nil)
 (ln const-decl "real" ln_exp nil)
 (= const-decl "[T, T -> boolean]" equalities nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (factorial def-decl "posnat" factorial "ints/")
 (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
 (nznum nonempty-type-eq-decl nil number_fields nil)
 (/= const-decl "boolean" notequal nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (< const-decl "bool" reals nil)
 (exp_neg_le1_ub const-decl "real" exp_approx nil)
 (posnat nonempty-type-eq-decl nil integers nil)
 (> const-decl "bool" reals nil)
 (nonneg_int nonempty-type-eq-decl nil integers nil)
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (>= const-decl "bool" reals nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (int nonempty-type-eq-decl nil integers nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (real nonempty-type-from-decl nil reals nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (boolean nonempty-type-decl nil booleans nil)
 (number nonempty-type-decl nil numbers nil))
 nil)
 (exp_neg_le1_lb_pos-1 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"
 (lemma "quadratic_min_val"
 ("a"
 "1/2"
 "b"
 "1"
 "c"
 "1"
 "x"
 "x!1"
 "f"
 "quadratic(1/2,1,1)"
 "minpt"
 "-1"))
 (("2"
 (assert)
 (("2"
 (case-replace
 "(4 * (1 / 2) - 1) / (4 * (1 / 2)) = 1/2")
 (("1"
 (expand "quadratic")
 (("1"
 (case-replace
 "x!1 ^ 2 = sq(x!1)")
 (("1"
 (case "x!1 ^ 3 / 6 >= -1/6")
 (("1"
 (rewrite "expt_x1")
 (("1" (assert) nil nil))
 nil)
 ("2"
 (hide -2 -3 2)
 (("2"
 (lemma
 "sq_le"
 ("nna" "-x!1" "nnb" "1"))
 (("2"
 (assert)
 (("2"
 (rewrite "sq_neg")
 (("2"
 (expand "^")
 (("2"
 (expand "expt" 1)
 (("2"
 (replace -2 1)
 (("2"
 (lemma
 "sq_nz_pos")
 (("2"
 (inst
 -
 "-x!1")
 (("2"
 (rewrite
 "sq_neg")
 (("2"
 (hide -3)
 (("2"
 (lemma
 "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"
 (hide-all-but 1)
 (("2" (grind) nil nil))
 nil))
 nil))
 nil)
 ("2"
 (hide-all-but 1)
 (("2" (grind) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ((strict_increasing? const-decl "bool" real_fun_preds "reals/")
 (sigma def-decl "real" sigma "reals/")
 (quadratic const-decl "real" quadratic "reals/")
 (sq const-decl "nonneg_real" sq "reals/")
 (sq_nz_pos judgement-tcc nil sq "reals/")
 (sq_neg formula-decl nil sq "reals/")
 (sq_le formula-decl nil sq "reals/")
 (sq_1 formula-decl nil sq "reals/"))
 shostak))
(exp_neg_ub_TCC1 0
 (exp_neg_ub_TCC1-1 nil 3295622180
 ("" (skosimp)
 (("" (typepred "floor(nx!1)")
 (("" (typepred "nx!1") (("" (assert) nil nil)) nil)) nil))
 nil)
 ((negreal nonempty-type-eq-decl nil real_types nil)
 (nonpos_real nonempty-type-eq-decl nil real_types nil)
 (floor const-decl "{i | i <= x & x numfield]" number_fields nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (< const-decl "bool" reals nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (integer nonempty-type-from-decl nil integers nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (<= const-decl "bool" reals nil)
 (real nonempty-type-from-decl nil reals nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (number nonempty-type-decl nil numbers nil)
 (NOT const-decl "[bool -> bool]" booleans nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (boolean nonempty-type-decl nil booleans nil)
 (minus_int_is_int application-judgement "int" integers nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil))
 shostak))
(exp_neg_ub_TCC2 0
 (exp_neg_ub_TCC2-1 nil 3295622180
 ("" (skosimp)
 (("" (lemma "exp_neg_ub_TCC1" ("nx" "nx!1"))
 (("" (assert) nil nil)) nil))
 nil)
 ((negreal nonempty-type-eq-decl nil real_types nil)
 (< const-decl "bool" reals nil)
 (nonpos_real nonempty-type-eq-decl nil real_types nil)
 (<= const-decl "bool" reals nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (real nonempty-type-from-decl nil reals nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (boolean nonempty-type-decl nil booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (exp_neg_ub_TCC1 subtype-tcc nil exp_approx nil)
 (minus_int_is_int application-judgement "int" integers nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
 real_types nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil))
 shostak))
(exp_neg_ub_TCC3 0
 (exp_neg_ub_TCC3-2 nil 3352452386
 ("" (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)
 ((""
 (lemma "both_sides_div_pos_lt1"
 ("x" "nx!1" "y" "0" "pz" "P"))
 (("1" (assert)
 (("1"
 (lemma "div_mult_pos_le2"
 ("py" "P" "z" "nx!1" "x" "-1"))
 (("1" (assert)
 (("1"
 (lemma "exp_neg_le1_bounds"
 ("x" "nx!1/P" "n" "1+n!1"))
 (("1" (assert)
 (("1" (flatten)
 (("1"
 (typepred "exp(nx!1 / P)")
 (("1"
 (lemma
 "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_div_nzreal_is_nzreal application-judgement "nzreal"
 real_types nil)
 (nnint_plus_posint_is_posint application-judgement "posint"
 integers nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (minus_int_is_int application-judgement "int" integers nil)
 (floor const-decl "{i | i <= x & x numfield]" number_fields nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (integer nonempty-type-from-decl nil integers nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (NOT const-decl "[bool -> bool]" booleans nil)
 (- const-decl "[numfield -> numfield]" number_fields nil)
 (int nonempty-type-eq-decl nil integers nil)
 (both_sides_div_pos_lt1 formula-decl nil real_props nil)
 (>= const-decl "bool" reals nil)
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (> const-decl "bool" reals nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (real_gt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (minus_odd_is_odd application-judgement "odd_int" integers nil)
 (div_mult_pos_le2 formula-decl nil real_props nil)
 (exp_neg_le1_bounds formula-decl nil exp_approx nil)
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (/= const-decl "boolean" notequal nil)
 (nznum nonempty-type-eq-decl nil number_fields nil)
 (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
 (expt_pos formula-decl nil exponentiation nil)
 (exp_neg_le1_ub const-decl "real" exp_approx nil)
 (exp const-decl "{py | x = ln(py)}" ln_exp nil)
 (ln const-decl "real" ln_exp nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (= const-decl "[T, T -> boolean]" equalities nil)
 (exp_neg_ub_TCC1 subtype-tcc nil exp_approx nil)
 (number nonempty-type-decl nil numbers nil)
 (boolean nonempty-type-decl nil booleans nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (real nonempty-type-from-decl nil reals nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (<= const-decl "bool" reals nil)
 (nonpos_real nonempty-type-eq-decl nil real_types nil)
 (< const-decl "bool" reals nil)
 (negreal nonempty-type-eq-decl nil real_types nil))
 nil)
 (exp_neg_ub_TCC3-1 nil 3295622180
 ("" (skosimp) (("" (assert) nil nil)) nil) nil shostak))
(exp_neg_lb_TCC1 0
 (exp_neg_lb_TCC1-1 nil 3295622181
 ("" (skosimp) (("" (assert) nil nil)) nil)
 ((real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
 real_types nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (minus_int_is_int application-judgement "int" integers nil))
 shostak))
(exp_neg_lb_TCC2 0
 (exp_neg_lb_TCC2-1 nil 3295622181
 ("" (skosimp*)
 (("" (assert)
 (("" (typepred "floor(nx!1)")
 (("" (name-replace "F" "floor(nx!1)")
 (("" (typepred "nx!1")
 (("" (name "P" "-F")
 (("" (replace -1)
 ((""
 (lemma "both_sides_div_pos_lt1"
 ("x" "nx!1" "y" "0" "pz" "P"))
 (("1" (assert)
 (("1"
 (lemma "div_mult_pos_le2"
 ("py" "P" "z" "nx!1" "x" "-1"))
 (("1" (assert)
 (("1"
 (lemma "exp_neg_le1_lb_pos"
 ("x" "nx!1/P" "pn" "1+n!1"))
 (("1" (assert)
 (("1"
 (lemma "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_div_nzreal_is_nzreal application-judgement "nzreal"
 real_types nil)
 (nnint_plus_posint_is_posint application-judgement "posint"
 integers nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (minus_int_is_int application-judgement "int" integers nil)
 (= const-decl "[T, T -> boolean]" equalities nil)
 (- const-decl "[numfield -> numfield]" number_fields nil)
 (int nonempty-type-eq-decl nil integers nil)
 (both_sides_div_pos_lt1 formula-decl nil real_props nil)
 (>= const-decl "bool" reals nil)
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (> const-decl "bool" reals nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (real_gt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (minus_odd_is_odd application-judgement "odd_int" integers nil)
 (div_mult_pos_le2 formula-decl nil real_props nil)
 (exp_neg_le1_lb_pos formula-decl nil exp_approx nil)
 (nonneg_int nonempty-type-eq-decl nil integers nil)
 (posnat nonempty-type-eq-decl nil integers nil)
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (/= const-decl "boolean" notequal nil)
 (nznum nonempty-type-eq-decl nil number_fields nil)
 (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
 (expt_pos formula-decl nil exponentiation nil)
 (exp_neg_le1_lb const-decl "real" exp_approx nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (boolean nonempty-type-decl nil booleans nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (NOT const-decl "[bool -> bool]" booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (real nonempty-type-from-decl nil reals nil)
 (<= const-decl "bool" reals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (integer nonempty-type-from-decl nil integers nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (< const-decl "bool" reals nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
 (nonpos_real nonempty-type-eq-decl nil real_types nil)
 (negreal nonempty-type-eq-decl nil real_types nil))
 shostak))
(exp_neg_bounds 0
 (exp_neg_bounds-1 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)
 ((""
 (lemma "both_sides_div_pos_lt1"
 ("pz" "P" "x" "nx!1" "y" "0"))
 (("1"
 (lemma "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"
 (lemma
 "exp_neg_le1_bounds"
 ("x" "nx!1/P" "n" "1+n!1"))
 (("1"
 (lemma
 "exp_neg_le1_lb_pos"
 ("x" "nx!1/P" "pn" "1+n!1"))
 (("1"
 (typepred "exp(nx!1 / P)")
 (("1"
 (assert)
 (("1"
 (flatten)
 (("1"
 (lemma
 "both_sides_expt_pos_lt"
 ("pm" "P"))
 (("1"
 (inst-cp
 -
 "exp_neg_le1_lb(1 + n!1, nx!1 / P)"
 "exp(nx!1 / P)")
 (("1"
 (inst
 -
 "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)
 ((minus_int_is_int application-judgement "int" integers nil)
 (exp_neg_lb const-decl "posreal" exp_approx nil)
 (negreal nonempty-type-eq-decl nil real_types nil)
 (nonpos_real nonempty-type-eq-decl nil real_types nil)
 (floor const-decl "{i | i <= x & x numfield]" number_fields nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (< const-decl "bool" reals nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (integer nonempty-type-from-decl nil integers nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (<= const-decl "bool" reals nil)
 (real nonempty-type-from-decl nil reals nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (number nonempty-type-decl nil numbers nil)
 (NOT const-decl "[bool -> bool]" booleans nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (boolean nonempty-type-decl nil booleans nil)
 (= const-decl "[T, T -> boolean]" equalities nil)
 (minus_odd_is_odd application-judgement "odd_int" integers nil)
 (div_mult_pos_le2 formula-decl nil real_props nil)
 (exp_scal formula-decl nil ln_exp nil)
 (/= const-decl "boolean" notequal nil)
 (nznum nonempty-type-eq-decl nil number_fields nil)
 (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
 (exp_neg_le1_lb_pos formula-decl nil exp_approx nil)
 (nonneg_int nonempty-type-eq-decl nil integers nil)
 (posnat nonempty-type-eq-decl nil integers nil)
 (posreal_exp application-judgement "posreal" exponentiation nil)
 (nzreal_exp application-judgement "nzreal" exponentiation nil)
 (both_sides_expt_pos_lt formula-decl nil exponentiation nil)
 (exp_neg_le1_ub const-decl "real" exp_approx nil)
 (n!1 skolem-const-decl "nat" exp_approx nil)
 (nx!1 skolem-const-decl "negreal" exp_approx nil)
 (P skolem-const-decl "int" exp_approx nil)
 (exp_neg_le1_lb const-decl "real" exp_approx nil)
 (exp const-decl "{py | x = ln(py)}" ln_exp nil)
 (ln const-decl "real" ln_exp nil)
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (exp_neg_le1_bounds formula-decl nil exp_approx nil)
 (div_cancel1 formula-decl nil real_props nil)
 (nonzero_real nonempty-type-eq-decl nil reals nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
 real_types nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (real_gt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (> const-decl "bool" reals nil)
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (>= const-decl "bool" reals nil)
 (both_sides_div_pos_lt1 formula-decl nil real_props nil)
 (int nonempty-type-eq-decl nil integers nil)
 (- const-decl "[numfield -> numfield]" number_fields nil)
 (exp_neg_ub const-decl "posreal" exp_approx nil))
 shostak))
(exp_ub_n_TCC1 0
 (exp_ub_n_TCC1-1 nil 3568465985 ("" (subtype-tcc) nil nil)
 ((boolean nonempty-type-decl nil booleans nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (NOT const-decl "[bool -> bool]" booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (real nonempty-type-from-decl nil reals nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (minus_even_is_even application-judgement "even_int" integers nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil))
 nil))
(exp_ub_n_TCC2 0
 (exp_ub_n_TCC2-1 nil 3568465985 ("" (subtype-tcc) nil nil)
 ((boolean nonempty-type-decl nil booleans nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (NOT const-decl "[bool -> bool]" booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (real nonempty-type-from-decl nil reals nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (minus_real_is_real application-judgement "real" reals nil))
 nil))
(exp_bounds 0
 (exp_bounds-1 nil 3295623866
 (""
 (case "FORALL (n: nat, x: real): n<=exp_approx_term_cutoff IMPLIES
 exp_lb(x, n) <= exp(x) AND exp(x) <= exp_ub(x, n)")
 (("1" (skeep)
 (("1" (inst - "min(n,exp_approx_term_cutoff)" "x")
 (("1" (assert)
 (("1" (split -)
 (("1" (expand "exp_lb")
 (("1" (expand "exp_ub")
 (("1" (expand "min")
 (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
 nil))
 nil)
 ("2" (assert) nil nil))
 nil))
 nil)
 ("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil))
 nil))
 nil))
 nil)
 ("2" (hide 2)
 (("2" (skosimp)
 (("2" (lemma "trichotomy" ("x" "x!1"))
 (("2" (split -1)
 (("1" (expand "exp_lb")
 (("1" (expand "exp_ub")
 (("1" (expand "exp_ub_n")
 (("1" (expand "exp_lb_n")
 (("1" (assert)
 (("1" (lift-if)
 (("1" (ground)
 (("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"
 (assert)
 (("1"
 (cross-mult 1)
 (("1" (cross-mult -3) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (lemma "exp_neg_bounds"
 ("n" "n!1" "nx" "-x!1"))
 (("2" (flatten)
 (("2"
 (lemma "exp_diff" ("x" "0" "y" "x!1"))
 (("2"
 (rewrite "exp_0")
 (("2"
 (replace -1)
 (("2"
 (assert)
 (("2"
 (cross-mult -2)
 (("2" (cross-mult 1) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (case "FORALL (aa,bb:real): aa<=exp(x!1) AND bb<=exp(x!1) IMPLIES max(aa,bb)<=exp(x!1)")
 (("1" (rewrite -1)
 (("1"
 (hide (-1 2))
 (("1"
 (lemma "exp_increasing")
 (("1"
 (expand "increasing?")
 (("1"
 (inst
 -
 "exp_approx_int_cutoff"
 "x!1")
 (("1"
 (assert)
 (("1"
 (case
 "1/exp_neg_ub(n!1,-exp_approx_int_cutoff)<=exp(exp_approx_int_cutoff)")
 (("1" (assert) nil nil)
 ("2"
 (hide 2)
 (("2"
 (lemma
 "exp_neg_bounds"
 ("n"
 "n!1"
 "nx"
 "-exp_approx_int_cutoff"))
 (("2"
 (flatten)
 (("2"
 (lemma "exp_diff")
 (("2"
 (inst
 -
 "0"
 "exp_approx_int_cutoff")
 (("2"
 (assert)
 (("2"
 (replace -1)
 (("2"
 (cross-mult
 -3)
 (("2"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (lemma "exp_increasing")
 (("2"
 (expand "increasing?")
 (("2"
 (inst - "floor(x!1)" "x!1")
 (("2"
 (assert)
 (("2"
 (rewrite "exp_int" -1)
 (("2"
 (lemma
 "both_sides_expt_pos_le_aux")
 (("2"
 (inst
 -
 "floor(x!1)-1"
 "2"
 "e")
 (("2"
 (assert)
 (("2"
 (expand "^")
 (("2"
 (assert)
 (("2"
 (lemma "e_bnds")
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (hide-all-but 1)
 (("2" (grind :exclude "exp") nil nil))
 nil))
 nil)
 ("4"
 (case "FORALL (aa,bb:real): exp(x!1)<=bb IMPLIES exp(x!1)<=max(aa,bb)")
 (("1" (inst?)
 (("1"
 (ground)
 (("1"
 (hide 2)
 (("1"
 (lemma "exp_increasing")
 (("1"
 (expand "increasing?")
 (("1"
 (inst - "x!1" "1+floor(x!1)")
 (("1"
 (assert)
 (("1"
 (lemma "exp_int")
 (("1"
 (inst - "1+floor(x!1)")
 (("1"
 (replaces -1)
 (("1"
 (lemma
 "both_sides_expt_pos_le_aux")
 (("1"
 (inst
 -
 "floor(x!1)"
 "e"
 "4")
 (("1"
 (expand "^")
 (("1"
 (lemma
 "e_bnds")
 (("1"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (hide-all-but 1)
 (("2" (grind :exclude "exp") nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (replaces -1)
 (("2" (assert)
 (("2" (expand "exp_lb")
 (("2" (expand "exp_ub")
 (("2" (assert)
 (("2" (expand "exp_lb_n")
 (("2" (expand "exp_ub_n")
 (("2" (assert) nil nil)) nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3" (expand "exp_lb")
 (("3" (expand "exp_lb_n")
 (("3" (assert)
 (("3" (expand "exp_ub")
 (("3" (expand "exp_ub_n")
 (("3" (assert)
 (("3" (lift-if)
 (("3" (ground)
 (("1" (expand "exp_neg_lb")
 (("1"
 (lemma "exp_neg_bounds")
 (("1"
 (expand "exp_neg_lb")
 (("1"
 (inst?)
 (("1" (assert) nil nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (lemma "exp_neg_bounds")
 (("2"
 (inst?)
 (("2" (assert) nil nil))
 nil))
 nil)
 ("3"
 (case "FORALL (aa,bb:real): bb<=exp(x!1) IMPLIES min(aa,bb)<=exp(x!1)")
 (("1"
 (rewrite -1)
 (("1"
 (hide 2)
 (("1"
 (lemma "exp_increasing")
 (("1"
 (expand "increasing?")
 (("1"
 (inst - "floor(x!1)" "x!1")
 (("1"
 (assert)
 (("1"
 (lemma "exp_int")
 (("1"
 (inst - "floor(x!1)")
 (("1"
 (replaces -1)
 (("1"
 (expand "^")
 (("1"
 (invoke
 (case "%1 <= %2")
 (! 1 1)
 (! -1 1))
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (hide (-1 2))
 (("2"
 (assert)
 (("2"
 (cross-mult
 1)
 (("2"
 (lemma
 "both_sides_expt_pos_le_aux")
 (("2"
 (inst
 -
 "-floor(x!1)-1"
 "e"
 "4")
 (("2"
 (assert)
 (("2"
 (lemma
 "e_bnds")
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (hide-all-but 1)
 (("2" (grind :exclude "exp") nil nil))
 nil))
 nil)
 ("4" (lemma "exp_increasing")
 (("4"
 (expand "increasing?")
 (("4"
 (inst
 -
 "x!1"
 "-exp_approx_int_cutoff")
 (("4"
 (assert)
 (("4"
 (lemma "exp_neg_bounds")
 (("4"
 (inst
 -
 "n!1"
 "-exp_approx_int_cutoff")
 (("4" (assert) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ((trichotomy formula-decl nil real_axioms nil)
 (posint_times_posint_is_posint application-judgement "posint"
 integers nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (times_div2 formula-decl nil real_props nil)
 (nonzero_real nonempty-type-eq-decl nil reals nil)
 (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (expt def-decl "real" exponentiation nil)
 (minus_int_is_int application-judgement "int" integers nil)
 (real_div_nzreal_is_real application-judgement "real" reals nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (posreal_min application-judgement
 "{z: posreal | z <= x AND z <= y}" real_defs nil)
 (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
 (exp_ub_n const-decl "posreal" exp_approx nil)
 (minus_even_is_even application-judgement "even_int" integers nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (posreal_max application-judgement
 "{z: posreal | z >= x AND z >= y}" real_defs nil)
 (posreal_div_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (nnrat_exp application-judgement "nnrat" exponentiation nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (minus_real_is_real application-judgement "real" reals nil)
 (exp_0 formula-decl nil ln_exp nil)
 (minus_odd_is_odd application-judgement "odd_int" integers nil)
 (real_minus_real_is_real application-judgement "real" reals nil)
 (div_mult_pos_lt1 formula-decl nil real_props nil)
 (exp_neg_ub const-decl "posreal" exp_approx nil)
 (div_mult_pos_le1 formula-decl nil real_props nil)
 (posreal_times_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (exp_diff formula-decl nil ln_exp nil)
 (- const-decl "[numfield -> numfield]" number_fields nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (negreal nonempty-type-eq-decl nil real_types nil)
 (< const-decl "bool" reals nil)
 (nonpos_real nonempty-type-eq-decl nil real_types nil)
 (exp_neg_bounds formula-decl nil exp_approx nil)
 (div_mult_pos_le2 formula-decl nil real_props nil)
 (exp_neg_lb const-decl "posreal" exp_approx nil)
 (div_mult_pos_lt2 formula-decl nil real_props nil)
 (NOT const-decl "[bool -> bool]" booleans nil)
 (floor const-decl "{i | i <= x & x numfield]" number_fields nil)
 (integer nonempty-type-from-decl nil integers nil)
 (^ const-decl "real" exponentiation nil)
 (OR const-decl "[bool, bool -> bool]" booleans nil)
 (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
 (nznum nonempty-type-eq-decl nil number_fields nil)
 (/= const-decl "boolean" notequal nil)
 (exp_increasing formula-decl nil ln_exp nil)
 (even_minus_even_is_even application-judgement "even_int" integers
 nil)
 (increasing? const-decl "bool" real_fun_preds "reals/")
 (both_sides_expt_pos_le_aux formula-decl nil exponentiation nil)
 (posreal_expt application-judgement "posreal" exponentiation nil)
 (nzreal_expt application-judgement "nzreal" exponentiation nil)
 (posnat_expt application-judgement "posnat" exponentiation nil)
 (e_bnds formula-decl nil ln_exp nil)
 (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (e const-decl "posreal" ln_exp nil)
 (int_minus_int_is_int application-judgement "int" integers nil)
 (nzreal_exp application-judgement "nzreal" exponentiation nil)
 (posreal_exp application-judgement "posreal" exponentiation nil)
 (exp_int formula-decl nil ln_exp nil)
 (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
 (exp_lb_n const-decl "posreal" exp_approx nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (real_gt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (n skolem-const-decl "nat" exp_approx nil)
 (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
 (int_min application-judgement "{k: int | k <= i AND k <= j}"
 real_defs nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (number nonempty-type-decl nil numbers nil)
 (boolean nonempty-type-decl nil booleans nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (real nonempty-type-from-decl nil reals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (int nonempty-type-eq-decl nil integers nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (>= const-decl "bool" reals nil)
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
 (<= const-decl "bool" reals nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (> const-decl "bool" reals nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (exp_lb const-decl "posreal" exp_approx nil)
 (= const-decl "[T, T -> boolean]" equalities nil)
 (ln const-decl "real" ln_exp nil)
 (exp const-decl "{py | x = ln(py)}" ln_exp nil)
 (exp_ub const-decl "posreal" exp_approx nil))
 shostak))
(exp_range_test_TCC1 0
 (exp_range_test_TCC1-1 nil 3568376623 ("" (subtype-tcc) nil nil)
 ((minus_nzint_is_nzint application-judgement "nzint" integers nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (rat_expt application-judgement "rat" exponentiation nil)
 (nzreal_expt application-judgement "nzreal" exponentiation nil)
 (exp_estimate const-decl "real" exp_series nil)
 (^ const-decl "real" exponentiation nil))
 nil))
(exp_range_test_TCC2 0
 (exp_range_test_TCC2-1 nil 3568376623 ("" (subtype-tcc) nil nil)
 ((^ const-decl "real" exponentiation nil)
 (exp_estimate const-decl "real" exp_series nil)
 (nzreal_expt application-judgement "nzreal" exponentiation nil)
 (int_expt application-judgement "int" exponentiation nil))
 nil))
(exp_range_test 0
 (exp_range_test-1 nil 3568376625 ("" (eval-formula) nil nil)
 ((TRUE const-decl "bool" booleans nil)
 (id const-decl "(bijective?[T, T])" identity nil)
 (bijective? const-decl "bool" functions nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (boolean nonempty-type-decl nil booleans nil))
 shostak))
(exp_range_test_lb_TCC1 0
 (exp_range_test_lb_TCC1-1 nil 3568572776 ("" (subtype-tcc) nil nil)
 ((minus_nzint_is_nzint application-judgement "nzint" integers nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (rat_expt application-judgement "rat" exponentiation nil)
 (nzreal_expt application-judgement "nzreal" exponentiation nil)
 (posint_times_posint_is_posint application-judgement "posint"
 integers nil)
 (even_times_int_is_even application-judgement "even_int" integers
 nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (real_plus_real_is_real application-judgement "real" reals nil)
 (exp_estimate const-decl "real" exp_series nil)
 (^ const-decl "real" exponentiation nil))
 nil))
(exp_range_test_lb_TCC2 0
 (exp_range_test_lb_TCC2-1 nil 3568572776 ("" (subtype-tcc) nil nil)
 ((int_expt application-judgement "int" exponentiation nil)
 (nzreal_expt application-judgement "nzreal" exponentiation nil)
 (posint_times_posint_is_posint application-judgement "posint"
 integers nil)
 (even_times_int_is_even application-judgement "even_int" integers
 nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (real_plus_real_is_real application-judgement "real" reals nil)
 (exp_estimate const-decl "real" exp_series nil)
 (^ const-decl "real" exponentiation nil))
 nil))
(exp_range_test_lb 0
 (exp_range_test_lb-1 nil 3568572777 ("" (eval-formula) nil nil)
 ((TRUE const-decl "bool" booleans nil)
 (id const-decl "(bijective?[T, T])" identity nil)
 (bijective? const-decl "bool" functions nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (boolean nonempty-type-decl nil booleans nil))
 shostak))
(exp_neg_ub_increasing 0
 (exp_neg_ub_increasing-1 nil 3568463896
 ("" (skeep)
 (("" (skoletin 1)
 (("" (expand "increasing?")
 (("" (skosimp*)
 (("" (expand "exp_neg_ub")
 (("" (expand "exp_neg_le1_ub")
 ((""
 (name "FF"
 "LAMBDA (xn:negreal,nn:posnat): exp_estimate(xn / nn,2+2*n) ^ nn")
 (("" (label "FFname" -1)
 ((""
 (case "FF(x!1,-floor(x!1)) <= FF(y!1,-floor(y!1))")
 (("1" (expand "FF") (("1" (propax) nil nil)) nil)
 ("2" (hide 2)
 (("2"
 (case "FORALL (NN:nat,MM:nat,xx,yy:(TT)): xx<=yy AND MM<=NN AND MM = floor(yy)-floor(xx) IMPLIES FF(xx,-floor(xx)) <= FF(yy,-floor(yy))")
 (("1" (assert)
 (("1"
 (inst - "floor(y!1)-floor(x!1)"
 "floor(y!1)-floor(x!1)" "x!1" "y!1")
 (("1" (assert) nil nil)) nil))
 nil)
 ("2" (assert)
 (("2" (hide (-2 2))
 (("2" (induct "NN")
 (("1"
 (skeep)
 (("1"
 (case "MM = 0")
 (("1"
 (assert)
 (("1"
 (hide -3)
 (("1"
 (case "floor(yy) = floor(xx)")
 (("1"
 (hide -4)
 (("1"
 (hide -2)
 (("1"
 (label "flooreq" -1)
 (("1"
 (replace -1)
 (("1"
 (assert)
 (("1"
 (lemma
 "exp_estimate_increasing")
 (("1"
 (inst
 -
 "2+2*n"
 "xx/-floor(yy)"
 "yy/-floor(yy)")
 (("1"
 (assert)
 (("1"
 (split -)
 (("1"
 (lemma
 "both_sides_expt_pos_le")
 (("1"
 (expand
 "FF"
 +)
 (("1"
 (inst?)
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (hide
 2)
 (("2"
 (assert)
 (("2"
 (lemma
 "exp_estimate_positive")
 (("2"
 (inst?)
 (("2"
 (split
 -)
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (assert)
 nil
 nil)
 ("3"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (lemma
 "exp_estimate_positive")
 (("3"
 (inst?)
 (("3"
 (assert)
 (("3"
 (split
 -)
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (assert)
 (("2"
 (cross-mult
 1)
 nil
 nil))
 nil)
 ("3"
 (assert)
 (("3"
 (mult-by
 -2
 "1/-floor(yy)")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (assert) nil nil))
 nil))
 nil))
 nil)
 ("2" (assert) nil nil))
 nil))
 nil)
 ("2"
 (skeep)
 (("2"
 (case "NOT j = 0")
 (("1"
 (skeep)
 (("1"
 (case "NOT MM = j+1")
 (("1"
 (inst - "MM" "xx" "yy")
 (("1" (assert) nil nil))
 nil)
 ("2"
 (replaces -1)
 (("2"
 (assert)
 (("2"
 (inst-cp - "1" "xx" "xx+1")
 (("1"
 (assert)
 (("1"
 (split -)
 (("1"
 (inst
 -
 "j"
 "xx+1"
 "yy")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (assert)
 (("2"
 (expand "TT")
 (("2"
 (typepred "xx")
 (("2"
 (expand "TT")
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (assert)
 nil
 nil))
 nil))
 nil)
 ("2"
 (typepred "xx")
 (("2"
 (expand "TT")
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (replaces -1)
 (("2"
 (assert)
 (("2"
 (skeep)
 (("2"
 (case "NOT MM = 1")
 (("1"
 (inst - "0" "xx" "yy")
 (("1" (assert) nil nil))
 nil)
 ("2"
 (replaces -1)
 (("2"
 (hide -3)
 (("2"
 (assert)
 (("2"
 (inst
 -
 "0"
 "floor(yy)"
 "yy")
 (("1"
 (assert)
 (("1"
 (assert)
 (("1"
 (lemma
 "floor_int")
 (("1"
 (inst
 -
 "floor(yy)")
 (("1"
 (replaces
 -1)
 (("1"
 (case
 "FF(xx,-floor(xx)) <= FF(floor(yy),-floor(yy))")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (case
 "NOT floor(yy) = floor(xx)+1")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (hide
 -4)
 (("2"
 (replaces
 -1)
 (("2"
 (case
 "FF(floor(xx)+1,-floor(xx)) <= FF(floor(xx) + 1, -(floor(xx) + 1)) AND FF(xx,-floor(xx)) <= FF(floor(xx)+1,-floor(xx))")
 (("1"
 (flatten)
 (("1"
 (assert)
 nil
 nil))
 nil)
 ("2"
 (hide
 (2
 3
 -1))
 (("2"
 (split
 +)
 (("1"
 (hide
 -1)
 (("1"
 (case
 "FORALL (N:posnat): N<=exp_approx_int_cutoff AND N>=2 IMPLIES FF(-N+1,N) <= FF(-N+1,N-1)")
 (("1"
 (inst
 -
 "-floor(xx)")
 (("1"
 (assert)
 (("1"
 (typepred
 "xx")
 (("1"
 (expand
 "TT")
 (("1"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (hide
 2)
 (("2"
 (skeep)
 (("2"
 (expand
 "FF")
 (("2"
 (lemma
 "exp_range_test")
 (("2"
 (inst
 -
 "N-1"
 "1+n")
 (("1"
 (assert)
 (("1"
 (case
 "(1+-N)/(N-1) = -1")
 (("1"
 (assert)
 (("1"
 (replaces
 -1)
 (("1"
 (assert)
 nil
 nil))
 nil))
 nil)
 ("2"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil)
 ("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (skosimp*)
 (("3"
 (assert)
 nil
 nil))
 nil)
 ("4"
 (skosimp*)
 (("4"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand
 "FF"
 +)
 (("2"
 (lemma
 "both_sides_expt_pos_le")
 (("2"
 (inst?)
 (("1"
 (assert)
 (("1"
 (hide
 2)
 (("1"
 (lemma
 "exp_estimate_increasing")
 (("1"
 (inst?)
 (("1"
 (assert)
 (("1"
 (split)
 (("1"
 (cross-mult
 1)
 nil
 nil)
 ("2"
 (typepred
 "floor(xx)")
 (("2"
 (mult-by
 -2
 "1/-floor(xx)")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (split)
 (("1"
 (cross-mult
 1)
 nil
 nil)
 ("2"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (hide
 2)
 (("2"
 (case
 "FORALL (rr:real): rr>0 IMPLIES (rr>=0 AND rr>0)")
 (("1"
 (rewrite
 -1)
 (("1"
 (hide
 2)
 (("1"
 (lemma
 "exp_estimate_positive")
 (("1"
 (inst?)
 (("1"
 (assert)
 (("1"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (assert)
 (("2"
 (skeep)
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (hide
 2)
 (("3"
 (case
 "FORALL (rr:real): rr>0 IMPLIES (rr>=0 AND rr>0)")
 (("1"
 (rewrite
 -1)
 (("1"
 (hide
 2)
 (("1"
 (lemma
 "exp_estimate_positive")
 (("1"
 (inst?)
 (("1"
 (assert)
 (("1"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (skosimp*)
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (typepred "yy")
 (("2"
 (expand "TT")
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (hide 2)
 (("3"
 (skosimp*)
 (("3" (assert) nil nil))
 nil))
 nil)
 ("4"
 (skosimp*)
 (("4" (assert) nil nil))
 nil))
 nil))
 nil))
 nil)
 ("3" (skosimp*) (("3" (assert) nil nil)) nil)
 ("4" (skosimp*) (("4" (assert) nil nil)) nil))
 nil))
 nil)
 ("3" (assert) nil nil) ("4" (assert) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ((IFF const-decl "[bool, bool -> bool]" booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (boolean nonempty-type-decl nil booleans nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (real nonempty-type-from-decl nil reals nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (<= const-decl "bool" reals nil)
 (nonpos_real nonempty-type-eq-decl nil real_types nil)
 (< const-decl "bool" reals nil)
 (negreal nonempty-type-eq-decl nil real_types nil)
 (= const-decl "[T, T -> boolean]" equalities nil)
 (>= const-decl "bool" reals nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (- const-decl "[numfield -> numfield]" number_fields nil)
 (minus_even_is_even application-judgement "even_int" integers nil)
 (minus_nzint_is_nzint application-judgement "nzint" integers nil)
 (exp_neg_ub const-decl "posreal" exp_approx nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (> const-decl "bool" reals nil)
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (increasing? const-decl "bool" real_fun_preds "reals/")
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (int nonempty-type-eq-decl nil integers nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
 (exp_neg_le1_ub const-decl "real" exp_approx nil)
 (TT skolem-const-decl "[negreal -> bool]" exp_approx nil)
 (pred type-eq-decl nil defined_types nil)
 (nat_induction formula-decl nil naturalnumbers nil)
 (exp_estimate_positive formula-decl nil exp_series nil)
 (div_mult_pos_le2 formula-decl nil real_props nil)
 (yy skolem-const-decl "(TT)" exp_approx nil)
 (n skolem-const-decl "nat" exp_approx nil)
 (xx skolem-const-decl "(TT)" exp_approx nil)
 (both_sides_expt_pos_le formula-decl nil exponentiation nil)
 (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
 nil)
 (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
 nil)
 (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
 real_types nil)
 (div_mult_pos_ge1 formula-decl nil real_props nil)
 (minus_odd_is_odd application-judgement "odd_int" integers nil)
 (exp_estimate_increasing formula-decl nil exp_series nil)
 (NOT const-decl "[bool -> bool]" booleans nil)
 (nnint_plus_posint_is_posint application-judgement "posint"
 integers nil)
 (xx skolem-const-decl "(TT)" exp_approx nil)
 (real_plus_real_is_real application-judgement "real" reals nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (yy skolem-const-decl "(TT)" exp_approx nil)
 (exp_range_test formula-decl nil exp_approx nil)
 (posint_times_posint_is_posint application-judgement "posint"
 integers nil)
 (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
 (div_cancel3 formula-decl nil real_props nil)
 (nonzero_real nonempty-type-eq-decl nil reals nil)
 (subrange type-eq-decl nil integers nil)
 (N skolem-const-decl "posnat" exp_approx nil)
 (div_mult_pos_gt1 formula-decl nil extra_real_props nil)
 (rat_times_rat_is_rat application-judgement "rat" rationals nil)
 (both_sides_times_pos_lt1 formula-decl nil real_props nil)
 (xx skolem-const-decl "(TT)" exp_approx nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (floor_int formula-decl nil floor_ceil nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (int_minus_int_is_int application-judgement "int" integers nil)
 (FF skolem-const-decl "[[negreal, posnat] -> real]" exp_approx nil)
 (real_gt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (floor const-decl "{i | i <= x & x bool]" booleans nil)
 (integer nonempty-type-from-decl nil integers nil)
 (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
 (nznum nonempty-type-eq-decl nil number_fields nil)
 (exp_estimate const-decl "real" exp_series nil)
 (^ const-decl "real" exponentiation nil)
 (/= const-decl "boolean" notequal nil)
 (OR const-decl "[bool, bool -> bool]" booleans nil)
 (posnat nonempty-type-eq-decl nil integers nil)
 (nonneg_int nonempty-type-eq-decl nil integers nil)
 (minus_int_is_int application-judgement "int" integers nil)
 (even_plus_even_is_even application-judgement "even_int" integers
 nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (npreal_div_posreal_is_npreal application-judgement "npreal"
 real_types nil)
 (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
 real_types nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (even_times_int_is_even application-judgement "even_int" integers
 nil)
 (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
 integers nil))
 nil))
(exp_neg_lb_increasing 0
 (exp_neg_lb_increasing-1 nil 3568478821
 ("" (skeep)
 (("" (skoletin 1)
 (("" (expand "increasing?")
 (("" (skosimp*)
 (("" (expand "exp_neg_lb")
 (("" (expand "exp_neg_le1_lb")
 ((""
 (name "FF"
 "LAMBDA (xn:negreal,nn:posnat): (exp_estimate(xn / nn,2+2*n)- 1.000001/factorial(2*n+3)) ^ nn")
 (("" (label "FFname" -1)
 ((""
 (case "FF(x!1,-floor(x!1)) <= FF(y!1,-floor(y!1))")
 (("1" (expand "FF") (("1" (propax) nil nil)) nil)
 ("2" (hide 2)
 (("2"
 (case "FORALL (NN:nat,MM:nat,xx,yy:(TT)): xx<=yy AND MM<=NN AND MM = floor(yy)-floor(xx) IMPLIES FF(xx,-floor(xx)) <= FF(yy,-floor(yy))")
 (("1" (assert)
 (("1"
 (inst - "floor(y!1)-floor(x!1)"
 "floor(y!1)-floor(x!1)" "x!1" "y!1")
 (("1" (assert) nil nil)) nil))
 nil)
 ("2" (assert)
 (("2" (hide (-2 2))
 (("2" (induct "NN")
 (("1"
 (skeep)
 (("1"
 (case "MM = 0")
 (("1"
 (assert)
 (("1"
 (hide -3)
 (("1"
 (case "floor(yy) = floor(xx)")
 (("1"
 (hide -4)
 (("1"
 (hide -2)
 (("1"
 (label "flooreq" -1)
 (("1"
 (replace -1)
 (("1"
 (assert)
 (("1"
 (lemma
 "exp_estimate_increasing")
 (("1"
 (inst
 -
 "2+2*n"
 "xx/-floor(yy)"
 "yy/-floor(yy)")
 (("1"
 (assert)
 (("1"
 (split -)
 (("1"
 (lemma
 "both_sides_expt_pos_le")
 (("1"
 (expand
 "FF"
 +)
 (("1"
 (inst?)
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (hide
 2)
 (("2"
 (lemma
 "exp_neg_le1_lb_pos")
 (("2"
 (expand
 "exp_neg_le1_lb")
 (("2"
 (inst
 -
 "n+1"
 "yy/-floor(xx)")
 (("2"
 (assert)
 (("2"
 (split
 -)
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (assert)
 (("2"
 (cross-mult
 1)
 nil
 nil))
 nil)
 ("3"
 (assert)
 (("3"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (lemma
 "exp_neg_le1_lb_pos")
 (("3"
 (expand
 "exp_neg_le1_lb")
 (("3"
 (inst
 -
 "n+1"
 "xx/-floor(xx)")
 (("3"
 (assert)
 (("3"
 (split
 -)
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (cross-mult
 1)
 nil
 nil)
 ("3"
 (assert)
 (("3"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (assert)
 (("2"
 (cross-mult
 1)
 nil
 nil))
 nil)
 ("3"
 (assert)
 (("3"
 (mult-by
 -2
 "1/-floor(yy)")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (assert) nil nil))
 nil))
 nil))
 nil)
 ("2" (assert) nil nil))
 nil))
 nil)
 ("2"
 (skeep)
 (("2"
 (case "NOT j = 0")
 (("1"
 (skeep)
 (("1"
 (case "NOT MM = j+1")
 (("1"
 (inst - "MM" "xx" "yy")
 (("1" (assert) nil nil))
 nil)
 ("2"
 (replaces -1)
 (("2"
 (assert)
 (("2"
 (inst-cp - "1" "xx" "xx+1")
 (("1"
 (assert)
 (("1"
 (split -)
 (("1"
 (inst
 -
 "j"
 "xx+1"
 "yy")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (assert)
 (("2"
 (expand "TT")
 (("2"
 (typepred "xx")
 (("2"
 (expand "TT")
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (assert)
 nil
 nil))
 nil))
 nil)
 ("2"
 (typepred "xx")
 (("2"
 (expand "TT")
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (replaces -1)
 (("2"
 (assert)
 (("2"
 (skeep)
 (("2"
 (case "NOT MM = 1")
 (("1"
 (inst - "0" "xx" "yy")
 (("1" (assert) nil nil))
 nil)
 ("2"
 (replaces -1)
 (("2"
 (hide -3)
 (("2"
 (assert)
 (("2"
 (inst
 -
 "0"
 "floor(yy)"
 "yy")
 (("1"
 (assert)
 (("1"
 (assert)
 (("1"
 (lemma
 "floor_int")
 (("1"
 (inst
 -
 "floor(yy)")
 (("1"
 (replaces
 -1)
 (("1"
 (case
 "FF(xx,-floor(xx)) <= FF(floor(yy),-floor(yy))")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (case
 "NOT floor(yy) = floor(xx)+1")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (hide
 -4)
 (("2"
 (replaces
 -1)
 (("2"
 (case
 "FF(floor(xx)+1,-floor(xx)) <= FF(floor(xx) + 1, -(floor(xx) + 1)) AND FF(xx,-floor(xx)) <= FF(floor(xx)+1,-floor(xx))")
 (("1"
 (flatten)
 (("1"
 (assert)
 nil
 nil))
 nil)
 ("2"
 (hide
 (2
 3
 -1))
 (("2"
 (split
 +)
 (("1"
 (hide
 -1)
 (("1"
 (case
 "FORALL (N:posnat): N<=exp_approx_int_cutoff AND N>=2 IMPLIES FF(-N+1,N) <= FF(-N+1,N-1)")
 (("1"
 (inst
 -
 "-floor(xx)")
 (("1"
 (assert)
 (("1"
 (typepred
 "xx")
 (("1"
 (expand
 "TT")
 (("1"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (hide
 2)
 (("2"
 (skeep)
 (("2"
 (expand
 "FF")
 (("2"
 (lemma
 "exp_range_test_lb")
 (("2"
 (inst
 -
 "N-1"
 "n+1")
 (("1"
 (assert)
 (("1"
 (case
 "(1-N)/(N-1) = -1")
 (("1"
 (replaces
 -1)
 (("1"
 (assert)
 nil
 nil))
 nil)
 ("2"
 (assert)
 nil
 nil))
 nil))
 nil)
 ("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (skosimp*)
 (("3"
 (assert)
 nil
 nil))
 nil)
 ("4"
 (skosimp*)
 (("4"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand
 "FF"
 +)
 (("2"
 (lemma
 "both_sides_expt_pos_le")
 (("2"
 (inst?)
 (("1"
 (assert)
 (("1"
 (hide
 2)
 (("1"
 (lemma
 "exp_estimate_increasing")
 (("1"
 (inst
 -
 "2+2*n"
 "xx/-floor(xx)"
 "(1+floor(xx))/-floor(xx)")
 (("1"
 (assert)
 (("1"
 (split)
 (("1"
 (cross-mult
 1)
 nil
 nil)
 ("2"
 (typepred
 "floor(xx)")
 (("2"
 (mult-by
 -2
 "1/-floor(xx)")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (split)
 (("1"
 (cross-mult
 1)
 nil
 nil)
 ("2"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (hide
 2)
 (("2"
 (case
 "FORALL (rr:real): rr>0 IMPLIES (rr>=0 AND rr>0)")
 (("1"
 (rewrite
 -1)
 (("1"
 (hide
 2)
 (("1"
 (lemma
 "exp_neg_le1_lb_pos")
 (("1"
 (expand
 "exp_neg_le1_lb")
 (("1"
 (inst
 -
 "n+1"
 "(1+floor(xx))/-floor(xx)")
 (("1"
 (assert)
 (("1"
 (split)
 (("1"
 (cross-mult
 1)
 nil
 nil)
 ("2"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (assert)
 (("2"
 (skeep)
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (hide
 2)
 (("3"
 (case
 "FORALL (rr:real): rr>0 IMPLIES (rr>=0 AND rr>0)")
 (("1"
 (rewrite
 -1)
 (("1"
 (hide
 2)
 (("1"
 (lemma
 "exp_neg_le1_lb_pos")
 (("1"
 (expand
 "exp_neg_le1_lb")
 (("1"
 (inst
 -
 "n+1"
 _)
 (("1"
 (inst?)
 (("1"
 (assert)
 (("1"
 (split)
 (("1"
 (cross-mult
 1)
 nil
 nil)
 ("2"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (skosimp*)
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (typepred "yy")
 (("2"
 (expand "TT")
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (hide 2)
 (("3"
 (skosimp*)
 (("3" (assert) nil nil))
 nil))
 nil)
 ("4"
 (skosimp*)
 (("4" (assert) nil nil))
 nil))
 nil))
 nil))
 nil)
 ("3" (skosimp*) (("3" (assert) nil nil)) nil)
 ("4" (skosimp*) (("4" (assert) nil nil)) nil))
 nil))
 nil)
 ("3" (assert) nil nil) ("4" (assert) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ((IFF const-decl "[bool, bool -> bool]" booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (boolean nonempty-type-decl nil booleans nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (real nonempty-type-from-decl nil reals nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (<= const-decl "bool" reals nil)
 (nonpos_real nonempty-type-eq-decl nil real_types nil)
 (< const-decl "bool" reals nil)
 (negreal nonempty-type-eq-decl nil real_types nil)
 (= const-decl "[T, T -> boolean]" equalities nil)
 (>= const-decl "bool" reals nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (- const-decl "[numfield -> numfield]" number_fields nil)
 (minus_even_is_even application-judgement "even_int" integers nil)
 (minus_nzint_is_nzint application-judgement "nzint" integers nil)
 (exp_neg_lb const-decl "posreal" exp_approx nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (> const-decl "bool" reals nil)
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (increasing? const-decl "bool" real_fun_preds "reals/")
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (int nonempty-type-eq-decl nil integers nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
 (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
 integers nil)
 (even_times_int_is_even application-judgement "even_int" integers
 nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (minus_int_is_int application-judgement "int" integers nil)
 (exp_neg_le1_lb const-decl "real" exp_approx nil)
 (TT skolem-const-decl "[negreal -> bool]" exp_approx nil)
 (pred type-eq-decl nil defined_types nil)
 (nat_induction formula-decl nil naturalnumbers nil)
 (posint_times_posint_is_posint application-judgement "posint"
 integers nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (div_mult_pos_lt1 formula-decl nil real_props nil)
 (div_mult_pos_le2 formula-decl nil real_props nil)
 (exp_neg_le1_lb_pos formula-decl nil exp_approx nil)
 (yy skolem-const-decl "(TT)" exp_approx nil)
 (n skolem-const-decl "nat" exp_approx nil)
 (xx skolem-const-decl "(TT)" exp_approx nil)
 (both_sides_expt_pos_le formula-decl nil exponentiation nil)
 (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
 nil)
 (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
 nil)
 (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
 real_types nil)
 (div_mult_pos_ge1 formula-decl nil real_props nil)
 (minus_odd_is_odd application-judgement "odd_int" integers nil)
 (exp_estimate_increasing formula-decl nil exp_series nil)
 (xx skolem-const-decl "(TT)" exp_approx nil)
 (real_plus_real_is_real application-judgement "real" reals nil)
 (yy skolem-const-decl "(TT)" exp_approx nil)
 (exp_range_test_lb formula-decl nil exp_approx nil)
 (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
 (subrange type-eq-decl nil integers nil)
 (N skolem-const-decl "posnat" exp_approx nil)
 (div_mult_pos_gt1 formula-decl nil extra_real_props nil)
 (rat_times_rat_is_rat application-judgement "rat" rationals nil)
 (both_sides_times_pos_lt1 formula-decl nil real_props nil)
 (xx skolem-const-decl "(TT)" exp_approx nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (floor_int formula-decl nil floor_ceil nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (int_minus_int_is_int application-judgement "int" integers nil)
 (FF skolem-const-decl "[[negreal, posnat] -> real]" exp_approx nil)
 (real_gt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (floor const-decl "{i | i <= x & x bool]" booleans nil)
 (integer nonempty-type-from-decl nil integers nil)
 (NOT const-decl "[bool -> bool]" booleans nil)
 (factorial def-decl "posnat" factorial "ints/")
 (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
 (nznum nonempty-type-eq-decl nil number_fields nil)
 (exp_estimate const-decl "real" exp_series nil)
 (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (^ const-decl "real" exponentiation nil)
 (/= const-decl "boolean" notequal nil)
 (OR const-decl "[bool, bool -> bool]" booleans nil)
 (posnat nonempty-type-eq-decl nil integers nil)
 (nonneg_int nonempty-type-eq-decl nil integers nil)
 (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
 (real_minus_real_is_real application-judgement "real" reals nil)
 (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
 (nnint_plus_posint_is_posint application-judgement "posint"
 integers nil)
 (even_plus_even_is_even application-judgement "even_int" integers
 nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (npreal_div_posreal_is_npreal application-judgement "npreal"
 real_types nil)
 (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
 real_types nil))
 nil))
(test_TCC1 0
 (test_TCC1-1 nil 3568479300 ("" (subtype-tcc) nil nil)
 ((boolean nonempty-type-decl nil booleans nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (NOT const-decl "[bool -> bool]" booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (real nonempty-type-from-decl nil reals nil)
 (< const-decl "bool" reals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (int nonempty-type-eq-decl nil integers nil)
 (>= const-decl "bool" reals nil)
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (below type-eq-decl nil naturalnumbers nil)
 (/= const-decl "boolean" notequal nil)
 (nzrat nonempty-type-eq-decl nil rationals nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (posrat_times_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
 nil)
 (rat_plus_rat_is_rat application-judgement "rat" rationals nil)
 (rat nonempty-type-eq-decl nil rationals nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (minus_nzint_is_nzint application-judgement "nzint" integers nil)
 (minus_even_is_even application-judgement "even_int" integers nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil))
 nil))
(test_TCC2 0
 (test_TCC2-1 nil 3568479300 ("" (subtype-tcc) nil nil)
 ((boolean nonempty-type-decl nil booleans nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (NOT const-decl "[bool -> bool]" booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (real nonempty-type-from-decl nil reals nil)
 (< const-decl "bool" reals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (int nonempty-type-eq-decl nil integers nil)
 (>= const-decl "bool" reals nil)
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (below type-eq-decl nil naturalnumbers nil)
 (/= const-decl "boolean" notequal nil)
 (nzrat nonempty-type-eq-decl nil rationals nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (posrat_times_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals
 nil)
 (rat_plus_rat_is_rat application-judgement "rat" rationals nil)
 (rat nonempty-type-eq-decl nil rationals nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (minus_nzint_is_nzint application-judgement "nzint" integers nil)
 (minus_even_is_even application-judgement "even_int" integers nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil))
 nil))
(test 0
 (test-1 nil 3568479302 ("" (eval-formula) nil nil)
 ((TRUE const-decl "bool" booleans nil)
 (id const-decl "(bijective?[T, T])" identity nil)
 (bijective? const-decl "bool" functions nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (boolean nonempty-type-decl nil booleans nil))
 shostak))
(exp_ub_increasing 0
 (exp_ub_increasing-1 nil 3568389268
 (""
 (case "(FORALL (n: nat): increasing?(LAMBDA (xn: negreal): exp_ub(xn, n))) AND (FORALL (n: nat): increasing?(LAMBDA (xp: posreal): exp_ub(xp, n))) AND (FORALL (n: nat): FORALL (xn:negreal): exp_ub(xn, n)<=1) AND (FORALL (n: nat): FORALL (xp:posreal): exp_ub(xp, n)>=1)")
 (("1" (flatten)
 (("1" (skeep)
 (("1" (inst - "n")
 (("1" (inst - "n")
 (("1" (inst - "n")
 (("1" (inst -4 "n")
 (("1" (assert)
 (("1" (expand "increasing?")
 (("1" (skosimp*)
 (("1" (case "y!1 < 0")
 (("1" (inst - "x!1" "y!1")
 (("1" (assert) nil nil)
 ("2" (assert) nil nil)
 ("3" (assert) nil nil))
 nil)
 ("2" (case "x!1 > 0")
 (("1" (inst -3 "x!1" "y!1")
 (("1" (assert) nil nil)
 ("2" (assert) nil nil)
 ("3" (assert) nil nil))
 nil)
 ("2" (assert)
 (("2" (case "exp_ub(0,n) = 1")
 (("1"
 (assert)
 (("1"
 (case "exp_ub(x!1,n)<=1")
 (("1"
 (case "exp_ub(y!1,n)>=1")
 (("1" (assert) nil nil)
 ("2"
 (inst -6 "y!1")
 (("2" (assert) nil nil))
 nil))
 nil)
 ("2"
 (inst -4 "x!1")
 (("2" (assert) nil nil))
 nil))
 nil))
 nil)
 ("2"
 (expand "exp_ub" 1)
 (("2"
 (expand "exp_ub_n")
 (("2" (propax) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (hide 2)
 (("2" (split)
 (("1" (lemma "exp_neg_ub_increasing")
 (("1" (skeep)
 (("1" (inst - "min(n,exp_approx_term_cutoff)")
 (("1" (expand "increasing?")
 (("1" (skosimp*)
 (("1" (assert)
 (("1" (case "min(n,30)<=30")
 (("1" (assert)
 (("1" (hide -1)
 (("1" (expand "exp_ub")
 (("1" (name "kk" "min(n,30)")
 (("1"
 (case
 "exp_ub_n(x!1,kk) <= exp_ub_n(y!1,kk)")
 (("1"
 (hide-all-but (-1 1))
 (("1"
 (expand "kk")
 (("1"
 (grind :exclude "exp_ub_n")
 nil
 nil))
 nil))
 nil)
 ("2"
 (hide 2)
 (("2"
 (expand "exp_ub_n")
 (("2"
 (lift-if)
 (("2"
 (lift-if)
 (("2"
 (assert)
 (("2"
 (lift-if)
 (("2"
 (assert)
 (("2"
 (ground)
 (("1"
 (inst - "x!1" "y!1")
 (("1"
 (assert)
 nil
 nil))
 nil)
 ("2"
 (inst - "-60" "y!1")
 (("2"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (assert)
 (("3"
 (hide-all-but 1)
 (("3"
 (expand "kk")
 (("3" (grind) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (expand "min")
 (("2" (lift-if) (("2" (ground) nil nil)) nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
 nil))
 nil))
 nil)
 ("2" (lemma "exp_neg_ub_increasing")
 (("2" (skeep)
 (("2" (inst - "min(n,exp_approx_term_cutoff)")
 (("1" (expand "increasing?")
 (("1" (skosimp*)
 (("1" (assert)
 (("1" (case "min(n,30)<=30")
 (("1" (assert)
 (("1" (hide -1)
 (("1" (expand "exp_ub")
 (("1" (name "kk" "min(n,30)")
 (("1"
 (case
 "exp_ub_n(x!1,kk) <= exp_ub_n(y!1,kk)")
 (("1"
 (hide-all-but (-1 1))
 (("1"
 (expand "kk")
 (("1"
 (grind :exclude "exp_ub_n")
 nil
 nil))
 nil))
 nil)
 ("2"
 (hide 2)
 (("2"
 (expand "exp_ub_n")
 (("2"
 (lift-if)
 (("2"
 (lift-if)
 (("2"
 (assert)
 (("2"
 (ground)
 (("1"
 (cross-mult 1)
 (("1"
 (lemma
 "exp_neg_lb_increasing")
 (("1"
 (inst - "kk")
 (("1"
 (assert)
 (("1"
 (expand
 "increasing?")
 (("1"
 (inst
 -
 "-y!1"
 "-x!1")
 (("1"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil)
 ("2"
 (assert)
 (("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (hide 1)
 (("2"
 (case
 "FORALL (aa,bb,cc:real): aa<=bb IMPLIES aa<=max(bb,cc)")
 (("1"
 (rewrite -1)
 (("1"
 (hide 2)
 (("1"
 (cross-mult 1)
 (("1"
 (lemma
 "exp_neg_lb_increasing")
 (("1"
 (inst - "kk")
 (("1"
 (assert)
 (("1"
 (expand
 "increasing?")
 (("1"
 (inst
 -
 "-60"
 "-x!1")
 (("1"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand
 "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil)
 ("2"
 (hide-all-but 1)
 (("2"
 (grind)
 nil
 nil))
 nil))
 nil))
 nil)
 ("3"
 (lemma
 "both_sides_expt_gt1_lt")
 (("3"
 (inst
 -
 "4"
 "1+floor(x!1)"
 "1+floor(y!1)")
 (("3"
 (expand "max")
 (("3"
 (lift-if)
 (("3"
 (lift-if)
 (("3"
 (lift-if)
 (("3"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (expand "min")
 (("3"
 (lift-if)
 (("3" (ground) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (expand "min")
 (("2" (lift-if) (("2" (ground) nil nil)) nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (expand "min")
 (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil))
 nil))
 nil))
 nil)
 ("3" (skeep)
 (("3" (skeep)
 (("3" (expand "exp_ub")
 (("3" (name "KK" "min(n,30)")
 (("3" (case "exp_ub_n(xn,KK) <=1")
 (("1" (lift-if)
 (("1" (expand "min")
 (("1" (lift-if) (("1" (ground) nil nil)) nil))
 nil))
 nil)
 ("2" (hide 2)
 (("2" (expand "exp_ub_n")
 (("2" (name "XK" "max(-60,xn)")
 (("2" (case "exp_neg_ub(KK,XK) <= 1")
 (("1" (expand "max")
 (("1" (lift-if) (("1" (ground) nil nil))
 nil))
 nil)
 ("2" (hide 2)
 (("2" (expand "exp_neg_ub")
 (("2"
 (lemma "both_sides_expt_pos_ge")
 (("2"
 (inst
 -
 "-floor(XK)"
 "1"
 "exp_neg_le1_ub(1 + KK, XK / -floor(XK))")
 (("1"
 (assert)
 (("1"
 (hide 2)
 (("1"
 (expand "exp_neg_le1_ub")
 (("1"
 (lemma
 "exp_estimate_increasing")
 (("1"
 (inst
 -
 "2+2*KK"
 "XK/-floor(XK)"
 "0")
 (("1"
 (assert)
 (("1"
 (split -)
 (("1"
 (rewrite
 "exp_estimate_0")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil)
 ("2"
 (cross-mult 1)
 (("2"
 (ground)
 (("2"
 (expand "max")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (cross-mult 1)
 nil
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (case
 "FORALL (rr:real): rr>0 IMPLIES (rr>=0 AND rr > 0)")
 (("1"
 (rewrite -1)
 (("1"
 (hide 2)
 (("1"
 (hide 2)
 (("1"
 (lemma
 "exp_neg_le1_lb_pos")
 (("1"
 (inst - "1+KK" _)
 (("1"
 (inst
 -
 "XK/-floor(XK)")
 (("1"
 (assert)
 (("1"
 (expand
 "exp_neg_le1_lb")
 (("1"
 (expand
 "exp_neg_le1_ub")
 (("1"
 (assert)
 (("1"
 (ground)
 (("1"
 (cross-mult
 1)
 (("1"
 (ground)
 (("1"
 (expand
 "max")
 (("1"
 (lift-if)
 (("1"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (cross-mult
 1)
 (("2"
 (ground)
 (("2"
 (expand
 "max")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2" (ground) nil nil))
 nil))
 nil))
 nil)
 ("2"
 (hide-all-but 1)
 (("2" (grind) nil nil))
 nil))
 nil)
 ("3"
 (expand "min")
 (("3"
 (lift-if)
 (("3" (ground) nil nil))
 nil))
 nil)
 ("4"
 (expand "max")
 (("4"
 (lift-if)
 (("4" (ground) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3" (expand "max")
 (("3" (lift-if) (("3" (ground) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3" (expand "min")
 (("3" (lift-if) (("3" (ground) nil nil)) nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("4" (skeep)
 (("4" (skeep)
 (("4" (expand "exp_ub")
 (("4" (name "KK" "min(n,30)")
 (("4" (case "exp_ub_n(xp,KK) >=1")
 (("1" (expand "min")
 (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)
 ("2" (hide 2)
 (("2" (expand "exp_ub_n")
 (("2" (lift-if)
 (("2" (ground)
 (("1" (cross-mult 1)
 (("1" (lemma "exp_neg_lb_increasing")
 (("1"
 (inst - "KK")
 (("1"
 (assert)
 (("1"
 (expand "increasing?")
 (("1"
 (expand "exp_neg_lb")
 (("1"
 (assert)
 (("1"
 (lemma
 "both_sides_expt_pos_ge")
 (("1"
 (inst
 -
 "-floor(-xp)"
 "1"
 "exp_neg_le1_lb(1 + KK, -xp / -floor(-xp))")
 (("1"
 (assert)
 (("1"
 (hide 2)
 (("1"
 (expand
 "exp_neg_le1_lb")
 (("1"
 (lemma
 "exp_estimate_increasing")
 (("1"
 (inst
 -
 "2+2*KK"
 "-xp / -floor(-xp)"
 "0")
 (("1"
 (assert)
 (("1"
 (split -)
 (("1"
 (rewrite
 "exp_estimate_0")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (expand
 "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil)
 ("2"
 (hide -1)
 (("2"
 (cross-mult
 1)
 nil
 nil))
 nil)
 ("3"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (case
 "FORALL (rr:real): rr>0 IMPLIES (rr>=0 AND rr > 0)")
 (("1"
 (rewrite -1)
 (("1"
 (hide (-1 -2))
 (("1"
 (hide 2)
 (("1"
 (lemma
 "exp_neg_le1_lb_pos")
 (("1"
 (inst?)
 (("1"
 (assert)
 (("1"
 (split)
 (("1"
 (cross-mult
 1)
 nil
 nil)
 ("2"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil)
 ("2"
 (expand
 "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil)
 ("2"
 (hide-all-but 1)
 (("2" (grind) nil nil))
 nil))
 nil)
 ("3"
 (expand "min")
 (("3"
 (lift-if)
 (("3"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2" (ground) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (case "floor(xp) >= 1")
 (("1" (lemma "both_sides_expt_pos_ge")
 (("1"
 (inst - "1+floor(xp)" "4" "1")
 (("1" (assert) nil nil))
 nil))
 nil)
 ("2" (assert) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3" (expand "min")
 (("3" (lift-if) (("3" (ground) nil nil)) nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ((div_mult_pos_lt1 formula-decl nil real_props nil)
 (xp skolem-const-decl "posreal" exp_approx nil)
 (real_times_real_is_real application-judgement "real" reals nil)
 (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
 real_types nil)
 (KK skolem-const-decl "{k: int | k <= n AND k <= 30}" exp_approx
 nil)
 (n skolem-const-decl "nat" exp_approx nil)
 (div_mult_pos_ge1 formula-decl nil real_props nil)
 (exp_neg_ub const-decl "posreal" exp_approx nil)
 (real_div_nzreal_is_real application-judgement "real" reals nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (minus_int_is_int application-judgement "int" integers nil)
 (xn skolem-const-decl "negreal" exp_approx nil)
 (XK skolem-const-decl "{p: real | p >= -60 AND p >= xn}" exp_approx
 nil)
 (n skolem-const-decl "nat" exp_approx nil)
 (KK skolem-const-decl "{k: int | k <= n AND k <= 30}" exp_approx
 nil)
 (exp_neg_le1_ub const-decl "real" exp_approx nil)
 (posnat nonempty-type-eq-decl nil integers nil)
 (nonneg_int nonempty-type-eq-decl nil integers nil)
 (exp_estimate_increasing formula-decl nil exp_series nil)
 (minus_odd_is_odd application-judgement "odd_int" integers nil)
 (div_mult_pos_neg_le1 formula-decl nil extra_real_props nil)
 (div_mult_pos_neg_le2 formula-decl nil extra_real_props nil)
 (exp_estimate_0 formula-decl nil exp_series nil)
 (even_plus_even_is_even application-judgement "even_int" integers
 nil)
 (even_times_int_is_even application-judgement "even_int" integers
 nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (expt_1i formula-decl nil exponentiation nil)
 (nnrat_exp application-judgement "nnrat" exponentiation nil)
 (posrat_exp application-judgement "posrat" exponentiation nil)
 (real_minus_real_is_real application-judgement "real" reals nil)
 (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
 (div_mult_pos_neg_lt1 formula-decl nil extra_real_props nil)
 (exp_neg_le1_lb const-decl "real" exp_approx nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (exp_neg_le1_lb_pos formula-decl nil exp_approx nil)
 (both_sides_expt_pos_ge formula-decl nil exponentiation nil)
 (n skolem-const-decl "nat" exp_approx nil)
 (both_sides_expt_gt1_lt formula-decl nil exponentiation nil)
 (NOT const-decl "[bool -> bool]" booleans nil)
 (floor const-decl "{i | i <= x & x numfield]" number_fields nil)
 (^ const-decl "real" exponentiation nil)
 (OR const-decl "[bool, bool -> bool]" booleans nil)
 (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
 (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
 (posreal_times_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (div_mult_pos_le1 formula-decl nil real_props nil)
 (exp_neg_lb const-decl "posreal" exp_approx nil)
 (/= const-decl "boolean" notequal nil)
 (nznum nonempty-type-eq-decl nil number_fields nil)
 (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
 (times_div2 formula-decl nil real_props nil)
 (nonzero_real nonempty-type-eq-decl nil reals nil)
 (div_mult_pos_le2 formula-decl nil real_props nil)
 (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (exp_neg_lb_increasing formula-decl nil exp_approx nil)
 (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
 nil)
 (posint_plus_nnint_is_posint application-judgement "posint"
 integers nil)
 (posint_exp application-judgement "posint" exponentiation nil)
 (posreal_div_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (posreal_max application-judgement
 "{z: posreal | z >= x AND z >= y}" real_defs nil)
 (kk skolem-const-decl "{k: int | k <= n AND k <= 30}" exp_approx
 nil)
 (exp_neg_ub_increasing formula-decl nil exp_approx nil)
 (int_min application-judgement "{k: int | k <= i AND k <= j}"
 real_defs nil)
 (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
 (n skolem-const-decl "nat" exp_approx nil)
 (minus_even_is_even application-judgement "even_int" integers nil)
 (- const-decl "[numfield -> numfield]" number_fields nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (kk skolem-const-decl "{k: int | k <= n AND k <= 30}" exp_approx
 nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (real_gt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (= const-decl "[T, T -> boolean]" equalities nil)
 (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
 (exp_ub_n const-decl "posreal" exp_approx nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (x!1 skolem-const-decl "real" exp_approx nil)
 (y!1 skolem-const-decl "real" exp_approx nil)
 (boolean nonempty-type-decl nil booleans nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (real nonempty-type-from-decl nil reals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (int nonempty-type-eq-decl nil integers nil)
 (>= const-decl "bool" reals nil)
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (<= const-decl "bool" reals nil)
 (nonpos_real nonempty-type-eq-decl nil real_types nil)
 (< const-decl "bool" reals nil)
 (negreal nonempty-type-eq-decl nil real_types nil)
 (increasing? const-decl "bool" real_fun_preds "reals/")
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (> const-decl "bool" reals nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (exp_ub const-decl "posreal" exp_approx nil))
 shostak))
(exp_lb_increasing 0
 (exp_lb_increasing-1 nil 3568630459
 (""
 (case "(FORALL (n: nat): increasing?(LAMBDA (xn: negreal): exp_lb(xn, n))) AND (FORALL (n: nat): increasing?(LAMBDA (xp: posreal): exp_lb(xp, n))) AND (FORALL (n: nat): FORALL (xn:negreal): exp_lb(xn, n)<=1) AND (FORALL (n: nat): FORALL (xp:posreal): exp_lb(xp, n)>=1)")
 (("1" (flatten)
 (("1" (skeep)
 (("1" (inst - "n")
 (("1" (inst - "n")
 (("1" (inst - "n")
 (("1" (inst -4 "n")
 (("1" (assert)
 (("1" (expand "increasing?")
 (("1" (skosimp*)
 (("1" (case "y!1 < 0")
 (("1" (inst - "x!1" "y!1")
 (("1" (assert) nil nil)
 ("2" (assert) nil nil)
 ("3" (assert) nil nil))
 nil)
 ("2" (case "x!1 > 0")
 (("1" (inst -3 "x!1" "y!1")
 (("1" (assert) nil nil)
 ("2" (assert) nil nil)
 ("3" (assert) nil nil))
 nil)
 ("2" (assert)
 (("2" (case "exp_lb(0,n) = 1")
 (("1"
 (assert)
 (("1"
 (case "exp_lb(x!1,n)<=1")
 (("1"
 (case "exp_lb(y!1,n)>=1")
 (("1" (assert) nil nil)
 ("2"
 (inst -6 "y!1")
 (("2" (assert) nil nil))
 nil))
 nil)
 ("2"
 (inst -4 "x!1")
 (("2" (assert) nil nil))
 nil))
 nil))
 nil)
 ("2"
 (expand "exp_lb" 1)
 (("2"
 (expand "exp_lb_n")
 (("2" (propax) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (hide 2)
 (("2" (split)
 (("1" (lemma "exp_neg_lb_increasing")
 (("1" (skeep)
 (("1" (inst - "min(n,exp_approx_term_cutoff)")
 (("1" (expand "increasing?")
 (("1" (skosimp*)
 (("1" (assert)
 (("1" (case "min(n,30)<=30")
 (("1" (assert)
 (("1" (expand "exp_lb")
 (("1" (name "kk" "min(n,30)")
 (("1"
 (case "exp_lb_n(x!1,kk) <= exp_lb_n(y!1,kk)")
 (("1"
 (hide-all-but (-1 1))
 (("1"
 (expand "kk")
 (("1"
 (grind :exclude "exp_lb_n")
 nil
 nil))
 nil))
 nil)
 ("2"
 (hide 2)
 (("2"
 (expand "exp_lb_n")
 (("2"
 (lift-if)
 (("2"
 (lift-if)
 (("2"
 (assert)
 (("2"
 (lift-if)
 (("2"
 (ground)
 (("1"
 (inst - "x!1" "y!1")
 (("1" (assert) nil nil))
 nil)
 ("2"
 (inst - "-60" "y!1")
 (("2" (assert) nil nil))
 nil)
 ("3"
 (lemma
 "both_sides_expt_gt1_lt")
 (("3"
 (inst
 -
 "4"
 "floor(x!1)"
 "floor(y!1)")
 (("3"
 (assert)
 (("3"
 (expand "min")
 (("3"
 (lift-if)
 (("3"
 (lift-if)
 (("3"
 (lift-if)
 (("3"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (expand "min")
 (("3"
 (lift-if)
 (("3" (ground) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (hide-all-but 1) (("2" (grind) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
 nil))
 nil))
 nil)
 ("2" (lemma "exp_neg_lb_increasing")
 (("2" (skeep)
 (("2" (inst - "min(n,exp_approx_term_cutoff)")
 (("1" (expand "increasing?")
 (("1" (skosimp*)
 (("1" (assert)
 (("1" (case "min(n,30)<=30")
 (("1" (assert)
 (("1" (hide -1)
 (("1" (expand "exp_lb")
 (("1" (name "kk" "min(n,30)")
 (("1"
 (case
 "exp_lb_n(x!1,kk) <= exp_lb_n(y!1,kk)")
 (("1"
 (hide-all-but (-1 1))
 (("1"
 (expand "kk")
 (("1"
 (grind :exclude "exp_lb_n")
 nil
 nil))
 nil))
 nil)
 ("2"
 (hide 2)
 (("2"
 (expand "exp_lb_n")
 (("2"
 (lift-if)
 (("2"
 (lift-if)
 (("2"
 (assert)
 (("2"
 (ground)
 (("1"
 (cross-mult 1)
 (("1"
 (lemma
 "exp_neg_ub_increasing")
 (("1"
 (inst - "kk")
 (("1"
 (assert)
 (("1"
 (expand
 "increasing?")
 (("1"
 (inst
 -
 "-y!1"
 "-x!1")
 (("1"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil)
 ("2"
 (assert)
 (("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (hide 1)
 (("2"
 (case
 "FORALL (aa,bb,cc:real): aa<=bb IMPLIES aa<=max(bb,cc)")
 (("1"
 (rewrite -1)
 (("1"
 (hide 2)
 (("1"
 (cross-mult 1)
 (("1"
 (lemma
 "exp_neg_ub_increasing")
 (("1"
 (inst - "kk")
 (("1"
 (assert)
 (("1"
 (expand
 "increasing?")
 (("1"
 (inst
 -
 "-60"
 "-x!1")
 (("1"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand
 "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil)
 ("2"
 (hide-all-but 1)
 (("2"
 (grind)
 nil
 nil))
 nil))
 nil))
 nil)
 ("3"
 (lemma
 "both_sides_expt_gt1_lt")
 (("3"
 (inst
 -
 "2"
 "floor(x!1)"
 "floor(y!1)")
 (("3"
 (expand "max")
 (("3"
 (lift-if)
 (("3"
 (lift-if)
 (("3"
 (lift-if)
 (("3"
 (assert)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (expand "min")
 (("3"
 (lift-if)
 (("3" (ground) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (expand "min")
 (("2" (lift-if) (("2" (ground) nil nil)) nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (expand "min")
 (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil))
 nil))
 nil))
 nil)
 ("3" (skeep)
 (("3" (skeep)
 (("3" (expand "exp_lb")
 (("3" (name "KK" "min(n,30)")
 (("3" (case "exp_lb_n(xn,KK) <=1")
 (("1" (lift-if)
 (("1" (expand "min")
 (("1" (lift-if) (("1" (ground) nil nil)) nil))
 nil))
 nil)
 ("2" (hide 2)
 (("2" (expand "exp_lb_n")
 (("2" (name "XK" "max(-60,xn)")
 (("2" (case "exp_neg_lb(KK,XK) <= 1")
 (("1" (expand "max")
 (("1" (lift-if) (("1" (ground) nil nil))
 nil))
 nil)
 ("2" (hide 2)
 (("2" (expand "exp_neg_lb")
 (("2"
 (lemma "both_sides_expt_pos_ge")
 (("2"
 (inst
 -
 "-floor(XK)"
 "1"
 "exp_neg_le1_lb(1 + KK, XK / -floor(XK))")
 (("1"
 (assert)
 (("1"
 (hide 2)
 (("1"
 (expand "exp_neg_le1_lb")
 (("1"
 (lemma
 "exp_estimate_increasing")
 (("1"
 (inst
 -
 "2+2*KK"
 "XK/-floor(XK)"
 "0")
 (("1"
 (assert)
 (("1"
 (split -)
 (("1"
 (rewrite
 "exp_estimate_0")
 (("1"
 (assert)
 nil
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil)
 ("2"
 (cross-mult 1)
 (("2"
 (ground)
 (("2"
 (expand "max")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3"
 (cross-mult 1)
 nil
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (case
 "FORALL (rr:real): rr>0 IMPLIES (rr>=0 AND rr > 0)")
 (("1"
 (rewrite -1)
 (("1"
 (hide 2)
 (("1"
 (hide 2)
 (("1"
 (lemma
 "exp_neg_le1_lb_pos")
 (("1"
 (inst?)
 (("1"
 (assert)
 (("1"
 (split)
 (("1"
 (cross-mult 1)
 (("1"
 (ground)
 (("1"
 (expand "max")
 (("1"
 (lift-if)
 (("1"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (cross-mult 1)
 (("2"
 (ground)
 (("2"
 (expand "max")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2" (ground) nil nil))
 nil))
 nil))
 nil)
 ("2"
 (hide-all-but 1)
 (("2" (grind) nil nil))
 nil))
 nil)
 ("3"
 (expand "min")
 (("3"
 (lift-if)
 (("3" (ground) nil nil))
 nil))
 nil)
 ("4"
 (expand "max")
 (("4"
 (lift-if)
 (("4" (ground) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3" (expand "max")
 (("3" (lift-if) (("3" (ground) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3" (expand "min")
 (("3" (lift-if) (("3" (ground) nil nil)) nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("4" (skeep)
 (("4" (skeep)
 (("4" (expand "exp_lb")
 (("4" (name "KK" "min(n,30)")
 (("4" (case "exp_lb_n(xp,KK) >=1")
 (("1" (expand "min")
 (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)
 ("2" (hide 2)
 (("2" (expand "exp_lb_n")
 (("2" (lift-if)
 (("2" (ground)
 (("1" (cross-mult 1)
 (("1" (expand "exp_neg_ub")
 (("1"
 (lemma "both_sides_expt_pos_ge")
 (("1"
 (inst
 -
 "-floor(-xp)"
 "1"
 "exp_neg_le1_ub(1 + KK, -xp / -floor(-xp))")
 (("1"
 (assert)
 (("1"
 (hide 2)
 (("1"
 (expand "exp_neg_le1_ub")
 (("1"
 (lemma
 "exp_estimate_increasing")
 (("1"
 (inst
 -
 "2+2*KK"
 "-xp / -floor(-xp)"
 "0")
 (("1"
 (assert)
 (("1"
 (rewrite
 "exp_estimate_0")
 (("1"
 (assert)
 (("1"
 (split)
 (("1"
 (cross-mult 1)
 nil
 nil)
 ("2"
 (cross-mult 1)
 nil
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (case
 "FORALL (rr:real): rr>0 IMPLIES (rr>=0 AND rr > 0)")
 (("1"
 (rewrite -1)
 (("1"
 (hide (-1 -2))
 (("1"
 (hide 2)
 (("1"
 (lemma
 "exp_neg_le1_lb_pos")
 (("1"
 (inst
 -
 "1+KK"
 "-xp/-floor(-xp)")
 (("1"
 (expand
 "exp_neg_le1_lb")
 (("1"
 (expand
 "exp_neg_le1_ub")
 (("1"
 (assert)
 (("1"
 (case
 "1000001/1000000 / factorial(3 + 2 * KK) > 0")
 (("1"
 (assert)
 (("1"
 (split)
 (("1"
 (cross-mult
 1)
 nil
 nil)
 ("2"
 (cross-mult
 1)
 nil
 nil))
 nil))
 nil)
 ("2"
 (assert)
 nil
 nil)
 ("3"
 (expand "min")
 (("3"
 (lift-if)
 (("3"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2"
 (ground)
 nil
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("2"
 (expand "min")
 (("2"
 (lift-if)
 (("2" (ground) nil nil))
 nil))
 nil))
 nil)
 ("2"
 (hide-all-but 1)
 (("2" (grind) nil nil))
 nil))
 nil)
 ("3"
 (expand "min")
 (("3"
 (lift-if)
 (("3" (ground) nil nil))
 nil))
 nil)
 ("4" (assert) nil nil))
 nil))
 nil))
 nil))
 nil)
 ("2" (case "floor(xp) >= 1")
 (("1" (lemma "both_sides_expt_pos_ge")
 (("1"
 (inst - "floor(xp)" "2" "1")
 (("1" (assert) nil nil))
 nil))
 nil)
 ("2" (assert) nil nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ("3" (expand "min")
 (("3" (lift-if) (("3" (ground) nil nil)) nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ((nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
 real_types nil)
 (xp skolem-const-decl "posreal" exp_approx nil)
 (n skolem-const-decl "nat" exp_approx nil)
 (KK skolem-const-decl "{k: int | k <= n AND k <= 30}" exp_approx
 nil)
 (exp_neg_le1_ub const-decl "real" exp_approx nil)
 (real_times_real_is_real application-judgement "real" reals nil)
 (factorial def-decl "posnat" factorial "ints/")
 (div_mult_pos_lt1 formula-decl nil real_props nil)
 (div_mult_pos_ge1 formula-decl nil real_props nil)
 (exp_neg_lb const-decl "posreal" exp_approx nil)
 (real_div_nzreal_is_real application-judgement "real" reals nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (minus_int_is_int application-judgement "int" integers nil)
 (xn skolem-const-decl "negreal" exp_approx nil)
 (XK skolem-const-decl "{p: real | p >= -60 AND p >= xn}" exp_approx
 nil)
 (n skolem-const-decl "nat" exp_approx nil)
 (KK skolem-const-decl "{k: int | k <= n AND k <= 30}" exp_approx
 nil)
 (exp_neg_le1_lb const-decl "real" exp_approx nil)
 (posnat nonempty-type-eq-decl nil integers nil)
 (nonneg_int nonempty-type-eq-decl nil integers nil)
 (exp_estimate_increasing formula-decl nil exp_series nil)
 (minus_odd_is_odd application-judgement "odd_int" integers nil)
 (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
 (real_minus_real_is_real application-judgement "real" reals nil)
 (div_mult_pos_neg_le1 formula-decl nil extra_real_props nil)
 (div_mult_pos_neg_le2 formula-decl nil extra_real_props nil)
 (exp_estimate_0 formula-decl nil exp_series nil)
 (even_plus_even_is_even application-judgement "even_int" integers
 nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (even_times_int_is_even application-judgement "even_int" integers
 nil)
 (expt_1i formula-decl nil exponentiation nil)
 (posrat_exp application-judgement "posrat" exponentiation nil)
 (div_mult_pos_neg_lt1 formula-decl nil extra_real_props nil)
 (exp_neg_le1_lb_pos formula-decl nil exp_approx nil)
 (both_sides_expt_pos_ge formula-decl nil exponentiation nil)
 (n skolem-const-decl "nat" exp_approx nil)
 (NOT const-decl "[bool -> bool]" booleans nil)
 (^ const-decl "real" exponentiation nil)
 (OR const-decl "[bool, bool -> bool]" booleans nil)
 (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
 (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
 (posreal_times_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (div_mult_pos_le1 formula-decl nil real_props nil)
 (exp_neg_ub const-decl "posreal" exp_approx nil)
 (/= const-decl "boolean" notequal nil)
 (nznum nonempty-type-eq-decl nil number_fields nil)
 (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
 (times_div2 formula-decl nil real_props nil)
 (nonzero_real nonempty-type-eq-decl nil reals nil)
 (div_mult_pos_le2 formula-decl nil real_props nil)
 (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (exp_neg_ub_increasing formula-decl nil exp_approx nil)
 (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
 nil)
 (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
 (posint_exp application-judgement "posint" exponentiation nil)
 (posreal_div_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (posreal_max application-judgement
 "{z: posreal | z >= x AND z >= y}" real_defs nil)
 (kk skolem-const-decl "{k: int | k <= n AND k <= 30}" exp_approx
 nil)
 (exp_neg_lb_increasing formula-decl nil exp_approx nil)
 (int_min application-judgement "{k: int | k <= i AND k <= j}"
 real_defs nil)
 (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
 (n skolem-const-decl "nat" exp_approx nil)
 (kk skolem-const-decl "{k: int | k <= n AND k <= 30}" exp_approx
 nil)
 (both_sides_expt_gt1_lt formula-decl nil exponentiation nil)
 (integer nonempty-type-from-decl nil integers nil)
 (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (floor const-decl "{i | i <= x & x numfield]" number_fields nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (nnrat_exp application-judgement "nnrat" exponentiation nil)
 (posreal_min application-judgement
 "{z: posreal | z <= x AND z <= y}" real_defs nil)
 (minus_even_is_even application-judgement "even_int" integers nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (real_gt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (= const-decl "[T, T -> boolean]" equalities nil)
 (exp_lb_n const-decl "posreal" exp_approx nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (x!1 skolem-const-decl "real" exp_approx nil)
 (y!1 skolem-const-decl "real" exp_approx nil)
 (boolean nonempty-type-decl nil booleans nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (real nonempty-type-from-decl nil reals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (int nonempty-type-eq-decl nil integers nil)
 (>= const-decl "bool" reals nil)
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (<= const-decl "bool" reals nil)
 (nonpos_real nonempty-type-eq-decl nil real_types nil)
 (< const-decl "bool" reals nil)
 (negreal nonempty-type-eq-decl nil real_types nil)
 (increasing? const-decl "bool" real_fun_preds "reals/")
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (> const-decl "bool" reals nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (exp_lb const-decl "posreal" exp_approx nil))
 nil))
(e_bounds 0
 (e_bounds-1 nil 3295625003
 ("" (skosimp)
 (("" (expand "e")
 (("" (expand "e_lb")
 (("" (expand "e_ub") (("" (rewrite "exp_bounds") nil nil))
 nil))
 nil))
 nil))
 nil)
 ((e const-decl "posreal" ln_exp nil)
 (e_ub const-decl "posreal" exp_approx nil)
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (>= const-decl "bool" reals nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (int nonempty-type-eq-decl nil integers nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (real nonempty-type-from-decl nil reals nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (boolean nonempty-type-decl nil booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (exp_bounds formula-decl nil exp_approx nil)
 (e_lb const-decl "posreal" exp_approx nil))
 shostak))
(e_bounds2 0
 (e_bounds2-1 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)
 ((exp_0 formula-decl nil ln_exp nil)
 (minus_odd_is_odd application-judgement "odd_int" integers nil)
 (exp_neg_le1_bounds formula-decl nil exp_approx nil)
 (rational_pred const-decl "[real -> boolean]" rationals nil)
 (rational nonempty-type-from-decl nil rationals nil)
 (integer_pred const-decl "[rational -> boolean]" integers nil)
 (int nonempty-type-eq-decl nil integers nil)
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (- const-decl "[numfield -> numfield]" number_fields nil)
 (real_minus_real_is_real application-judgement "real" reals nil)
 (exp_neg_le1_ub const-decl "real" exp_approx nil)
 (^ const-decl "real" exponentiation nil)
 (expt def-decl "real" exponentiation nil)
 (factorial def-decl "posnat" factorial "ints/")
 (sigma def-decl "real" sigma "reals/")
 (exp_estimate const-decl "real" exp_series nil)
 (even_times_int_is_even application-judgement "even_int" integers
 nil)
 (posint_times_posint_is_posint application-judgement "posint"
 integers nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (nzint_times_nzint_is_nzint application-judgement "nzint" integers
 nil)
 (nzreal_expt application-judgement "nzreal" exponentiation nil)
 (int_expt application-judgement "int" exponentiation nil)
 (real_gt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
 nil)
 (real_plus_real_is_real application-judgement "real" reals nil)
 (exp_neg_le1_lb const-decl "real" exp_approx nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (even_minus_odd_is_odd application-judgement "odd_int" integers
 nil)
 (exp_diff formula-decl nil ln_exp nil)
 (div_mult_pos_lt2 formula-decl nil real_props nil)
 (posreal_times_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (div_mult_pos_lt1 formula-decl nil real_props nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (posreal_div_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (boolean nonempty-type-decl nil booleans nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (number_field_pred const-decl "[number -> boolean]" number_fields
 nil)
 (number_field nonempty-type-from-decl nil number_fields nil)
 (real_pred const-decl "[number_field -> boolean]" reals nil)
 (real nonempty-type-from-decl nil reals nil)
 (< const-decl "bool" reals nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (/= const-decl "boolean" notequal nil)
 (nznum nonempty-type-eq-decl nil number_fields nil)
 (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
 (>= const-decl "bool" reals nil)
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (> const-decl "bool" reals nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (e const-decl "posreal" ln_exp nil))
 nil))
(e_bound 0
 (e_bound-1 nil 3307358139
 ("" (lemma "e_bounds2")
 (("" (expand "e_lb")
 (("" (expand "e_ub") (("" (flatten) (("" (assert) nil nil)) nil))
 nil))
 nil))
 nil)
 ((e_lb const-decl "posreal" exp_approx nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (e_ub const-decl "posreal" exp_approx nil)
 (e_bounds2 formula-decl nil exp_approx nil))
 shostak)))

Messung V0.5 in Prozent

¤ 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.495Bemerkung: (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-30) ¤

*Eine klare Vorstellung vom Zielzustand

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

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.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.