| products/sources/formale Sprachen/PVS/exact_real_arith/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: bcclf90.cfg Sprache: LispUntersuchung PVS© |
|
||||||
|
(sincosx
(real_3pi16_TCC1 0 (real_3pi16_TCC1-1 nil 3393563994 ("" (lemma "pi_bnds") (("" (flatten) (("" (assert) nil nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (pi_bnds formula-decl nil atan "trig_fnd/")) nil)) (cauchy_real_3pi16_TCC1 0 (cauchy_real_3pi16_TCC1-1 nil 3393563994 ("" (expand "cauchy_real_3pi16?") (("" (inst + "0") (("1" (expand "cauchy_prop") (("1" (propax) nil nil)) nil) ("2" (lemma "pi_bnds") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (pi const-decl "posreal" atan "trig_fnd/") (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_3pi16 nonempty-type-eq-decl nil sincosx nil) (cauchy_prop const-decl "bool" cauchy nil) (posint_exp application-judgement "posint" exponentiation nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (pi_bnds formula-decl nil atan "trig_fnd/") (cauchy_real_3pi16? const-decl "bool" sincosx nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (cauchy_nnsreal_TCC1 0 (cauchy_nnsreal_TCC1-1 nil 3393747713 ("" (expand "cauchy_nnsreal?") (("" (inst + "0") (("" (expand "cauchy_prop") (("" (propax) nil nil)) nil)) nil)) 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (nnsreal nonempty-type-eq-decl nil sincosx nil) (cauchy_prop const-decl "bool" cauchy nil) (posint_exp application-judgement "posint" exponentiation nil) (cauchy_nnsreal? const-decl "bool" sincosx nil)) nil)) (subtype_TCC1 0 (subtype_TCC1-1 nil 3393563994 ("" (grind) nil nil) nil nil)) (subtype_TCC2 0 (subtype_TCC2-1 nil 3393747713 ("" (skosimp) (("" (typepred "x!1") (("" (expand "cauchy_real?") (("" (expand "cauchy_nnsreal?") (("" (skosimp) (("" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_nnsreal nonempty-type-eq-decl nil sincosx nil) (cauchy_nnsreal? const-decl "bool" sincosx 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) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nnsreal nonempty-type-eq-decl nil sincosx nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (cauchy_real? const-decl "bool" cauchy nil)) nil)) (subtype_TCC3 0 (subtype_TCC3-1 nil 3393747713 ("" (skosimp) (("" (typepred "x!1") (("" (expand "cauchy_real_3pi16?") (("" (expand "cauchy_real?") (("" (skosimp) (("" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_real_3pi16 nonempty-type-eq-decl nil sincosx nil) (cauchy_real_3pi16? const-decl "bool" sincosx 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) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (cauchy_real? const-decl "bool" cauchy nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan "trig_fnd/") (real_3pi16 nonempty-type-eq-decl nil sincosx nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx "trig_fnd/") (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (cauchy_sin_series_TCC1 0 (cauchy_sin_series_TCC1-1 nil 3393414809 ("" (skosimp) (("" (expand "cauchy_nzreal?") (("" (inst + "factorial(1+2*n!1)") (("" (rewrite "int_lemma") nil nil)) nil)) nil)) nil) ((int_times_int_is_int application-judgement "int" integers 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) (cauchy_nzreal? const-decl "bool" cauchy nil) (int_lemma formula-decl nil int nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (factorial def-decl "posnat" factorial "ints/") (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (odd_plus_even_is_odd application-judgement "odd_int" integers nil)) nil)) (cauchy_cos_series_TCC1 0 (cauchy_cos_series_TCC1-1 nil 3393414809 ("" (skosimp) (("" (expand "cauchy_nzreal?") (("" (inst + "factorial(2*n!1)") (("" (rewrite "int_lemma") nil nil)) nil)) nil)) nil) ((cauchy_nzreal? const-decl "bool" cauchy nil) (int_lemma formula-decl nil int nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (factorial def-decl "posnat" factorial "ints/") (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (int_times_int_is_int application-judgement "int" integers 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)) nil)) (sin_series_lemma 0 (sin_series_lemma-1 nil 3393414810 ("" (skosimp) (("" (expand "cauchy_sin_series") (("" (expand "sin_term") (("" (lemma "div_lemma" ("x" "(-1) ^ n!1" "cx" "cauchy_int((-1) ^ n!1)" "nzy" "factorial(1 + 2 * n!1)" "nzcy" "cauchy_int(factorial(1 + 2 * n!1))")) (("" (rewrite "expt_1i") (("" (rewrite "int_lemma") (("" (rewrite "int_lemma") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_sin_series const-decl "cauchy_real" sincosx nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (factorial def-decl "posnat" factorial "ints/") (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (cauchy_int const-decl "cauchy_real" int nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy 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) (div_lemma formula-decl nil div nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (int_exp application-judgement "int" exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (int_lemma formula-decl nil int nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (posint_exp application-judgement "posint" exponentiation nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_times_int_is_int application-judgement "int" integers nil) (expt_1i formula-decl nil exponentiation nil) (sin_term const-decl "real" trig_approx "trig_fnd/")) shostak)) (cos_series_lemma 0 (cos_series_lemma-1 nil 3393414930 ("" (skosimp) (("" (expand "cauchy_cos_series") (("" (expand "cos_term") (("" (rewrite "expt_1i") (("" (case-replace "n!1=0") (("1" (rewrite "expt_x0") (("1" (expand "factorial") (("1" (lemma "div_lemma" ("x" "1" "cx" "cauchy_int(1)" "nzy" "1" "nzcy" "cauchy_int(1)")) (("1" (rewrite "int_lemma") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "div_lemma" ("x" "(-1) ^ n!1" "nzy" "factorial(2 * n!1)" "cx" "cauchy_int((-1) ^ n!1)" "nzcy" "cauchy_int(factorial(2 * n!1))")) (("2" (rewrite "int_lemma") (("2" (rewrite "int_lemma") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_cos_series const-decl "cauchy_real" sincosx nil) (int_times_int_is_int application-judgement "int" integers 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) (expt_1i formula-decl nil exponentiation 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) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_exp application-judgement "int" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (posint_exp application-judgement "posint" exponentiation nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (- const-decl "[numfield -> numfield]" number_fields nil) (expt_x0 formula-decl nil exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (div_lemma formula-decl nil div nil) (cauchy_real? const-decl "bool" cauchy nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_int const-decl "cauchy_real" int nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (int_lemma formula-decl nil int nil) (factorial def-decl "posnat" factorial "ints/") (= const-decl "[T, T -> boolean]" equalities nil) (cos_term const-decl "real" trig_approx "trig_fnd/")) shostak)) (cauchy_sin_drx_TCC1 0 (cauchy_sin_drx_TCC1-1 nil 3393418937 ("" (expand "cauchys_real?") (("" (lemma "sin_series_lemma") (("" (expand "cauchys_prop") (("" (inst + "sin_term(1)") nil nil)) nil)) nil)) nil) ((sin_series_lemma formula-decl nil sincosx 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) (sin_term const-decl "real" trig_approx "trig_fnd/") (cauchys_prop const-decl "bool" sum nil) (cauchys_real? const-decl "bool" sum nil)) nil)) (cauchy_sin_drx_TCC2 0 (cauchy_sin_drx_TCC2-2 nil 3508597737 ("" (skosimp) (("" (typepred "csnx!1") (("" (expand "cauchy_nnsreal?") (("" (skosimp) (("" (typepred "x!1") (("" (expand "cauchy_real?") (("" (expand "<=" -1) (("" (split -1) (("1" (lemma "powerseries_lemma" ("x" "x!1" "cx" "csnx!1" "xs" "sin_term(1)" "cxs" "cauchy_sin_series")) (("1" (replace -4) (("1" (lemma "sin_series_lemma") (("1" (replace -1) (("1" (hide -1) (("1" (inst + "sin(sqrt(x!1))/sqrt(x!1)") (("1" (hide -4) (("1" (expand "cauchy_prop") (("1" (skosimp) (("1" (inst - "2+p!1") (("1" (inst - "2+p!1") (("1" (name-replace "CPS" "cauchy_powerseries(csnx!1, cauchy_sin_series, 2 + p!1)(2 + p!1)") (("1" (flatten) (("1" (expand "powerseries") (("1" (lemma "sin_approx_sin" ("a" "sqrt(x!1)" "n" "2+p!1")) (("1" (expand "sin_approx") (("1" (expand "sin_term" -1 2) (("1" (rewrite "abs_div") (("1" (rewrite "abs_mult") (("1" (expand "abs" -1 4) (("1" (assert) (("1" (typepred "factorial(7 + 2 * p!1)") (("1" (assert) (("1" (hide -1) (("1" (rewrite "abs_expt" -1 :dir rl) (("1" (expand "abs" -1 2) (("1" (rewrite "expt_1i") (("1" (lemma "expt_plus" ("n0x" "sqrt(x!1)" "i" "1" "j" "6+2*p!1")) (("1" (lemma "expt_times" ("n0x" "sqrt(x!1)" "i" "2" "j" "3+p!1")) (("1" (rewrite "expt_x2") (("1" (rewrite "sq_rew") (("1" (replace -1 -2) (("1" (rewrite "expt_x1") (("1" (replace -2 -3) (("1" (expand "abs" -3 2) (("1" (assert) (("1" (hide -1 -2) (("1" (case-replace "sigma(0, 2 + p!1, LAMBDA (i:nat): IF i = 0 THEN sin_term(1)(i) ELSE sin_term(1)(i) * x!1 ^ i ENDIF)=sigma(0, 2 + p!1, sin_term(sqrt(x!1)))/sqrt(x!1)") (("1" (hide -1) (("1" (lemma "div_mult_pos_le1" ("py" "sqrt(x!1)" "x" "x!1 ^ (3 + p!1) / factorial(7 + 2 * p!1)" "z" "abs(sin(sqrt(x!1)) - sigma(0, 2 + p!1, sin_term(sqrt(x!1))))")) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (lemma "abs_div" ("x" "sin(sqrt(x!1)) - sigma(0, 2 + p!1, sin_term(sqrt(x!1)))" "n0y" "sqrt(x!1)")) (("1" (expand "abs" -1 3) (("1" (replace -1 -2 rl) (("1" (assert) (("1" (hide -1) (("1" (rewrite "minus_div2" -1 :dir rl) (("1" (name-replace "SIN_APPROX" "sigma(0, 2 + p!1, sin_term(sqrt(x!1))) / sqrt(x!1)") (("1" (name-replace "SIN_" "sin(sqrt(x!1)) / sqrt(x!1)") (("1" (case "abs(SIN_APPROX-CPS/2 ^ (2 + p!1))<2^-(2+p!1)") (("1" (case "abs(SIN_-CPS / 2 ^ (2 + p!1)) < 2 ^ -(1 + p!1)") (("1" (hide -2 -3 -4 -5) (("1" (expand "round") (("1" (typepred "floor(1 / 2 + CPS / 4)") (("1" (name-replace "RR" "floor(1 / 2 + CPS / 4)") (("1" (rewrite "expt_plus") (("1" (rewrite "expt_x2") (("1" (rewrite "expt_inverse") (("1" (rewrite "expt_plus") (("1" (rewrite "expt_x1") (("1" (name-replace "P2" "2^p!1") (("1" (lemma "div_mult_pos_lt2" ("py" "P2" "z" "1/2" "x" "abs(SIN_ - CPS / (4 * P2))")) (("1" (replace -1 -4) (("1" (hide -1) (("1" (lemma "abs_mult" ("x" "SIN_ - CPS / (4 * P2)" "y" "P2")) (("1" (expand "abs" -1 3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case "x!1 ^ (3 + p!1) / factorial(7 + 2 * p!1) < 2^-(2+p!1)") (("1" (name-replace "DRL1" "x!1 ^ (3 + p!1) / factorial(7 + 2 * p!1)") (("1" (case-replace "2 ^ -(1 + p!1)=2*2 ^ -(2 + p!1)") (("1" (rewrite "expt_inverse" 1) (("1" (name-replace "P2" "2 ^ (2 + p!1)") (("1" (hide-all-but (-2 -3 -4 1)) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "expt_inverse") (("2" (rewrite "expt_inverse") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_plus") (("2" (rewrite "expt_x1") (("2" (rewrite "expt_x2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 -6 1)) (("2" (lemma "both_sides_expt_pos_lt" ("px" "x!1" "py" "1/2" "pm" "3+p!1")) (("2" (assert) (("2" (rewrite "div_mult_pos_lt1") (("2" (lemma "inv_expt") (("2" (inst -1 "3+p!1" "2") (("2" (replaces -1) (("2" (rewrite "expt_inverse" 1) (("2" (name-replace "DRL1" "x!1 ^ (3 + p!1)") (("2" (rewrite "expt_plus") (("2" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.59 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 |
