Quellcode-Bibliothek atan_approx.prf
Sprache: Lisp
(atan_approxnil 3392566953"" (skeep)"" (expand "atan_pos_le1_ub" )"" (expand "atan_series_n" )"" (expand "sigma" 1 1)"" (expand "sigma" 1 1)"" (move-terms 1 r 1)"" (assert )"" (expand "atan_series_term" )"" (expand "atan_series_coef" )"" (lemma "not_even_m1_pow" )"" (inst?)"" (split -1)"1" (replaces -1)"1" (lemma "even_m1_pow" )"1" "1" "1" "1" case "(x ^ (5 + 4 * n)) * (1 / (5 + 4 * n)) < (x ^ (5 + 4 * n)) / (3 + 4 * n)" )"1" case "(x ^ (5 + 4 * n)) / (3 + 4 * n) <= (x ^ (3 + 4 * n)) / (3 + 4 * n)" )"1" (assert ) nil nil )"2" "2" "2" rewrite "both_sides_expt_lt1_le" )"2" case "x=1" )"1" "1" nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "x ^ (5+4 *n) > 0" )"1" "aa" "x^(5+4*n)" )"1" nil nil ))nil )"2" "2" rewrite "expt_pos" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))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 )"real" atan_approx nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" sigma "reals/" )"real" reals nil )"posint" nil )"odd_int" integers nil )"even_int" integersnil )"real" reals nil )nil booleans nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[nat -> real]" atan nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )nil exponentiation nil )"real" reals nil )"boolean" notequal nil )"real" exponentiation nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil exponentiation nil )"posint" exponentiation nil )"posnat" exponentiation nil )"posint" nil )"even_int" integersnil )"odd_int" integersnil )nil real_props nil )"real" exponentiation nil )nil real_props nil )"[T, T -> boolean]" equalities nil )nil real_props nil )"posrat" nil )nil real_props nil )nil real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil exponentiation nil )"odd_int" integers nil )"real" reals nil )"bool" integers nil )"rat" atan nil )"nzrat" rationalsnil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" atan nil ))nil 3392570203"" (skeep)"" (expand "atan_pos_le1_lb" )"" (expand "atan_series_n" )"" (expand "sigma" 1 2)"" (expand "sigma" 1 2)"" (move-terms 1 r 3)"" (assert )"" (expand "atan_series_term" )"" (expand "atan_series_coef" )"" (lemma "not_even_m1_pow" )"" (inst -1 "3+2*n" )"" (split -1)"1" (replaces -1)"1" (lemma "even_m1_pow" )"1" "1" "1" "1" case "(x ^ (5 + 4 * n))/(7 + 4 * n) < (x ^ (5 + 4 * n)) * (1 / (5 + 4 * n))" )"1" case "(x ^ (7 + 4 * n))/(7+4*n) <= (x ^ (5 + 4 * n))/(7+4*n)" )"1" (assert ) nil nil )"2" "2" "2" rewrite "both_sides_expt_lt1_le" )"2" "x=1" )"1" (grind) nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "x ^ (5+4*n) > 0" )"1" "aa" "x^(5+4*n)" )"1" nil nil ))nil )"2" "2" rewrite "expt_pos" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))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 )"real" atan_approx nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" sigma "reals/" )"posint" nil )"odd_int" integers nil )"even_int" integersnil )"real" reals nil )"real" reals nil )nil booleans nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[nat -> real]" atan nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )nil exponentiation nil )"real" reals nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" exponentiation nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil exponentiation nil )nil real_props nil )"real" exponentiation nil )nil real_props nil )"odd_int" integersnil )"even_int" integersnil )"posint" nil )"posnat" exponentiation nil )"posint" exponentiation nil )"[T, T -> boolean]" equalities nil )nil real_props nil )"posrat" nil )nil real_props nil )nil real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil exponentiation nil )"odd_int" integers nil )"real" reals nil )"bool" integers nil )"rat" atan nil )"nzrat" rationalsnil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" atan nil ))nil 3295292840"" (skosimp)"" (expand "atan_pos_le1_lb" )"" (expand "atan_pos_le1_ub" )"" (case "FORALL (n:posnat): 0 < x!1^n/n" )"1" case "FORALL (n,m:posnat): n < m => x!1^m/m < x!1^n/n" )"1" "atan_series_n(x!1, 1 + 2 * n!1) < atan(x!1)" )"1" (lemma "atan_series" ("x" "x!1" "n" "1+2*n!1" ))"1" (rewrite "abs_expt" -1 :dir rl)"1" (expand "abs" -1)"1" (assert )"1" (expand "atan_series_n" )"1" (expand "sigma" -1)"1" "UB" "sigma(0, 2 * n!1, atan_series_term(x!1))" )"1" (hide -2)"1" expand "atan_series_term" )"1" expand "atan_series_coef" )"1" "not_even_m1_pow" "i" "1+2*n!1" ))"1" "1" replace -1)"1" "3+4*n!1" "5+4*n!1" )"1" (assert ) nil nil ))nil ))nil )"2" "2" expand "even?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "atan_series" ("x" "x!1" "n" "2+2*n!1" ))"2" (rewrite "abs_expt" -1 :dir rl)"2" (expand "abs" )"2" (assert )"2" (expand "atan_series_n" )"2" (expand "sigma" -1)"2" "LB" "sigma(0, 1 + 2 * n!1, atan_series_term(x!1))" )"2" expand "atan_series_term" )"2" expand "atan_series_coef" )"2" "even_m1_pow" "i" "2+2*n!1" ))"2" "1" replace -1)"1" "1" "5 + 4 * n!1" "7 + 4 * n!1" )"1" assert )"1" "7 + 4 * n!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "even?" )"2" "n!1+1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (case-replace "x!1=1" )"1" (rewrite "expt_1i" )"1" (rewrite "expt_1i" )"1" (lemma "both_sides_div_pos_lt2" )"1" (inst - "m!1" "n!2" "1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" "both_sides_expt_lt1_lt" "lt1x" "x!1" "i" "m!1" "j" "n!2" ))"1" (assert )"1" "lt_div_lt_pos1" "px" "x!1 ^ m!1" "y" "x!1 ^ n!2" "pz" "n!2" "w" "m!1" ))"1" (assert ) nil nil )"2" (lemma "expt_pos" ("px" "x!1" "i" "m!1" ))"2" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (lemma "expt_pos" ("px" "x!1" "i" "n!2" ))"1" (rewrite "div_mult_pos_lt2" )"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" atan_approx nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )nil real_props nil )"posint" exponentiation nil )nil exponentiation nil )nil exponentiation nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil exponentiation nil )"real_abs_lt_pi2" atan nil )nil atan nil )"posreal" atan nil )nil real_types nil )nil real_types nil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" atan nil )nil naturalnumbers nil )"odd_int" integers nil )"posint" nil )nil reals nil )nil exponentiation nil )"odd_int" integers nil )"(total_order?[real])" nil )"nnreal" nil )"posint" nil )"nzreal" real_typesnil )"(strict_total_order?[real])" real_props nil )"nnreal" exponentiation nil )"real" sigma "reals/" )"int" exponentiation nil )"nzreal" exponentiation nil )"nzrat" rationalsnil )"rat" atan nil )"odd_int" integers nil )"bool" integers nil )nil exponentiation nil )"real" reals nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )nil sigma "reals/" )nil sigma "reals/" )"[nat -> real]" atan nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil atan nil )"real" reals nil )"even_int" integersnil )"posrat" nil )"real" reals nil )"posint" nil )nil exponentiation nil )"[bool, bool -> bool]" booleans nil )nil real_props nil )"real" atan_approx nil ))nil 3403980230"" case "FORALL (n: nat, px: posreal): ") "1" case "FORALL (n: nat,pn:posnat, px: posreal): ") "1" (skosimp)"1" (inst - "n!1" "m!1-n!1" "px!1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (induct "pn" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (skosimp*)"3" (case-replace "j!1=0" )"1" (assert )"1" (hide -1 -2 -3)"1" (inst - "n!1" "px!1" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert )"2" (inst - "n!1" "px!1" )"2" (assert )"2" (inst - "j!1+n!1" "px!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "atan_pos_le1_lb" )"2" (expand "atan_series_n" )"2" (expand "sigma" 1 2)"2" (expand "sigma" 1 2)"2" "SUM" "sigma(0, 1 + 2 * n!1, atan_series_term(px!1))" )"2" (expand "atan_series_term" )"2" (expand "atan_series_coef" )"2" (expand "^" )"2" (expand "expt" 1 3)"2" (expand "expt" 1 3)"2" (expand "expt" 1 4)"2" "expt((-1), 2 + 2 * n!1)=1" )"1" "expt(px!1, 5 + 4 * n!1)" )"1" "1" "PX" "expt(px!1, 5 + 4 * n!1)" )"1" "posreal_times_posreal_is_posreal" "px" "PX" "py" "1 / (5 + 4 * n!1)-sq(px!1)/(7 + 4 * n!1)" ))"1" expand "sq" )"1" (assert ) nil nil ))nil )"2" "2" "div_mult_pos_lt1" "py" "7+4*n!1" "z" "sq(px!1)" "x" "1/(5+4*n!1)" ))"2" "sq_nz_pos" "nz" "px!1" ))"2" "div_mult_pos_lt2" "py" "5 + 4 * n!1" "z" "7 + 4 * n!1" "x" "1" ))"2" "sq_le" "nna" "px!1" "nnb" "1" ))"2" rewrite "sq_1" )"2" assert )"2" "LHS" "sq(px!1) / (7 + 4 * n!1)" )"2" "RHS" "1 / (5 + 4 * n!1)" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "expt_times" "n0x" "-1" "i" "2" "j" "1+n!1" ))"2" expand "^" -1 1)"2" expand "^" -1 1)"2" replace -1)"2" "2" expand "expt" )"2" expand "expt" )"2" expand "expt" )"2" rewrite "sq_rew" )"2" rewrite "sq_neg" )"2" assert )"2" rewrite "sq_1" )"2" rewrite "expt_1i" )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 )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" sigma "reals/" )"[nat -> real]" atan nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"odd_int" integers nil )"real" reals nil )"int" exponentiation nil )"nzrat" rationalsnil )"rat" atan nil )"nzreal" nil )"real" exponentiation nil )"odd_int" integers nil )"nzint" integersnil )nil exponentiation nil )"posint" exponentiation nil )nil exponentiation nil )NOT const-decl "[bool -> bool]" booleans nil )"odd_int" integers nil )"posreal" nil )"posrat" nil )nil sq "reals/" )nil reals nil )nil sq "reals/" )"nonneg_rat" nil )"posrat" nil )"posint" nil )nil rationals nil )nil rationals nil )nil sq "reals/" )nil real_props nil )nil real_props nil )"nprat" rationalsnil )"posreal" sq "reals/" )"posreal" nil )"nonneg_real" sq "reals/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil real_types nil )"real" reals nil )"even_int" integersnil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"real" atan nil )nil integers nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" atan_approx nil )"nat" atan_approx nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )nil defined_types nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"posint" nil )"odd_int" integers nil )"posint" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"real" atan_approx nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil )nil 3403980073 ("" (postpone) nil nil ) nil nil 3403980306"" case "FORALL (n: nat, px: posreal): ") "1" case "FORALL (n: nat,pn:posnat, px: posreal): ") "1" (skosimp)"1" (inst - "n!1" "m!1-n!1" "px!1" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (induct "pn" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (skosimp*)"3" (case-replace "j!1=0" )"1" (assert )"1" (hide -1 -2 -3)"1" (inst - "n!1" "px!1" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert )"2" (inst - "n!1" "px!1" )"2" (assert )"2" (inst - "j!1+n!1" "px!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp)"2" (expand "atan_pos_le1_ub" )"2" (expand "atan_series_n" )"2" (expand "sigma" 1 2)"2" (expand "sigma" 1 2)"2" "SUM" "sigma(0, 2 * n!1, atan_series_term(px!1))" )"2" (move-terms 1 l)"2" (assert )"2" (expand "atan_series_term" )"2" (expand "atan_series_coef" )"2" (expand "^" )"2" (expand "expt" 1 3)"2" expand "expt" 1 3)"2" expand "expt" 1 4)"2" "expt((-1), 1 + 2 * n!1)= -1" )"1" "1" "expt(px!1, 3 + 4 * n!1)" )"1" "1" case "5 > 3 * (px!1 * px!1)" )"1" case "4 * n!1 >= 4 * (n!1 * px!1 * px!1)" )"1" assert )"1" nil nil ))nil )"2" "2" "n!1" )"2" "4" )"2" rewrite "sq" "2" "sq_le" )"2" "2" rewrite "sq_1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sq" :dir rl)"2" "sq_le" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "not_even_m1_pow" )"2" "1+2*n!1" )"2" "1" expand "^" -1 1)"1" (propax) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" sigma "reals/" )"[nat -> real]" atan nil )"[numfield, numfield -> numfield]" number_fields nil )nil sigma "reals/" )nil sigma "reals/" )OR const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"int" exponentiation nil )"nzrat" rationalsnil )"rat" atan nil )"nzreal" nil )"real" exponentiation nil )"odd_int" integers nil )"nzint" integersnil )"bool" integers nil )nil exponentiation nil )nil real_props nil )nil real_props nil )nil real_props nil )"posint" nil )"real" reals nil )"nat" atan_approx nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )"rat" rationals nil )"nonneg_real" sq "reals/" )"posreal" sq "reals/" )nil sq "reals/" )nil sq "reals/" )"posrat" nil )nil integers nil )nil extra_tegies nil )nil extra_tegies nil )nil extra_tegies nil )"nzrat" rationals nil )"posrat" nil )"nnreal" nil )"posreal" nil )nil extra_real_propsnil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" reals nil )"nnreal" nil )"posreal" nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )"odd_int" integers nil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"int" exponentiation nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"odd_int" integers nil )"even_int" integersnil )"real" reals nil )"[bool, bool -> bool]" booleans nil )"real" atan nil )nil integers nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" atan_approx nil )"nat" atan_approx nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nonneg_int" nil )nil defined_types nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"posint" nil )"odd_int" integers nil )"posint" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"real" atan_approx nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))nil 3392596237"" (skeep)"" (expand "pi_lbn" :assert ? none)"" (div-by 1 "4" )"" (lemma "atan_pos_le1_lb_lt" )"" (inst?)"" (lemma "atan_pos_le1_ub_lt" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"real" atan_approx nil )nil atan_approx nil )nil atan_approx nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"posint" nil )"(total_order?[real])" nil )nil reals nil )nil extra_real_props nil )"real" reals nil )"posint" nil )"posrat" nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"real" atan_approx nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" atan_approx nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"real" reals nil ))nil 3404043396"" (skeep)"" (case "forall(i,n:nat):pi_lbn(n) < pi_lbn(n+1+i)" )"1" (inst -1 "k-n-1" "n" ) (("1" (assert ) nil nil )) nil )"2" (hide 2)"2" (induct "i" )"1" (skosimp)"1" (assert ) (("1" (rewrite "pi_lbn_lt" ) nil nil )) nil ))nil )"2" (skeep)"2" (skosimp)"2" (inst -1 "n!1+1" )"2" (lemma "pi_lbn_lt" )"2" (inst -1 "n!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" atan_approx nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posint" nil )"posint" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil integers nil )"int" integers nil )"(total_order?[real])" nil )nil defined_types nil )nil naturalnumbers nil )nil atan_approx nil ))nil ))"closer bounds" 3307959333"" (skosimp)"" (expand "pi_lbn" )"" (expand "pi_ubn" )"" (lemma "atan_1" )"" (lemma "atan_pos_le1_bounds" ("x" "1/5" "n" "n!1" ))"" (lemma "atan_pos_le1_bounds" ("x" "1/239" "n" "n!1" ))"" (assert )"" (flatten)"" (rewrite "pi_value" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"real" atan_approx nil )nil atan nil )nil atan nil )"real" reals nil )"nzreal" real_typesnil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"posrat" nil )nil atan_approx nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" atan_approx nil ))nil 3307959315"" (skosimp)"" (expand "pi_lbn" )"" (expand "pi_ubn" )"" (lemma "atan_1" )"" (lemma "atan_pos_le1_bounds" ("x" "1/5" "n" "n!1" ))"" (lemma "atan_pos_le1_bounds" ("x" "1/239" "n" "n!1" ))"" (assert )"" (flatten)"" (expand "pi" )"" (assert ) nil ))))))))))))))))))nil )"posreal" atan nil )nil atan nil ))nil )nil 3295296628"" (skosimp)"" (expand "pi_lb" )"" (expand "pi_ub" )"" (lemma "atan_1" )"" (lemma "atan_pos_le1_bounds" ("x" "1/5" "n" "n!1" ))"" (lemma "atan_pos_le1_bounds" ("x" "1/239" "n" "n!1" ))"" (assert )"" (flatten)"" (expand "pi" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil atan nil )"posreal" atan nil ))nil 3392568685"" (skeep)"" (case "pi_lbn(n) > 0" )"1" (assert ) nil nil )"2" (hide 2)"2" (case "pi_lbn(0) > 0" )"1" (lemma "pi_lbn_LT" )"1" (inst -1 "0" "n" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil )"2" (hide 2) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"real" atan_approx nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nat" atan_approx nil )nil integers nil )"(strict_total_order?[real])" real_props nil )nil atan_approx nil )"real" exponentiation nil )"real" exponentiation nil )"rat" atan nil )"[nat -> real]" atan nil )"real" sigma "reals/" )"real" atan nil )"real" atan_approx nil )"real" atan_approx nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )"int" exponentiation nil )"nzreal" exponentiation nil )"odd_int" integers nil )"nzreal" exponentiation nil )"int" exponentiation nil )"nzrat" rationalsnil )"posrat" nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"rat" rationals nil )"real" reals nil )"posrat" nil )"real" reals nil )"real" reals nil ))nil ))nil 3392568935"" (skeep)"" (case "pi_ubn(n) > 0" )"1" (assert ) nil nil )"2" (hide 2)"2" (lemma "pi_bounds" )"2" (inst?)"2" (flatten)"2" (lemma "pi_lb_pos" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" atan_approx nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil atan_approx nil )"(strict_total_order?[real])" real_props nil )"posreal" atan_approx nil )nil atan_approx nil ))nil ))nil 3403980370 ("" (grind) nil nil )"real" atan_approx nil )"posreal" atan_approx nil )"real" exponentiation nil )"real" exponentiation nil )"rat" atan nil )"[nat -> real]" atan nil )"real" sigma "reals/" )"real" atan nil )"real" atan_approx nil )"real" atan_approx nil )"real" atan_approx nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )"int" exponentiation nil )"nzreal" exponentiation nil )"odd_int" integers nil )"nzreal" exponentiation nil )"int" exponentiation nil )"nzrat" rationalsnil )"posrat" nil )"(total_order?[real])" nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"rat" rationals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"posrat" nil )"real" reals nil )"real" reals nil )"posreal" atan_approx nil ))nil 3295359235 ("" (grind) nil nil )"posreal" atan_approx nil )"real" atan_approx nil )"posreal" atan_approx nil )"real" exponentiation nil )"real" exponentiation nil )"rat" atan nil )"[nat -> real]" atan nil )"real" sigma "reals/" )"real" atan nil )"real" atan_approx nil )"real" atan_approx nil )"real" atan_approx nil )"posreal" atan_approx nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nzint" integersnil )"int" exponentiation nil )"nzreal" exponentiation nil )"odd_int" integers nil )"nzreal" exponentiation nil )"int" exponentiation nil )"nzrat" rationalsnil )"posrat" nil )"(total_order?[real])" nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"rat" rationals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"posrat" nil )"real" reals nil )"real" reals nil )"posreal" atan_approx nil )"(strict_total_order?[real])" real_props nil ))nil 3307959374"" (lemma "pi_bounds2" )"" (flatten)"" (lemma "pi_bounds" )"" (inst?) (("" (flatten) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"posreal" atan_approx nil )"posreal" atan_approx nil )"(strict_total_order?[real])" real_props nil )nil atan_approx nil )nil atan_approx nil ))nil )nil 3307959056 ("" (judgement-tcc) nil nil ) nil nil ))nil 3403980535"" (skosimp)"" (expand "pi_lbn" )"" "atan_pos_le1_ub_dec" "n" "n!1" "m" "m!1" "px" "1/239" ))"" "atan_pos_le1_lb_inc" "n" "n!1" "m" "m!1" "px" "1/5" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil )"real" atan_approx nil )nil atan_approx nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil )"(total_order?[real])" nil )"posrat" nil )nil atan_approx nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil ))nil ))nil 3403980556"" (skosimp)"" (expand "pi_ubn" )"" (assert )"" "atan_pos_le1_lb_inc" "px" "1/239" "n" "n!1" "m" "m!1" ))"" "atan_pos_le1_ub_dec" "px" "1/5" "n" "n!1" "m" "m!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"real" atan_approx nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil atan_approx nil )"posrat" nil )"(total_order?[real])" nil )nil atan_approx nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"real" reals nil ))nil ))nil 3295358904 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3295360144"" (skosimp)"" (expand "atan_pos_lb" )"" (expand "atan_pos_ub" )"" (case-replace "x!1<=1" )"1" (lemma "atan_pos_le1_bounds" ("x" "x!1" "n" "n!1" ))"1" (assert ) nil nil )) nil )"2" (assert )"2" (lemma "atan_inv" ("px" "x!1" ))"2" (lemma "pi_bounds" ("n" "n!1" ))"2" "atan_pos_le1_bounds" ("x" "1/x!1" "n" "n!1" ))"2" (rewrite "div_mult_pos_lt2" -1)"2" (rewrite "div_mult_pos_le1" -1)"2" (flatten)"2" (assert )"2" (expand "max" )"2" (lift-if)"2" assert )"2" "2" assert )"2" "1" expand "atan_pos_le1_lb" )"1" "atan_strict_increasing" )"1" expand "strict_increasing?" )"1" "1" "x!1" )"1" assert )"1" assert )"1" case "%1 <= %2" )"1" assert )nil nil )"2" "2" "atan_pos_le1_bounds" )"2" expand "atan_pos_le1_lb" )"2" "n!1" "1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" atan_approx nil )"posreal" nil )"real" atan_approx nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )"nzreal" real_typesnil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil atan_approx nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )nil atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_props nil )nil atan nil )"real" atan nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"posreal" atan nil )nil atan nil )"real_abs_lt_pi2" atan nil )"posint" nil )"odd_int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"bool" real_fun_preds "reals/" )"real" atan_approx nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"real" reals nil )nil real_props nil )nil atan_approx nil )"real" reals nil )"nzreal" nil )"real" atan_approx nil )"posreal" atan_approx nil ))nil 3295360690 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3295360690 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3295360768"" (skosimp)"" (expand "atan_lb" )"" (expand "atan_ub" )"" (case-replace "x!1>0" )"1" (lemma "atan_pos_bounds" ("n" "n!1" "x" "x!1" ))"1" (assert )"1" (flatten) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (case-replace "x!1=0" )"1" (rewrite "atan_0" ) (("1" (assert ) nil nil )) nil )"2" (lemma "atan_pos_bounds" ("n" "n!1" "x" "-x!1" ))"2" (assert )"2" (rewrite "atan_neg" )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" atan_approx nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )"nzreal" real_typesnil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil atan_approx nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"real" reals nil )nil atan nil )nil atan nil )"[T, T -> boolean]" equalities nil )"real" atan_approx nil ))nil 3559564948"" (skeep)"" (expand "increasing?" )"" (skolem 1 ("xx" "yy" ))"" (flatten)"" (expand "atan_lb" )"" (assert )"" (expand "atan_pos_lb" )"" (expand "atan_pos_le1_ub" )"" (expand "atan_pos_le1_lb" )"" (expand "atan_pos_ub" )"" (expand "atan_pos_le1_ub" )"" (expand "atan_pos_le1_lb" )"" (lift-if)"" (lift-if)"" "" "" "" "" assert )"" "1" "atan_series_n_increasing" )"1" "1" (assert ) nil nil ))nil ))nil )"2" "atan_series_n_increasing" )"2" "1+2*n" "xx" "1" )"2" (assert ) nil nil ))nil ))nil )"3" "atan_series_n_increasing" )"3" "2*n" "1/yy" "1/xx" )"1" "1" expand "max" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil )"4" "atan_series_n_increasing" )"4" "1+2*n" "xx" "yy" )"4" assert )"4" replace -4)"4" rewrite "atan_series_n_a0" )nil nil ))nil ))nil ))nil ))nil )"5" "atan_series_n_increasing" )"5" "1+2*n" "xx" "1" )"5" assert )"5" replace -3)"5" rewrite "atan_series_n_a0" )"5" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"6" "atan_series_n_increasing" )"6" "2*n" "0" "-xx" )"6" "1+2*n" "0" "yy" )"6" assert )"6" rewrite "atan_series_n_a0" )"6" rewrite "atan_series_n_a0" )"6" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" "atan_series_n_increasing" )"7" "2*n" "0" "-xx" )"7" "1+2*n" "0" "1" )"7" assert )"7" rewrite "atan_series_n_a0" )"7" rewrite "atan_series_n_a0" )"7" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"8" "atan_series_n_increasing" )"8" "2*n" "0" "-xx" )"8" assert )"8" rewrite "atan_series_n_a0" )"8" assert )nil nil ))nil ))nil ))nil ))nil )"9" "atan_series_n_increasing" )"9" "2*n" "-yy" "-xx" )"9" (assert ) nil nil ))nil ))nil )"10" case "%1 >= %2 AND %3 >= 0" )"1" "1" (assert ) nil nil ))nil )"2" "2" "1" "atan_series_n_increasing" )"1" "1+2*n" "1/(-xx)" "1" )"1" assert )"1" "1" "atan_bounds" )"1" "1+2*n" "1" )"1" "1" expand "atan_lb" "1" expand "atan_pos_lb" )"1" expand "atan_pos_le1_lb" )"1" case "%1 <= %2" )"1" assert )nil nil )"2" "2" "atan_bounds" )"2" "n" "1" )"2" "2" case "NOT atan(1) = pi/4" )"1" "1" expand "pi" )"1" expand "atan" )"1" assert )nil nil ))nil ))nil ))nil )"2" expand "atan_lb" )"2" expand "atan_pos_lb" )"2" expand "atan_pos_le1_lb" )"2" case "atan(1) <= pi/2" )"1" assert )"1" "pi_bounds" )"1" "n" )"1" "1" assert )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 )"2" nil nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" "atan_series_n_increasing" )"2" "1+2*n" "0" "yy" )"2" assert )"2" rewrite "atan_series_n_a0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"11" case "%1 >= 0 AND %2 >= 0" )"1" "1" (assert ) nil nil ))nil )"2" "2" "1" assert )"1" "atan_series_n_increasing" )"1" "2*n" "0" "1" )"1" assert )"1" rewrite "atan_series_n_a0" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "atan_series_n_increasing" )"2" "1+2*n" "0" "1" )"2" assert )"2" rewrite "atan_series_n_a0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"12" "atan_series_n_increasing" )"12" "1+2*n" "1/(-xx)" "1" )"1" assert )"1" "1" "atan_bounds" )"1" "n" "1" )"1" expand "atan_lb" )"1" expand "atan_pos_lb" )"1" expand "atan_pos_le1_lb" )"1" "1" "pi_bounds" )"1" "n" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil ))nil ))nil )"13" "atan_series_n_increasing" )"13" "2*n" "-yy" "1" )"13" (assert ) nil nil ))nil ))nil )"14" "14" "atan_series_n_increasing" )"14" "1+2*n" "1/-xx" "1/-yy" )"1" "1" expand "max" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_fun_preds "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" atan_approx nil )"real" reals nil )"posreal" atan_approx nil )"real" atan_approx nil )"real" reals nil )"nzreal" nil )"posint" nil )"odd_int" integers nil )"(total_order?[real])" nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil atan nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" atan_approx nil )"real" atan_approx nil )nil real_props nil )nil real_props nil )"real" reals nil )"real" reals nil )nil real_props nil )nil reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil atan nil )"[numfield -> numfield]" number_fields nil )nil atan_approx nil )"bool" reals nil )"nzreal" real_typesnil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )nil atan_approx nil )"real_abs_lt_pi2" atan nil )nil atan nil )"posreal" atan nil ) (< const-decl "bool" reals nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )"real" atan nil )"real" atan_approx nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil real_types nil )nil real_types nil )nil real_props nil )"odd_int" integers nil )nil extra_tegies nil )nil extra_tegies nil )nil extra_tegies nil )"real" atan_approx nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" atan_approx nil )"posreal" nil )"posreal" atan_approx nil )"real" atan_approx nil ))nil 3559667287"" (skeep)"" (expand "increasing?" )"" (skolem 1 ("xx" "yy" ))"" (flatten)"" (expand "atan_ub" )"" (assert )"" (expand "atan_pos_ub" )"" (expand "atan_pos_le1_ub" )"" (expand "atan_pos_le1_lb" )"" (expand "atan_pos_lb" )"" (expand "atan_pos_le1_ub" )"" (expand "atan_pos_le1_lb" )"" (lift-if)"" (lift-if)"" "" "" "" "" assert )"" "1" "atan_series_n_increasing" )"1" "1" (assert ) nil nil ))nil ))nil )"2" "atan_series_n_increasing" )"2" "2*n" "xx" "1" )"2" (assert ) nil nil ))nil ))nil )"3" "atan_series_n_increasing" )"3" "1+2*n" "1/yy" "1/xx" )"1" "1" expand "max" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil )"4" "atan_series_n_increasing" )"4" "2*n" "xx" "yy" )"4" assert )"4" replace -4)"4" rewrite "atan_series_n_a0" )nil nil ))nil ))nil ))nil ))nil )"5" "atan_series_n_increasing" )"5" "2*n" "xx" "1" )"5" assert )"5" replace -3)"5" rewrite "atan_series_n_a0" )"5" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"6" "atan_series_n_increasing" )"6" "1+2*n" "0" "-xx" )"6" "2*n" "0" "yy" )"6" assert )"6" rewrite "atan_series_n_a0" )"6" rewrite "atan_series_n_a0" )"6" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"7" "atan_series_n_increasing" )"7" "1+2*n" "0" "-xx" )"7" "2*n" "0" "1" )"7" assert )"7" rewrite "atan_series_n_a0" )"7" rewrite "atan_series_n_a0" )"7" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"8" "atan_series_n_increasing" )"8" "1+2*n" "0" "-xx" )"8" assert )"8" rewrite "atan_series_n_a0" )"8" assert )nil nil ))nil ))nil ))nil ))nil )"9" "atan_series_n_increasing" )"9" "1+2*n" "-yy" "-xx" )"9" (assert ) nil nil ))nil ))nil )"10" case "%1 >=0 AND %2 >= 0" )"1" "1" (assert ) nil nil ))nil )"2" "2" "1" "atan_series_n_increasing" )"1" "1+2*n" "0" "1" )"1" assert )"1" rewrite "atan_series_n_a0" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "atan_series_n_increasing" )"2" "2*n" "0" "yy" )"2" assert )"2" rewrite "atan_series_n_a0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"11" case "%1 >= 0 AND %2 >= 0" )"1" "1" (assert ) nil nil ))nil )"2" "2" "1" assert )"1" "atan_series_n_increasing" )"1" "1+2*n" "0" "1" )"1" assert )"1" rewrite "atan_series_n_a0" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "atan_series_n_increasing" )"2" "2*n" "0" "1" )"2" assert )"2" rewrite "atan_series_n_a0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"12" "atan_series_n_increasing" )"12" "1+2*n" "0" "1" )"12" assert )"12" rewrite "atan_series_n_a0" )"12" assert )nil nil ))nil ))nil ))nil ))nil )"13" "atan_series_n_increasing" )"13" "1+2*n" "-yy" "1" )"13" (assert ) nil nil ))nil ))nil )"14" "14" "atan_series_n_increasing" )"14" "2*n" "1/-xx" "1/-yy" )"1" "1" expand "max" )"1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil )"2" nil nil )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_fun_preds "reals/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" atan_approx nil )"real" reals nil )"posreal" atan_approx nil )"real" atan_approx nil )"posint" nil )"odd_int" integers nil )"real" reals nil )"nzreal" nil )"(total_order?[real])" nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil atan nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" atan_approx nil )"real" atan_approx nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )nil real_props nil )"real" reals nil )"real" reals nil )nil real_props nil )nil reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil atan nil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" atan nil )"real" atan_approx nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_props nil )"odd_int" integers nil )"nzreal" real_typesnil )nil extra_tegies nil )nil extra_tegies nil )nil extra_tegies nil )NOT const-decl "[bool -> bool]" booleans nil )"real" atan_approx nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" atan_approx nil )"posreal" nil )"posreal" atan_approx nil )"real" atan_approx nil ))nil ))nil 3403980658"" (skosimp)"" (expand "atan_pos_lb" )"" (case-replace "px!1 <= 1" )"1" "atan_pos_le1_lb_inc" "px" "px!1" "n" "n!1" "m" "m!1" ))"1" (assert ) nil nil )) nil )"2" (assert )"2" (case "1<px!1" )"1" (hide 1)"1" "div_mult_pos_lt1" "py" "px!1" "z" "1" "x" "1" ))"1" (assert )"1" "atan_pos_le1_ub_dec" "px" "1/px!1" "n" "n!1" "m" "m!1" ))"1" (assert )"1" (lemma "pi_lb_inc" ("n" "n!1" "m" "m!1" ))"1" (assert )"1" (lemma "atan_pos_le1_lb_inc" )"1" (inst - "m!1" "n!1" "1" )"1" assert )"1" expand "max" )"1" "1" "1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"posreal" atan_approx nil )"posreal" nil )"real" atan_approx nil )"real" reals nil )"posreal" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil atan_approx nil )nil atan_approx nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_props nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil atan_approx nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil ) (<= const-decl "bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3403980715"" (skosimp)"" (expand "atan_pos_ub" )"" (case-replace "px!1 <= 1" )"1" "atan_pos_le1_ub_dec" "px" "px!1" "n" "n!1" "m" "m!1" ))"1" (assert ) nil nil )) nil )"2" (assert )"2" (case "1<px!1" )"1" (hide 1)"1" "div_mult_pos_lt1" "py" "px!1" "z" "1" "x" "1" ))"1" (assert )"1" "atan_pos_le1_lb_inc" "px" "1/px!1" "n" "n!1" "m" "m!1" ))"1" (assert )"1" (lemma "pi_ub_dec" ("n" "n!1" "m" "m!1" ))"1" (lemma "atan_pos_le1_ub_dec" )"1" (inst - "m!1" "n!1" "1" )"1" (assert )"1" expand "max" )"1" "1" "1" "1" (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 )"posreal" atan_approx nil )"posreal" nil )"real" atan_approx nil )"real" reals nil )"posreal" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil atan_approx nil )nil atan_approx nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil real_props nil )"bool" reals nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil atan_approx nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil ) (<= const-decl "bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3403980748"" (skosimp)"" (expand "pi_lbn" )"" (rewrite "pi_value" )"" (rewrite "atan_1" )"" (lemma "atan_pos_le1_bounds" ("x" "1/5" "n" "n!1" ))"" (lemma "atan_pos_le1_bounds" ("x" "1/239" "n" "n!1" ))"" (assert )"" (flatten)"" (hide -1 -4)"" (expand "atan_pos_le1_ub" )"" (expand "atan_pos_le1_lb" )"" "atan_series" "x" "1/5" "n" "2*n!1+1" ))"" (expand "abs" -1 1)"" (assert )"" "atan_series" "x" "1/239" "n" "2*n!1" ))"" expand "abs" -1 1)"" "expt_pos" "px" "1/5" "i" "5+4*n!1" ))"" "posreal_div_posreal_is_posreal" "px" "(1 / 5) ^ (5 + 4 * n!1)" "py" "5 + 4 * n!1" ))"" expand "abs" -4)"" "expt_pos" "px" "1/239" "i" "3+4*n!1" ))"" "posreal_div_posreal_is_posreal" "px" "(1 / 239) ^ (3 + 4 * n!1)" "py" "3 + 4 * n!1" ))"" expand "abs" -5)"" (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 )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"posint" nil )"odd_int" integers nil )"posrat" nil )"real" atan_approx nil )nil atan nil )"real" atan_approx nil )"posint" nil )"odd_int" integers nil )nil atan nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{r: posrat | r >= q}" nil )nil real_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil exponentiation nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" atan_approx nil )"(total_order?[real])" nil )"real" reals nil )"posrat" nil )"(strict_total_order?[real])" real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil atan_approx nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"nzreal" real_typesnil )"posrat" nil )"even_int" integers nil )"nzint" integers nil )"real" reals nil )"real" reals nil )nil atan nil ))nil ))nil 3403980777"" (skosimp)"" (expand "pi_ubn" )"" (rewrite "pi_value" )"" (rewrite "atan_1" )"" (lemma "atan_pos_le1_bounds" ("x" "1/5" "n" "n!1" ))"" (lemma "atan_pos_le1_bounds" ("x" "1/239" "n" "n!1" ))"" (assert )"" (flatten)"" (hide -2 -3)"" (expand "atan_pos_le1_ub" )"" (expand "atan_pos_le1_lb" )"" "atan_series" "x" "1/239" "n" "2*n!1+1" ))"" (expand "abs" -1 1)"" (assert )"" "atan_series" "x" "1/5" "n" "2*n!1" ))"" expand "abs" -1 1)"" "expt_pos" "px" "1/239" "i" "5+4*n!1" ))"" "posreal_div_posreal_is_posreal" "px" "(1 / 239) ^ (5 + 4 * n!1)" "py" "5 + 4 * n!1" ))"" expand "abs" -4)"" "expt_pos" "px" "1/5" "i" "3+4*n!1" ))"" "posreal_div_posreal_is_posreal" "px" "(1 / 5) ^ (3 + 4 * n!1)" "py" "3 + 4 * n!1" ))"" expand "abs" -5)"" (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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"posint" nil )"odd_int" integers nil )"posrat" nil )"real" atan_approx nil )nil atan nil )"real" atan_approx nil )"posint" nil )"odd_int" integers nil )nil atan nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{r: posrat | r >= q}" nil )nil real_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil exponentiation nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" atan_approx nil )"(total_order?[real])" nil )"posrat" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil atan_approx nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"nzreal" real_typesnil )"posrat" nil )"real" reals nil )"real" reals nil )nil atan nil ))nil ))nil 3403980807"" (skosimp)"" (expand "pi_lbn" )"" (expand "atan_pos_le1_lb" )"" (expand "atan_pos_le1_ub" )"" (expand "atan_series_n" )"" "SUM1" "sigma(0, 1 + 2 * n!1, atan_series_term(1 / 5))" )"" (replace -1)"" "SUM2" "sigma(0, 2 * n!1, atan_series_term(1 / 239))" )"" (replace -1)"" (expand "sigma" 1)"" (expand "sigma" 1)"" (replace -1)"" (replace -2)"" (assert )"" expand "atan_series_term" )"" expand "atan_series_coef" )"" "" "expt_times" "n0x" "-1" "i" "2" "j" "n!1+1" ))"" expand "^" -1 2)"" expand "expt" -1)"" expand "expt" -1)"" expand "expt" -1)"" rewrite "sq_rew" )"" rewrite "sq_neg" )"" rewrite "expt_1i" )"" replace -1)"" assert )"" "expt_plus" "n0x" "-1" "i" "2+2*n!1" "j" "1" ))"" replace "" rewrite "expt_x1" )"" replace "" "expt_plus" "n0x" "-1" "i" "1" "j" "2*n!1" ))"" rewrite "expt_x1" )"" "expt_times" "n0x" "-1" "i" "2" "j" "n!1" ))"" expand "^" "" expand "expt" "" expand "expt" "" expand "expt" "" rewrite "sq_rew" )"" rewrite "sq_neg" )"" rewrite "expt_1i" )"" replace "" replace "" "" "expt_plus" "n0x" "1/5" "i" "2" "j" "5+4*n!1" ))"" "expt_plus" "n0x" "1/239" "i" "2" "j" "3+4*n!1" ))"" expand "^" "" expand "^" "" expand "expt" )"" expand "expt" )"" expand "expt" )"" replace "" replace "" "" assert )"" "DRL1" "(1 / 239) ^ (3 + 4 * n!1)" )"" "DRL2" "(1 / 5) ^ (5 + 4 * n!1)" )"" assert )"" "16 * ((1 / 5 * (1 / 5) * (-1 / (7 + 4 * n!1))) * DRL2) = -16*(DRL2 * (1 / (175 + 100 * n!1)))" )"1" "1" assert )"1" "-4 * (DRL1 * (-1 / (3 + 4 * n!1))) = 4 * (DRL1 * (1 / (3 + 4 * n!1)))" )"1" "1" assert )"1" assert )"1" "both_sides_times1" "n0z" "DRL1" "x" "-4 * ((1 / 239 * (1 / 239) * (1 / (5 + 4 * n!1))))" "y" "-4*(1 / (285605 + 228484 * n!1))" ))"1" replace "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "both_sides_times1" "n0z" "DRL2" "x" "16 * ((1 / 5 * (1 / 5) * (-1 / (7 + 4 * n!1))))" "y" "-16 *(1 / (175 + 100 * n!1))" ))"2" replace "2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posint" nil )"odd_int" integers nil )"posrat" nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"posrat" nil )"real" atan_approx nil )"real" atan_approx nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[nat -> real]" atan nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"int" exponentiation nil )"nzreal" exponentiation nil )"nzrat" rationalsnil )"nzrat" rationalsnil )"rat" atan nil )"posint" nil )"odd_int" integers nil )nil exponentiation nil )nil reals nil )"[numfield -> numfield]" number_fields nil )"real" exponentiation nil )nil exponentiation nil )nil exponentiation nil )"odd_int" integers nil )nil rationals nil )"bool" reals nil )nil rationals nil )nil real_props nil )nil reals nil )"nzint" integers nil )"even_int" integers nil )"nprat" rationalsnil )"posrat" exponentiation nil )"even_int" integersnil )"odd_int" integersnil )"odd_int" integers nil )"rat" rationals nil )nil exponentiation nil )"real" exponentiation nil )"rat" rationals nil )"rat" rationals nil )"posrat" nil )"even_int" integersnil )"real" reals nil )"real" reals nil )"real" reals nil )"real" atan nil )"real" atan_approx nil ))nil ))nil 3555079683"" (skeep)"" (invoke (name "K1" "%1" ) (! 1 2))"" (replaces -1)"" (expand "pi_ubn" )"" (expand "atan_pos_le1_lb" )"" (expand "atan_pos_le1_ub" )"" (expand "atan_series_n" )"" (expand "sigma" + 1)"" (expand "sigma" + 1)"" (expand "sigma" + 2)"" (expand "sigma" + 2)"" (expand "atan_series_term" )"" (expand "atan_series_coef" )"" case "FORALL (nn:nat): (-1)^(2*nn+1) = -1 AND (-1)^(2*nn)=1" )"1" "n+1" )"1" "1" assert )"1" "1" "1" "n" )"1" "1" "1" "1" assert )"1" expand "K1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "nn" )"1" (grind) nil nil )"2" (grind) nil nil )"3" "3" expand "^" )"3" expand "expt" +)"3" expand "expt" +)"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posrat" nil )"posint" nil )"odd_int" integers nil )"rat" rationals nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"bool" reals nil )"real" exponentiation nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil naturalnumbers nil )nil rationals nil )"real" atan_approx nil )"real" atan_approx nil )"real" sigma "reals/" )"rat" rationals nil )"[nat -> real]" atan nil )"odd_int" integers nil )"posint" nil )"odd_int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"rat" atan_approx nil )"posint" nil )"even_int" integersnil )nil defined_types nil )nil naturalnumbers nil )"nzreal" exponentiation nil )"int" exponentiation nil )"(total_order?[real])" nil )"nzint" integersnil )"real" exponentiation nil )"rat" atan nil )"nzrat" rationalsnil )"nzrat" rationalsnil )"nzreal" exponentiation nil )"int" exponentiation nil )"real" atan nil )"real" atan_approx nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"posrat" nil )"rat" rationals nil )"posreal" atan_approx nil ))nil ))nil 3552315150"" (skeep)"" (skoletin 1)"" (label "xdiffname" -1)"" (rewrite "pi_lb_diff" )"" (name "A1" "(1/5)^(4*n+5)" )"" (name "A2" "(1/239)^(4*n+3)" )"" (replace -2)"" (replace -1)"" (name "B1" "1/(4*n+5)" )"" (replace -1)"" (name "B2" "1/(4*n+3)" )"" (replace -1)"" (name "C1" "1/(25*(4*n+7))" )"" (replace -1)"" "C2" "1/(57121*(4*n+5))" )"" replace -1)"" "D1" "B1-C1" )"" "D2" "B2-C2" )"" case "A1 > 0 AND A2 > 0 AND B1 > 0 AND B2 > 0 AND C1 > 0 AND C2 > 0 AND B1 > 0 AND B2 > 0 AND A1 > 0 AND A2 > 0 AND D1 > 0 AND D2 > 0" )"1" "tps" -1)"1" "tps" )"1" case "NOT xdiff = 16*A1*D1 + 4*A2*D2" )"1" assert )"1" "1" "1" "1" "1" "1" "1" "1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" "xdiffname" )"2" "2" "tps" )"2" "2" "1" case "16*A1*D1 > 14 * (1 / 5) ^ (5 * n + 5) AND 4*A2*D2 > 0" )"1" nil nil )"2" "2" "1" case "A1*D1 > (1 / 5) ^ (5 * n + 5)" )"1" assert )nil nil )"2" "2" case "D1 > (1/5)^n" )"1" "A1" )"1" expand "A1" "1" rewrite "expt_plus" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" expand "D1" )"2" expand "B1" "2" expand "C1" "2" rewrite "div_expt" )"2" case "1^n=1" )"1" replace "1" case "(1/2)*(1/(5+4*n)) > 1/5^n AND 1 / (175 + 100 * n) < (1/2)*(1/(5+4*n))" )"1" "1" assert )nil nil ))nil )"2" "2" "1" "1" case "FORALL (nk:nat): 5^(nk+5) > 10+8*(nk+5)" )"1" "n-5" )"1" assert )nil nil )"2" assert )nil nil ))nil )"2" "nk" )"1" assert )"1" "1" nil nil ))nil ))nil )"2" "2" assert )"2" expand "^" )"2" expand "expt" "2" "5" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "FORALL (nk:nat): 1^nk = 1" )"1" nil nil )"2" "nk" )"1" "1" nil nil ))nil )"2" "2" expand "^" )"2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "posreal_times_posreal_is_posreal" )"2" "A2" "D2" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "A2*D2 < (1 / 5) ^ (3 + 4 * n) AND A1*D1 < (1/25)*(1 / 5) ^ (3 + 4 * n)" )"1" "1" assert )nil nil ))nil )"2" "2" "1" expand "D2" "1" "posreal_times_posreal_is_posreal" )"1" "A2" "C2" )"1" case "A2*B2 < (1 / 5) ^ (3 + 4 * n)" )"1" assert )nil nil )"2" "2" case "A2 < (1 / 5) ^ (3 + 4 * n)" )"1" case "B2 < 1" )"1" "1" assert )nil nil ))nil )"2" "2" expand "B2" "2" nil nil ))nil ))nil ))nil )"2" "2" expand "A2" "2" rewrite "div_expt" )"2" rewrite "div_expt" )"2" case "1^(3+4*n) = 1" )"1" "1" "1" "both_sides_expt_pos_lt_aux" )"1" "2+4*n" "1" "5" "239" )"1" expand "^" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (nk:nat): 1^nk = 1" )"1" nil nil )"2" "2" "nk" )"1" expand "^" )"1" expand "expt" )"1" nil nil ))nil ))nil )"2" "2" expand "^" )"2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "A1 <= (1/25) * (1 / 5) ^ (3 + 4 * n) AND D1 < 1" )"1" "1" "1" assert )nil nil ))nil ))nil )"2" "2" "1" expand "A1" "1" expand "^" )"1" expand "expt" "1" expand "expt" "1" assert )nil nil ))nil ))nil ))nil ))nil )"2" case "B1 < 1" )"1" assert )nil nil )"2" "2" expand "B1" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "A1" +)"1" rewrite "expt_pos" )nil nil ))nil )"2" expand "A2" +)"2" rewrite "expt_pos" )nil nil ))nil )"3" expand "B1" +)"3" nil nil ))nil )"4" expand "B2" +)"4" nil nil ))nil )"5" expand "C1" +)"5" nil nil ))nil )"6" expand "C2" +)"6" nil nil ))nil )"7" expand "B1" +)"7" nil nil ))nil )"8" expand "B2" +)"8" nil nil ))nil )"9" expand "A1" +)"9" nil nil ))nil )"10" expand "A2" +)"10" rewrite "expt_pos" )nil nil ))nil )"11" case "B1 > C1" )"1" (assert ) nil nil )"2" expand "B1" +)"2" expand "C1" +)"2" nil nil ))nil ))nil ))nil )"12" case "B2 > C2" )"1" (assert ) nil nil )"2" expand "B2" +)"2" expand "C2" +)"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans nil )"posreal" atan_approx nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"real" atan_approx nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"posint" nil )"posrat" nil )"posrat" nil )"odd_int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"even_int" integersnil )"nnrat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )nil atan_approx nil )"posrat" exponentiation nil )"odd_int" integers nil )"posint" nil )"odd_int" integers nil )"posint" nil )"rat" rationals nil )"rat" rationals nil )"rat" rationals nil )"posrat" atan_approx nil )nil exponentiation nil )NOT const-decl "[bool -> bool]" booleans nil )"odd_int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"posrat" atan_approx nil )nil exponentiation nil )nil reals nil )nil real_types nil )nil real_types nil )nil real_props nil )"rat" atan_approx nil )"posrat" atan_approx nil )"int" integers nil )"nat" atan_approx nil )"int" integers nil )"real" exponentiation nil )"posnat" exponentiation nil )nil naturalnumbers nil )nil defined_types nil )"even_int" integersnil )nil extra_real_props nil )"even_int" integersnil )nil real_props nil )nil extra_real_props nil )nil reals nil )nil real_props nil )nil real_props nil )nil real_props nil )"posint" exponentiation nil )nil exponentiation nil )"posrat" atan_approx nil )"(strict_total_order?[real])" real_props nil )"posrat" atan_approx nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil extra_real_props nil )"posrat" atan_approx nil )nil exponentiation nil )"rat" atan_approx nil )"posrat" exponentiation nil )"(total_order?[real])" nil )"bool" reals nil )nil rationals nil )"posrat" nil )nil rationals nil )"bool" reals nil )nil rationals nil ))nil 3554119553"" case "NOT FORALL (nb6:below(6)): LET xquot = pi_lbn(nb6) / pi_lbn(nb6 + 1) IN AND xquot <= 1") "1" (hide 2) (("1" (eval-formula) nil nil )) nil )"2" (skeep)"2" (case "NOT n>5" )"1" (inst - "n" ) (("1" (assert ) nil nil )) nil )"2" (hide -2)"2" (skoletin 1)"2" (name "xdiff" "pi_lbn(n+1)-pi_lbn(n)" )"2" (case "NOT xquot = 1 - xdiff/pi_lbn(n+1)" )"1" (assert )"1" (replace -2)"1" (replace -1 :dir rl) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (case "xquot <= 1" )"1" (assert )"1" case "xdiff/pi_lbn(n+1) <= 14.5 * (1 / 5) ^ (3 + 4 * n)" )"1" (assert ) nil nil )"2" (hide 2)"2" (lemma "pi_lb_diff_bounds" )"2" (inst?)"2" (assert )"2" replace -4)"2" "2" case "25/8 <= pi_lbn(1+n)" )"1" "1" "1" (assert ) nil nil ))nil ))nil )"2" "2" case "FORALL (kk:nat): 25/8 <= pi_lbn(kk)" )"1" (inst?) nil nil )"2" "2" "kk" )"1" nil nil )"2" "2" "pi_lb_inc" )"2" "j+1" "j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "pi_lb_inc" )"2" (inst - "n+1" "n" )"2" (assert )"2" (expand "xquot" 1)"2" (cross-mult 1) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"odd_int" integers nil )nil atan_approx nil )"(total_order?[real])" nil )nil atan_approx nil )nil naturalnumbers nil )nil defined_types nil )nil real_props nil )nil reals nil )nil real_props nil )"posreal" nil )nil real_props nil )"real" reals nil )nil extra_real_props nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"odd_int" integers nil )"posreal" atan_approx nil )"posrat" exponentiation nil )"(total_order?[real])" nil )"real" reals nil )"posint" nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nnrat" exponentiation nil )"posrat" nil )"[T, T -> boolean]" equalities nil )"[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"nat" atan_approx nil )"(strict_total_order?[real])" real_props nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )"posreal" nil )"posint" nil )"posreal" atan_approx nil )"posrat" nil )"odd_int" integers nil )"rat" rationals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" reals nil )nil naturalnumbers nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"real" atan_approx nil ))nil 3566172731"" (skeep)"" (skoletin 1)"" (label "xdiffname" -1)"" (rewrite "pi_ub_diff" )"" (case "(1/5)^(5+4*n) = (1/25)*(1/5)^(3+4*n)" )"1" (replaces -1)"1" (assert )"1" case "(1/239)^(7+4*n) = (1/239^2)*(1/239)^(5+4*n)" )"1" (replaces -1)"1" (assert )"1" (invoke (name "K1" "%1" ) (! -1 2 1))"1" (invoke (name "K2" "%1" ) (! -2 2 2))"1" (invoke (name "K3" "%1" ) (! -3 2 3))"1" (invoke (name "K4" "%1" ) (! -4 2 4))"1" replace -1)"1" replace -2)"1" replace -3)"1" replace -4)"1" case "K1/2 >= 32 * (1 / 5) ^ (3 + 5 * n)" )"1" case "K2 < K1" )"1" case "2*K1 < (7/5) * (1 / 5) ^ (3 + 4 * n)" )"1" assert )"1" case "K4 < K2/2" )"1" case "K3 < K1/2" )"1" assert )"1" case "K1 > 0 AND K2 > 0 AND K4 > 0 AND K3 > 0" )"1" "1" case "K1 + K2 - K4 - K3 >= K1/2" )"1" case "K1 + K2 - K4 - K3 < 2*K1" )"1" assert )"1" replace "xdiffname" "1" assert )"1" "^" )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )"2" "2" "2" expand "K1" )"2" expand "K3" )"2" case "1/(5+4*n) < 1/(3+4*n)" )"1" case "16 * ((1 / 5) ^ (3 + 4 * n) * (1 / 25)) < ") "1" "1" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "K4" )"2" expand "K2" )"2" case "1/(7+4*n) < 1/(5+4*n)" )"1" case "4 * ((1 / 239) ^ (5 + 4 * n) * (1 / 239 ^ 2)) < ") "1" "1" assert )nil nil ))nil )"2" assert )"2" expand "^" "2" expand "expt" "2" expand "expt" "2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" expand "K1" )"2" case "1/(3+4*n) <= 1/23" )"1" "(1/5)^(3+4*n)" )"1" assert )nil nil ))nil )"2" "2" case "EXISTS (kk:nat): n = kk+5" )"1" "1" "1" nil nil ))nil ))nil )"2" "n-5" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "K1" )"2" expand "K2" )"2" case "(1/239)^(4*n+5) < (1/5)^(3+4*n) AND 1/(5+4*n) < 1/(3+4*n)" )"1" "1" "1" assert )nil nil ))nil ))nil )"2" "2" "1" "both_sides_expt_pos_lt_aux" )"1" "2+4*n" "1/239" "1/5" )"1" assert )"1" expand "^" )"1" expand "expt" "1" expand "expt" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "K1" )"2" assert )"2" "expt_plus" )"2" "3+4*n" "n" "1/5" )"2" assert )"2" replace -1)"2" case "(1/(3+4*n)) > 4*(1/5)^n" )"1" "8 * (((1 / 5) ^ (3 + 4 * n)))" )"1" assert )nil nil ))nil )"2" "2" case "FORALL (kk:nat): 1/(3+4*(kk+5)) > 4*(1/5)^(kk+5)" )"1" "n-5" )"1" assert )nil nil ))nil )"2" "2" "kk" )"1" assert )"1" nil nil ))nil )"2" "2" expand "^" )"2" expand "expt" "2" assert )"2" case "(23+4*j)/(27+4*j) > 4/5" )"1" "1" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (lemma "expt_plus" )"2" (inst - "2" "5+4*n" "1/239" )"2" (assert )"2" (replaces -1)"2" (rewrite "div_expt" )"2" rewrite "div_expt" )"2" assert )"2" case "1^2 = 1" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (lemma "expt_plus" )"2" (inst - "3+4*n" "2" "1/5" )"2" (assert )"2" (replaces -1)"2" (rewrite "div_expt" )"2" (rewrite "div_expt" )"2" (case "FORALL (kk:nat): 1^kk = 1" )"1" (inst?)"1" "1" case "1^2 = 1" )"1" "1" assert )"1" case "5^2 = 25" )"1" "1" (assert ) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "kk" )"1" (grind) nil nil )"2" "2" expand "^" )"2" expand "expt" 1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans nil )"posreal" atan_approx nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"real" atan_approx nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"posint" nil )"posrat" nil )"posrat" nil )"odd_int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"even_int" integersnil )"nnrat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )nil atan_approx nil )"posrat" exponentiation nil )"odd_int" integers nil )"posint" nil )"rat" rationals nil )"rat" rationals nil )"posrat" nil )"posint" exponentiation nil )nil reals nil )nil extra_real_props nil )"nonneg_rat" nil )nil extra_real_props nil )nil naturalnumbers nil )nil defined_types nil )"nzrat" rationalsnil )nil real_props nil )nil exponentiation nil )"bool" reals nil )"(total_order?[real])" nil )nil extra_real_propsnil )nil real_props nil )nil real_props nil )"int" integers nil )"int" integers nil )"posrat" atan_approx nil )"real" exponentiation nil )"posrat" atan_approx nil )"(strict_total_order?[real])" real_props nil )"posrat" atan_approx nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil extra_real_props nil )nil real_types nil )nil real_types nil )nil reals nil )nil real_props nil )"odd_int" integers nil )"posint" nil )nil real_props nil )nil real_props nil )"posrat" atan_approx nil )"even_int" integersnil )"posrat" exponentiation nil )nil exponentiation nil )"odd_int" integers nil )nil rationals nil )"bool" reals nil )nil rationals nil )nil exponentiation nil )"posnat" exponentiation nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil )nil 3566172669"" (skeep)"" (skoletin 1)"" (label "xdiffname" -1)"" (rewrite "pi_ub_diff" )"" (case "(1/5)^(5+4*n) = (1/25)*(1/5)^(3+4*n)" )"1" (replaces -1)"1" (assert )"1" case "(1/239)^(7+4*n) = (1/239^2)*(1/239)^(5+4*n)" )"1" (replaces -1)"1" (assert )"1" (invoke (name "K1" "%1" ) (! -1 2 1))"1" (invoke (name "K2" "%1" ) (! -2 2 2))"1" (invoke (name "K4" "%1" ) (! -3 2 3))"1" (invoke (name "K3" "%1" ) (! -4 2 4))"1" replace -1)"1" replace -2)"1" replace -3)"1" replace -4)"1" case "K1/2 >= 32 * (1 / 5) ^ (3 + 5 * n)" )"1" case "K2 < K1" )"1" case "2*K1 < (7/5) * (1 / 5) ^ (3 + 4 * n)" )"1" assert )"1" case "K3 < K2/2" )"1" case "K4 < K1/2" )"1" assert )"1" case "K1 > 0 AND K2 > 0 AND K3 > 0 AND K4 > 0" )"1" "1" case "K1 + K2 - K3 - K4 >= K1/2" )"1" case "K1 + K2 - K3 - K4 < 2*K1" )"1" assert )"1" replace "xdiffname" "1" assert )"1" "^" )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )"2" "2" "2" expand "K1" )"2" expand "K4" )"2" case "1/(5+4*n) < 1/(3+4*n)" )"1" case "16 * ((1 / 5) ^ (3 + 4 * n) * (1 / 25)) < ") "1" "1" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "K3" )"2" expand "K2" )"2" case "1/(7+4*n) < 1/(5+4*n)" )"1" case "4 * ((1 / 239) ^ (5 + 4 * n) * (1 / 239 ^ 2)) < ") "1" "1" assert )nil nil ))nil )"2" assert )"2" expand "^" "2" expand "expt" "2" expand "expt" "2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" expand "K1" )"2" case "1/(3+4*n) <= 1/23" )"1" "(1/5)^(3+4*n)" )"1" assert )nil nil ))nil )"2" "2" case "EXISTS (kk:nat): n = kk+5" )"1" "1" "1" nil nil ))nil ))nil )"2" "n-5" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "K1" )"2" expand "K2" )"2" case "(1/239)^(4*n+5) < (1/5)^(3+4*n) AND 1/(5+4*n) < 1/(3+4*n)" )"1" "1" "1" assert )nil nil ))nil ))nil )"2" "2" "1" "both_sides_expt_pos_lt_aux" )"1" "2+4*n" "1/239" "1/5" )"1" assert )"1" expand "^" )"1" expand "expt" "1" expand "expt" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "K1" )"2" assert )"2" "expt_plus" )"2" "3+4*n" "n" "1/5" )"2" assert )"2" replace -1)"2" case "(1/(3+4*n)) > 4*(1/5)^n" )"1" "8 * (((1 / 5) ^ (3 + 4 * n)))" )"1" assert )nil nil ))nil )"2" "2" case "FORALL (kk:nat): 1/(3+4*(kk+5)) > 4*(1/5)^(kk+5)" )"1" "n-5" )"1" assert )nil nil ))nil )"2" "2" "kk" )"1" assert )"1" nil nil ))nil )"2" "2" expand "^" )"2" expand "expt" "2" assert )"2" case "(23+4*j)/(27+4*j) > 4/5" )"1" "1" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (lemma "expt_plus" )"2" (inst - "2" "5+4*n" "1/239" )"2" (assert )"2" (replaces -1)"2" (rewrite "div_expt" )"2" rewrite "div_expt" )"2" assert )"2" case "1^2 = 1" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (lemma "expt_plus" )"2" (inst - "3+4*n" "2" "1/5" )"2" (assert )"2" (replaces -1)"2" (rewrite "div_expt" )"2" (rewrite "div_expt" )"2" (case "FORALL (kk:nat): 1^kk = 1" )"1" (inst?)"1" "1" case "1^2 = 1" )"1" "1" assert )"1" case "5^2 = 25" )"1" "1" (assert ) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "kk" )"1" (grind) nil nil )"2" "2" expand "^" )"2" expand "expt" 1)"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 3555081842"" (skeep)"" (skoletin 1)"" (label "xdiffname" -1)"" (rewrite "pi_ub_diff" )"" (case "(1/5)^(5+4*n) = (1/25)*(1/5)^(3+4*n)" )"1" (replaces -1)"1" (assert )"1" case "(1/239)^(7+4*n) = (1/239^2)*(1/239)^(5+4*n)" )"1" (replaces -1)"1" (assert )"1" (invoke (name "K1" "%1" ) (! -1 2 1))"1" (invoke (name "K2" "%1" ) (! -2 2 2))"1" (invoke (name "K3" "%1" ) (! -3 2 3))"1" (invoke (name "K4" "%1" ) (! -4 2 4))"1" replace -1)"1" replace -2)"1" replace -3)"1" replace -4)"1" case "K1/2 >= 32 * (1 / 5) ^ (3 + 5 * n)" )"1" case "K2 < K1" )"1" case "2*K1 < (7/5) * (1 / 5) ^ (3 + 4 * n)" )"1" assert )"1" case "K3 < K2/2" )"1" case "K4 < K1/2" )"1" assert )"1" case "K1 > 0 AND K2 > 0 AND K3 > 0 AND K4 > 0" )"1" "1" case "K1 + K2 - K3 - K4 >= K1/2" )"1" case "K1 + K2 - K3 - K4 < 2*K1" )"1" assert )"1" replace "xdiffname" "1" assert )"1" "^" )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )"2" "2" "2" expand "K1" )"2" expand "K4" )"2" case "1/(5+4*n) < 1/(3+4*n)" )"1" case "16 * ((1 / 5) ^ (3 + 4 * n) * (1 / 25)) < ") "1" "1" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "K3" )"2" expand "K2" )"2" case "1/(7+4*n) < 1/(5+4*n)" )"1" case "4 * ((1 / 239) ^ (5 + 4 * n) * (1 / 239 ^ 2)) < ") "1" "1" assert )nil nil ))nil )"2" assert )"2" expand "^" "2" expand "expt" "2" expand "expt" "2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" expand "K1" )"2" case "1/(3+4*n) <= 1/23" )"1" "(1/5)^(3+4*n)" )"1" assert )nil nil ))nil )"2" "2" case "EXISTS (kk:nat): n = kk+5" )"1" "1" "1" nil nil ))nil ))nil )"2" "n-5" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "K1" )"2" expand "K2" )"2" case "(1/239)^(4*n+5) < (1/5)^(3+4*n) AND 1/(5+4*n) < 1/(3+4*n)" )"1" "1" "1" assert )nil nil ))nil ))nil )"2" "2" "1" "both_sides_expt_pos_lt_aux" )"1" "2+4*n" "1/239" "1/5" )"1" assert )"1" expand "^" )"1" expand "expt" "1" expand "expt" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "K1" )"2" assert )"2" "expt_plus" )"2" "3+4*n" "n" "1/5" )"2" assert )"2" replace -1)"2" case "(1/(3+4*n)) > 4*(1/5)^n" )"1" "8 * (((1 / 5) ^ (3 + 4 * n)))" )"1" assert )nil nil ))nil )"2" "2" case "FORALL (kk:nat): 1/(3+4*(kk+5)) > 4*(1/5)^(kk+5)" )"1" "n-5" )"1" assert )nil nil ))nil )"2" "2" "kk" )"1" assert )"1" nil nil ))nil )"2" "2" expand "^" )"2" expand "expt" "2" assert )"2" case "(23+4*j)/(27+4*j) > 4/5" )"1" "1" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide (-1 2))"2" (lemma "expt_plus" )"2" (inst - "2" "5+4*n" "1/239" )"2" (assert )"2" (replaces -1)"2" (rewrite "div_expt" )"2" rewrite "div_expt" )"2" assert )"2" case "1^2 = 1" )"1" (assert ) nil nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (lemma "expt_plus" )"2" (inst - "3+4*n" "2" "1/5" )"2" (assert )"2" (replaces -1)"2" (rewrite "div_expt" )"2" (rewrite "div_expt" )"2" (case "FORALL (kk:nat): 1^kk = 1" )"1" (inst?)"1" "1" case "1^2 = 1" )"1" "1" assert )"1" case "5^2 = 25" )"1" "1" (assert ) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "kk" )"1" (grind) nil nil )"2" "2" expand "^" )"2" expand "expt" 1)"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 3565741552"" case "NOT FORALL (nn:subrange(0,15)): LET xquot = pi_ubn(nn + 1) / pi_ubn(nn) IN AND xquot <= 1") "1" (eval-formula) nil nil )"2" (skeep)"2" (case "NOT n>=15" )"1" (inst - "n" ) (("1" (assert ) nil nil )) nil )"2" (hide -2)"2" (lemma "pi_ub_diff_bounds" )"2" (inst - "n" )"2" (split -)"1" (skoletin 1)"1" (skoletin -2 :old? t)"1" (flatten)"1" (split)"1" (mult-by -3 "1/pi_ubn(n)" )"1" (assert )"1" case "NOT xdiff * (1/pi_ubn(n)) = 1 - xquot" )"1" (assert ) nil nil )"2" "2" assert )"2" case "1/pi_ubn(n) < 1/2" )"1" " ((1 / 5) ^ (3 + 4 * n))" )"1" (assert ) nil nil ))nil )"2" case "FORALL (nn:nat): pi_ubn(nn+15) > 2" )"1" "n-15" )"1" assert )"1" nil nil ))nil ))nil )"2" "2" case "FORALL (nn:nat): pi_lbn(nn+15) > 2" )"1" "1" "nn" )"1" "pi_bounds" )"1" "nn+15" )"1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "nn" )"1" assert )"1" nil nil ))nil )"2" "2" assert )"2" "pi_lb_inc" )"2" "16+j" "15+j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "xquot" +)"2" (cross-mult 1)"2" (lemma "pi_ub_dec" )"2" "1+n" "n" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"posrat" exponentiation nil )"posrat" nil )"nnrat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"posreal" atan_approx nil )nil atan_approx nil )nil real_props nil )nil real_props nil )"odd_int" integers nil )"posint" nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil reals nil )nil real_props nil )"even_int" integersnil )"posint" nil )nil real_props nil )nil real_props nil )"int" integers nil )"real" atan_approx nil )"posreal" atan_approx nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )nil atan_approx nil )nil defined_types nil )nil naturalnumbers nil )nil atan_approx nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posreal" nil )"bool" reals nil )"real" reals nil )nil atan_approx nil )"(total_order?[real])" nil )"nat" atan_approx nil )"(total_order?[real])" nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )"posreal" nil )"posint" nil )"posreal" atan_approx nil )"posrat" nil )"odd_int" integers nil )"rat" rationals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )nil naturalnumbers nil )"real" atan_approx nil ))nil )nil 3565741534"" case "NOT FORALL (nn:subrange(0,15)): LET xquot = pi_ubn(nn + 1) / pi_ubn(nn) IN AND xquot <= 1") "1" (eval-formula) nil )"2" (skeep)"2" (case "NOT n>=15" )"1" (inst - "n" ) (("1" (assert ) nil )))"2" (hide -2)"2" (lemma "pi_ub_diff_bounds" )"2" (inst - "n" )"2" (split -)"1" (skoletin 1)"1" (skoletin -2)"1" (flatten)"1" (split)"1" (mult-by -3 "1/pi_ubn(n)" )"1" (assert )"1" case "NOT xdiff * (1/pi_ubn(n)) = 1 - xquot" )"1" (assert ) nil )"2" "2" assert )"2" case "1/pi_ubn(n) < 1/2" )"1" " ((1 / 5) ^ (3 + 4 * n))" )"1" (assert ) nil )))"2" case "FORALL (nn:nat): pi_ubn(nn+15) > 2" )"1" "n-15" )"1" assert )"1" (cross-mult 1) nil )))))"2" "2" case "FORALL (nn:nat): pi_lbn(nn+15) > 2" )"1" "1" "nn" )"1" "pi_bounds" )"1" "nn+15" )"1" assert )"1" nil )))))))))))"2" "2" "nn" )"1" assert )"1" nil )))"2" "2" assert )"2" "pi_lb_inc" )"2" "16+j" "15+j" )"2" assert )nil )))))))))))))))))))))))))))))))"2" (expand "xquot" +)"2" (cross-mult 1)"2" (lemma "pi_ub_dec" )"2" "1+n" "n" )"2" (assert ) nil )))))))))))))))))"2" (assert ) nil ))))))))))))))nil )nil nil )nil 3555152240"" case "NOT FORALL (nn:subrange(0,15)): LET xquot = pi_ubn(nn + 1) / pi_ubn(nn) IN AND xquot <= 1") "1" (eval-formula) nil nil )"2" (skeep)"2" (case "NOT n>=15" )"1" (inst - "n" ) (("1" (assert ) nil nil )) nil )"2" (hide -2)"2" (lemma "pi_ub_diff_bounds" )"2" (inst - "n" )"2" (split -)"1" (skoletin 1)"1" (skoletin -2 :old? t)"1" (flatten)"1" (split)"1" (mult-by -3 "1/pi_ubn(n)" )"1" (assert )"1" case "NOT xdiff * (1/pi_ubn(n)) = 1 - xquot" )"1" (assert ) nil nil )"2" "2" assert )"2" case "1/pi_ubn(n) < 1/2" )"1" " ((1 / 5) ^ (3 + 4 * n))" )"1" (assert ) nil nil ))nil )"2" case "FORALL (nn:nat): pi_ubn(nn+15) > 2" )"1" "n-15" )"1" assert )"1" nil nil ))nil ))nil )"2" "2" case "FORALL (nn:nat): pi_lbn(nn+15) > 2" )"1" "1" "nn" )"1" "pi_bounds" )"1" "nn+15" )"1" assert )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "nn" )"1" assert )"1" nil nil ))nil )"2" "2" assert )"2" "pi_lb_inc" )"2" "16+j" "15+j" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "xquot" +)"2" (cross-mult 1)"2" (lemma "pi_ub_dec" )"2" "1+n" "n" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak)))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.680Bemerkung:
(vorverarbeitet am 2026-05-01)
¤ *Bot Zugriff
2026-05-26
