| products/sources/formale Sprachen/PVS/exact_real_arith/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: log.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(log (cauchy_ln_small_TCC1 0
(cauchy_ln_small_TCC1-1 nil 3394161634 ("" (expand "cauchy_ln_small?") (("" (inst + "0") (("" (rewrite "int_lemma") 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) (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]" number_fields nil) (ln_smallreal nonempty-type-eq-decl nil log nil) (int_lemma formula-decl nil int 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) (cauchy_ln_small? const-decl "bool" log nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (subtype_TCC1 0 (subtype_TCC1-1 nil 3394109924 ("" (skosimp) (("" (typepred "x!1") (("" (expand "cauchy_ln_small?") (("" (skosimp) (("" (expand "cauchy_real?") (("" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_ln_small nonempty-type-eq-decl nil log nil) (cauchy_ln_small? const-decl "bool" log 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) (ln_smallreal nonempty-type-eq-decl nil log nil) (- const-decl "[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) (AND const-decl "[bool, bool -> bool]" booleans nil) (cauchy_real? const-decl "bool" cauchy nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (cauchy_ln_med_TCC1 0 (cauchy_ln_med_TCC1-1 nil 3394161634 ("" (expand "cauchy_ln_med?") (("" (inst + "1") (("" (rewrite "int_lemma") 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) (ln_medreal nonempty-type-eq-decl nil log 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) (int_lemma formula-decl nil int nil) (cauchy_ln_med? const-decl "bool" log nil)) nil)) (subtype_TCC2 0 (subtype_TCC2-1 nil 3394127143 ("" (skosimp) (("" (typepred "x!1") (("" (expand "cauchy_ln_med?") (("" (expand "cauchy_posreal?") (("" (skosimp) (("" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_ln_med nonempty-type-eq-decl nil log nil) (cauchy_ln_med? const-decl "bool" log 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_posreal? const-decl "bool" cauchy nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ln_medreal nonempty-type-eq-decl nil log nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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)) nil)) (cauchy_gt_quarter_TCC1 0 (cauchy_gt_quarter_TCC1-1 nil 3394175254 ("" (expand "cauchy_gt_quarter?") (("" (inst + "1") (("" (rewrite "int_lemma") 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) (< const-decl "bool" reals nil) (posreal_gt_quarter nonempty-type-eq-decl nil log 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) (int_lemma formula-decl nil int nil) (cauchy_gt_quarter? const-decl "bool" log nil)) nil)) (subtype_TCC3 0 (subtype_TCC3-1 nil 3394161634 ("" (skosimp) (("" (typepred "x!1") (("" (expand "cauchy_gt_quarter?") (("" (skosimp) (("" (expand "cauchy_posreal?") (("" (inst + "x!2") nil nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_gt_quarter nonempty-type-eq-decl nil log nil) (cauchy_gt_quarter? const-decl "bool" log 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_gt_quarter nonempty-type-eq-decl nil log nil) (< const-decl "bool" reals 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) (cauchy_posreal? const-decl "bool" cauchy nil)) nil)) (cauchy_ln_series_TCC1 0 (cauchy_ln_series_TCC1-1 nil 3394113740 ("" (skosimp) (("" (expand "cauchy_nzreal?") (("" (inst + "n!1") (("1" (rewrite "int_lemma") nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((cauchy_nzreal? const-decl "bool" cauchy nil) (int_lemma formula-decl nil int nil) (nzreal nonempty-type-eq-decl nil reals nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal 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) (n!1 skolem-const-decl "nat" log nil)) nil)) (cauchy_ln_series_TCC2 0 (cauchy_ln_series_TCC2-1 nil 3394113740 ("" (skosimp) (("" (expand "cauchy_nzreal?") (("" (inst + "n!1") (("1" (rewrite "int_lemma") nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((cauchy_nzreal? const-decl "bool" cauchy nil) (int_lemma formula-decl nil int nil) (nzreal nonempty-type-eq-decl nil reals nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (/= const-decl "boolean" notequal 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) (n!1 skolem-const-decl "nat" log nil)) nil)) (ln_series_lemma_TCC1 0 (ln_series_lemma_TCC1-1 nil 3394113740 ("" (skosimp) (("" (assert) nil nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (ln_series_lemma 0 (ln_series_lemma-1 nil 3394113751 ("" (skosimp) (("" (expand "cauchy_ln_series") (("" (typepred "n!1") (("" (expand ">=") (("" (expand "<=") (("" (split -1) (("1" (assert) (("1" (expand "lnT") (("1" (case "even?(n!1)") (("1" (assert) (("1" (expand "even?") (("1" (skosimp) (("1" (replace -1) (("1" (rewrite "expt_times") (("1" (rewrite "expt_x2") (("1" (rewrite "expt_1i") (("1" (replace -1 * rl) (("1" (hide -1) (("1" (lemma "div_lemma" ("x" "-1" "nzy" "n!1" "cx" "cauchy_int(-1)" "nzcy" "cauchy_int(n!1)")) (("1" (rewrite "int_lemma") (("1" (rewrite "int_lemma") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (rewrite "even_iff_not_odd") (("2" (expand "odd?") (("2" (skosimp) (("2" (replace -1) (("2" (rewrite "expt_plus") (("2" (rewrite "expt_times") (("2" (rewrite "expt_x2") (("2" (rewrite "expt_1i") (("2" (replace -1 * rl) (("2" (hide -1) (("2" (lemma "div_lemma" ("x" "1" "nzy" "n!1" "cx" "cauchy_int(1)" "nzcy" "cauchy_int(n!1)")) (("2" (rewrite "int_lemma") (("2" (rewrite "int_lemma") (("2" (rewrite "expt_x1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (lemma "unique_cauchy_zero" ("x" "0")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cauchy_ln_series const-decl "cauchy_real" log nil) (lnT const-decl "real_gtm1_le1" ln_exp_series_alt "lnexp_fnd/") (mult_divides2 application-judgement "(divides(m))" divides nil) (odd? const-decl "bool" integers nil) (expt_x1 formula-decl nil exponentiation nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (expt_plus formula-decl nil exponentiation nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (even_iff_not_odd formula-decl nil naturalnumbers 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) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (expt_times formula-decl nil exponentiation nil) (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (int_times_int_is_int application-judgement "int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (rat_exp application-judgement "rat" exponentiation nil) (expt_1i formula-decl nil exponentiation nil) (int_lemma formula-decl nil int nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nzreal? const-decl "bool" cauchy 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) (div_lemma formula-decl nil div nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (expt_x2 formula-decl nil inv nil) (even? const-decl "bool" integers 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) (unique_cauchy_zero formula-decl nil cauchy nil) (<= const-decl "bool" reals nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (ln_estimate_lemma_TCC1 0 (ln_estimate_lemma_TCC1-1 nil 3394115362 ("" (skosimp) (("" (expand "cauchys_real?") (("" (lemma "ln_series_lemma") (("" (inst + "lambda n:IF n = 0 THEN 0 ELSE lnT(1)(n - 1) ENDIF") (("1" (expand "cauchys_prop") (("1" (propax) nil nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((cauchys_real? const-decl "bool" sum nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (IF const-decl "[boolean, T, T -> T]" if_def nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (real_gtm1_le1 nonempty-type-eq-decl nil ln_exp_series_alt "lnexp_fnd/") (lnT const-decl "real_gtm1_le1" ln_exp_series_alt "lnexp_fnd/") (cauchys_prop const-decl "bool" sum nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (ln_series_lemma formula-decl nil log nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (ln_estimate_lemma 0 (ln_estimate_lemma-1 nil 3394115371 ("" (skosimp) (("" (expand "ln_estimate") (("" (lemma "powerseries_lemma" ("x" "ssx!1" "cx" "cssx!1" "xs" "LAMBDA n: IF n = 0 THEN 0 ELSE lnT(1)(n-1) ENDIF" "cxs" "cauchy_ln_series" "m" "n!1")) (("1" (expand "powerseries") (("1" (replace -2) (("1" (lemma "ln_series_lemma") (("1" (replace -1) (("1" (hide -1) (("1" (name-replace "CPS" "cauchy_powerseries(cssx!1, cauchy_ln_series, n!1)") (("1" (expand "lnT") (("1" (case-replace "(LAMBDA (i:nat): IF i = 0 THEN 0 ELSE -(-1) ^ i / i * ssx!1 ^ i ENDIF)=(LAMBDA (nn: nat): IF nn = 0 THEN 0 ELSE -(-ssx!1) ^ nn / nn ENDIF)") (("1" (hide-all-but 1) (("1" (apply-extensionality :hide? t) (("1" (case-replace "x!1=0") (("1" (assert) (("1" (case-replace "(-ssx!1) ^ x!1 = (-1) ^ x!1* ssx!1 ^ x!1") (("1" (assert) nil nil) ("2" (hide 3) (("2" (case-replace "ssx!1=0") (("1" (expand "^") (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "mult_expt" ("n0x" "-1" "n0y" "ssx!1" "i" "x!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) nil nil)) nil)) nil) ("2" (skosimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((ln_estimate const-decl "real" ln_exp_series_alt "lnexp_fnd/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (powerseries const-decl "real" powerseries nil) (ln_series_lemma formula-decl nil log nil) (expt def-decl "real" exponentiation nil) (int_times_int_is_int application-judgement "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) (minus_even_is_even application-judgement "even_int" integers nil) (int_expt application-judgement "int" exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (mult_expt formula-decl nil exponentiation nil) (int_exp application-judgement "int" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (cauchys_real? const-decl "bool" sum nil) (cauchys_real nonempty-type-eq-decl nil sum nil) (cauchy_powerseries const-decl "cauchy_real" powerseries nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (powerseries_lemma formula-decl nil powerseries 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) (cauchy_real? const-decl "bool" cauchy nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_ln_small? const-decl "bool" log nil) (cauchy_ln_small nonempty-type-eq-decl nil log nil) (cauchy_ln_series const-decl "cauchy_real" log 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]" number_fields nil) (ln_smallreal nonempty-type-eq-decl nil log nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (real_gtm1_le1 nonempty-type-eq-decl nil ln_exp_series_alt "lnexp_fnd/") (lnT const-decl "real_gtm1_le1" ln_exp_series_alt "lnexp_fnd/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (cauchy_ln_drx_TCC1 0 (cauchy_ln_drx_TCC1-1 nil 3394115362 ("" (lemma "ln_series_lemma") (("" (expand "cauchys_real?") (("" (inst + "lambda n:IF n = 0 THEN 0 ELSE lnT(1)(n - 1) ENDIF") (("1" (expand "cauchys_prop") (("1" (propax) nil nil)) nil) ("2" (skosimp) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((cauchys_real? const-decl "bool" sum nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (cauchys_prop const-decl "bool" sum nil) (lnT const-decl "real_gtm1_le1" ln_exp_series_alt "lnexp_fnd/") (real_gtm1_le1 nonempty-type-eq-decl nil ln_exp_series_alt "lnexp_fnd/") (<= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (ln_series_lemma formula-decl nil log nil)) nil)) (ln_drx_lemma_TCC1 0 (ln_drx_lemma_TCC1-1 nil 3394113740 ("" (subtype-tcc) nil nil) ((^ const-decl "real" exponentiation nil) (cauchy_prop const-decl "bool" cauchy nil) (posnat_expt application-judgement "posnat" exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil)) (ln_drx_lemma 0 (ln_drx_lemma-2 nil 3508599150 ("" (skosimp) (("" (lemma "ln_estimate_lemma" ("ssx" "ssx!1" "cssx" "cssx!1")) (("" (expand "cauchy_ln_drx") (("" (expand "cauchy_prop" 1) (("" (skosimp) (("" (inst - "2+p!1") (("" (assert) (("" (lemma "ln_estimate_bnd" ("z" "ssx!1" "n" "2+p!1")) (("" (name-replace "LOG_" "ln(1 + ssx!1)") (("" (name-replace "CPS" "cauchy_powerseries(cssx!1, cauchy_ln_series, 2 + p!1)") (("" (name-replace "EST" "ln_estimate(ssx!1, 2 + p!1)") (("" (expand "round") (("" (typepred "floor(1 / 2 + CPS(2 + p!1) / 4)") (("" (name-replace "RR" "floor(1 / 2 + CPS(2 + p!1) / 4)") (("" (hide -5) (("" (expand "cauchy_prop") (("" (inst - "2+p!1") (("" (flatten) (("" (case "abs(LOG_ - EST)*2^p!1 < 1/4") (("1" (hide -4) (("1" (case "abs(LOG_* 2 ^ p!1 - CPS(2 + p!1)/4) < 1/2") (("1" (hide -2 -5 -6) (("1" (name-replace "P2" "2 ^ p!1") (("1" (grind) nil nil)) nil)) nil) ("2" (hide -2 -3 2) (("2" (lemma "abs_mult" ("x" "LOG_-EST" "y" "2^p!1")) (("2" (expand "abs" -1 3) (("2" (replace -1 -2 rl) (("2" (hide -1) (("2" (rewrite "expt_plus") (("2" (rewrite "expt_x2") (("2" (name-replace "P2" "2^p!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (name-replace "ABS" "abs(LOG_ - EST)") (("2" (typepred "ssx!1") (("2" (case "abs(ssx!1) ^ (2 + p!1 + 1) <= 1/2^(3+p!1)") (("1" (case "1 <= IF ssx!1 < 0 THEN 1 + ssx!1 ELSE 1 ENDIF * (2 + p!1 + 1)") (("1" (lemma "le_div_le_pos" ("nnx" "abs(ssx!1) ^ (2 + p!1 + 1)" "y" "1 / 2 ^ (3 + p!1)" "pz" "1" "w" "IF ssx!1 < 0 THEN 1 + ssx!1 ELSE 1 ENDIF * (2 + p!1 + 1)")) (("1" (replace -3) (("1" (replace -2) (("1" (name-replace "RHS" "abs(ssx!1) ^ (2 + p!1 + 1) / (IF ssx!1 < 0 THEN 1 + ssx!1 ELSE 1 ENDIF * (2 + p!1 + 1))") (("1" (rewrite "div_div2") (("1" (lemma "both_sides_expt_gt1_lt" ("gt1x" "2" "i" "2+p!1" "j" "3+p!1")) (("1" (assert) (("1" (hide -3 -4) (("1" (lemma "div_mult_pos_lt2" ("py" "2^p!1" "x" "ABS" "z" "1/4")) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (rewrite "div_div2") (("1" (lemma "both_sides_div_pos_lt2" ("pz" "1" "px" "2 ^ (3 + p!1)" "py" "2 ^ (2 + p!1)")) (("1" (assert) (("1" (lemma "expt_plus" ("n0x" "2" "i" "2" "j" "p!1")) (("1" (rewrite "expt_x2") (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -3 1)) (("2" (case-replace "ssx!1<0") (("1" (lemma "both_sides_times_pos_le1" ("pz" "3+p!1" "x" "-1/2" "y" "ssx!1")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -2 1)) (("2" (case-replace "ssx!1=0") (("1" (expand "^" 1 1) (("1" (expand "expt" 1 1) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "both_sides_expt_pos_le" ("px" "abs(ssx!1)" "py" "1/2" "pm" "3+p!1")) (("1" (flatten) (("1" (hide -1) (("1" (split -1) (("1" (rewrite "inv_expt") (("1" (assert) nil nil)) nil) ("2" (hide 2 3) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ln_smallreal nonempty-type-eq-decl nil log nil) (- const-decl "[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) (AND const-decl "[bool, bool -> bool]" booleans nil) (cauchy_ln_small nonempty-type-eq-decl nil log nil) (cauchy_ln_small? const-decl "bool" log 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) (ln_estimate_lemma formula-decl nil log nil) (posint_exp application-judgement "posint" exponentiation nil) (cauchy_prop const-decl "bool" cauchy nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (ln_estimate_bnd formula-decl nil ln_exp_series_alt "lnexp_fnd/") (< const-decl "bool" reals nil) (real_gtm1_le1 nonempty-type-eq-decl nil ln_exp_series_alt "lnexp_fnd/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (cauchy_ln_series const-decl "cauchy_real" log nil) (cauchy_powerseries const-decl "cauchy_real" powerseries nil) (cauchys_real nonempty-type-eq-decl nil sum nil) (cauchys_real? const-decl "bool" sum nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (round const-decl "int" prelude_aux nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (both_sides_expt_pos_le formula-decl nil exponentiation nil) (posnat nonempty-type-eq-decl nil integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (inv_expt formula-decl nil exponentiation nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nat_expt application-judgement "nat" exponentiation nil) (expt def-decl "real" exponentiation nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (both_sides_expt_gt1_lt formula-decl nil exponentiation nil) (both_sides_div_pos_lt2 formula-decl nil real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (div_div2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (le_div_le_pos formula-decl nil real_props nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (expt_x2 formula-decl nil inv nil) (even_times_int_is_even application-judgement "even_int" integers nil) (int_times_int_is_int application-judgement "int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (expt_plus formula-decl nil exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (abs_mult formula-decl nil real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posint nonempty-type-eq-decl nil integers nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (integer nonempty-type-from-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (ln_estimate const-decl "real" ln_exp_series_alt "lnexp_fnd/") (= const-decl "[T, T -> boolean]" equalities 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) (ln const-decl "real" ln_exp "lnexp_fnd/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (cauchy_ln_drx const-decl "int" log nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) nil) (ln_drx_lemma-1 nil 3394116656 ("" (skosimp) (("" (lemma "ln_estimate_lemma" ("ssx" "ssx!1" "cssx" "cssx!1")) (("" (expand "cauchy_ln_drx") (("" (expand "cauchy_prop" 1) (("" (skosimp) (("" (inst - "2+p!1") (("" (assert) (("" (lemma "ln_estimate_bnd" ("z" "ssx!1" "n" "2+p!1")) (("" (name-replace "LOG" "ln(1 + ssx!1)") (("" (name-replace "CPS" "cauchy_powerseries(cssx!1, cauchy_ln_series, 2 + p!1)") (("" (name-replace "EST" "ln_estimate(ssx!1, 2 + p!1)") (("" (expand "round") (("" (typepred "floor(1 / 2 + CPS(2 + p!1) / 4)") (("" (name-replace "RR" "floor(1 / 2 + CPS(2 + p!1) / 4)") (("" (hide -5) (("" (expand "cauchy_prop") (("" (inst - "2+p!1") (("" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.42 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 |
