(power_series_derivnil 3472465975"" (lemma "connected_deriv_domain[T]" )"" (lemma "connected_domain" )"" (lemma "not_one_element" ) (("" (assert ) nil nil )) nil ))nil ))nil )nil power_series_deriv nil )nil power_series_deriv nil )nil deriv_domain_def"analysis/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" power_series_deriv nil )nil power_series_deriv nil ))nil 3471695693"" (lemma "connected_domain" ) (("" (propax) nil nil )) nil )nil power_series_deriv nil )) nil ))nil 3471698428"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil power_series_deriv nil )) nil ))nil 3471698428"" (skosimp*) (("" (lemma "open" ) (("" (inst?) nil nil )) nil )) nil )nil power_series_deriv nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" power_series_deriv nil )nil power_series_deriv nil )"real" reals nil ))nil ))nil 3471698428"" (lemma "ball" ) (("" (assert ) nil nil )) nil )"real" reals nil )nil power_series_deriv nil ))nil ))nil 3297517343 ("" (subtype-tcc) nil nil )"sequence[real]" power_series nil )"sequence[real]" series nil )"bool" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )nil power_series_deriv nil )"[real -> boolean]" power_series_deriv nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" power_series_conv nil )"real" reals nil ))nil 3297517343"" (skosimp*)"" (assert )"" (lemma "deriv_domain[T]" ) (("" (inst?) nil nil )) nil )) nil ))nil )nil power_series_deriv nil )) shostak))nil 3299589853"" (skosimp*)"" (lemma "deriv_powerseries_conv" )"" (inst?) (("" (assert ) (("" (inst?) nil nil )) nil )) nil ))nil ))nil )nil power_series_deriv nil )"[real -> boolean]" power_series_deriv nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil power_series_derivseq nil )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil ))nil 3471698428 ("" (subtype-tcc) nil nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"odd_int" integers nil )nil real_types nil )nil real_types nil )"bool" reals nil )"real" power_series_deriv nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"sequence[real]" power_series nil )"sequence[real]" series nil )"bool" convergence_sequences "analysis/" )"bool" convergence_sequences "analysis/" )nil power_series_deriv nil )"[real -> boolean]" power_series_deriv nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"bool" power_series_conv nil )"real" convergence_sequences "analysis/" )"set" sets nil )"setof[real]" convergence_functions "analysis/" )"real" derivatives_def "analysis/" )"bool" convergence_functions "analysis/" )"bool" lim_of_functions "analysis/" )"bool" lim_of_functions "analysis/" )"bool" derivatives_def "analysis/" )"bool" derivatives "analysis/" )"real" reals nil )"real" reals nil ))nil ))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" "(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" "FA" "(LAMBDA x: limit(powerseries(a!1)(x)))" )"1" replace -1)"1" "FG" "(LAMBDA x: limit(series(deriv_powerseq(a!1, x))))" )"1" "limit(series(deriv_powerseq(a!1, x!1))) = FG(x!1)" )"1" "derivative_squeeze_delta[T]" )"1" "1" assert )"1" "1" "(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" "1" "1" case "xp!1 /= 0" )"1" "1" "(LAMBDA (h: (A[T](x!1))): abs(h)*inf_sum(2,A2seq(a!1,x!1,xp!1)))" )"1" "1" "LL" "inf_sum(2, A2seq(a!1, x!1, xp!1))" )"1" "cv_scal[(A[T](x!1))]" )"1" "0" "LL" "(LAMBDA (h: (A[T](x!1))): abs(h))" "0" )"1" expand "*" )"1" assert )"1" "1" "1" "cv_abs[(A[T](x!1))]" )"1" "1" expand "restrict" )"1" expand "abs" )"1" nil nil ))nil ))nil )"2" expand "adh" )"2" "deriv_domain" )"2" expand "deriv_domain?" )"2" "2" "2" "2" "2" "1" "1" nil nil ))nil )"2" "2" "y!1" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "conv_series?" )"2" "A2_conv[T]" )"2" "a!1" "x!1" "xp!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )nil nil ))nil )"2" "abs(xp!1 - x!1)" )"1" "1" "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" "inf_sum_scal" )"1" "1" "A2_conv[T]" )"1" "1" assert )"1" replace "1" "1" "inf_sum_le" )"1" "abs(Gseq(a!1, x!1, h!1))" "abs(h!1)*A2seq(a!1, x!1, xp!1)" "2" )"1" "1" "inf_sum_Gseq_abs[T]" )"1" "1" "x!1" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "Gseq" )"2" "abs(abs(LAMBDA (k): IF k < 2 THEN k * a!1(k)IF n!1 < 2 THEN abs(n!1 * a!1(n!1))") "1" expand "A2seq" )"1" assert )"1" "1" expand "*" )"1" "TK" "GET_tk(x!1, h!1, n!1)" )"1" rewrite "abs_mult" )"1" "abs(TK ^ (n!1 - 1) - x!1 ^ (n!1 - 1)) <= max (abs(x!1), abs(xp!1)) ^ (n!1 - 2)) * abs(n!1 - 1) * abs(h!1)") "1" "abs(a!1(n!1))*abs(n!1)" )"1" assert )nil nil ))nil )"2" "2" "MAX" "max(abs(x!1), abs(xp!1))" )"2" replace "2" "mean_value_abs[T]" )"2" "TK" "x!1" "(LAMBDA (x:T): x^(n!1-1))" )"2" "deriv_x_to_n[T]" )"2" "(n!1-1)" "1" )"2" assert )"2" "2" "(LAMBDA (x: T): 1 * x ^ (n!1 - 1)) = (LAMBDA (x: T): x ^ (n!1 - 1))" )"1" "1" assert )"1" "TK = x!1" )"1" assert )"1" rewrite "abs_0" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "2" "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = ") "1" "1" "abs_neg" )"1" "x!1 ^ (n!1 - 1) - TK ^ (n!1 - 1)" )"1" replace "1" replace "1" rewrite "abs_mult" )"1" "NM1" "abs((n!1 - 1))" )"1" "1" "abs(c!1 ^ (n!1 - 2)) <= abs(MAX ^ (n!1 - 2))" )"1" "abs(x!1 - TK) <= abs(h!1)" )"1" "1" "NM1" )"1" assert )nil nil ))nil )"2" "1" "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" "2" "2" "GET_tk(x!1, h!1, n!1)" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "TK" )"2" "2" case "abs(c!1) <= abs(MAX)" )"1" "both_sides_expt_pos_ge" )"1" "n!1 = 2" )"1" assert )nil nil )"2" "c!1 = 0" )"1" "zero_hat" )"1" "1" replace "1" expand "abs" "1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "(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" "abs_eq_0" )"2" "2" assert )nil nil ))nil ))nil )"3" "abs_eq_0" )"3" "3" assert )nil nil ))nil ))nil )"4" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "^" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "deriv" "2" assert )"2" "(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" nil nil ))nil )"3" expand "derivable?" "3" "3" "not_one_element" )"3" "3" "deriv_domain" )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"4" "open" )"4" "4" "deriv_domain" )"4" "4" expand "deriv_domain?" )"4" "4" expand "derivable?" "4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "abs" "2" "GG" "GET_tk(x!1, h!1, n!1) ^ (n!1 - 1)" )"2" "XX" "x!1 ^ (n!1 - 1)" )"2" "a!1(n!1) * GG * n!1 - a!1(n!1) * XX * n!1 = ") "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" "3" assert )nil nil ))nil ))nil )"4" assert )"4" "4" assert )nil nil ))nil ))nil )"5" assert )"5" "5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "convergent_scal" )"3" "abs(h!1)" "series(A2seq(a!1, x!1, xp!1), 2)" )"3" assert )"3" "series_m_scal" )"3" "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 "2" nil nil ))nil )"3" "Gseq_conv[T]" )"3" "3" "x!1" )"3" assert )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "deriv_domain" )"4" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" "2" "A2_conv[T]" )"2" "2" assert )"2" expand "conv_series?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "x!1 >= 0" )"1" "open" )"1" "x!1" )"1" "1" "x!1 + delta!1/2" )"1" nil nil )"2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "open" )"2" "x!1" )"2" "2" "x!1 - delta!1/2" )"1" nil nil )"2" "x!1 - delta!1/2" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "NQ" )"1" expand "inf_sum" )"1" replace "1" "(FA(x!1 + x!2) - FA(x!1)) / x!2 = LAMBDA k:") "1" "inf_sum_eq" )"1" "1" "(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" "1" assert )"1" replace "1" assert )"1" rewrite "lim_deriv_alt" "1" expand "inf_sum" )"1" "1" rewrite "limit_diff" "1" rewrite "series_m_diff" )"1" "series((LAMBDA k: IF k < 2 THEN k* a!1(k)LAMBDA k:IF k < 2 THEN k* a!1(k)") "1" "1" "limit_eq_rew" )"1" "1" "1" nil nil )"2" "2" "series_m_diff" )"2" "1" replace "1" "1" "convergent_diff" )"1" "1" assert )"1" "1" "deriv_powerseries_conv[T]" )"1" "1" assert )"1" "1" "1" "conv_scaf2[T]" )"1" "1" "x!1" )"1" assert )"1" "1" assert )"1" "end_series_conv" )"1" "1" assert )"1" "1" "end_series_conv" )"1" "1" assert )nil nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "end_series_conv" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "Gseq_conv[T]" )"3" "3" "x!1" )"3" assert )"3" expand "conv_series?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" rewrite "series_m_eq" )"1" "1" "1" expand "-" )"1" expand "deriv_powerseq" )"1" expand "Gseq" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "series" )"2" "1" rewrite "sigma_first" )"1" assert )"1" expand "deriv_powerseq" )"1" assert )"1" expand "-" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "x!3 = 0" )"1" expand "sigma" )"1" nil nil ))nil )"2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil )"2" "2" "1" assert )"1" "end_series_conv" )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "conv_scaf2[T]" )"3" "3" "x!1" )"3" assert )"3" "1" "1" assert )nil nil ))nil )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "2" "2" "k!1 = 1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "conv_scaf3[T]" )"3" "3" "3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" expand "conv_series?" )"4" "conv_scaf2[T]" )"4" "4" "x!1" )"4" assert )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" expand "inf_sum" )"2" expand "powerseries" )"2" rewrite "limit_diff" "2" rewrite "series_diff" )"2" expand "powerseq" )"2" expand "-" )"2" "(LAMBDA (x: nat): IF x = 0 THEN a!1(0)IF x = 0 THEN a!1(0) ELSE a!1(x) * x!1 ^ x ENDIF) =LAMBDA (x: nat):IF x = 0 THEN 0") "1" "1" "1" "limit_scal" )"1" "1" "1/x!2" )"1" replace "1" "1" rewrite "series_scal" )"1" rewrite "series_first" "1" assert )nil nil )"2" "2" "(LAMBDA (x_1: nat): IF x_1 = 0 THEN 0LAMBDA k:") "1" "1" "conv_scaf3[T]" )"1" "1" expand "conv_series?" )"1" assert )"1" "x!1" )"1" "x!2" )"1" "end_series_conv" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "conv_series?" )"3" "conv_scaf3[T]" )"3" "3" "x!1" )"3" assert )"3" "x!2" )"3" expand "conv_series?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "Gseq_conv[T]" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "not_one_element" )"3" "3" "deriv_domain" )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "deriv_domain" )"3" expand "deriv_domain?" )"3" "3" "Gseq_conv" )"3" "a!1" "x!1" )"3" assert )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "Gseq_conv" )"4" "4" assert )"4" "4" "deriv_domain" )"4" 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 )nil power_series_deriv nil )nil power_series_deriv nil )"[real -> boolean]" power_series_deriv nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil power_series_derivseq nil )nil derivatives "analysis/" )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )"sequence[real]" series nil )"sequence[real]" power_series_derivseqnil )"[T, T -> boolean]" equalities nil )"real" reals nil )nil derivatives_alt"analysis/" )"real" power_series_deriv_scaf nil )"real" series nil )"bool" series nil )"real" derivatives_def "analysis/" )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"setof[nzreal]" derivatives_def "analysis/" )nil defined_types nil )nil reals nil )"boolean" notequal nil )"posreal" nil )"posreal" power_series_deriv nil )"nzreal" nil )"posreal" power_series_deriv nil )"real" reals nil )"T" power_series_deriv nil )"T" power_series_deriv nil )"real" power_series_deriv_scaf nil )"[numfield, numfield -> numfield]" number_fields nil )nil power_series_deriv_scaf nil )"(total_order?[real])" nil )nil series nil )nil power_series_deriv_scaf nil )"(total_order?[real])" nil )nil real_types nil )nil integers nil )"{tk: between[T](x, x + h) | ((x + h) ^ k - x ^ k) / h = k * tk ^ (k - 1)}" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil integers nil )nil integers nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"int" integers nil )"nnreal" nil )"{j: posint | j >= i}" nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )nil real_props nil )"{z: nonneg_real | z >= x AND z >= y}" real_defs nil )nil abs_lems "reals/" )nil power_series_deriv nil )"bool" derivatives "analysis/" )"[T -> real]" derivatives "analysis/" )"real" reals nil )"real" exponentiation nil )"real" reals nil )nil extra_real_props nil )"nnreal" exponentiation nil )"odd_int" integersnil )"even_int" integersnil )nil exponentiation nil )nil exponentiation nil )MAX skolem-const-decl"{z: nonneg_real | z >= abs(x!1) AND z >= abs(xp!1)}" nil )"T" power_series_deriv nil )nil exponent_props "reals/" )nil abs_lems "reals/" )nil exponent_props "reals/" )"upfrom(2)" power_series_deriv nil )"nnrat" exponentiation nil )nil exponentiation nil )"odd_int" integers nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil abs_lems "reals/" )"bool" derivatives_def "analysis/" )"real" derivatives_def "analysis/" )nil derivatives "analysis/" )"bool" deriv_domain_def "analysis/" )nil derivative_props "analysis/" )nil extra_real_propsnil )"bool" reals nil )"{j: nonneg_int | j >= i}" nil )nil real_props nil )nil convergence_ops "analysis/" )nil series nil )"sequence[real]" series nil )"sequence[real]" series nil )nil series nil )"[bool, bool -> bool]" booleans nil )"{y: posreal | y >= x}" nil )"(strict_total_order?[real])" real_props nil )"setof[real]" convergence_functions "analysis/" )set type-eq-decl nil sets nil ) (fullset const-decl "set" sets nil )"R" restrict nil )nil power_series_deriv nil )"[numfield, numfield -> numfield]" number_fields nil )"{u: nzreal | T_pred(u + x!1)}" nil )"nnreal" exponentiation nil )"(strict_total_order?[real])" real_props nil )"nzreal" real_typesnil )NOT const-decl "[bool -> bool]" booleans nil )nil real_types nil )"real" reals nil )nil lim_of_functions "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil lim_of_functions "analysis/" )nil power_series_deriv_scaf nil )"[bool, bool -> bool]" booleans nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil real_types nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil power_series_derivseq nil )nil series nil )nil sigma "reals/" )nil sigma "reals/" )"real" sigma "reals/" )"posint" nil )"even_int" integersnil )nil sigma "reals/" )nil series nil )nil power_series_deriv_scaf nil )nil series nil )nil convergence_ops "analysis/" )nil power_series_deriv_scaf nil )"[T -> real]" real_fun_ops "reals/" )nil convergence_ops "analysis/" )"nzreal" nil )nil power_series_deriv_scaf nil )"(A[T](x!1))" power_series_deriv nil )nil series nil )nil series nil )nil convergence_ops "analysis/" )nil series nil )nil series nil )"sequence[real]" power_series nil )"real" convergence_sequences "analysis/" )"sequence[real]" power_series_deriv nil )"sequence[real]" power_series nil )"bool" convergence_sequences "analysis/" )"bool" power_series_conv nil )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil power_series_deriv nil ))nil )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" "(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" "FA" "(LAMBDA x: limit(powerseries(a!1)(x)))" )"1" replace -1)"1" "FG" "(LAMBDA x: limit(series(deriv_powerseq(a!1, x))))" )"1" "limit(series(deriv_powerseq(a!1, x!1))) = FG(x!1)" )"1" "derivative_squeeze_delta[T]" )"1" "1" assert )"1" "1" "(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" "1" "1" case "xp!1 /= 0" )"1" "1" "(LAMBDA (h: (A[T](x!1))): abs(h)*inf_sum(2,A2seq(a!1,x!1,xp!1)))" )"1" "1" "LL" "inf_sum(2, A2seq(a!1, x!1, xp!1))" )"1" "cv_scal[(A[T](x!1))]" )"1" "0" "LL" "(LAMBDA (h: (A[T](x!1))): abs(h))" "0" )"1" expand "*" )"1" assert )"1" "1" "1" "cv_abs[(A[T](x!1))]" )"1" "1" expand "restrict" )"1" expand "abs" )"1" nil nil ))nil ))nil )"2" "adh_A_lem[T]" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "conv_series?" )"2" "A2_conv[T]" )"2" "a!1" "x!1" "xp!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )nil nil ))nil )"2" "abs(xp!1 - x!1)" )"1" "1" "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" "inf_sum_scal" )"1" "1" "A2_conv[T]" )"1" "1" assert )"1" replace "1" "1" "inf_sum_le" )"1" "abs(Gseq(a!1, x!1, h!1))" "abs(h!1)*A2seq(a!1, x!1, xp!1)" "2" )"1" "1" "inf_sum_Gseq_abs[T]" )"1" "1" "x!1" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "Gseq" )"2" "abs(abs(LAMBDA (k): IF k < 2 THEN k * a!1(k)IF n!1 < 2 THEN abs(n!1 * a!1(n!1))") "1" expand "A2seq" )"1" assert )"1" "1" expand "*" )"1" "TK" "GET_tk(x!1, h!1, n!1)" )"1" rewrite "abs_mult" )"1" "abs(TK ^ (n!1 - 1) - x!1 ^ (n!1 - 1)) <= max (abs(x!1), abs(xp!1)) ^ (n!1 - 2)) * abs(n!1 - 1) * abs(h!1)") "1" "abs(a!1(n!1))*abs(n!1)" )"1" assert )nil nil ))nil )"2" "2" "MAX" "max(abs(x!1), abs(xp!1))" )"2" replace "2" "mean_value_abs[T]" )"2" "TK" "x!1" "(LAMBDA (x:T): x^(n!1-1))" )"2" "deriv_x_to_n[T]" )"2" "(n!1-1)" "1" )"2" assert )"2" "2" "(LAMBDA (x: T): 1 * x ^ (n!1 - 1)) = (LAMBDA (x: T): x ^ (n!1 - 1))" )"1" "1" assert )"1" "TK = x!1" )"1" assert )"1" rewrite "abs_0" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "2" "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = ") "1" "1" "abs_neg" )"1" "x!1 ^ (n!1 - 1) - TK ^ (n!1 - 1)" )"1" replace "1" replace "1" rewrite "abs_mult" )"1" "NM1" "abs((n!1 - 1))" )"1" "1" "abs(c!1 ^ (n!1 - 2)) <= abs(MAX ^ (n!1 - 2))" )"1" "abs(x!1 - TK) <= abs(h!1)" )"1" "1" "NM1" )"1" assert )nil nil ))nil )"2" "1" "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" "2" "2" "GET_tk(x!1, h!1, n!1)" )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "TK" )"2" "2" case "abs(c!1) <= abs(MAX)" )"1" "both_sides_expt_pos_ge" )"1" "n!1 = 2" )"1" assert )nil nil )"2" "c!1 = 0" )"1" "zero_hat" )"1" "1" replace "1" expand "abs" "1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "(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" "abs_eq_0" )"2" "2" assert )nil nil ))nil ))nil )"3" "abs_eq_0" )"3" "3" assert )nil nil ))nil ))nil )"4" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "^" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "deriv" "2" assert )"2" "(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" nil nil ))nil )"3" expand "derivable" "3" "3" "not_one_element" )"3" nil nil ))nil ))nil ))nil )"4" "open" )"4" nil nil ))nil )"5" "5" assert )"5" "5" expand "derivable" "5" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "abs" "2" "GG" "GET_tk(x!1, h!1, n!1) ^ (n!1 - 1)" )"2" "XX" "x!1 ^ (n!1 - 1)" )"2" "a!1(n!1) * GG * n!1 - a!1(n!1) * XX * n!1 = ") "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" "3" assert )nil nil ))nil ))nil )"4" assert )"4" "4" assert )nil nil ))nil ))nil )"5" assert )"5" "5" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "convergent_scal" )"3" "abs(h!1)" "series(A2seq(a!1, x!1, xp!1), 2)" )"3" assert )"3" "series_m_scal" )"3" "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 "2" nil nil ))nil )"3" "Gseq_conv[T]" )"3" "3" "x!1" )"3" assert )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"4" nil nil )"5" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" "2" "A2_conv[T]" )"2" "2" assert )"2" expand "conv_series?" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"3" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" case "x!1 >= 0" )"1" "open" )"1" "x!1" )"1" "1" "x!1 + delta!1/2" )"1" nil nil )"2" "2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "open" )"2" "x!1" )"2" "2" "x!1 - delta!1/2" )"1" nil nil )"2" "x!1 - delta!1/2" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" expand "NQ" )"1" expand "inf_sum" )"1" replace "1" "(FA(x!1 + x!2) - FA(x!1)) / x!2 = LAMBDA k:") "1" "inf_sum_eq" )"1" "1" "(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" "1" assert )"1" replace "1" assert )"1" rewrite "lim_deriv_alt" "1" expand "inf_sum" )"1" "1" rewrite "limit_diff" "1" rewrite "series_m_diff" )"1" "series((LAMBDA k: IF k < 2 THEN k* a!1(k)LAMBDA k:IF k < 2 THEN k* a!1(k)") "1" "1" "limit_eq_rew" )"1" "1" "1" nil nil )"2" "2" "series_m_diff" )"2" "1" replace "1" "1" "convergent_diff" )"1" "1" assert )"1" "1" "deriv_powerseries_conv[T]" )"1" "1" assert )"1" "1" "1" "conv_scaf2[T]" )"1" "1" "x!1" )"1" assert )"1" "1" assert )"1" "end_series_conv" )"1" "1" assert )"1" "1" "end_series_conv" )"1" "1" assert )nil nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "end_series_conv" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "Gseq_conv[T]" )"3" "3" "x!1" )"3" assert )"3" expand "conv_series?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" rewrite "series_m_eq" )"1" "1" "1" expand "-" )"1" expand "deriv_powerseq" )"1" expand "Gseq" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "series" )"2" "1" rewrite "sigma_first" )"1" assert )"1" expand "deriv_powerseq" )"1" assert )"1" expand "-" )"1" nil nil ))nil ))nil ))nil ))nil )"2" "x!3 = 0" )"1" expand "sigma" )"1" nil nil ))nil )"2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" assert )nil nil ))nil )"4" "4" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil )"2" "2" "1" assert )"1" "end_series_conv" )"1" "1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "3" "conv_scaf2[T]" )"3" "3" "x!1" )"3" assert )"3" "1" "1" assert )nil nil ))nil )"2" assert )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "2" "2" "2" "k!1 = 1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "conv_scaf3[T]" )"3" "3" "3" assert )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"4" "4" expand "conv_series?" )"4" "conv_scaf2[T]" )"4" "4" "x!1" )"4" assert )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil )"3" "3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" expand "inf_sum" )"2" expand "powerseries" )"2" rewrite "limit_diff" "2" rewrite "series_diff" )"2" expand "powerseq" )"2" expand "-" )"2" "(LAMBDA (x: nat): IF x = 0 THEN a!1(0)IF x = 0 THEN a!1(0) ELSE a!1(x) * x!1 ^ x ENDIF) =LAMBDA (x: nat):IF x = 0 THEN 0") "1" "1" "1" "limit_scal" )"1" "1" "1/x!2" )"1" replace "1" "1" rewrite "series_scal" )"1" rewrite "series_first" "1" assert )nil nil )"2" "2" "(LAMBDA (x_1: nat): IF x_1 = 0 THEN 0LAMBDA k:") "1" "1" "conv_scaf3[T]" )"1" "1" expand "conv_series?" )"1" assert )"1" "x!1" )"1" "x!2" )"1" "end_series_conv" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "2" replace "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" "3" expand "conv_series?" )"3" "conv_scaf3[T]" )"3" "3" "x!1" )"3" assert )"3" "x!2" )"3" expand "conv_series?" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "Gseq_conv[T]" )"2" "2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" "not_one_element" )"3" nil nil ))nil )"4" nil nil ))nil ))nil )"3" "3" "3" "Gseq_conv" )"3" "3" assert )"3" nil nil ))nil ))nil ))nil ))nil ))nil )"4" (skosimp*) nil nil )"5" "connected_domain" )"5" 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 )"real" convergence_sequences "analysis/" )"sequence[real]" power_series nil )nil series nil )nil series nil )nil convergence_ops "analysis/" )nil series nil )nil series nil )nil power_series_deriv_scaf nil )nil convergence_ops "analysis/" )nil power_series_deriv_scaf nil )nil convergence_ops "analysis/" )nil series nil )nil power_series_deriv_scaf nil )nil series nil )nil sigma "reals/" )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )nil series nil )nil power_series_derivseq nil )nil power_series_deriv_scaf nil )nil lim_of_functions "analysis/" )nil lim_of_functions "analysis/" )nil derivatives_def "analysis/" )"setof[real]" convergence_functions "analysis/" )nil series nil )"sequence[real]" series nil )nil series nil )nil convergence_ops "analysis/" )nil derivative_props "analysis/" )nil derivatives "analysis/" )"real" derivatives_def "analysis/" )nil abs_lems "reals/" )nil exponent_props "reals/" )nil abs_lems "reals/" )nil exponent_props "reals/" )"[T -> real]" derivatives "analysis/" )nil abs_lems "reals/" )"{tk: between[T](x, x + h) | ((x + h) ^ k - x ^ k) / h = k * tk ^ (k - 1)}" nil )nil power_series_deriv_scaf nil )nil series nil )nil power_series_deriv_scaf nil )"real" power_series_deriv_scaf nil )"setof[nzreal]" derivatives_def "analysis/" )"real" derivatives_def "analysis/" )"real" power_series_deriv_scaf nil )"sequence[real]" power_series_derivseqnil )nil derivatives "analysis/" )nil power_series_derivseqnil ))nil )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" "(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" "FA" "(LAMBDA x: limit(powerseries(a!1)(x)))" )"1" replace -1)"1" "FG" "(LAMBDA x: limit(series(deriv_powerseq(a!1, x))))" )"1" "limit(series(deriv_powerseq(a!1, x!1))) = FG(x!1)" )"1" "derivative_squeeze_delta[T]" )"1" "1" assert )"1" "1" "(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" "1" "1" case "xp!1 /= 0" )"1" "1" "(LAMBDA (h: (A[T](x!1))): abs(h)*inf_sum(2,A2seq(a!1,x!1,xp!1)))" )"1" "1" "LL" "inf_sum(2, A2seq(a!1, x!1, xp!1))" )"1" "cv_scal[(A[T](x!1))]" )"1" "0" "LL" "(LAMBDA (h: (A[T](x!1))): abs(h))" "0" )"1" expand "*" )"1" assert )"1" "1" "1" "cv_abs[(A[T](x!1))]" )"1" "1" expand "restrict" )"1" expand "abs" )"1" nil nil ))nil ))nil )"2" "adh_A_lem[T]" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil )"2" "2" expand "conv_series?" )"2" "A2_conv[T]" )"2" "a!1" "x!1" "xp!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" assert )nil nil ))nil )"2" "abs(xp!1 - x!1)" )"1" "1" "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" "inf_sum_scal" )"1" "1" "A2_conv[T]" )"1" "1" assert )"1" replace "1" "1" "inf_sum_le" )"1" "abs(Gseq(a!1, x!1, h!1))" "abs(h!1)*A2seq(a!1, x!1, xp!1)" "2" )"1" "1" "inf_sum_Gseq_abs[T]" )"1" "1" "x!1" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "Gseq" )"2" "abs(abs(LAMBDA (k): IF k < 2 THEN k * a!1(k)IF n!1 < 2 THEN abs(n!1 * a!1(n!1))") "1" expand "A2seq" )"1" assert )"1" "1" expand "*" )"1" "TK" "GET_tk(x!1, h!1, n!1)" )"1" rewrite "abs_mult" )"1" "abs(TK ^ (n!1 - 1) - x!1 ^ (n!1 - 1)) <= max (abs(x!1), abs(xp!1)) ^ (n!1 - 2)) * abs(n!1 - 1) * abs(h!1)") "1" "abs(a!1(n!1))*abs(n!1)" )"1" assert )nil nil ))nil )"2" "2" "MAX" "max(abs(x!1), abs(xp!1))" )"2" replace "2" "mean_value_abs[T]" )"2" "TK" "x!1" "(LAMBDA (x:T): x^(n!1-1))" )"2" "deriv_x_to_n[T]" )"2" "(n!1-1)" "1" )"2" assert )"2" "2" "(LAMBDA (x: T): 1 * x ^ (n!1 - 1)) = (LAMBDA (x: T): x ^ (n!1 - 1))" )"1" "1" assert )"1" "TK = x!1" )"1" assert )"1" rewrite "abs_0" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "2" "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = ") "1" "1" "abs_neg" )"1" "x!1 ^ (n!1 - 1) - TK ^ (n!1 - 1)" )"1" replace "1" replace "1" rewrite "abs_mult" )"1" "NM1" "abs((n!1 - 1))" )"1" "1" "abs(c!1 ^ (n!1 - 2)) <= abs(MAX ^ (n!1 - 2))" )"1" "abs(x!1 - TK) <= abs(h!1)" )"1" "1" "NM1" )"1" assert )nil nil ))nil )"2" "1" "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil )"2" "2" "2" "GET_tk(x!1, h!1, n!1)" )"2"
Messung V0.5 in Prozent C=100 H=99 G=99
¤ 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.218Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-01)
¤ *Eine klare Vorstellung vom Zielzustand
