| products/Sources/formale Sprachen/GAP/lib/ (NIST Fortran ©) Datei vom 18.9.2025 mit Größe 36 kB |
|
Quellcode-Bibliothek power_series_derivseq.prfSprache: Lisp |
|||||||||||||||
|
(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" (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" (replace -1) (("2" (assert) (("2" (expand "powerseq") (("2" (assert) (("2" (inst -2 "1") (("2" (assert) (("2" (rewrite "abs_mult") (("2" (assert) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (inst - "n!1") (("3" (lemma "abs_eq_0") (("3" (inst - "x!1") (("3" (assert) (("3" (case-replace "abs(a!1(n!1) * x!1 ^ (n!1 - 1) * n!1) = n!1 * abs(a!1(n!1) * y!1^n!1)/ abs(y!1) * abs(x!1 / y!1) ^ (n!1 - 1)") (("1" (hide -1) (("1" (expand "powerseq") (("1" (mult-by -1 "abs(x!1 / y!1) ^ (n!1 - 1)") (("1" (rewrite "abs_mult") (("1" (mult-by -1 "n!1") (("1" (assert) (("1" (mult-by 3 "abs(y!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (rewrite "abs_mult") (("2" (rewrite "abs_div") (("2" (rewrite "div_expt") (("2" (assert) (("2" (rewrite "abs_mult") (("2" (rewrite "abs_mult") (("2" (case-replace "abs(y!1 ^ n!1) = abs(y!1)*abs(y!1 ^ (n!1-1))") (("1" (expand "abs" 1 3) (("1" (rewrite "abs_hat" +) (("1" (rewrite "abs_hat" +) (("1" (field 1) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (case-replace "y!1 ^ n!1 = y!1*y!1 ^ (n!1-1)") (("1" (rewrite "abs_mult") nil nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) ((powerseries_bounded formula-decl nil power_series nil) (ratio_test_gt_N formula-decl nil series nil) (abs_hat formula-decl nil exponent_props "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) (tail_series_conv2 formula-decl nil series nil) (zero_series_conv formula-decl nil series nil) (zero_hat formula-decl nil exponent_props "reals/")) nil) (deriv_powerseries_conv-4 nil 3297690436 ("" (skosimp*) (("" (expand "deriv_powerseq") (("" (case-replace "x!1 = 0") (("1" (lemma "tail_series_conv2") (("1" (inst - "2" "_") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (case-replace "(LAMBDA n: 2 * (a!1(2 + n) * 0 ^ (1 + n)) + n * a!1(2 + n) * 0 ^ (1 + n)) = (LAMBDA n: 0)") (("1" (rewrite "zero_series_conv") nil nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "^") (("2" (expand "expt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "abs_eq_0") (("2" (inst?) (("2" (assert) (("2" (lemma "powerseries_abs_conv") (("2" (inst?) (("2" (replace -2) (("2" (hide -2) (("2" (case "EXISTS (r: T): abs(x!1) < r") (("1" (skosimp*) (("1" (lemma "conv_series_scal") (("1" (inst?) (("1" (assert) (("1" (inst - "x!1") (("1" (assert) (("1" (hide 4) (("1" (lemma "series_scal") (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "(LAMBDA n: x!1 * IF n = 0 THEN 0 ELSE n * a!1(n) * x!1 ^ (n - 1) ENDIF) = (LAMBDA n: IF n = 0 THEN 0 ELSE n * a!1(n) * x!1 ^ n ENDIF)") (("1" (hide -1) (("1" (lemma "comparison_test_gen") (("1" (inst -1 "(LAMBDA (k: nat): IF k = 0 THEN 0 ELSE k * a!1(k) * x!1 ^ k ENDIF)" "abs(powerseq(a!1, r!1))") (("1" (assert) (("1" (hide 2) (("1" (inst?) (("1" (assert) (("1" (lemma "lim_n_pow_1divn") (("1" (expand "convergence") (("1" (inst - "r!1/abs(x!1) - 1") (("1" (skosimp*) (("1" (inst + "n!1") (("1" (skosimp*) (("1" (lift-if) (("1" (ground) (("1" (rewrite "abs_0") (("1" (assert) (("1" (hide-all-but 1) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "powerseq") (("2" (expand "abs" 2 2) (("2" (case "n!2 >= n!1 IMPLIES n!2^^(1/n!2) < r!1/abs(x!1)") (("1" (case "n!2 >= n!1 IMPLIES n!2*abs(x!1^n!2) < r!1^n!2 ") (("1" (hide -2 -6) (("1" (assert) (("1" (case "r!1 ^ n!2 = abs(r!1 ^ n!2)") (("1" (replace -1 -2) (("1" (hide -1) (("1" (case-replace "a!1(n!2) = 0") (("1" (assert) nil nil) ("2" (rewrite "abs_mult" +) (("2" (rewrite "abs_mult" +) (("2" (rewrite "abs_mult" +) (("2" (expand "abs" 3 3) (("2" (mult-by -1 "abs(a!1(n!2))") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -5 3) (("2" (assert) (("2" (lemma "hathat_lem1") (("2" (inst?) (("2" (assert) (("2" (lemma "hathat_lem2") (("2" (inst?) (("2" (replace -1) (("2" (assert) (("2" (hide -1) (("2" (rewrite "hathat_nat") (("2" (rewrite "hathat_nat") (("2" (cross-mult -1) (("1" (assert) (("1" (lemma "expt_pos") (("1" (inst?) (("1" (assert) (("1" (lemma "expt_of_abs") (("1" (inst?) (("1" (inst - "n!2") (("1" (expand "^") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "expt_pos") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (hide -5 3) (("2" (inst - "n!2") (("2" (assert) (("2" (expand "n2n") (("2" (expand "abs" -2 1) (("2" (case "n!2 ^^ (1 / n!2) >= 1") (("1" (assert) nil nil) ("2" (hide -2 2) (("2" (case-replace "n!2 = 1") (("1" (rewrite "hathat_nat") (("1" (hide-all-but 1) (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^^") (("2" (lemma "ln_increasing") (("2" (expand "increasing?") (("2" (inst - "exp((1 / n!2) * ln(n!2))" "1") (("2" (assert) (("2" (rewrite "ln_exp") (("2" (hide 2) (("2" (rewrite "ln_1") (("2" (lemma "ln_increasing") (("2" (expand "increasing?") (("2" (cross-mult -2) (("2" (inst - "1" "n!2") (("2" (assert) (("2" (lemma "ln_1") (("2" (assert) (("2" (lemma "ln_bij") (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "injective?") (("2" (inst - "1" "n!2") (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "r!1 / abs(x!1) > 1") (("1" (assert) nil nil) ("2" (hide 2 3) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (lift-if) (("2" (ground) (("2" (expand "^") (("2" (expand expt 2 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (lemma "open") (("2" (hide -2) (("2" (case "x!1 >= 0") (("1" (inst - "x!1") (("1" (skosimp*) (("1" (inst + "x!1 + delta!1/2") (("1" (expand "abs") (("1" (assert) nil nil)) nil) ("2" (inst - "x!1+delta!1/2") (("2" (assert) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "-x!1") (("1" (skosimp*) (("1" (inst + "-x!1+delta!1/2") (("1" (expand "abs") (("1" (assert) nil nil)) nil) ("2" (inst - "-x!1+delta!1/2") (("2" (assert) (("2" (expand "abs") (("2" (assert) nil nil)) 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)) nil)) nil)) nil)) nil)) nil)) nil) ((zero_series_conv formula-decl nil series nil) (tail_series_conv2 formula-decl nil series nil) (powerseries_abs_conv formula-decl nil power_series_conv nil) (conv_series_scal formula-decl nil series nil) (series_scal formula-decl nil series nil) (comparison_test_gen formula-decl nil series nil) (increasing? const-decl "bool" real_fun_preds "reals/") (convergence const-decl "bool" convergence_sequences "analysis/") (abs const-decl "sequence[real]" series nil) (powerseq const-decl "sequence[real]" power_series nil)) nil) (deriv_powerseries_conv-3 nil 3297517507 ("" (skosimp*) (("" (expand "deriv_powerseq") (("" (case-replace "x!1 = 0") (("1" (lemma "tail_series_conv2") (("1" (inst - "2" "_") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (case-replace "(LAMBDA n: 2 * (a!1(2 + n) * 0 ^ (1 + n)) + n * a!1(2 + n) * 0 ^ (1 + n)) = (LAMBDA n: 0)") (("1" (rewrite "zero_series_conv") nil nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (expand "^") (("2" (expand "expt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "abs_eq_0") (("2" (inst?) (("2" (assert) (("2" (lemma "powerseries_abs_conv") (("2" (inst?) (("2" (replace -2) (("2" (hide -2) (("2" (case "EXISTS (r: T): abs(x!1) < r") (("1" (skosimp*) (("1" (lemma "conv_series_scal") (("1" (inst?) (("1" (assert) (("1" (inst - "x!1") (("1" (assert) (("1" (hide 4) (("1" (lemma "series_scal") (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (case-replace "(LAMBDA n: x!1 * IF n = 0 THEN 0 ELSE n * a!1(n) * x!1 ^ (n - 1) ENDIF) = (LAMBDA n: IF n = 0 THEN 0 ELSE n * a!1(n) * x!1 ^ n ENDIF)") (("1" (hide -1) (("1" (lemma "comparison_test_gen") (("1" (inst -1 "(LAMBDA (k: nat): IF k = 0 THEN 0 ELSE k * a!1(k) * x!1 ^ k ENDIF)" "abs(powerseq(a!1, r!1))") (("1" (assert) (("1" (hide 2) (("1" (inst?) (("1" (assert) (("1" (lemma "lim_n_pow_1divn") (("1" (expand "convergence") (("1" (inst - "r!1/abs(x!1) - 1") (("1" (skosimp*) (("1" (inst + "n!1") (("1" (skosimp*) (("1" (lift-if) (("1" (ground) (("1" (assert) (("1" (expand "abs" 1) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (expand "powerseq") (("2" (assert) (("2" (case-replace "abs(LAMBDA (k: nat): a!1(k) * r!1 ^ k)(n!2) = abs(a!1(n!2)) * abs(r!1 ^ n!2)") (("1" (hide -1) (("1" (case "n!2 >= n!1 IMPLIES n!2^^(1/n!2) < r!1/abs(x!1)") (("1" (case "n!2 >= n!1 IMPLIES n!2*abs(x!1^n!2) < r!1^n!2 ") (("1" (hide -2 -6) (("1" (assert) (("1" (case "r!1 ^ n!2 = abs(r!1 ^ n!2)") (("1" (replace -1 -2) (("1" (hide -1) (("1" (case-replace "a!1(n!2) = 0") (("1" (assert) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "abs_mult" +) (("2" (rewrite "abs_mult" +) (("2" (case-replace "abs(n!2) = n!2") (("1" (hide -1) (("1" (mult-by -1 "abs(a!1(n!2))") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "abs") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "abs") (("2" (lift-if) (("2" (lemma "expt_pos") (("2" (expand "^") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -5 3) (("2" (flatten) (("2" (assert) (("2" (assert) (("2" (hide -3) (("2" (lemma "hathat_lem1") (("2" (inst?) (("2" (assert) (("2" (lemma "hathat_lem2") (("2" (inst?) (("2" (replace -1) (("2" (assert) (("2" (hide -1) (("2" (rewrite "hathat_nat") (("2" (rewrite "hathat_nat") (("2" (cross-mult -1) (("1" (assert) (("1" (lemma "expt_pos") (("1" (inst?) (("1" (assert) (("1" (lemma "expt_of_abs") (("1" (inst?) (("1" (inst - "n!2") (("1" (expand "^") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "expt_pos") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (assert) (("2" (hide -5 3) (("2" (inst - "n!2") (("2" (assert) (("2" (expand "n2n") (("2" (expand "abs" -2 1) (("2" (case "n!2 ^^ (1 / n!2) >= 1") (("1" (assert) nil nil) ("2" (hide -2 2) (("2" (case-replace "n!2 = 1") (("1" (rewrite "hathat_nat") (("1" (hide-all-but 1) (("1" (expand "^") (("1" (expand "expt") (("1" (expand "expt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^^") (("2" (lemma "ln_increasing") (("2" (expand "increasing?") (("2" (inst - "exp((1 / n!2) * ln(n!2))" "1") (("2" (assert) (("2" (rewrite "ln_exp") (("2" (hide 2) (("2" (rewrite "ln_1") (("2" (lemma "ln_increasing") (("2" (expand "increasing?") (("2" (cross-mult -2) (("2" (inst - "1" "n!2") (("2" (assert) (("2" (lemma "ln_1") (("2" (assert) (("2" (lemma "ln_bij") (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "injective?") (("2" (inst - "1" "n!2") (("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)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (expand "abs" 1 1) (("2" (rewrite "abs_mult") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "r!1 / abs(x!1) > 1") (("1" (assert) nil nil) ("2" (hide 2 3) (("2" (cross-mult 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (lift-if) (("2" (ground) (("2" (expand "^") (("2" (expand expt 2 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (lemma "open") (("2" (hide -2) (("2" (case "x!1 >= 0") (("1" (inst - "x!1") (("1" (skosimp*) (("1" (inst + "x!1 + delta!1/2") (("1" (expand "abs") (("1" (assert) nil nil)) nil) ("2" (inst - "x!1+delta!1/2") (("2" (assert) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "-x!1") (("1" (skosimp*) (("1" (inst + "-x!1+delta!1/2") (("1" (expand "abs") (("1" (assert) nil nil)) nil) ("2" (inst - "-x!1+delta!1/2") (("2" (assert) (("2" (expand "abs") (("2" (assert) nil nil)) 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)) nil)) nil)) nil)) nil)) nil)) nil) ((powerseq const-decl "sequence[real]" power_series nil) (abs const-decl "sequence[real]" series nil) (convergence const-decl "bool" convergence_sequences "analysis/") (increasing? const-decl "bool" real_fun_preds "reals/") (comparison_test_gen formula-decl nil series nil) (series_scal formula-decl nil series nil) (conv_series_scal formula-decl nil series nil) (tail_series_conv2 formula-decl nil series nil) (zero_series_conv formula-decl nil series nil)) nil) (deriv_powerseries_conv-2 nil 3297173514 ("" (skosimp*) (("" (lemma "powerseries_abs_conv") (("" (inst?) (("" (assert) (("" (replace -2) (("" (hide -2) (("" (lemma "open") (("" (inst - "x!1") (("" (skosimp*) (("" (name "DDD" "IF x!1 >= 0 THEN x!1+delta!1/2 ELSE x!1-delta!1/2 ENDIF") (("" (inst - "DDD") (("" (split -2) (("1" (inst - "DDD") (("1" (lemma "comparison_test_gen") (("1" (inst -1 "(LAMBDA (k: nat): IF k = 0 THEN 0 ELSE k * a!1(k) * x!1 ^ (k - 1) ENDIF)" "abs(powerseq(a!1, DDD))") (("1" (assert) (("1" (hide -3 2) (("1" (lemma "deriv_prep") (("1" (inst -1 "delta!1/2" "x!1") (("1" (skosimp*) (("1" (inst + "N!1") (("1" (skosimp*) (("1" (inst -1 "n!1") (("1" (assert) (("1" (expand "powerseq") (("1" (assert) (("1" (lemma "abs_mult") (("1" (inst -1 "a!1(n!1)" "x!1 ^ (n!1 - 1) * n!1 ") (("1" (replace -1) (("1" (hide -1) (("1" (expand "abs" 1 3) (("1" (case-replace "a!1(n!1) = 0") (("1" (hide -1 -2) (("1" (grind) nil nil)) nil) ("2" (lemma "abs_mult") (("2" (inst -1 "a!1(n!1)" "DDD^n!1") (("2" (replace -1) (("2" (hide -1) (("2" (div-by 2 "abs(a!1(n!1))") (("1" (case "x!1 >= 0") (("1" (assert) (("1" (replace -5 * rl) (("1" (hide -5) (("1" (case-replace "abs((delta!1 / 2 + x!1) ^ n!1) = (abs(x!1) + delta!1 / 2) ^ n!1") (("1" (assert) (("1" (hide-all-but (-1 1)) (("1" (expand "abs" 1 2) (("1" (lemma "abs_hat") (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (expand "abs") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -4 * rl) (("2" (hide -4) (("2" (expand "abs" -1 2) (("2" (lemma "abs_hat") (("2" (inst?) (("2" (replace -1) (("2" (hide -1) (("2" (expand "abs" 3 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 2)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((powerseq const-decl "sequence[real]" power_series nil) (abs const-decl "sequence[real]" series nil) (abs_hat formula-decl nil exponent_props "reals/") (comparison_test_gen formula-decl nil series nil)) nil) (deriv_powerseries_conv-1 nil 3279280814 ("" (skosimp*) (("" (lemma "powerseries_abs_conv") (("" (inst?) (("" (assert) (("" (replace -2) (("" (hide -2) (("" (lemma "open") (("" (inst - "x!1") (("" (skosimp*) (("" (name "DDD" "x!1+delta!1/2") (("" (inst - "DDD") (("" (split -2) (("1" (inst - "DDD") (("1" (lemma "comparison_test_gen") (("1" (inst -1 "(LAMBDA (k: nat): IF k = 0 THEN 0 ELSE k * a!1(k) * x!1 ^ (k - 1) ENDIF)" "abs(powerseq(a!1, DDD))") (("1" (assert) (("1" (hide -3 2) (("1" (lemma "deriv_prep") (("1" (inst -1 "delta!1" "x!1") (("1" (skosimp*) (("1" (inst + "N!1") (("1" (skosimp*) (("1" (inst -1 "n!1") (("1" (assert) (("1" (expand "powerseq") (("1" (assert) (("1" (lemma "abs_mult") (("1" (inst -1 "a!1(n!1)" "x!1 ^ (n!1 - 1) * n!1 ") (("1" (replace -1) (("1" (hide -1) (("1" (expand "abs" 1 3) (("1" (case-replace "a!1(n!1) = 0") (("1" (hide -1 -2) (("1" (grind) nil nil)) nil) ("2" (lemma "abs_mult") (("2" (inst -1 "a!1(n!1)" "DDD^n!1") (("2" (replace -1) (("2" (hide -1) (("2" (div-by 2 "abs(a!1(n!1))") (("1" (postpone) nil nil) ("2" (postpone) 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" (postpone) nil nil)) nil)) nil)) nil) ("2" (hide -2 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((comparison_test_gen formula-decl nil series nil) (powerseq const-decl "sequence[real]" power_series nil) (abs const-decl "sequence[real]" series nil)) nil)) (derivseq_conv 0 (derivseq_conv-1 nil 3279280814 ("" (skosimp*) (("" (lemma "deriv_powerseries_conv") (("" (inst?) (("" (replace -2) (("" (assert) (("" (inst?) (("" (lemma "tail_series_conv") (("" (inst?) (("" (inst -1 "1") (("" (assert) (("" (hide -2) (("" (case-replace "powerseq(derivseq(a!1), x!1) = (LAMBDA n: deriv_powerseq(a!1, x!1)(1 + n))") (("" (hide =1 2) (("" (expand "powerseq") (("" (apply-extensionality 1 :hide? t) (("" (expand "derivseq") (("" (expand "deriv_powerseq") (("" (lift-if) (("" (ground) (("" (replace -1) (("" (hide -2 -3) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((deriv_powerseries_conv formula-decl nil power_series_derivseq nil) (T formal-subtype-decl nil power_series_derivseq nil) (T_pred const-decl "[real -> boolean]" power_series_derivseq nil) (deriv_powerseq const-decl "sequence[real]" power_series_derivseq nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (powerseq const-decl "sequence[real]" power_series nil) (derivseq const-decl "sequence[real]" power_series_derivseq nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (expt def-decl "real" exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (tail_series_conv formula-decl nil series nil) (sequence type-eq-decl nil sequences 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)) nil)) (deriv_series_shift_TCC1 0 (deriv_series_shift_TCC1-1 nil 3279280814 ("" (skosimp*) (("" (lemma "deriv_powerseries_conv") (("" (inst?) (("" (replace -2) (("" (assert) (("" (expand "deriv_powerseq") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((deriv_powerseries_conv formula-decl nil power_series_derivseq nil) (deriv_powerseq const-decl "sequence[real]" power_series_derivseq nil) (T formal-subtype-decl nil power_series_derivseq nil) (T_pred const-decl "[real -> boolean]" power_series_derivseq nil) (sequence type-eq-decl nil sequences 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)) nil)) (deriv_series_shift_TCC2 0 (deriv_series_shift_TCC2-1 nil 3279280814 ("" (skosimp*) (("" (rewrite "derivseq_conv") nil nil)) nil) ((derivseq_conv formula-decl nil power_series_derivseq 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) (sequence type-eq-decl nil sequences nil) (T_pred const-decl "[real -> boolean]" power_series_derivseq nil) (T formal-subtype-decl nil power_series_derivseq nil)) nil)) (deriv_series_shift 0 (deriv_series_shift-3 "we" 3403525340 ("" (skosimp*) (("" (expand "powerseq") (("" (expand "derivseq") (("" (expand "deriv_powerseq") (("" (lemma "limit_series_shift") (("" (inst?) (("1" (inst -1 "1") (("1" (split -1) (("1" (rewrite "sigma_rew") (("1" (assert) (("1" (case-replace "(LAMBDA (k: nat): IF k = 0 THEN 1 * a!1(1) ELSE a!1(1 + k) * x!1 ^ k + k * a!1(1 + k) * x!1 ^ k ENDIF) = ((LAMBDA n: a!1(1 + n) * x!1 ^ n + n * a!1(1 + n) * x!1 ^ n))") (("1" (assert) (("1" (hide 2) (("1" (apply-extensionality 1 :hide? t) (("1" (lift-if) (("1" (ground) (("1" (hide -2 -3) (("1" (replace -1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "deriv_powerseries_conv") (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "deriv_powerseries_conv") (("2" (inst?) (("2" (replace -2) (("2" (assert) (("2" (inst - "x!1") (("2" (expand "deriv_powerseq") (("2" (propax) 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) ((powerseq const-decl "sequence[real]" power_series nil) (deriv_powerseq const-decl "sequence[real]" power_series_derivseq 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) (x!1 skolem-const-decl "T" power_series_derivseq nil) (T formal-subtype-decl nil power_series_derivseq nil) (T_pred const-decl "[real -> boolean]" power_series_derivseq nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (AND const-decl "[bool, 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) (sequence type-eq-decl nil sequences nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (deriv_powerseries_conv formula-decl nil power_series_derivseq nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (expt def-decl "real" exponentiation nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers 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) (real_plus_real_is_real application-judgement "real" reals nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (sigma_rew formula-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (limit_series_shift formula-decl nil series nil) (derivseq const-decl "sequence[real]" power_series_derivseq nil) (real_times_real_is_real application-judgement "real" reals nil)) nil) (deriv_series_shift-2 "we" 3297672214 ("" (skosimp*) (("" (expand "powerseq") (("" (expand "derivseq") (("" (expand "deriv_powerseq") (("" (lemma "limit_series_shift") (("" (inst?) (("1" (inst -1 "1") (("1" (split -1) (("1" (expand "sigma") (("1" (case-replace "(LAMBDA (k: nat): IF k = 0 THEN 1 * a!1(1) ELSE a!1(1 + k) * x!1 ^ k + k * a!1(1 + k) * x!1 ^ k ENDIF) = ((LAMBDA n: a!1(1 + n) * x!1 ^ n + n * a!1(1 + n) * x!1 ^ n))") (("1" (assert) (("1" (hide 2) (("1" (apply-extensionality 1 :hide? t) (("1" (lift-if) (("1" (ground) (("1" (hide -2 -3) (("1" (replace -1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "deriv_powerseries_conv") (("2" (inst?) (("2" (replace -2) (("2" (assert) (("2" (inst - "x!1") (("2" (expand "deriv_powerseq") (("2" (propax) 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) ((powerseq const-decl "sequence[real]" power_series nil) (sigma def-decl "real" sigma "reals/") (limit_series_shift formula-decl nil series nil)) nil) (as "we" 3297671925 ("" (skosimp*) (("" (expand "powerseq") (("" (expand "derivseq") (("" (expand "deriv_powerseq") (("" (lemma "limit_series_shift") (("" (inst?) (("1" (inst -1 "1") (("1" (split -1) (("1" (expand "sigma") (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (lemma "deriv_powerseries_conv") (("2" (inst?) (("2" (replace -2) (("2" (inst?) (("1" (expand "deriv_powerseq") (("1" (assert) (("1" (postpone) nil nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((limit_series_shift formula-decl nil series nil) (sigma def-decl "real" sigma "reals/") (powerseq const-decl "sequence[real]" power_series nil)) shostak) (deriv_series_shift-1 nil 3279280814 ("" (skosimp*) (("" (expand "powerseq") (("" (expand "derivseq") (("" (expand "deriv_powerseq") (("" (lemma "limit_series_shift") (("" (inst?) (("1" (inst -1 "1") (("1" (split -1) (("1" (expand "sigma") (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (lemma "deriv_powerseries_conv") (("2" (inst?) (("2" (replace -2) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((powerseq const-decl "sequence[real]" power_series nil) (sigma def-decl "real" sigma "reals/") (limit_series_shift formula-decl nil series nil)) nil)) (conv_derivseq 0 (conv_derivseq-1 nil 3298199522 ("" (skosimp*) (("" (expand "conv_powerseries?") (("" (skosimp*) (("" (lemma "derivseq_conv") (("" (inst?) (("" (expand "conv_powerseries?") (("" (inst?) (("" (replace -2) (("" (expand "powerseries") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((conv_powerseries? const-decl "bool" power_series_conv nil) (derivseq_conv formula-decl nil power_series_derivseq nil) (powerseries const-decl "sequence[real]" power_series nil) (T_pred const-decl "[real -> boolean]" power_series_derivseq nil) (T formal-subtype-decl nil power_series_derivseq nil) (sequence type-eq-decl nil sequences 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)) shostak)) (deriv_powerseq_lem 0 (deriv_powerseq_lem-1 nil 3279280814 ("" (skosimp*) (("" (expand "powerseq") (("" (case-replace "n!1 = 0") (("1" (expand "deriv_powerseq") (("1" (split +) (("1" (lemma "const_derivable_fun[T]") (("1" (expand "const_fun") (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "deriv_const_fun[T]") (("2" (expand "const_fun") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "deriv_exp_fun[T]") (("2" (inst -1 "(LAMBDA x: x)" "n!1") (("2" (assert) (("2" (split -1) (("1" (flatten) (("1" (split) (("1" (expand "^" -1) (("1" (hide -2) (("1" (lemma "scal_derivable_fun[T]") (("1" (inst -1 "a!1(n!1)" "(LAMBDA t: t^n!1)") (("1" (expand "*") (("1" (assert) (("1" (lemma "deriv_scal_fun[T]") (("1" (inst -1 "a!1(n!1)" "(LAMBDA x: x^n!1)") (("1" (expand "*" -1) (("1" (hide -1) (("1" (expand "^" -2) (("1" (hide -2) (("1" (case-replace "deriv((LAMBDA x: x)) = const_fun(1)") (("1" (expand "restrict") (("1" (propax) nil nil)) nil) ("2" (expand "restrict") (("2" (propax) nil nil)) nil) ("3" (expand "restrict") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "deriv_powerseq") (("2" (lemma "deriv_scal_fun[T]") (("2" (inst -1 "a!1(n!1)" "(LAMBDA x: x^n!1)") (("1" (expand "*" -1) (("1" (replace -1) (("1" (hide -1) (("1" (assert) (("1" (expand "^" -2) (("1" (replace -2) (("1" (hide -2) (("1" (expand "*") (("1" (case-replace "deriv((LAMBDA x: x)) = const_fun(1)") (("1" (expand "const_fun") (("1" (hide -1 -2) (("1" (ground) (("1" (apply-extensionality 1 :hide? t) (("1" (lift-if) (("1" (ground) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2 3) (("2" (lemma "deriv_id_fun[T]") (("2" (expand "const_fun") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "identity_derivable_fun[T]") (("3" (expand "I") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "identity_derivable_fun[T]") (("2" (expand "I") (("2" (expand "^" -2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (lemma "identity_derivable_fun[T]") (("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (powerseq const-decl "sequence[real]" power_series nil) (deriv_exp_fun formula-decl nil derivatives "analysis/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (n!1 skolem-const-decl "nat" power_series_derivseq nil) (int_minus_int_is_int application-judgement "int" integers nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (I const-decl "(bijective?[T, T])" identity nil) (identity_derivable_fun formula-decl nil derivatives "analysis/") (deriv_id_fun formula-decl nil derivatives "analysis/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (IF const-decl "[boolean, T, T -> T]" if_def 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) (^ const-decl "[T -> real]" real_fun_ops "reals/") (scal_derivable_fun formula-decl nil derivatives "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (deriv_scal_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (deriv const-decl "[T -> real]" derivatives "analysis/") (constant_seq2 application-judgement "(convergent_nz?)" convergence_ops "analysis/") (const_fun_continuous application-judgement "continuous_fun" continuous_functions "analysis/") (derivable_const application-judgement "deriv_fun" derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (restrict const-decl "R" restrict nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (deriv_powerseq const-decl "sequence[real]" power_series_derivseq nil) (deriv_const_fun formula-decl nil derivatives "analysis/") (const_derivable_fun formula-decl nil derivatives "analysis/") (T_pred const-decl "[real -> boolean]" power_series_derivseq nil) (T formal-subtype-decl nil power_series_derivseq nil) (sequence type-eq-decl nil sequences nil) (expt_x0 formula-decl nil exponentiation 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sigma_power_derivable_TCC1 0 (sigma_power_derivable_TCC1-1 nil 3403524860 ("" (subtype-tcc) nil nil) nil nil)) (sigma_power_derivable 0 (sigma_power_derivable-3 nil 3403525533 ("" (induct "n") (("1" (skosimp*) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "powerseq") (("1" (expand "^") (("1" (expand "expt") (("1" (lemma "const_derivable_fun[T]") (("1" (inst -1 "a!1(0)") (("1" (expand "const_fun") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (lemma "sum_derivable_fun[T]") (("2" (inst -1 "(LAMBDA x: powerseq(a!1, x)(1 + j!1))" "(LAMBDA x: sigma(0, j!1, powerseq(a!1, x)))") (("2" (expand "+" -1) (("2" (assert) (("2" (hide 2) (("2" (inst?) (("2" (assert) (("2" (hide -1) (("2" (lemma "deriv_powerseq_lem") (("2" (inst?) (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sum_derivable_fun formula-decl nil derivatives "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (deriv_powerseq_lem formula-decl nil power_series_derivseq nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (^ const-decl "real" exponentiation nil) (const_derivable_fun formula-decl nil derivatives "analysis/") (expt def-decl "real" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (nat_induction formula-decl nil naturalnumbers nil) (powerseq const-decl "sequence[real]" power_series nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (derivable? const-decl "bool" derivatives "analysis/") (T formal-subtype-decl nil power_series_derivseq nil) (T_pred const-decl "[real -> boolean]" power_series_derivseq nil) (sequence type-eq-decl nil sequences nil) (pred type-eq-decl nil defined_types 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)) nil) (sigma_power_derivable-2 nil 3297176600 ("" (induct "n") (("1" (skosimp*) (("1" (expand "sigma") (("1" (expand "powerseq") (("1" (expand "^") (("1" (expand "expt") (("1" (lemma "const_derivable_fun[T]") (("1" (inst -1 "a!1(0)") (("1" (expand "const_fun") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (lemma "sum_derivable_fun[T]") (("2" (inst -1 "(LAMBDA x: powerseq(a!1, x)(1 + j!1))" "(LAMBDA x: sigma(0, j!1, powerseq(a!1, x)))") (("2" (expand "+" -1) (("2" (assert) (("2" (hide 2) (("2" (inst?) (("2" (assert) (("2" (hide -1) (("2" (lemma "deriv_powerseq_lem") (("2" (inst?) (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sum_derivable_fun formula-decl nil derivatives "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (const_derivable_fun formula-decl nil derivatives "analysis/") (powerseq const-decl "sequence[real]" power_series nil) (sigma def-decl "real" sigma "reals/")) nil) (sigma_power_derivable-1 nil 3279280814 ("" (induct "n") (("1" (skosimp*) (("1" (expand "sigma") (("1" (expand "powerseq") (("1" (expand "^") (("1" (expand "expt") (("1" (lemma "const_derivable_fun[real]") (("1" (inst -1 "a!1(0)") (("1" (expand "const_fun") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (lemma "sum_derivable_fun[real]") (("2" (inst -1 "(LAMBDA x: powerseq(a!1, x)(1 + j!1))" "(LAMBDA x: sigma(0, j!1, powerseq(a!1, x)))") (("2" (expand "+" -1) (("2" (assert) (("2" (hide 2) (("2" (inst?) (("2" (assert) (("2" (hide -1) (("2" (lemma "deriv_powerseq_lem") (("2" (inst?) (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sum_derivable_fun formula-decl nil derivatives "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (const_derivable_fun formula-decl nil derivatives "analysis/") (powerseq const-decl "sequence[real]" power_series nil) (sigma def-decl "real" sigma "reals/")) nil)) (deriv_sigma_power_TCC1 0 (deriv_sigma_power_TCC1-1 nil 3279280814 ("" (skosimp*) (("" (lemma "sigma_power_derivable") (("" (inst?) nil nil)) nil)) nil) ((sigma_power_derivable formula-decl nil power_series_derivseq 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) (sequence type-eq-decl nil sequences nil)) nil)) (deriv_sigma_power 0 (deriv_sigma_power-2 nil 3297176628 ("" (induct "n" 1) (("1" (skosimp*) (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "powerseq") (("1" (expand "deriv_powerseq") (("1" (expand "^") (("1" (expand "expt") (("1" (lemma "deriv_const_fun[T]") (("1" (expand "const_fun") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (lemma "deriv_sum_fun[T]") (("2" (inst -1 "(LAMBDA x: powerseq(a!1, x)(1 + j!1))" "(LAMBDA x: sigma(0, j!1, powerseq(a!1, x)))") (("1" (expand "+" -1) (("1" (replace -1) (("1" (hide -1) (("1" (apply-extensionality 1 :hide? t) (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "deriv_powerseq_lem") (("1" (inst?) (("1" (flatten) (("1" (replace -2) (("1" (hide -2) (("1" (expand "deriv_powerseq") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (skosimp*) (("2" (rewrite "sigma_power_derivable") nil nil)) nil)) nil) ("3" (skosimp*) (("3" (hide -1) (("3" (lemma "deriv_powerseq_lem") (("3" (inst?) (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (rewrite "sigma_power_derivable") nil nil)) nil) ("3" (hide -1 2) (("3" (lemma "deriv_powerseq_lem") (("3" (inst?) (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (rewrite "sigma_power_derivable") nil nil)) nil)) nil)) nil) ((deriv_sum_fun formula-decl nil derivatives "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (sigma_power_derivable formula-decl nil power_series_derivseq nil) (real_times_real_is_real application-judgement "real" reals nil) (deriv_powerseq_lem formula-decl nil power_series_derivseq nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (j!1 skolem-const-decl "nat" power_series_derivseq nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (a!1 skolem-const-decl "sequence[real]" power_series_derivseq nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (expt def-decl "real" exponentiation nil) (deriv_const_fun formula-decl nil derivatives "analysis/") (^ const-decl "real" exponentiation nil) (nat_induction formula-decl nil naturalnumbers nil) (deriv_powerseq const-decl "sequence[real]" power_series_derivseq nil) (deriv const-decl "[T -> real]" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types 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) (sequence type-eq-decl nil sequences nil) (T_pred const-decl "[real -> boolean]" power_series_derivseq nil) (T formal-subtype-decl nil power_series_derivseq nil) (derivable? const-decl "bool" derivatives "analysis/") (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/") (sigma def-decl "real" sigma "reals/") (powerseq const-decl "sequence[real]" power_series nil)) nil) (deriv_sigma_power-1 nil 3279280814 ("" (induct "n" 1) (("1" (skosimp*) (("1" (expand "sigma") (("1" (expand "powerseq") (("1" (expand "deriv_powerseq") (("1" (expand "^") (("1" (expand "expt") (("1" (lemma "deriv_const_fun[real]") (("1" (expand "const_fun") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (lemma "deriv_sum_fun[real]") (("2" (inst -1 "(LAMBDA x: powerseq(a!1, x)(1 + j!1))" "(LAMBDA x: sigma(0, j!1, powerseq(a!1, x)))") (("1" (expand "+" -1) (("1" (replace -1) (("1" (hide -1) (("1" (apply-extensionality 1 :hide? t) (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "deriv_powerseq_lem") (("1" (inst?) (("1" (flatten) (("1" (replace -2) (("1" (hide -2) (("1" (expand "deriv_powerseq") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (rewrite "sigma_power_derivable") nil nil)) nil) ("3" (lemma "deriv_powerseq_lem") (("3" (inst?) (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (rewrite "sigma_power_derivable") nil nil)) nil) ("3" (hide -1 2) (("3" (lemma "deriv_powerseq_lem") (("3" (inst?) (("3" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (rewrite "sigma_power_derivable") nil nil)) nil)) nil)) nil) ((deriv_sum_fun formula-decl nil derivatives "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (deriv_const_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (deriv const-decl "[T -> real]" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (sigma def-decl "real" sigma "reals/") (powerseq const-decl "sequence[real]" power_series nil)) nil)) (deriv_sigma_power_conv 0 (deriv_sigma_power_conv-1 nil 3279280814 ("" (skosimp*) (("" (lemma "deriv_powerseries_conv") (("" (inst?) (("" (replace -2) (("" (assert) (("" (inst -1 "x1!1") (("" (lemma "deriv_sigma_power") (("" (inst?) (("" (case-replace "(LAMBDA (n: nat): deriv(LAMBDA x: sigma(0, n, powerseq(a!1, x)))(x1!1)) = (LAMBDA (n: nat): (LAMBDA x: sigma(0, n, deriv_powerseq(a!1, x)))(x1!1))") (("1" (hide -1 -2) (("1" (expand "deriv_powerseq") (("1" (assert) (("1" (expand "series") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("1" (inst?) (("1" (assert) (("1" (replace -1) (("1" (hide -1 -2) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 2) (("2" (skosimp*) (("2" (rewrite "sigma_power_derivable") nil nil)) nil)) nil)) nil)) nil) ("3" (hide -1 -2 2) (("3" (skosimp*) (("3" (rewrite "sigma_power_derivable") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((deriv_powerseries_conv formula-decl nil power_series_derivseq nil) (T formal-subtype-decl nil power_series_derivseq nil) (T_pred const-decl "[real -> boolean]" power_series_derivseq nil) (sigma_power_derivable formula-decl nil power_series_derivseq nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (a!1 skolem-const-decl "sequence[real]" power_series_derivseq nil) (series const-decl "sequence[real]" series nil) (deriv_powerseq const-decl "sequence[real]" power_series_derivseq nil) (powerseq const-decl "sequence[real]" power_series nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (deriv const-decl "[T -> real]" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (= const-decl "[T, T -> boolean]" equalities nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (deriv_sigma_power formula-decl nil power_series_derivseq nil) (sequence type-eq-decl nil sequences 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)) nil)) (deriv_conv_prep_TCC1 0 (deriv_conv_prep_TCC1-1 nil 3403524860 ("" (subtype-tcc) nil nil) ((powerseries const-decl "sequence[real]" power_series nil) (series const-decl "sequence[real]" series nil) (convergence const-decl "bool" convergence_sequences "analysis/") (convergent? const-decl "bool" convergence_sequences "analysis/") (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) (conv_powerseries? const-decl "bool" power_series_conv nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (deriv_conv_prep 0 (deriv_conv_prep-1 nil 3279280814 ("" (skosimp*) (("" (lemma "deriv_powerseries_conv") (("" (inst?) (("" (replace -2) (("" (assert) (("" (expand "deriv_powerseq") (("" (inst?) (("" (expand "series") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((deriv_powerseries_conv formula-decl nil power_series_derivseq nil) (deriv_powerseq const-decl "sequence[real]" power_series_derivseq nil) (series const-decl "sequence[real]" series nil) (T_pred const-decl "[real -> boolean]" power_series_derivseq nil) (T formal-subtype-decl nil power_series_derivseq nil) (sequence type-eq-decl nil sequences 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)) nil)) (deriv_powerseq_cont 0 (deriv_powerseq_cont-2 nil 3297176902 ("" (induct "n") (("1" (expand "sigma") (("1" (expand "deriv_powerseq") (("1" (expand "sigma") (("1" (skosimp*) (("1" (lemma "const_fun_continuous[T]") (("1" (expand "const_fun") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (lemma "sum_fun_continuous[T]") (("2" (inst -1 "(LAMBDA x: deriv_powerseq(a!1, x)(1 + j!1))" "(LAMBDA x: sigma(0, j!1, deriv_powerseq(a!1, x)))") (("1" (expand "+" -1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (inst?) nil nil)) nil) ("3" (hide 2) (("3" (hide -1) (("3" (name-replace "J1" "j!1+1") (("3" (expand "deriv_powerseq") (("3" (case "J1 > 0") (("1" (assert) (("1" (lemma "prod_fun_continuous[T]") (("1" (inst -1 "(LAMBDA x: a!1(J1)*J1)" "(LAMBDA x: x ^ (J1-1))") (("1" (ground) (("1" (lemma "const_fun_continuous[T]") (("1" (expand "const_fun") (("1" (inst?) (("1" (expand "*") (("1" (case-replace "(LAMBDA x: IF J1 = 1 THEN a!1(1) ELSE a!1(J1) * x ^ (J1 - 1) * J1 ENDIF) = (LAMBDA (x_1: T): a!1(J1) * x_1 ^ (J1 - 1) * (("1" (hide 2) (("1" (apply-extensionality 1 :hide? t) (("1" (lift-if) (("1" (ground) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "x_to_n_continuous[T]") (("2" (inst?) nil nil)) nil)) nil) ("3" (lemma "const_fun_continuous[T]") (("3" (expand "const_fun") (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sum_fun_continuous judgement-tcc nil continuous_functions "analysis/") (posint nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (prod_fun_continuous judgement-tcc nil continuous_functions "analysis/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (x_to_n_continuous formula-decl nil continuous_functions "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (expt_x0 formula-decl nil exponentiation nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (J1 skolem-const-decl "posint" power_series_derivseq nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (continuous_fun nonempty-type-eq-decl nil continuous_functions "analysis/") (j!1 skolem-const-decl "nat" power_series_derivseq nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (a!1 skolem-const-decl "sequence[real]" power_series_derivseq nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (const_fun_continuous judgement-tcc nil continuous_functions "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (nat_induction formula-decl nil naturalnumbers nil) (deriv_powerseq const-decl "sequence[real]" power_series_derivseq nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (continuous? const-decl "bool" continuous_functions "analysis/") (T formal-subtype-decl nil power_series_derivseq nil) (T_pred const-decl "[real -> boolean]" power_series_derivseq nil) (sequence type-eq-decl nil sequences nil) (pred type-eq-decl nil defined_types 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)) nil) (deriv_powerseq_cont-1 nil 3279280814 ("" (induct "n") (("1" (expand "sigma") (("1" (expand "deriv_powerseq") (("1" (skosimp*) (("1" (lemma "const_fun_continuous[real]") (("1" (expand "const_fun") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "sigma" 1) (("2" (lemma "sum_fun_continuous[real]") (("2" (inst -1 "(LAMBDA x: deriv_powerseq(a!1, x)(1 + j!1))" "(LAMBDA x: sigma(0, j!1, deriv_powerseq(a!1, x)))") (("1" (expand "+" -1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (inst?) nil nil)) nil) ("3" (hide 2) (("3" (hide -1) (("3" (name-replace "J1" "j!1+1") (("3" (expand "deriv_powerseq") (("3" (case "J1 > 0") (("1" (assert) (("1" (lemma "prod_fun_continuous[real]") (("1" (inst -1 "(LAMBDA x: a!1(J1)*J1)" "(LAMBDA x: x ^ (J1-1))") (("1" (expand "*") (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (lemma "x_to_n_continuous") (("2" (inst?) nil nil)) nil)) nil) ("3" (lemma "const_fun_continuous[real]") (("3" (expand "const_fun") (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (reveal -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sum_fun_continuous judgement-tcc nil continuous_functions "analysis/") (prod_fun_continuous judgement-tcc nil continuous_functions "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (continuous_fun nonempty-type-eq-decl nil continuous_functions "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (const_fun_continuous judgement-tcc nil continuous_functions "analysis/") (sigma def-decl "real" sigma "reals/")) nil)) (lim_deriv_alt_TCC1 0 (lim_deriv_alt_TCC1-1 nil 3299583090 ("" (skosimp*) (("" (lemma "deriv_powerseries_conv") (("" (inst?) (("" (assert) (("" (inst?) (("" (lemma "end_series_conv") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((deriv_powerseries_conv formula-decl nil power_series_derivseq nil) (end_series_conv formula-decl nil series nil) (deriv_powerseq const-decl "sequence[real]" power_series_derivseq nil) (T_pred const-decl "[real -> boolean]" power_series_derivseq nil) (T formal-subtype-decl nil power_series_derivseq nil) (sequence type-eq-decl nil sequences 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)) shostak)) (lim_deriv_alt 0 (lim_deriv_alt-1 nil 3299582635 ("" (skosimp*) (("" (expand "series") (("" (case-replace "(LAMBDA (n: nat): sigma(0, n, deriv_powerseq(a!1, x!1))) = (LAMBDA (n: nat): sigma(1, n, deriv_powerseq(a!1, x!1)))") (("" (hide 2) (("" (apply-extensionality 1 :hide? t) (("" (lemma "sigma_first") (("" (inst?) (("" (assert) (("" (case "x!2 = 0") (("1" (replace -1) (("1" (expand "sigma") (("1" (expand "deriv_powerseq") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (expand "deriv_powerseq") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((series const-decl "sequence[real]" series nil) (series const-decl "sequence[real]" series nil) (sigma_first formula-decl nil sigma "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (deriv_powerseq const-decl "sequence[real]" power_series_derivseq nil) (T formal-subtype-decl nil power_series_derivseq nil) (T_pred const-decl "[real -> boolean]" power_series_derivseq nil) (sequence type-eq-decl nil sequences nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities 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)) nil)))
¤ 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.1.83Bemerkung: (vorverarbeitet am 2026-04-27) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26