| products/sources/formale Sprachen/PVS/series/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: fundamental_theorem.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(power_series_derivseq
(IMP_power_series_conv_TCC1 0 (IMP_power_series_conv_TCC1-1 nil 3297687390 ("" (lemma "not_one_element") (("" (propax) nil nil)) nil) ((not_one_element formula-decl nil power_series_derivseq nil)) shostak)) (IMP_power_series_conv_TCC2 0 (IMP_power_series_conv_TCC2-1 nil 3297687390 ("" (lemma "connected_domain") (("" (lemma "connected_deriv_domain[T]") (("" (lemma "not_one_element") (("" (assert) nil nil)) nil)) nil)) nil) ((T formal-subtype-decl nil power_series_derivseq nil) (T_pred const-decl "[real -> boolean]" power_series_derivseq 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) (connected_deriv_domain formula-decl nil deriv_domain_def "analysis/") (not_one_element formula-decl nil power_series_derivseq nil) (connected_domain formula-decl nil power_series_derivseq nil)) shostak)) (IMP_power_series_conv_TCC3 0 (IMP_power_series_conv_TCC3-1 nil 3297687390 ("" (lemma "open") (("" (propax) nil nil)) nil) ((open formula-decl nil power_series_derivseq nil)) shostak)) (deriv_powerseq_TCC1 0 (deriv_powerseq_TCC1-1 nil 3279280814 ("" (subtype-tcc) nil 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) (T_pred const-decl "[real -> boolean]" power_series_derivseq nil) (T formal-subtype-decl nil power_series_derivseq 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (/= const-decl "boolean" notequal nil)) nil)) (deriv_powerseries_conv 0 (deriv_powerseries_conv-6 nil 3320063098 ("" (skosimp*) (("" (expand "conv_powerseries?") (("" (case-replace "x!1 = 0") (("1" (case-replace "deriv_powerseq(a!1, 0) = (LAMBDA n: IF n = 1 THEN a!1(1) ELSE 0 ENDIF)") (("1" (hide -1) (("1" (lemma "tail_series_conv2") (("1" (inst?) (("1" (inst - "2") (("1" (assert) (("1" (hide 2) (("1" (rewrite "zero_series_conv") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "deriv_powerseq") (("2" (apply-extensionality 1 :hide? t) (("1" (lift-if) (("1" (ground) (("1" (lemma "zero_hat") (("1" (hide -3) (("1" (inst?) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "(EXISTS (y:T): abs(x!1) < y)") (("1" (skosimp*) (("1" (case "abs(y!1) > 0") (("1" (inst - "y!1") (("1" (lemma "powerseries_bounded") (("1" (inst?) (("1" (assert) (("1" (rewrite "bounded?_lem") (("1" (skosimp*) (("1" (lemma "comparison_test") (("1" (name "BS" "(LAMBDA n: IF n = 0 THEN 0 ELSE n*B!1/abs(y!1)*abs(x!1/y!1)^(n-1) ENDIF)") (("1" (inst - "deriv_powerseq(a!1, x!1)" "BS") (("1" (assert) (("1" (hide 3) (("1" (prop) (("1" (case-replace "B!1 = 0") (("1" (case-replace "BS = (LAMBDA n: 0)") (("1" (rewrite "zero_series_conv") nil nil) ("2" (replace -2 * rl) (("2" (apply-extensionality 1 :hide? t) (("1" (lift-if) (("1" (ground) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "(EXISTS (NN: posnat): (NN+1)/NN*abs(x!1/y!1) < 1)") (("1" (skosimp*) (("1" (lemma "ratio_test_gt_N") (("1" (inst?) (("1" (assert) (("1" (hide 3) (("1" (inst + "NN!1") (("1" (inst + "(NN!1 + 1) / NN!1 * abs(x!1 / y!1)") (("1" (assert) (("1" (skosimp*) (("1" (case "BS(n!1) /= 0") (("1" (assert) (("1" (flatten) (("1" (name "RR" "abs(x!1/y!1)") (("1" (replace -1) (("1" (case "RR < 1") (("1" (case-replace "BS(1 + n!1) / BS(n!1) = (n!1+1)/n!1* RR") (("1" (rewrite "abs_mult") (("1" (case-replace "abs(RR) = RR") (("1" (rewrite "abs_div") (("1" (rewrite "abs_div") (("1" (expand "abs" 2) (("1" (field 2) nil nil)) nil)) nil)) nil) ("2" (replace -3 * rl) (("2" (rewrite "abs_abs") nil nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (replace -5 * rl) (("2" (assert) (("2" (assert) (("2" (case-replace "RR ^ n!1 = RR*RR ^ (n!1-1)") (("1" (name-replace "RRnm1" "RR ^ (n!1 - 1)") (("1" (field 2) nil nil)) nil) ("2" (hide 2 3) (("2" (hide-all-but 1) (("2" (expand "^") (("2" (expand "expt" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -6 -7 1)) (("2" (rewrite "abs_div") (("2" (assert) (("2" (expand "abs" -1 2) (("2" (replace -1 * rl) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (flatten) (("2" (replace -4 * rl) (("2" (assert) (("2" (hide -4) (("2" (mult-cases -1) (("1" (typepred "B!1") (("1" (case-replace "B!1 = 0") (("1" (reveal 4) (("1" (field -2) nil nil)) nil)) nil)) nil) ("2" (lemma "expt_pos") (("2" (inst?) (("1" (assert) nil nil) ("2" (rewrite "abs_div") (("2" (expand "abs" 1 2) (("2" (cross-mult 1) (("2" (assert) (("2" (lemma "abs_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (mult-cases 1) (("2" (rewrite "abs_div") (("2" (expand "abs" 1 2) (("2" (cross-mult 1) (("2" (assert) (("2" (lemma "abs_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -5 3) (("2" (case "EXISTS (NBIG: posnat): NBIG > abs(x!1)/(y!1 - abs(x!1))") (("1" (skosimp*) (("1" (inst + "NBIG!1") (("1" (rewrite "abs_div") (("1" (cross-mult -1) (("1" (cross-mult 1) (("1" (assert) (("1" (expand "abs" 1 3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (inst + "ceiling(abs(x!1) / (y!1 - abs(x!1)))+1") (("1" (assert) nil nil) ("2" (assert) (("2" (case-replace "(abs(x!1) / (y!1 - abs(x!1))) > 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (cross-mult 1) (("2" (assert) (("2" (lemma "abs_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (assert) (("2" (expand "deriv_powerseq") (("2" (lift-if) (("2" (ground) (("1" (rewrite "abs_0") (("1" (assert) nil nil)) nil) ("2" (inst?) (("2" (replace -1) (("2" (expand "powerseq") (("2" (assert) (("2" (rewrite "abs_mult") (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "powerseq") (("3" (inst - "n!1") (("3" (rewrite "abs_mult") (("3" (hide -4) (("3" (expand "abs" 2 2) (("3" (rewrite "abs_mult") (("3" (assert) (("3" (rewrite "abs_mult" -) (("3" (rewrite "exponentiation.abs_expt") (("3" (rewrite "div_expt") (("3" (rewrite "abs_div") (("3" (div-by -1 "abs(y!1 ^ n!1)") (("1" (case-replace "abs(y!1 ^ n!1) = abs(y!1)*abs(y!1 ^(n!1-1))") (("1" (hide -1) (("1" (mult-by -1 "abs(x!1 ^ (n!1 - 1)) * n!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "^") (("2" (expand "expt" 1 1) (("2" (rewrite "abs_mult") nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 3) (("2" (lemma "exponentiation.abs_expt") (("2" (inst?) (("2" (assert) (("2" (replace -1 * rl) (("2" (hide -1) (("2" (rewrite "expt_pos") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide -1 3) (("2" (lemma "open") (("2" (case "x!1 >= 0") (("1" (expand "abs") (("1" (assert) (("1" (inst?) (("1" (skosimp*) (("1" (inst + "x!1 + delta!1/2") (("1" (assert) nil nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (assert) (("2" (inst - "-x!1") (("1" (skosimp*) (("1" (inst + "-x!1 + delta!1/2") (("1" (assert) nil nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "ball") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((conv_powerseries? const-decl "bool" power_series_conv nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (powerseries_bounded formula-decl nil power_series nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (ratio_test_gt_N formula-decl nil series nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (le_times_le_pos formula-decl nil real_props nil) (both_sides_plus_le1 formula-decl nil real_props nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (FDX_13 skolem-const-decl "posnat" power_series_derivseq nil) (FDX_12 skolem-const-decl "nat" power_series_derivseq nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (div_cancel3 formula-decl nil real_props nil) (cross_mult formula-decl nil real_props nil) (times_div2 formula-decl nil real_props nil) (pos_times_gt formula-decl nil real_props nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (abs_div formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (abs_abs formula-decl nil real_props nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (abs_mult formula-decl nil real_props nil) (expt def-decl "real" exponentiation nil) (nonzero_times3 formula-decl nil real_props nil) (zero_times1 formula-decl nil real_props nil) (both_sides_times1 formula-decl nil real_props nil) (div_cancel2 formula-decl nil real_props nil) (zero_times3 formula-decl nil real_props nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (expt_pos formula-decl nil exponentiation nil) (posreal nonempty-type-eq-decl nil real_types nil) (NN!1 skolem-const-decl "posnat" power_series_derivseq nil) (real_minus_real_is_real application-judgement "real" reals nil) (div_mult_pos_gt2 formula-decl nil extra_real_props nil) (times_div1 formula-decl nil real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (integer nonempty-type-from-decl nil integers nil) (<= const-decl "bool" reals nil) (ceiling const-decl "{i | x <= i & i < x + 1}" floor_ceil nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (y!1 skolem-const-decl "T" power_series_derivseq nil) (x!1 skolem-const-decl "T" power_series_derivseq nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (nzreal nonempty-type-eq-decl nil reals nil) (abs_expt formula-decl nil exponentiation nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (times_div_cancel2 formula-decl nil extra_real_props nil) (n!1 skolem-const-decl "nat" power_series_derivseq nil) (both_sides_div_pos_le1 formula-decl nil real_props nil) (div_expt formula-decl nil exponentiation nil) (div_mult_pos_le2 formula-decl nil real_props nil) (expt_x1 formula-decl nil exponentiation nil) (expt_x0 formula-decl nil exponentiation nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (abs_0 formula-decl nil abs_lems "reals/") (comparison_test formula-decl nil series nil) (bounded?_lem formula-decl nil real_fun_preds "reals/") (powerseq const-decl "sequence[real]" power_series nil) (open formula-decl nil power_series_derivseq nil) (delta!1 skolem-const-decl "posreal" power_series_derivseq nil) (ball formula-decl nil power_series_derivseq nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (delta!1 skolem-const-decl "posreal" power_series_derivseq nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" 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) (sequence type-eq-decl nil sequences nil) (deriv_powerseq const-decl "sequence[real]" power_series_derivseq nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (tail_series_conv2 formula-decl nil series nil) (zero_series_conv formula-decl nil series nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (hat_02n formula-decl nil power_series nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (T formal-subtype-decl nil power_series_derivseq nil) (T_pred const-decl "[real -> boolean]" power_series_derivseq 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil) (deriv_powerseries_conv-5 nil 3298131703 ("" (skosimp*) (("" (expand "conv_powerseries?") (("" (case-replace "x!1 = 0") (("1" (case-replace "deriv_powerseq(a!1, 0) = (LAMBDA n: IF n = 1 THEN a!1(1) ELSE 0 ENDIF)") (("1" (hide -1) (("1" (lemma "tail_series_conv2") (("1" (inst?) (("1" (inst - "2") (("1" (assert) (("1" (hide 2) (("1" (rewrite "zero_series_conv") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "deriv_powerseq") (("2" (apply-extensionality 1 :hide? t) (("1" (lift-if) (("1" (ground) (("1" (lemma "zero_hat") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (lemma "ball") (("3" (hide -3 2) (("3" (inst - "x!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "(EXISTS (y:T): abs(x!1) < y)") (("1" (skosimp*) (("1" (case "abs(y!1) > 0") (("1" (inst - "y!1") (("1" (lemma "powerseries_bounded") (("1" (inst?) (("1" (assert) (("1" (rewrite "bounded?_lem") (("1" (skosimp*) (("1" (lemma "comparison_test") (("1" (name "BS" "(LAMBDA n: IF n = 0 THEN 0 ELSE n*B!1/abs(y!1)*abs(x!1/y!1)^(n-1) ENDIF)") (("1" (inst - "deriv_powerseq(a!1, x!1)" "BS") (("1" (assert) (("1" (hide 3) (("1" (prop) (("1" (case-replace "B!1 = 0") (("1" (case-replace "BS = (LAMBDA n: 0)") (("1" (rewrite "zero_series_conv") nil nil) ("2" (replace -2 * rl) (("2" (apply-extensionality 1 :hide? t) (("1" (lift-if) (("1" (ground) nil nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "(EXISTS (NN: posnat): (NN+1)/NN*abs(x!1/y!1) < 1)") (("1" (skosimp*) (("1" (lemma "ratio_test_gt_N") (("1" (inst?) (("1" (assert) (("1" (hide 3) (("1" (inst + "NN!1") (("1" (inst + "(NN!1 + 1) / NN!1 * abs(x!1 / y!1)") (("1" (assert) (("1" (skosimp*) (("1" (case "BS(n!1) /= 0") (("1" (assert) (("1" (flatten) (("1" (name "RR" "abs(x!1/y!1)") (("1" (replace -1) (("1" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.94 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 |
