| products/sources/formale sprachen/PVS/trig/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: taylor_help.pvs Sprache: PVSOriginal von: PVS© |
|
||||||
|
(atan_approx
(atan_pos_le1_ub_lt 0 (atan_pos_le1_ub_lt-1 nil 3408809781 ("" (skeep) (("" (expand "atan_pos_le1_ub") (("" (expand "atan_series_n") (("" (expand "sigma" 1 1) (("" (expand "sigma" 1 1) (("" (move-terms 1 r 1) (("1" (assert) (("1" (expand "atan_series_term") (("1" (expand "atan_series_coef") (("1" (lemma "not_even_m1_pow") (("1" (inst?) (("1" (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) ("2" (skosimp*) (("2" (assert) 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/") (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (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_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) (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (atan_series_n const-decl "real" atan nil)) nil)) (atan_pos_le1_lb_lt 0 (atan_pos_le1_lb_lt-1 nil 3408809815 ("" (skeep) (("" (expand "atan_pos_le1_lb") (("" (expand "atan_series_n") (("" (expand "sigma" 1 2) (("" (expand "sigma" 1 2) (("" (move-terms 1 r 3) (("1" (assert) (("1" (expand "atan_series_term") (("1" (expand "atan_series_coef") (("1" (lemma "not_even_m1_pow") (("1" (inst -1 "3+2*n") (("1" (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) ("2" (skosimp*) (("2" (assert) 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/") (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans 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_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_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) (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (atan_series_n const-decl "real" atan nil)) nil)) (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) ((atan const-decl "real_abs_lt_pi2" atan nil) (atan_series_n const-decl "real" atan nil) (sigma def-decl "real" sigma "reals/") (atan_series_coef const-decl "rat" atan nil) (atan_series_term const-decl "[nat -> real]" atan nil) (atan_series formula-decl nil atan nil)) shostak)) (atan_pos_le1_lb_inc 0 (atan_pos_le1_lb_inc-1 nil 3408809885 ("" (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))") (("1" (expand "atan_series_term") (("1" (expand "atan_series_coef") (("1" (expand "^") (("1" (expand "expt" 1 3) (("1" (expand "expt" 1 3) (("1" (expand "expt" 1 4) (("1" (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" (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) ("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" (rewrite "expt_1i") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((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/") (integer nonempty-type-from-decl nil integers nil) (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) (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/") (nonneg_rat nonempty-type-eq-decl nil rationals nil) (posrat nonempty-type-eq-decl nil rationals nil) (sq_1 formula-decl nil sq "reals/") (posint_times_posint_is_posint application-judgement "posint" integers nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (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_ub_dec 0 (atan_pos_le1_ub_dec-1 nil 3408809912 ("" (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))") (("1" (move-terms 1 l) (("1" (assert) (("1" (expand "atan_series_term") (("1" (expand "atan_series_coef") (("1" (expand "^") (("1" (expand "expt" 1 3) (("1" (expand "expt" 1 3) (("1" (expand "expt" 1 4) (("1" (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) ("2" (skosimp*) (("2" (assert) 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/") (integer nonempty-type-from-decl nil integers nil) (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 3408810052 ("" (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)) nil)) (pi_lbn_LT 0 (pi_lbn_LT-1 nil 3408810072 ("" (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (pi_lbn_lt formula-decl nil atan_approx nil)) nil)) (pi_bounds 0 (pi_bounds-3 "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) (("" (expand "pi") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak) (pi_bounds-2 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) ((atan_1 formula-decl nil atan nil)) nil) (pi_bounds-1 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) ((atan_1 formula-decl nil atan nil)) shostak)) (pi_lb_pos 0 (pi_lb_pos-2 nil 3408810176 ("" (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) ((pi_lbn const-decl "real" atan_approx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (> const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (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) (n skolem-const-decl "nat" atan_approx nil) (above nonempty-type-eq-decl nil integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (pi_lbn_LT formula-decl nil atan_approx nil) (expt def-decl "real" exponentiation nil) (^ const-decl "real" exponentiation nil) (atan_series_coef const-decl "rat" atan nil) (atan_series_term const-decl "[nat -> real]" atan nil) (sigma def-decl "real" sigma "reals/") (atan_series_n const-decl "real" atan nil) (atan_pos_le1_lb const-decl "real" atan_approx nil) (atan_pos_le1_ub const-decl "real" atan_approx nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (int_expt application-judgement "int" exponentiation nil) (nzreal_expt application-judgement "nzreal" exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (int_exp application-judgement "int" exponentiation nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (posrat_expt application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (real_plus_real_is_real application-judgement "real" reals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.221 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.Bot Zugriff |
