| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/series/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 MB |
|
Quelle power_series_deriv.prfSprache: Lisp |
|||||||||||||||
|
(power_series_deriv (deriv_domain 0 (deriv_domain-1 nil 3472465975 ("" (lemma "connected_deriv_domain[T]") (("" (lemma "connected_domain") (("" (lemma "not_one_element") (("" (assert) nil nil)) nil)) nil)) nil) ((connected_domain formula-decl nil power_series_deriv nil) (not_one_element formula-decl nil power_series_deriv nil) (connected_deriv_domain formula-decl nil deriv_domain_def "analysis/") (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) (T_pred const-decl "[real -> boolean]" power_series_deriv nil) (T formal-subtype-decl nil power_series_deriv nil)) shostak)) (IMP_power_series_deriv_scaf_TCC1 0 (IMP_power_series_deriv_scaf_TCC1-1 nil 3471695693 ("" (lemma "connected_domain") (("" (propax) nil nil)) nil) ((connected_domain formula-decl nil power_series_deriv nil)) nil)) (IMP_power_series_deriv_scaf_TCC2 0 (IMP_power_series_deriv_scaf_TCC2-1 nil 3471698428 ("" (lemma "not_one_element") (("" (propax) nil nil)) nil) ((not_one_element formula-decl nil power_series_deriv nil)) nil)) (IMP_power_series_deriv_scaf_TCC3 0 (IMP_power_series_deriv_scaf_TCC3-1 nil 3471698428 ("" (skosimp*) (("" (lemma "open") (("" (inst?) nil nil)) nil)) nil) ((open formula-decl nil power_series_deriv 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) (T_pred const-decl "[real -> boolean]" power_series_deriv nil) (T formal-subtype-decl nil power_series_deriv nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (IMP_power_series_deriv_scaf_TCC4 0 (IMP_power_series_deriv_scaf_TCC4-1 nil 3471698428 ("" (lemma "ball") (("" (assert) nil nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (ball formula-decl nil power_series_deriv nil)) nil)) (powerseries_deriv_TCC1 0 (powerseries_deriv_TCC1-1 nil 3297517343 ("" (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_deriv nil) (T_pred const-decl "[real -> boolean]" power_series_deriv 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)) shostak)) (powerseries_deriv_TCC2 0 (powerseries_deriv_TCC2-1 nil 3297517343 ("" (skosimp*) (("" (assert) (("" (lemma "deriv_domain[T]") (("" (inst?) nil nil)) nil)) nil)) nil) ((deriv_domain formula-decl nil power_series_deriv nil)) shostak)) (powerseries_deriv_TCC3 0 (powerseries_deriv_TCC3-1 nil 3299589853 ("" (skosimp*) (("" (lemma "deriv_powerseries_conv") (("" (inst?) (("" (assert) (("" (inst?) nil nil)) nil)) nil)) nil)) nil) ((T formal-subtype-decl nil power_series_deriv nil) (T_pred const-decl "[real -> boolean]" power_series_deriv 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) (deriv_powerseries_conv 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)) shostak)) (powerseries_deriv_TCC4 0 (powerseries_deriv_TCC4-1 nil 3471698428 ("" (subtype-tcc) nil nil) ((nat nonempty-type-eq-decl nil naturalnumbers 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (l!1 skolem-const-decl "real" power_series_deriv nil) (>= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans 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_deriv nil) (T_pred const-decl "[real -> boolean]" power_series_deriv 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) (limit const-decl "real" convergence_sequences "analysis/") (fullset const-decl "set" sets nil) (adh const-decl "setof[real]" convergence_functions "analysis/") (NQ const-decl "real" derivatives_def "analysis/") (convergence const-decl "bool" convergence_functions "analysis/") (convergence const-decl "bool" lim_of_functions "analysis/") (convergent? const-decl "bool" lim_of_functions "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) nil)) (powerseries_deriv 0 (powerseries_deriv-11 nil 3445341646 ("" (skosimp*) (("" (lemma "not_one_element") (("" (lemma "connected_domain") (("" (lemma "deriv_powerseries_conv") (("" (inst?) (("" (assert) (("" (expand "conv_powerseries?") (("" (lemma "deriv_fun_def[T]") (("1" (inst?) (("1" (inst - "(LAMBDA x: limit(series(deriv_powerseq(a!1, x))))") (("1" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (name "FA" "(LAMBDA x: limit(powerseries(a!1)(x)))") (("1" (replace -1) (("1" (name "FG" "(LAMBDA x: limit(series(deriv_powerseq(a!1, x))))") (("1" (case-replace "limit(series(deriv_powerseq(a!1, x!1))) = FG(x!1)") (("1" (lemma "derivative_squeeze_delta[T]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (case-replace "(LAMBDA (h: (A[T](x!1))): (NQ(FA, x!1)(h) - FG(x!1))) = (LAMBDA (h: (A[T](x!1))): inf_sum(2,Gseq(a!1,x!1,h)))") (("1" (case "EXISTS xp: abs(xp) > abs(x!1) AND (xp >= 0 IFF x!1 >= 0)") (("1" (skosimp*) (("1" (hide -2 -3) (("1" (case "xp!1 /= 0") (("1" (flatten) (("1" (inst + "(LAMBDA (h: (A[T](x!1))): abs(h)*inf_sum(2,A2seq(a!1,x!1,xp!1)))") (("1" (split +) (("1" (name-replace "LL" "inf_sum(2, A2seq(a!1, x!1, xp!1))") (("1" (lemma "cv_scal[(A[T](x!1))]") (("1" (inst - "0" "LL" "(LAMBDA (h: (A[T](x!1))): abs(h))" "0") (("1" (expand "*") (("1" (assert) (("1" (hide 2) (("1" (hide-all-but 1) (("1" (lemma "cv_abs[(A[T](x!1))]") (("1" (inst?) (("1" (expand "restrict") (("1" (expand "abs") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "adh") (("2" (lemma "deriv_domain") (("2" (expand "deriv_domain?") (("2" (skosimp*) (("2" (inst?) (("2" (inst - x!1) (("2" (skosimp*) (("2" (inst + y!1) (("1" (hide 2) (("1" (grind) nil nil)) nil) ("2" (hide 2) (("2" (typepred "y!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "conv_series?") (("2" (lemma "A2_conv[T]") (("2" (inst - "a!1" "x!1" "xp!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("2" (inst + "abs(xp!1 - x!1)") (("1" (skosimp*) (("1" (hide -4 -5 -6 -7 -10) (("1" (case "(LAMBDA (h: (A[T](x!1))): (NQ(FA, x!1)(h) - FG(x!1)))(h!1) = (LAMBDA (h: (A[T](x!1))): inf_sum(2, Gseq(a!1, x!1, h)))(h!1)") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "inf_sum_scal") (("1" (inst?) (("1" (lemma "A2_conv[T]") (("1" (inst?) (("1" (assert) (("1" (replace -2) (("1" (hide -2) (("1" (lemma "inf_sum_le") (("1" (inst - "abs(Gseq(a!1, x!1, h!1))" "abs(h!1)*A2seq(a!1, x!1, xp!1)" "2") (("1" (split -1) (("1" (lemma "inf_sum_Gseq_abs[T]") (("1" (inst?) (("1" (inst - "x!1") (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "Gseq") (("2" (case-replace "abs(abs(LAMBDA (k): IF k < 2 THEN k * a!1(k) ELSE k * a!1(k) * GET_tk(x!1, h!1, k) ^ (k - 1) - k * a!1(k) * x!1 ^ (k - 1) ENDIF) (n!1)) = IF n!1 < 2 THEN abs(n!1 * a!1(n!1)) ELSE abs(n!1) * abs(a!1(n!1)) * abs(GET_tk(x!1, h!1, n!1) ^ (n!1 - 1) - x!1 ^ (n!1 - 1)) ENDIF") (("1" (expand "A2seq") (("1" (assert) (("1" (hide -1 -2 -5) (("1" (expand "*") (("1" (name-replace "TK" "GET_tk(x!1, h!1, n!1)") (("1" (rewrite "abs_mult") (("1" (case-replace "abs(TK ^ (n!1 - 1) - x!1 ^ (n!1 - 1)) <= abs(max(abs(x!1), abs(xp!1)) ^ (n!1 - 2)) * abs(n!1 - 1) * abs(h!1)") (("1" (mult-by -1 "abs(a!1(n!1))*abs(n!1)") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (name "MAX" "max(abs(x!1), abs(xp!1))") (("2" (replace -1) (("2" (lemma "mean_value_abs[T]") (("2" (inst - "TK" "x!1" "(LAMBDA (x:T): x^(n!1-1))") (("2" (lemma "deriv_x_to_n[T]") (("2" (inst - "(n!1-1)" "1") (("2" (assert) (("2" (flatten) (("2" (case-replace "(LAMBDA (x: T): 1 * x ^ (n!1 - 1)) = (LAMBDA (x: T): x ^ (n!1 - 1))") (("1" (hide -1) (("1" (assert) (("1" (case-replace "TK = x!1") (("1" (assert) (("1" (rewrite "abs_0") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (case-replace "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = (n!1-1)*c!1^(n!1-2)") (("1" (hide -1 -2 -3) (("1" (lemma "abs_neg") (("1" (inst - "x!1 ^ (n!1 - 1) - TK ^ (n!1 - 1)") (("1" (replace -1 - rl) (("1" (replace -4 + rl) (("1" (rewrite "abs_mult") (("1" (name-replace "NM1" "abs((n!1 - 1))") (("1" (hide -1 -4 -8 -9) (("1" (case-replace "abs(c!1 ^ (n!1 - 2)) <= abs(MAX ^ (n!1 - 2))") (("1" (case-replace "abs(x!1 - TK) <= abs(h!1)") (("1" (mult-ineq -1 -2) (("1" (mult-by -1 "NM1") (("1" (assert) nil nil)) nil) ("2" (prop) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 3) (("2" (reveal -16) (("2" (typepred "GET_tk(x!1, h!1, n!1)") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (typepred "TK") (("2" (reveal -27 -28) (("2" (case "abs(c!1) <= abs(MAX)") (("1" (lemma "both_sides_expt_pos_ge") (("1" (case-replace "n!1 = 2") (("1" (assert) nil nil) ("2" (case-replace "c!1 = 0") (("1" (lemma "zero_hat") (("1" (inst?) (("1" (replace -1) (("1" (expand "abs" 2) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (inst - "(n!1 - 2)" "abs(MAX)" "abs(c!1)") (("1" (assert) (("1" (rewrite "abs_hat") (("1" (rewrite "abs_hat") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "abs_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "abs_eq_0") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind :exclude "^") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (expand "deriv" -2) (("2" (assert) (("2" (case-replace "(LAMBDA (x_1: T): deriv((LAMBDA (x: T): x ^ (n!1 - 1)), x_1))(c!1) = (LAMBDA (x: T): (x ^ (n!1 - 2)) * n!1 - x ^ (n!1 - 2))(c!1)") (("1" (assert) nil nil) ("2" (replace -2) (("2" (propax) nil nil)) nil) ("3" (expand "derivable?" -1) (("3" (inst?) (("3" (lemma "not_one_element") (("3" (skosimp*) (("3" (lemma "deriv_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (lemma "open") (("4" (skosimp*) (("4" (lemma "deriv_domain") (("4" (inst?) (("4" (expand "deriv_domain?") (("4" (hide -1 -2 -3) (("4" (expand "derivable?" -1) (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) 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" (expand "abs" 1 2) (("2" (name-replace "GG" "GET_tk(x!1, h!1, n!1) ^ (n!1 - 1)") (("2" (name-replace "XX" "x!1 ^ (n!1 - 1)") (("2" (case-replace "a!1(n!1) * GG * n!1 - a!1(n!1) * XX * n!1 = a!1(n!1) * n!1 *(GG - XX)") (("1" (hide -1) (("1" (rewrite "abs_mult") (("1" (rewrite "abs_mult") (("1" (rewrite "abs_mult") (("1" (rewrite "abs_mult") (("1" (rewrite "abs_abs") (("1" (rewrite "abs_abs") (("1" (rewrite "abs_abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (assert) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (assert) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "convergent_scal") (("3" (inst - "abs(h!1)" "series(A2seq(a!1, x!1, xp!1), 2)") (("3" (assert) (("3" (lemma "series_m_scal") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -3) (("2" (propax) nil nil)) nil) ("3" (lemma "Gseq_conv[T]") (("3" (inst?) (("3" (inst - "x!1") (("3" (assert) (("3" (skosimp*) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (lemma "deriv_domain") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "A2_conv[T]") (("2" (inst?) (("2" (assert) (("2" (expand "conv_series?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) nil nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -) (("2" (case "x!1 >= 0") (("1" (lemma "open") (("1" (inst - "x!1") (("1" (skosimp*) (("1" (inst + "x!1 + delta!1/2") (("1" (grind) nil nil) ("2" (inst?) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "open") (("2" (inst - "x!1") (("2" (skosimp*) (("2" (inst + "x!1 - delta!1/2") (("1" (grind) nil nil) ("2" (inst - "x!1 - delta!1/2") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("1" (expand "NQ") (("1" (expand "inf_sum") (("1" (replace -2 * rl) (("1" (case-replace "(FA(x!1 + x!2) - FA(x!1)) / x!2 = inf_sum(1,(LAMBDA k: a!1(k)*(((x!1+x!2)^k - x!1^k)/x!2)))") (("1" (lemma "inf_sum_eq") (("1" (inst?) (("1" (inst - "(LAMBDA k: IF k < 2 THEN k*a!1(k) ELSE a!1(k)*k*GET_tk(x!1,x!2,k)^(k-1) ENDIF)") (("1" (assert) (("1" (assert) (("1" (split -1) (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (rewrite "lim_deriv_alt" +) (("1" (expand "inf_sum") (("1" (hide -1 -2) (("1" (rewrite "limit_diff" :dir rl) (("1" (rewrite "series_m_diff") (("1" (case-replace "series((LAMBDA k: IF k < 2 THEN k* a!1(k) ELSE k* a!1(k)* GET_tk(x!1, x!2,k) ^ (k - 1) ENDIF) - deriv_powerseq(a!1, x!1), 1) = series((LAMBDA k: IF k < 2 THEN k* a!1(k) ELSE k * a!1(k)*GET_tk(x!1, x!2,k) ^ (k - 1) ENDIF) - deriv_powerseq(a!1, x!1), 2)") (("1" (hide -1) (("1" (lemma "limit_eq_rew") (("1" (inst?) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (lemma "series_m_diff") (("2" (inst?) (("1" (replace -1 * rl) (("1" (hide -1) (("1" (lemma "convergent_diff") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (lemma "deriv_powerseries_conv[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (prop) (("1" (lemma "conv_scaf2[T]") (("1" (inst?) (("1" (inst -1 "x!1") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (lemma "end_series_conv") (("1" (inst?) (("1" (assert) (("1" (hide -2) (("1" (lemma "end_series_conv") (("1" (inst?) (("1" (assert) nil nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "end_series_conv") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "Gseq_conv[T]") (("3" (inst?) (("3" (inst - "x!1") (("3" (assert) (("3" (expand "conv_series?") (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (rewrite "series_m_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (expand "-") (("1" (expand "deriv_powerseq") (("1" (expand "Gseq") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "series") (("2" (apply-extensionality 1 :hide? t) (("1" (rewrite "sigma_first") (("1" (assert) (("1" (expand "deriv_powerseq") (("1" (assert) (("1" (expand "-") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case-replace "x!3 = 0") (("1" (expand "sigma") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (inst? -3) (("1" (assert) (("1" (lemma "end_series_conv") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "conv_scaf2[T]") (("3" (inst?) (("3" (inst - "x!1") (("3" (assert) (("3" (inst?) (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (hide 2) (("2" (lift-if) (("2" (ground) (("2" (case-replace "k!1 = 1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "conv_scaf3[T]") (("3" (inst?) (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (expand "conv_series?") (("4" (lemma "conv_scaf2[T]") (("4" (inst?) (("4" (inst - "x!1") (("4" (assert) (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -3 * rl) (("2" (expand "inf_sum") (("2" (expand "powerseries") (("2" (rewrite "limit_diff" :dir rl) (("2" (rewrite "series_diff") (("2" (expand "powerseq") (("2" (expand "-") (("2" (case-replace "(LAMBDA (x: nat): IF x = 0 THEN a!1(0) ELSE a!1(x) * (x!1 + x!2) ^ x ENDIF - IF x = 0 THEN a!1(0) ELSE a!1(x) * x!1 ^ x ENDIF) = (LAMBDA (x: nat): IF x = 0 THEN 0 ELSE a!1(x) * (x!1 + x!2) ^ x - a!1(x) * x!1 ^ x ENDIF)") (("1" (hide -1) (("1" (hide -) (("1" (lemma "limit_scal") (("1" (inst?) (("1" (inst - "1/x!2") (("1" (replace -1 * rl) (("1" (hide -1) (("1" (rewrite "series_scal") (("1" (rewrite "series_first" +) (("1" (assert) nil nil) ("2" (hide 2) (("2" (case-replace "(LAMBDA (x_1: nat): 1 / x!2 * IF x_1 = 0 THEN 0 ELSE a!1(x_1) * (x!1 + x!2) ^ x_1 - a!1(x_1) * x!1 ^ x_1 ENDIF) = (LAMBDA k: a!1(k) * (((x!1 + x!2) ^ k - x!1 ^ k) / x!2))") (("1" (hide -1) (("1" (lemma "conv_scaf3[T]") (("1" (inst?) (("1" (expand "conv_series?") (("1" (assert) (("1" (inst - "x!1") (("1" (inst - "x!2") (("1" (lemma "end_series_conv") (("1" (inst?) (("1" (assert) 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" (replace -1) (("2" (assert) nil nil)) nil)) 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) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (hide -1 -2 -3) (("3" (expand "conv_series?") (("3" (lemma "conv_scaf3[T]") (("3" (inst?) (("3" (inst - "x!1") (("3" (assert) (("3" (inst - "x!2") (("3" (expand "conv_series?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "Gseq_conv[T]") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (lemma "not_one_element") (("3" (skosimp*) (("3" (lemma "deriv_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "deriv_domain") (("3" (expand "deriv_domain?") (("3" (skosimp*) (("3" (lemma "Gseq_conv") (("3" (inst - "a!1" "x!1") (("3" (assert) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "Gseq_conv") (("4" (inst?) (("4" (assert) (("4" (skosimp*) (("4" (lemma "deriv_domain") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "not_one_element?") (("2" (propax) nil nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (assert) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "deriv_domain") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((not_one_element formula-decl nil power_series_deriv nil) (T formal-subtype-decl nil power_series_deriv nil) (T_pred const-decl "[real -> boolean]" power_series_deriv 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) (deriv_powerseries_conv formula-decl nil power_series_derivseq nil) (deriv_fun_def formula-decl nil derivatives "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (series const-decl "sequence[real]" series nil) (deriv_powerseq const-decl "sequence[real]" power_series_derivseq nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_minus_real_is_real application-judgement "real" reals nil) (derivative_squeeze_delta formula-decl nil derivatives_alt "analysis/") (Gseq const-decl "real" power_series_deriv_scaf nil) (inf_sum const-decl "real" series nil) (conv_series? const-decl "bool" series nil) (NQ const-decl "real" derivatives_def "analysis/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (A const-decl "setof[nzreal]" derivatives_def "analysis/") (setof type-eq-decl nil defined_types nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (delta!1 skolem-const-decl "posreal" power_series_deriv nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (delta!1 skolem-const-decl "posreal" power_series_deriv nil) (real_times_real_is_real application-judgement "real" reals nil) (x!1 skolem-const-decl "T" power_series_deriv nil) (xp!1 skolem-const-decl "T" power_series_deriv nil) (A2seq const-decl "real" power_series_deriv_scaf nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (Gseq_conv formula-decl nil power_series_deriv_scaf nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (inf_sum_le formula-decl nil series nil) (inf_sum_Gseq_abs formula-decl nil power_series_deriv_scaf nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal type-eq-decl nil real_types nil) (upfrom nonempty-type-eq-decl nil integers nil) (GET_tk const-decl "{tk: between[T](x, x + h) | ((x + h) ^ k - x ^ k) / h = k * tk ^ (k - 1)}" power_series_deriv_scaf nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (^ const-decl "real" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (abs_mult formula-decl nil real_props nil) (nonneg_real_max application-judgement "{z: nonneg_real | z >= x AND z >= y}" real_defs nil) (abs_0 formula-decl nil abs_lems "reals/") (open formula-decl nil power_series_deriv nil) (derivable? const-decl "bool" derivatives "analysis/") (deriv const-decl "[T -> real]" derivatives "analysis/") (minus_real_is_real application-judgement "real" reals nil) (expt def-decl "real" exponentiation nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (le_times_le_any1 formula-decl nil extra_real_props nil) (nnreal_expt application-judgement "nnreal" exponentiation nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (even_minus_even_is_even application-judgement "even_int" integers nil) (expt_x0 formula-decl nil exponentiation nil) (expt_x1 formula-decl nil exponentiation nil) (MAX skolem-const-decl "{z: nonneg_real | z >= abs(x!1) AND z >= abs(xp!1)}" power_series_deriv nil) (c!1 skolem-const-decl "T" power_series_deriv nil) (abs_hat formula-decl nil exponent_props "reals/") (abs_eq_0 formula-decl nil abs_lems "reals/") (zero_hat formula-decl nil exponent_props "reals/") (n!1 skolem-const-decl "upfrom(2)" power_series_deriv nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (both_sides_expt_pos_ge formula-decl nil exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (abs_neg formula-decl nil abs_lems "reals/") (derivable? const-decl "bool" derivatives_def "analysis/") (deriv const-decl "real" derivatives_def "analysis/") (deriv_x_to_n formula-decl nil derivatives "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (mean_value_abs formula-decl nil derivative_props "analysis/") (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (<= const-decl "bool" reals nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (abs_abs formula-decl nil real_props nil) (convergent_scal formula-decl nil convergence_ops "analysis/") (series_m_scal formula-decl nil series nil) (series const-decl "sequence[real]" series nil) (abs const-decl "sequence[real]" series nil) (inf_sum_scal formula-decl nil series nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (adh const-decl "setof[real]" convergence_functions "analysis/") (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil) (restrict const-decl "R" restrict nil) (deriv_domain formula-decl nil power_series_deriv nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (y!1 skolem-const-decl "{u: nzreal | T_pred(u + x!1)}" power_series_deriv nil) (nnreal_exp application-judgement "nnreal" exponentiation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (cv_abs formula-decl nil lim_of_functions "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (cv_scal formula-decl nil lim_of_functions "analysis/") (A2_conv formula-decl nil power_series_deriv_scaf nil) (IFF const-decl "[bool, bool -> bool]" booleans 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (lim_deriv_alt formula-decl nil power_series_derivseq nil) (series_m_diff formula-decl nil series nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (sigma_first formula-decl nil sigma "reals/") (series_m_eq formula-decl nil series nil) (conv_scaf2 formula-decl nil power_series_deriv_scaf nil) (end_series_conv formula-decl nil series nil) (convergent_diff formula-decl nil convergence_ops "analysis/") (limit_eq_rew formula-decl nil power_series_deriv_scaf nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (limit_diff formula-decl nil convergence_ops "analysis/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (conv_scaf3 formula-decl nil power_series_deriv_scaf nil) (x!2 skolem-const-decl "(A[T](x!1))" power_series_deriv nil) (inf_sum_eq formula-decl nil series nil) (series_diff formula-decl nil series nil) (limit_scal formula-decl nil convergence_ops "analysis/") (series_first formula-decl nil series nil) (series_scal formula-decl nil series nil) (powerseq const-decl "sequence[real]" power_series nil) (limit const-decl "real" convergence_sequences "analysis/") (a!1 skolem-const-decl "sequence[real]" power_series_deriv nil) (powerseries const-decl "sequence[real]" power_series nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (conv_powerseries? const-decl "bool" power_series_conv 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) (connected_domain formula-decl nil power_series_deriv nil)) nil) (powerseries_deriv-10 nil 3374403867 ("" (skosimp*) (("" (lemma "not_one_element") (("" (lemma "connected_domain") (("" (lemma "deriv_powerseries_conv") (("" (inst?) (("" (assert) (("" (expand "conv_powerseries?") (("" (lemma "deriv_fun_def[T]") (("1" (inst?) (("1" (inst - "(LAMBDA x: limit(series(deriv_powerseq(a!1, x))))") (("1" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (name "FA" "(LAMBDA x: limit(powerseries(a!1)(x)))") (("1" (replace -1) (("1" (name "FG" "(LAMBDA x: limit(series(deriv_powerseq(a!1, x))))") (("1" (case-replace "limit(series(deriv_powerseq(a!1, x!1))) = FG(x!1)") (("1" (lemma "derivative_squeeze_delta[T]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (case-replace "(LAMBDA (h: (A[T](x!1))): (NQ(FA, x!1)(h) - FG(x!1))) = (LAMBDA (h: (A[T](x!1))): inf_sum(2,Gseq(a!1,x!1,h)))") (("1" (case "EXISTS xp: abs(xp) > abs(x!1) AND (xp >= 0 IFF x!1 >= 0)") (("1" (skosimp*) (("1" (hide -2 -3) (("1" (case "xp!1 /= 0") (("1" (flatten) (("1" (inst + "(LAMBDA (h: (A[T](x!1))): abs(h)*inf_sum(2,A2seq(a!1,x!1,xp!1)))") (("1" (split +) (("1" (name-replace "LL" "inf_sum(2, A2seq(a!1, x!1, xp!1))") (("1" (lemma "cv_scal[(A[T](x!1))]") (("1" (inst - "0" "LL" "(LAMBDA (h: (A[T](x!1))): abs(h))" "0") (("1" (expand "*") (("1" (assert) (("1" (hide 2) (("1" (hide-all-but 1) (("1" (lemma "cv_abs[(A[T](x!1))]") (("1" (inst?) (("1" (expand "restrict") (("1" (expand "abs") (("1" (propax) nil nil)) nil)) nil) ("2" (lemma "adh_A_lem[T]") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "conv_series?") (("2" (lemma "A2_conv[T]") (("2" (inst - "a!1" "x!1" "xp!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("2" (inst + "abs(xp!1 - x!1)") (("1" (skosimp*) (("1" (hide -4 -5 -6 -7 -10) (("1" (case "(LAMBDA (h: (A[T](x!1))): (NQ(FA, x!1)(h) - FG(x!1)))(h!1) = (LAMBDA (h: (A[T](x!1))): inf_sum(2, Gseq(a!1, x!1, h)))(h!1)") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "inf_sum_scal") (("1" (inst?) (("1" (lemma "A2_conv[T]") (("1" (inst?) (("1" (assert) (("1" (replace -2) (("1" (hide -2) (("1" (lemma "inf_sum_le") (("1" (inst - "abs(Gseq(a!1, x!1, h!1))" "abs(h!1)*A2seq(a!1, x!1, xp!1)" "2") (("1" (split -1) (("1" (lemma "inf_sum_Gseq_abs[T]") (("1" (inst?) (("1" (inst - "x!1") (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "Gseq") (("2" (case-replace "abs(abs(LAMBDA (k): IF k < 2 THEN k * a!1(k) ELSE k * a!1(k) * GET_tk(x!1, h!1, k) ^ (k - 1) - k * a!1(k) * x!1 ^ (k - 1) ENDIF) (n!1)) = IF n!1 < 2 THEN abs(n!1 * a!1(n!1)) ELSE abs(n!1) * abs(a!1(n!1)) * abs(GET_tk(x!1, h!1, n!1) ^ (n!1 - 1) - x!1 ^ (n!1 - 1)) ENDIF") (("1" (expand "A2seq") (("1" (assert) (("1" (hide -1 -2 -5) (("1" (expand "*") (("1" (name-replace "TK" "GET_tk(x!1, h!1, n!1)") (("1" (rewrite "abs_mult") (("1" (case-replace "abs(TK ^ (n!1 - 1) - x!1 ^ (n!1 - 1)) <= abs(max(abs(x!1), abs(xp!1)) ^ (n!1 - 2)) * abs(n!1 - 1) * abs(h!1)") (("1" (mult-by -1 "abs(a!1(n!1))*abs(n!1)") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (name "MAX" "max(abs(x!1), abs(xp!1))") (("2" (replace -1) (("2" (lemma "mean_value_abs[T]") (("2" (inst - "TK" "x!1" "(LAMBDA (x:T): x^(n!1-1))") (("2" (lemma "deriv_x_to_n[T]") (("2" (inst - "(n!1-1)" "1") (("2" (assert) (("2" (flatten) (("2" (case-replace "(LAMBDA (x: T): 1 * x ^ (n!1 - 1)) = (LAMBDA (x: T): x ^ (n!1 - 1))") (("1" (hide -1) (("1" (assert) (("1" (case-replace "TK = x!1") (("1" (assert) (("1" (rewrite "abs_0") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (case-replace "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = (n!1-1)*c!1^(n!1-2)") (("1" (hide -1 -2 -3) (("1" (lemma "abs_neg") (("1" (inst - "x!1 ^ (n!1 - 1) - TK ^ (n!1 - 1)") (("1" (replace -1 - rl) (("1" (replace -4 + rl) (("1" (rewrite "abs_mult") (("1" (name-replace "NM1" "abs((n!1 - 1))") (("1" (hide -1 -4 -8 -9) (("1" (case-replace "abs(c!1 ^ (n!1 - 2)) <= abs(MAX ^ (n!1 - 2))") (("1" (case-replace "abs(x!1 - TK) <= abs(h!1)") (("1" (mult-ineq -1 -2) (("1" (mult-by -1 "NM1") (("1" (assert) nil nil)) nil) ("2" (prop) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 3) (("2" (reveal -16) (("2" (typepred "GET_tk(x!1, h!1, n!1)") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (typepred "TK") (("2" (reveal -27 -28) (("2" (case "abs(c!1) <= abs(MAX)") (("1" (lemma "both_sides_expt_pos_ge") (("1" (case-replace "n!1 = 2") (("1" (assert) nil nil) ("2" (case-replace "c!1 = 0") (("1" (lemma "zero_hat") (("1" (inst?) (("1" (replace -1) (("1" (expand "abs" 2) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (inst - "(n!1 - 2)" "abs(MAX)" "abs(c!1)") (("1" (assert) (("1" (rewrite "abs_hat") (("1" (rewrite "abs_hat") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "abs_eq_0") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "abs_eq_0") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil) ("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (grind :exclude "^") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (expand "deriv" -2) (("2" (assert) (("2" (case-replace "(LAMBDA (x_1: T): deriv((LAMBDA (x: T): x ^ (n!1 - 1)), x_1))(c!1) = (LAMBDA (x: T): (x ^ (n!1 - 2)) * n!1 - x ^ (n!1 - 2))(c!1)") (("1" (assert) nil nil) ("2" (replace -2) (("2" (propax) nil nil)) nil) ("3" (expand "derivable" -1) (("3" (inst?) (("3" (lemma "not_one_element") (("3" (skosimp*) nil nil)) nil)) nil)) nil) ("4" (lemma "open") (("4" (skosimp*) nil nil)) nil) ("5" (skosimp*) (("5" (assert) (("5" (hide-all-but (-2 1)) (("5" (expand "derivable" -1) (("5" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (apply-extensionality 1 :hide? t) 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" (expand "abs" 1 2) (("2" (name-replace "GG" "GET_tk(x!1, h!1, n!1) ^ (n!1 - 1)") (("2" (name-replace "XX" "x!1 ^ (n!1 - 1)") (("2" (case-replace "a!1(n!1) * GG * n!1 - a!1(n!1) * XX * n!1 = a!1(n!1) * n!1 *(GG - XX)") (("1" (hide -1) (("1" (rewrite "abs_mult") (("1" (rewrite "abs_mult") (("1" (rewrite "abs_mult") (("1" (rewrite "abs_mult") (("1" (rewrite "abs_abs") (("1" (rewrite "abs_abs") (("1" (rewrite "abs_abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (assert) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("5" (assert) (("5" (skosimp*) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "convergent_scal") (("3" (inst - "abs(h!1)" "series(A2seq(a!1, x!1, xp!1), 2)") (("3" (assert) (("3" (lemma "series_m_scal") (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -3) (("2" (propax) nil nil)) nil) ("3" (lemma "Gseq_conv[T]") (("3" (inst?) (("3" (inst - "x!1") (("3" (assert) (("3" (skosimp*) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) nil nil) ("5" (skosimp*) nil nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "A2_conv[T]") (("2" (inst?) (("2" (assert) (("2" (expand "conv_series?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) nil nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -) (("2" (case "x!1 >= 0") (("1" (lemma "open") (("1" (inst - "x!1") (("1" (skosimp*) (("1" (inst + "x!1 + delta!1/2") (("1" (grind) nil nil) ("2" (inst?) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "open") (("2" (inst - "x!1") (("2" (skosimp*) (("2" (inst + "x!1 - delta!1/2") (("1" (grind) nil nil) ("2" (inst - "x!1 - delta!1/2") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("1" (expand "NQ") (("1" (expand "inf_sum") (("1" (replace -2 * rl) (("1" (case-replace "(FA(x!1 + x!2) - FA(x!1)) / x!2 = inf_sum(1,(LAMBDA k: a!1(k)*(((x!1+x!2)^k - x!1^k)/x!2)))") (("1" (lemma "inf_sum_eq") (("1" (inst?) (("1" (inst - "(LAMBDA k: IF k < 2 THEN k*a!1(k) ELSE a!1(k)*k*GET_tk(x!1,x!2,k)^(k-1) ENDIF)") (("1" (assert) (("1" (assert) (("1" (split -1) (("1" (assert) (("1" (replace -1) (("1" (assert) (("1" (rewrite "lim_deriv_alt" +) (("1" (expand "inf_sum") (("1" (hide -1 -2) (("1" (rewrite "limit_diff" :dir rl) (("1" (rewrite "series_m_diff") (("1" (case-replace "series((LAMBDA k: IF k < 2 THEN k* a!1(k) ELSE k* a!1(k)* GET_tk(x!1, x!2,k) ^ (k - 1) ENDIF) - deriv_powerseq(a!1, x!1), 1) = series((LAMBDA k: IF k < 2 THEN k* a!1(k) ELSE k * a!1(k)*GET_tk(x!1, x!2,k) ^ (k - 1) ENDIF) - deriv_powerseq(a!1, x!1), 2)") (("1" (hide -1) (("1" (lemma "limit_eq_rew") (("1" (inst?) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (lemma "series_m_diff") (("2" (inst?) (("1" (replace -1 * rl) (("1" (hide -1) (("1" (lemma "convergent_diff") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (lemma "deriv_powerseries_conv[T]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (prop) (("1" (lemma "conv_scaf2[T]") (("1" (inst?) (("1" (inst -1 "x!1") (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (lemma "end_series_conv") (("1" (inst?) (("1" (assert) (("1" (hide -2) (("1" (lemma "end_series_conv") (("1" (inst?) (("1" (assert) nil nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "end_series_conv") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "Gseq_conv[T]") (("3" (inst?) (("3" (inst - "x!1") (("3" (assert) (("3" (expand "conv_series?") (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (rewrite "series_m_eq") (("1" (hide 2) (("1" (skosimp*) (("1" (expand "-") (("1" (expand "deriv_powerseq") (("1" (expand "Gseq") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "series") (("2" (apply-extensionality 1 :hide? t) (("1" (rewrite "sigma_first") (("1" (assert) (("1" (expand "deriv_powerseq") (("1" (assert) (("1" (expand "-") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case-replace "x!3 = 0") (("1" (expand "sigma") (("1" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (inst? -3) (("1" (assert) (("1" (lemma "end_series_conv") (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "conv_scaf2[T]") (("3" (inst?) (("3" (inst - "x!1") (("3" (assert) (("3" (inst?) (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (hide 2) (("2" (lift-if) (("2" (ground) (("2" (case-replace "k!1 = 1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "conv_scaf3[T]") (("3" (inst?) (("3" (inst?) (("3" (assert) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (expand "conv_series?") (("4" (lemma "conv_scaf2[T]") (("4" (inst?) (("4" (inst - "x!1") (("4" (assert) (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -3 * rl) (("2" (expand "inf_sum") (("2" (expand "powerseries") (("2" (rewrite "limit_diff" :dir rl) (("2" (rewrite "series_diff") (("2" (expand "powerseq") (("2" (expand "-") (("2" (case-replace "(LAMBDA (x: nat): IF x = 0 THEN a!1(0) ELSE a!1(x) * (x!1 + x!2) ^ x ENDIF - IF x = 0 THEN a!1(0) ELSE a!1(x) * x!1 ^ x ENDIF) = (LAMBDA (x: nat): IF x = 0 THEN 0 ELSE a!1(x) * (x!1 + x!2) ^ x - a!1(x) * x!1 ^ x ENDIF)") (("1" (hide -1) (("1" (hide -) (("1" (lemma "limit_scal") (("1" (inst?) (("1" (inst - "1/x!2") (("1" (replace -1 * rl) (("1" (hide -1) (("1" (rewrite "series_scal") (("1" (rewrite "series_first" +) (("1" (assert) nil nil) ("2" (hide 2) (("2" (case-replace "(LAMBDA (x_1: nat): 1 / x!2 * IF x_1 = 0 THEN 0 ELSE a!1(x_1) * (x!1 + x!2) ^ x_1 - a!1(x_1) * x!1 ^ x_1 ENDIF) = (LAMBDA k: a!1(k) * (((x!1 + x!2) ^ k - x!1 ^ k) / x!2))") (("1" (hide -1) (("1" (lemma "conv_scaf3[T]") (("1" (inst?) (("1" (expand "conv_series?") (("1" (assert) (("1" (inst - "x!1") (("1" (inst - "x!2") (("1" (lemma "end_series_conv") (("1" (inst?) (("1" (assert) 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" (replace -1) (("2" (assert) nil nil)) nil)) 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) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (hide -1 -2 -3) (("3" (expand "conv_series?") (("3" (lemma "conv_scaf3[T]") (("3" (inst?) (("3" (inst - "x!1") (("3" (assert) (("3" (inst - "x!2") (("3" (expand "conv_series?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (lemma "Gseq_conv[T]") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (lemma "not_one_element") (("3" (skosimp*) nil nil)) nil) ("4" (skosimp*) nil nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 2) (("3" (lemma "Gseq_conv") (("3" (inst?) (("3" (assert) (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) nil nil) ("5" (lemma "connected_domain") (("5" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (assert) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((limit const-decl "real" convergence_sequences "analysis/") (powerseq const-decl "sequence[real]" power_series nil) (series_scal formula-decl nil series nil) (series_first formula-decl nil series nil) (limit_scal formula-decl nil convergence_ops "analysis/") (series_diff formula-decl nil series nil) (inf_sum_eq formula-decl nil series nil) (conv_scaf3 formula-decl nil power_series_deriv_scaf nil) (limit_diff formula-decl nil convergence_ops "analysis/") (limit_eq_rew formula-decl nil power_series_deriv_scaf nil) (convergent_diff formula-decl nil convergence_ops "analysis/") (end_series_conv formula-decl nil series nil) (conv_scaf2 formula-decl nil power_series_deriv_scaf nil) (series_m_eq formula-decl nil series nil) (sigma_first formula-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (series_m_diff formula-decl nil series nil) (lim_deriv_alt formula-decl nil power_series_derivseq nil) (A2_conv formula-decl nil power_series_deriv_scaf nil) (cv_scal formula-decl nil lim_of_functions "analysis/") (cv_abs formula-decl nil lim_of_functions "analysis/") (adh_A_lem formula-decl nil derivatives_def "analysis/") (adh const-decl "setof[real]" convergence_functions "analysis/") (inf_sum_scal formula-decl nil series nil) (abs const-decl "sequence[real]" series nil) (series_m_scal formula-decl nil series nil) (convergent_scal formula-decl nil convergence_ops "analysis/") (mean_value_abs formula-decl nil derivative_props "analysis/") (deriv_x_to_n formula-decl nil derivatives "analysis/") (deriv const-decl "real" derivatives_def "analysis/") (abs_neg formula-decl nil abs_lems "reals/") (zero_hat formula-decl nil exponent_props "reals/") (abs_eq_0 formula-decl nil abs_lems "reals/") (abs_hat formula-decl nil exponent_props "reals/") (deriv const-decl "[T -> real]" derivatives "analysis/") (abs_0 formula-decl nil abs_lems "reals/") (GET_tk const-decl "{tk: between[T](x, x + h) | ((x + h) ^ k - x ^ k) / h = k * tk ^ (k - 1)}" power_series_deriv_scaf nil) (inf_sum_Gseq_abs formula-decl nil power_series_deriv_scaf nil) (inf_sum_le formula-decl nil series nil) (Gseq_conv formula-decl nil power_series_deriv_scaf nil) (A2seq const-decl "real" power_series_deriv_scaf nil) (A const-decl "setof[nzreal]" derivatives_def "analysis/") (NQ const-decl "real" derivatives_def "analysis/") (Gseq const-decl "real" power_series_deriv_scaf nil) (deriv_powerseq const-decl "sequence[real]" power_series_derivseq nil) (deriv_fun_def formula-decl nil derivatives "analysis/") (deriv_powerseries_conv formula-decl nil power_series_derivseq nil)) nil) (powerseries_deriv-9 nil 3299837690 ("" (skosimp*) (("" (lemma "not_one_element") (("" (lemma "connected_domain") (("" (lemma "deriv_powerseries_conv") (("" (inst?) (("" (assert) (("" (expand "conv_powerseries?") (("" (lemma "deriv_fun_def[T]") (("1" (inst?) (("1" (inst - "(LAMBDA x: limit(series(deriv_powerseq(a!1, x))))") (("1" (split -1) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (name "FA" "(LAMBDA x: limit(powerseries(a!1)(x)))") (("1" (replace -1) (("1" (name "FG" "(LAMBDA x: limit(series(deriv_powerseq(a!1, x))))") (("1" (case-replace "limit(series(deriv_powerseq(a!1, x!1))) = FG(x!1)") (("1" (lemma "derivative_squeeze_delta[T]") (("1" (inst?) (("1" (assert) (("1" (hide 2) (("1" (case-replace "(LAMBDA (h: (A[T](x!1))): (NQ(FA, x!1)(h) - FG(x!1))) = (LAMBDA (h: (A[T](x!1))): inf_sum(2,Gseq(a!1,x!1,h)))") (("1" (case "EXISTS xp: abs(xp) > abs(x!1) AND (xp >= 0 IFF x!1 >= 0)") (("1" (skosimp*) (("1" (hide -2 -3) (("1" (case "xp!1 /= 0") (("1" (flatten) (("1" (inst + "(LAMBDA (h: (A[T](x!1))): abs(h)*inf_sum(2,A2seq(a!1,x!1,xp!1)))") (("1" (split +) (("1" (name-replace "LL" "inf_sum(2, A2seq(a!1, x!1, xp!1))") (("1" (lemma "cv_scal[(A[T](x!1))]") (("1" (inst - "0" "LL" "(LAMBDA (h: (A[T](x!1))): abs(h))" "0") (("1" (expand "*") (("1" (assert) (("1" (hide 2) (("1" (hide-all-but 1) (("1" (lemma "cv_abs[(A[T](x!1))]") (("1" (inst?) (("1" (expand "restrict") (("1" (expand "abs") (("1" (propax) nil nil)) nil)) nil) ("2" (lemma "adh_A_lem[T]") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) nil nil) ("3" (skosimp*) nil nil)) nil) ("2" (hide 2) (("2" (expand "conv_series?") (("2" (lemma "A2_conv[T]") (("2" (inst - "a!1" "x!1" "xp!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("2" (inst + "abs(xp!1 - x!1)") (("1" (skosimp*) (("1" (hide -4 -5 -6 -7 -10) (("1" (case "(LAMBDA (h: (A[T](x!1))): (NQ(FA, x!1)(h) - FG(x!1)))(h!1) = (LAMBDA (h: (A[T](x!1))): inf_sum(2, Gseq(a!1, x!1, h)))(h!1)") (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "inf_sum_scal") (("1" (inst?) (("1" (lemma "A2_conv[T]") (("1" (inst?) (("1" (assert) (("1" (replace -2) (("1" (hide -2) (("1" (lemma "inf_sum_le") (("1" (inst - "abs(Gseq(a!1, x!1, h!1))" "abs(h!1)*A2seq(a!1, x!1, xp!1)" "2") (("1" (split -1) (("1" (lemma "inf_sum_Gseq_abs[T]") (("1" (inst?) (("1" (inst - "x!1") (("1" (assert) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (expand "Gseq") (("2" (case-replace "abs(abs(LAMBDA (k): IF k < 2 THEN k * a!1(k) ELSE k * a!1(k) * GET_tk(x!1, h!1, k) ^ (k - 1) - k * a!1(k) * x!1 ^ (k - 1) ENDIF) (n!1)) = IF n!1 < 2 THEN abs(n!1 * a!1(n!1)) ELSE abs(n!1) * abs(a!1(n!1)) * abs(GET_tk(x!1, h!1, n!1) ^ (n!1 - 1) - x!1 ^ (n!1 - 1)) ENDIF") (("1" (expand "A2seq") (("1" (assert) (("1" (hide -1 -2 -5) (("1" (expand "*") (("1" (name-replace "TK" "GET_tk(x!1, h!1, n!1)") (("1" (rewrite "abs_mult") (("1" (case-replace "abs(TK ^ (n!1 - 1) - x!1 ^ (n!1 - 1)) <= abs(max(abs(x!1), abs(xp!1)) ^ (n!1 - 2)) * abs(n!1 - 1) * abs(h!1)") (("1" (mult-by -1 "abs(a!1(n!1))*abs(n!1)") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (name "MAX" "max(abs(x!1), abs(xp!1))") (("2" (replace -1) (("2" (lemma "mean_value_abs[T]") (("2" (inst - "TK" "x!1" "(LAMBDA (x:T): x^(n!1-1))") (("2" (lemma "deriv_x_to_n[T]") (("2" (inst - "(n!1-1)" "1") (("2" (assert) (("2" (flatten) (("2" (case-replace "(LAMBDA (x: T): 1 * x ^ (n!1 - 1)) = (LAMBDA (x: T): x ^ (n!1 - 1))") (("1" (hide -1) (("1" (assert) (("1" (case-replace "TK = x!1") (("1" (assert) (("1" (rewrite "abs_0") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (case-replace "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = (n!1-1)*c!1^(n!1-2)") (("1" (hide -1 -2 -3) (("1" (lemma "abs_neg") (("1" (inst - "x!1 ^ (n!1 - 1) - TK ^ (n!1 - 1)") (("1" (replace -1 - rl) (("1" (replace -4 + rl) (("1" (rewrite "abs_mult") (("1" (name-replace "NM1" "abs((n!1 - 1))") (("1" (hide -1 -4 -8 -9) (("1" (case-replace "abs(c!1 ^ (n!1 - 2)) <= abs(MAX ^ (n!1 - 2))") (("1" (case-replace "abs(x!1 - TK) <= abs(h!1)") (("1" (mult-ineq -1 -2) (("1" (mult-by -1 "NM1") (("1" (assert) nil nil)) nil) ("2" (prop) (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide -1 -2 -3 3) (("2" (reveal -16) (("2" (typepred "GET_tk(x!1, h!1, n!1)") (("2" (grind) --> -------------------- --> maximum size reached --> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.660Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-01) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26