|
(atan_approx
(atan_pos_le1_ub_lt 0
(atan_pos_le1_ub_lt-1 nil 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"
(inst?)
(("1"
(split -1)
(("1"
(replaces -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"
(hide -1 2)
(("2"
(grind-reals)
(("2"
(rewrite
"both_sides_expt_lt1_le")
(("2"
(case "x=1")
(("1"
(replaces -1)
(("1"
(grind)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(case "x ^ (5+4 *n) > 0")
(("1"
(name-replace
"aa"
"x^(5+4*n)")
(("1"
(grind-reals)
nil
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite "expt_pos")
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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((atan_pos_le1_ub const-decl "real" atan_approx 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)
(sigma def-decl "real" sigma "reals/")
(real_plus_real_is_real application-judgement "real" reals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IFF 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 "[numfield, numfield -> numfield]" number_fields 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)
(atan_series_term const-decl "[nat -> real]" atan nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(- const-decl "[numfield, numfield -> numfield]" number_fields 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)
(not_even_m1_pow formula-decl nil exponentiation nil)
(even_m1_pow formula-decl nil exponentiation nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields 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)
(both_sides_expt_lt1_le formula-decl nil exponentiation nil)
(posint_exp application-judgement "posint" exponentiation nil)
(posnat_expt application-judgement "posnat" exponentiation nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(le_times_le_pos formula-decl nil real_props nil)
(expt def-decl "real" exponentiation nil)
(nonzero_times1 formula-decl nil real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(both_sides_div_pos_le1 formula-decl nil real_props nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(times_div1 formula-decl nil real_props nil)
(lt_div_lt_pos1 formula-decl nil real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(expt_pos formula-decl nil exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(even? const-decl "bool" integers nil)
(atan_series_coef const-decl "rat" atan nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(int_exp application-judgement "int" exponentiation nil)
(atan_series_n const-decl "real" atan nil))
shostak))
(atan_pos_le1_lb_lt 0
(atan_pos_le1_lb_lt-1 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"
(inst?)
(("1"
(split -1)
(("1"
(replaces -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"
(hide -1 2)
(("2"
(grind-reals)
(("2"
(rewrite
"both_sides_expt_lt1_le")
(("2"
(case-replace "x=1")
(("1" (grind) nil nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(case "x ^ (5+4*n) > 0")
(("1"
(name-replace
"aa"
"x^(5+4*n)")
(("1"
(grind-reals)
nil
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite "expt_pos")
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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((atan_pos_le1_lb const-decl "real" atan_approx 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)
(sigma def-decl "real" sigma "reals/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IFF 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)
(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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(atan_series_term const-decl "[nat -> real]" atan nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields 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)
(not_even_m1_pow formula-decl nil exponentiation nil)
(even_m1_pow formula-decl nil exponentiation nil)
(real_div_nzreal_is_real application-judgement "real" reals 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 "real" exponentiation 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)
(both_sides_expt_lt1_le formula-decl nil exponentiation nil)
(nonzero_times1 formula-decl nil real_props nil)
(expt def-decl "real" exponentiation nil)
(le_times_le_pos formula-decl nil real_props nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(posnat_expt application-judgement "posnat" exponentiation nil)
(posint_exp application-judgement "posint" exponentiation nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(both_sides_div_pos_le1 formula-decl nil real_props nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(times_div1 formula-decl nil real_props nil)
(lt_div_lt_pos1 formula-decl nil real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(expt_pos formula-decl nil exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(even? const-decl "bool" integers nil)
(atan_series_coef const-decl "rat" atan nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(int_exp application-judgement "int" exponentiation nil)
(atan_series_n const-decl "real" atan nil))
shostak))
(atan_pos_le1_bounds 0
(atan_pos_le1_bounds-1 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"
(case-replace
"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"
(name-replace "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"
(lemma
"not_even_m1_pow"
("i" "1+2*n!1"))
(("1"
(split -1)
(("1"
(replace -1)
(("1"
(inst - "3+4*n!1" "5+4*n!1")
(("1" (assert) nil nil))
nil))
nil)
("2"
(hide-all-but -1)
(("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"
(name-replace "LB"
"sigma(0, 1 + 2 * n!1, atan_series_term(x!1))")
(("2"
(expand "atan_series_term")
(("2"
(expand "atan_series_coef")
(("2"
(lemma
"even_m1_pow"
("i" "2+2*n!1"))
(("2"
(split -1)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(inst
-
"5 + 4 * n!1"
"7 + 4 * n!1")
(("1"
(assert)
(("1"
(inst-cp
-
"7 + 4 * n!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "even?")
(("2"
(inst + "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"
(lemma "both_sides_expt_lt1_lt"
("lt1x" "x!1" "i" "m!1" "j" "n!2"))
(("1" (assert)
(("1"
(lemma "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)
((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)
(atan_pos_le1_lb const-decl "real" atan_approx 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)
(numfield nonempty-type-eq-decl nil number_fields 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)
(>= 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)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(both_sides_div_pos_lt2 formula-decl nil real_props nil)
(posint_exp application-judgement "posint" exponentiation nil)
(expt_1i formula-decl nil exponentiation nil)
(expt_pos formula-decl nil exponentiation nil)
(lt_div_lt_pos1 formula-decl nil real_props 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)
(both_sides_expt_lt1_lt formula-decl nil exponentiation nil)
(atan const-decl "real_abs_lt_pi2" atan nil)
(real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
(pi const-decl "posreal" atan nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(atan_series_n const-decl "real" atan nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(abs_expt formula-decl nil exponentiation nil)
(even_plus_odd_is_odd application-judgement "odd_int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_exp application-judgement "nnreal" exponentiation nil)
(sigma def-decl "real" sigma "reals/")
(int_exp application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(atan_series_coef const-decl "rat" atan nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(even? const-decl "bool" integers nil)
(not_even_m1_pow formula-decl nil exponentiation nil)
(real_times_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(<= const-decl "bool" reals nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(atan_series_term const-decl "[nat -> real]" atan nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(atan_series formula-decl nil atan nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(minus_real_is_real application-judgement "real" reals nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(even_m1_pow formula-decl nil exponentiation nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(atan_pos_le1_ub const-decl "real" atan_approx nil))
shostak))
(atan_pos_le1_lb_inc 0
(atan_pos_le1_lb_inc-2 nil 3403980230
(""
(case "FORALL (n: nat, px: posreal):
px <= 1 => atan_pos_le1_lb(n, px) < atan_pos_le1_lb(n+1, px)")
(("1"
(case "FORALL (n: nat,pn:posnat, px: posreal):
px <= 1 => atan_pos_le1_lb(n, px) < atan_pos_le1_lb(n+pn, px)")
(("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"
(name-replace "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"
(case-replace
"expt((-1), 2 + 2 * n!1)=1")
(("1"
(typepred "expt(px!1, 5 + 4 * n!1)")
(("1"
(hide -1 -3)
(("1"
(name-replace
"PX"
"expt(px!1, 5 + 4 * n!1)")
(("1"
(lemma
"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"
(hide 2)
(("2"
(lemma
"div_mult_pos_lt1"
("py"
"7+4*n!1"
"z"
"sq(px!1)"
"x"
"1/(5+4*n!1)"))
(("2"
(lemma
"sq_nz_pos"
("nz" "px!1"))
(("2"
(lemma
"div_mult_pos_lt2"
("py"
"5 + 4 * n!1"
"z"
"7 + 4 * n!1"
"x"
"1"))
(("2"
(lemma
"sq_le"
("nna"
"px!1"
"nnb"
"1"))
(("2"
(rewrite "sq_1")
(("2"
(assert)
(("2"
(name-replace
"LHS"
"sq(px!1) / (7 + 4 * n!1)")
(("2"
(name-replace
"RHS"
"1 / (5 + 4 * n!1)")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(lemma
"expt_times"
("n0x" "-1" "i" "2" "j" "1+n!1"))
(("2"
(expand "^" -1 1)
(("2"
(expand "^" -1 1)
(("2"
(replace -1)
(("2"
(hide -1)
(("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)
((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)
(sigma def-decl "real" sigma "reals/")
(atan_series_term const-decl "[nat -> real]" atan nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(int_exp application-judgement "int" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(atan_series_coef const-decl "rat" atan nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(expt def-decl "real" exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(expt_1i formula-decl nil exponentiation nil)
(posint_exp application-judgement "posint" exponentiation nil)
(expt_times formula-decl nil exponentiation nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(odd_times_odd_is_odd application-judgement "odd_int" integers nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(sq_nz_pos judgement-tcc nil sq "reals/")
(nzreal nonempty-type-eq-decl nil reals nil)
(sq_le formula-decl nil sq "reals/")
(nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat"
rationals nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(posrat nonempty-type-eq-decl nil rationals nil)
(nonneg_rat nonempty-type-eq-decl nil rationals nil)
(sq_1 formula-decl nil sq "reals/")
(div_mult_pos_lt2 formula-decl nil real_props nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(nprat_div_posrat_is_nprat application-judgement "nprat" rationals
nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sq const-decl "nonneg_real" sq "reals/")
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(posreal_times_posreal_is_posreal judgement-tcc nil real_types nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(^ const-decl "real" exponentiation nil)
(posreal_expt application-judgement "posreal" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(posreal_exp application-judgement "posreal" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(atan_series_n const-decl "real" atan nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(m!1 skolem-const-decl "nat" atan_approx nil)
(n!1 skolem-const-decl "nat" atan_approx 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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(even_plus_odd_is_odd application-judgement "odd_int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(atan_pos_le1_lb const-decl "real" atan_approx nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
nil)
(atan_pos_le1_lb_inc-1 nil 3403980073 ("" (postpone) nil nil) nil
shostak))
(atan_pos_le1_ub_dec 0
(atan_pos_le1_ub_dec-1 nil 3403980306
(""
(case "FORALL (n: nat, px: posreal):
px <= 1 => atan_pos_le1_ub(n, px) > atan_pos_le1_ub(n+1, px)")
(("1"
(case "FORALL (n: nat,pn:posnat, px: posreal):
px <= 1 => atan_pos_le1_ub(n, px) > atan_pos_le1_ub(n+pn, px)")
(("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"
(name-replace "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"
(case-replace
"expt((-1), 1 + 2 * n!1)= -1")
(("1"
(hide -1)
(("1"
(cancel-by
1
"expt(px!1, 3 + 4 * n!1)")
(("1"
(hide -1 2)
(("1"
(case
"5 > 3 * (px!1 * px!1)")
(("1"
(case
"4 * n!1 >= 4 * (n!1 * px!1 * px!1)")
(("1"
(assert)
(("1"
(grind-reals)
nil
nil))
nil)
("2"
(hide -1 2)
(("2"
(cancel-by 1 "n!1")
(("2"
(cancel-by 2 "4")
(("2"
(rewrite
"sq"
:dir
rl)
(("2"
(lemma "sq_le")
(("2"
(inst?)
(("2"
(rewrite
"sq_1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite "sq" :dir rl)
(("2"
(lemma "sq_le")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(lemma "not_even_m1_pow")
(("2"
(inst -1 "1+2*n!1")
(("2"
(split -1)
(("1"
(expand "^" -1 1)
(("1" (propax) nil nil))
nil)
("2"
(hide 1)
(("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)
((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)
(sigma def-decl "real" sigma "reals/")
(atan_series_term const-decl "[nat -> real]" atan nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(int_exp application-judgement "int" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(atan_series_coef const-decl "rat" atan nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(expt def-decl "real" exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nzint_times_nzint_is_nzint application-judgement "nzint" integers
nil)
(even? const-decl "bool" integers nil)
(not_even_m1_pow formula-decl nil exponentiation nil)
(ge_times_ge_pos formula-decl nil real_props nil)
(minus_div1 formula-decl nil real_props nil)
(neg_div_gt formula-decl nil real_props nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(CBD_2 skolem-const-decl "nat" atan_approx nil)
(both_sides_times_pos_ge1 formula-decl nil real_props nil)
(pos_div_gt formula-decl nil real_props nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(zero_times1 formula-decl nil real_props nil)
(rat_times_rat_is_rat application-judgement "rat" rationals nil)
(sq const-decl "nonneg_real" sq "reals/")
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sq_1 formula-decl nil sq "reals/")
(sq_le formula-decl nil sq "reals/")
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(posint nonempty-type-eq-decl nil integers nil)
(add_neg formula-decl nil extra_tegies nil)
(neg_div formula-decl nil extra_tegies nil)
(zero_div formula-decl nil extra_tegies nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(odd_times_odd_is_odd application-judgement "odd_int" integers nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(^ const-decl "real" exponentiation nil)
(posreal_expt application-judgement "posreal" exponentiation nil)
(nzreal_expt application-judgement "nzreal" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(posreal_exp application-judgement "posreal" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(atan_series_n const-decl "real" atan nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(m!1 skolem-const-decl "nat" atan_approx nil)
(n!1 skolem-const-decl "nat" atan_approx 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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(even_plus_odd_is_odd application-judgement "odd_int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(atan_pos_le1_ub const-decl "real" atan_approx nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
nil))
(pi_lbn_lt 0
(pi_lbn_lt-1 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)
((pi_lbn const-decl "real" atan_approx nil)
(atan_pos_le1_lb_lt formula-decl nil atan_approx nil)
(atan_pos_le1_ub_lt formula-decl nil atan_approx 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_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(times_div_cancel1 formula-decl nil extra_real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields 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)
(atan_pos_le1_lb const-decl "real" atan_approx nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(atan_pos_le1_ub const-decl "real" atan_approx nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(both_sides_div_pos_lt1 formula-decl nil real_props nil)
(real_times_real_is_real application-judgement "real" reals nil))
shostak))
(pi_lbn_LT 0
(pi_lbn_LT-1 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)
((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(pi_lbn const-decl "real" atan_approx nil)
(< const-decl "bool" reals 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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.82 Sekunden
(vorverarbeitet)
¤
|
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 ist noch experimentell.
|
