(power_series_deriv_scafnil 3471698080"" (lemma "connected_domain" )"" (lemma "not_one_element" )"" (lemma "connected_deriv_domain[T]" ) (("" (assert ) nil nil ))nil ))nil ))nil )nil power_series_deriv_scaf 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_scaf nil )nil power_series_deriv_scaf nil )nil power_series_deriv_scaf nil ))nil 3299583481"" (lemma "connected_domain" ) (("" (propax) nil nil )) nil )nil power_series_deriv_scaf nil ))nil 3299583481"" (lemma "not_one_element" ) (("" (propax) nil nil )) nil )nil power_series_deriv_scaf nil ))nil 3299583481"" (lemma "open" ) (("" (propax) nil nil )) nil )nil power_series_deriv_scaf nil )) shostak))nil 3299583481"" (lemma "ball" )"" (skosimp*) (("" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )"real" reals nil )nil power_series_deriv_scaf nil )"[real -> boolean]" power_series_deriv_scaf 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_deriv_scaf nil ))nil 3298801888"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"real" reals nil ))nil 3298801888"" (skosimp*) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil ))nil 3298801888"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil ))nil 3298801536"" (skosimp*)"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" )"" (lemma "mean_value[T]" )"1" (inst - "x!1" "x!1 + h!1" "(LAMBDA (x:T): x^k!1)" )"1" (assert )"1" (lemma "deriv_x_to_n[T]" )"1" (inst - "k!1" "1" )"1" (assert )"1" (flatten)"1" (assert )"1" (split -3)"1" (skosimp*)"1" "c!1" )"1" assert )"1" "(LAMBDA (x: T): 1 * x ^ k!1) = (LAMBDA (x: T): x ^ k!1)" )"1" "1" case "deriv(LAMBDA (x: T): x ^ k!1)(c!1) = LAMBDA (x: T): x ^ (k!1 - 1) * k!1)(c!1)") "1" expand "deriv" -1)"1" replace -1)"1" (assert ) nil nil ))nil ))nil )"2" "2" assert )"2" replace -5)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert )"2" "mean_value[T]" )"2" "x!1+h!1" "x!1" "(LAMBDA (x:T): x^k!1)" )"1" assert )"1" "1" "c!1" )"1" assert )"1" "(LAMBDA (x: T): 1 * x ^ k!1) = (LAMBDA (x: T): x ^ k!1)" )"1" "1" case "deriv(LAMBDA (x: T): x ^ k!1)(c!1) = LAMBDA (x: T): x ^ (k!1 - 1) * k!1)(c!1)") "1" expand "deriv" -1)"1" replace -1)"1" assert )nil nil ))nil ))nil )"2" "2" assert )"2" replace -5)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" "h!1" )"2" expand "A" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "deriv_domain[T]" )"2" (propax) nil nil )) nil ))nil ))nil )"2" (assert )"2" (typepred "h!1" )"2" (expand "A" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (lemma "not_one_element" ) (("2" (propax) nil nil ))nil )"3" (lemma "connected_domain" ) (("3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )"bool" sets nil )"bool" sets nil )nil power_series_deriv_scaf nil )nil power_series_deriv_scaf nil )"real" reals nil )"(A(x!1))" power_series_deriv_scaf nil )"T" power_series_deriv_scaf nil )"setof[nzreal]" derivatives_def "analysis/" )nil defined_types nil )nil reals nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"real" exponentiation nil )nil integers nil )"bool" reals nil )nil integers nil )nil derivatives "analysis/" )"bool" deriv_domain_def "analysis/" )"real" reals nil )"T" power_series_deriv_scaf nil )NOT const-decl "[bool -> bool]" booleans nil )"int" integers nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[T -> real]" derivatives "analysis/" )nil derivatives "analysis/" )"bool" derivatives "analysis/" )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil taylors "analysis/" )"T" power_series_deriv_scaf nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil power_series_deriv_scaf nil )"(strict_total_order?[real])" real_props nil )nil booleans nil )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )nil derivative_props "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_scaf nil )nil power_series_deriv_scaf nil )"bool" sets nil ))nil 3298736072"" "(LAMBDA (d: [x: T, (A[T](x)), posnat]): ") "1" (skosimp*)"1" (lemma "GET_tk_prep" ) (("1" (inst?) nil nil )) nil )) nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil )"5" (skosimp*)"5" (lemma "not_one_element" ) (("5" (inst?) nil nil )) nil ))nil )"6" (skosimp*)"6" (lemma "connected_domain" )"6" (inst?) (("6" (inst?) (("6" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )nil power_series_deriv_scaf nil )"(p)" sets nil )"bool" sets nil )set type-eq-decl nil sets nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil taylors "analysis/" )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"setof[nzreal]" derivatives_def "analysis/" )nil defined_types nil )nil booleans nil )"[real -> boolean]" power_series_deriv_scaf nil )nil reals nil )"boolean" notequal 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_deriv_scaf nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )"int" integers nil ))nil 3298736072 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" power_series_deriv_scaf nil )nil power_series_deriv_scaf nil )"boolean" notequal nil )nil reals nil )nil defined_types nil )"setof[nzreal]" derivatives_def "analysis/" )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil ))nil 3298736073 ("" (subtype-tcc) nil nil )"real" reals nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" power_series_deriv_scaf nil )nil power_series_deriv_scaf nil )nil reals nil )nil defined_types nil )"setof[nzreal]" derivatives_def "analysis/" )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )"boolean" notequal nil ))nil 3298801889"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3298999556"" (skosimp*) (("" (assert ) nil nil )) nil )"int" integers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3352091397"" (skosimp*)"" (lemma "conv_series_shift" )"" (inst?)"1" (inst - "2" )"1" (assert )"1" (hide 2)"1" (lemma "derivseq_conv" )"1" (inst - "a!1" "_" )"1" (replace -2)"1" (lemma "derivseq_conv" )"1" (inst - "derivseq(a!1)" "_" )"1" "conv_powerseries?(derivseq(a!1))" )"1" (expand "derivseq" )"1" (expand "powerseq" )"1" "powerseries_abs_conv" )"1" expand "powerseries" )"1" expand "powerseq" )"1" "NP2NP1" "(LAMBDA n: (n+2)*(n+1))" )"1" "(LAMBDA n: NP2NP1(n)*a!1(2 + n))" )"1" expand "abs" -2)"1" "1" "x!1" )"1" assert )"1" "(LAMBDA (n: nat): abs(NP2NP1(n) * a!1(2 + n) * x!1 ^ n)) LAMBDA n:") "1" "1" "1" replace "1" assert )"1" "1" rewrite "abs_mult" "1" rewrite "abs_mult" "1" rewrite "abs_mult" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" assert )"2" "2" rewrite "abs_mult" "2" rewrite "abs_mult" "2" rewrite "abs_mult" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "x!2" )"2" "(LAMBDA (k: nat): LAMBDA (k: nat): NP2NP1(k) * a!1(2 + k) * x!2 ^ k") "2" "2" "2" replace "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 2)"2" (expand "conv_powerseries?" )"2" "2" "2" expand "powerseries" )"2" (inst?) 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 series nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"bool" power_series_conv nil )"sequence[real]" power_series nil )"sequence[real]" power_series nil )"posint" nil )"(divides(m))" divides nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"bool" reals nil )nil integers nil )"sequence[real]" series nil )"posint" nil )"(total_order?[real])" nil )nil real_props nil )"sequence[real]" power_series_deriv_scafnil )"[nat -> posint]" power_series_deriv_scafnil )"even_int" integersnil )"even_int" integersnil )nil power_series_conv nil )"real" reals nil )"real" reals nil )"(divides(n))" divides nil )"nonneg_int" nil )"sequence[real]" power_series_derivseq nil )nil power_series_derivseq nil )"{j: posint | j >= i}" nil )"real" exponentiation nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sequences 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]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )"[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"[real -> boolean]" power_series_deriv_scaf nil )nil power_series_deriv_scaf nil )"T" power_series_deriv_scaf nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"nnreal" nil )"nonneg_int" nil ))nil )nil 3352091069"" (skosimp*)"" (lemma "conv_series_shift" )"" (inst?)"1" (inst - "2" )"1" (assert )"1" (hide 2)"1" (lemma "derivseq_conv" )"1" (inst - "a!1" "_" )"1" (replace -2)"1" (lemma "derivseq_conv" )"1" (inst - "derivseq(a!1)" "_" )"1" "conv_powerseries?(derivseq(a!1))" )"1" (expand "derivseq" )"1" (rewrite "apow_rew" )"1" expand "apowerseq" )"1" "powerseries_abs_conv" )"1" expand "powerseries" )"1" rewrite "apow_rew" )"1" expand "apowerseq" )"1" "NP2NP1" "(LAMBDA n: (n+2)*(n+1))" )"1" "(LAMBDA n: NP2NP1(n)*a!1(2 + n))" )"1" expand "abs" -2)"1" rewrite "abs_mult" -)"1" "1" "x!1" )"1" assert )"1" "(LAMBDA (n: nat): IF n = 0 THEN abs(NP2NP1(0)) * abs(a!1(2))LAMBDA n:") "1" "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" "1" replace "1" assert )"1" "1" "1" replace "1" assert )"1" assert )"1" "1" nil )))))))))"2" "2" nil )))))))))))))))))))))))))"2" "2" "2" "2" "x!2" )"2" "(LAMBDA (k: nat): IF k = 0 THEN 2 * a!1(2)LAMBDA (k: nat):IF k = 0 THEN NP2NP1(0) * a!1(2)") "2" "2" "2" "2" replace "2" assert )nil )))))))))))))))))))))))))))))))))))))))))))"2" (hide 2)"2" (expand "conv_powerseries?" )"2" "2" "2" expand "powerseries" )"2" nil )))))))))))))))))))))))))))))"2" (skosimp*) (("2" (assert ) nil ))))))))nil )nil nil )nil 3298998432"" (skosimp*)"" (lemma "conv_series_shift" )"" (inst?)"1" (inst - "2" )"1" (assert )"1" (hide 2)"1" (lemma "derivseq_conv" )"1" (inst - "a!1" "_" )"1" (replace -2)"1" (lemma "derivseq_conv" )"1" (inst - "derivseq(a!1)" "_" )"1" "conv_powerseries?(derivseq(a!1))" )"1" (expand "derivseq" )"1" (expand "powerseq" )"1" "powerseries_abs_conv" )"1" expand "powerseries" )"1" expand "powerseq" )"1" "NP2NP1" "(LAMBDA n: (n+2)*(n+1))" )"1" "(LAMBDA n: NP2NP1(n)*a!1(2 + n))" )"1" expand "abs" -2)"1" rewrite "abs_mult" -)"1" "1" "x!1" )"1" assert )"1" "(LAMBDA (n: nat): IF n = 0 THEN abs(NP2NP1(0)) * abs(a!1(2))LAMBDA n:") "1" "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" "1" replace "1" assert )"1" "1" "1" replace "1" assert )"1" assert )"1" "1" nil nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "x!2" )"2" "(LAMBDA (k: nat): IF k = 0 THEN 2 * a!1(2)LAMBDA (k: nat):IF k = 0 THEN NP2NP1(0) * a!1(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 ))nil ))nil ))nil )"2" (hide 2)"2" (expand "conv_powerseries?" )"2" "2" "2" expand "powerseries" )"2" (inst?) 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 series nil )"sequence[real]" power_series nil )"sequence[real]" series nil )nil power_series_conv nil )"sequence[real]" power_series_derivseq nil )nil power_series_derivseq nil ))nil 3299340671"" (skosimp*) (("" (assert ) nil nil )) nil )"{y: posreal | y >= x}" nil )"{z: nonneg_real | z >= x AND z >= y}" real_defs nil )"(strict_total_order?[real])" real_props nil ))nil 3352112983"" (skosimp*)"" (expand "powerseq" )"" "abs(LAMBDA (k: nat): a!1(k) * x!1 ^ k) = LAMBDA (k: nat): abs(a!1(k) * x!1 ^ k))") "1" (hide -1)"1" "(LAMBDA (k_1: nat): abs(a!1)(k_1) * abs(x!1) ^ k_1) = LAMBDA (k_1: nat): abs(a!1(k_1)) * abs(x!1^ k_1))") "1" (hide -1)"1" (apply-extensionality 1 :hide? t)"1" (rewrite "abs_mult" ) nil nil )"2" (skosimp*)"2" (assert )"2" (rewrite "abs_mult" :dir rl)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality 1 :hide? t)"2" (expand "abs" 1 1)"2" (assert )"2" (lemma "abs_expt" )"2" (expand "^" )"2" (inst?)"2" (replace -1 :dir rl)"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "abs" )"2" (apply-extensionality 1 :hide? t)"1" (lift-if)"1" (ground)"1" (expand "abs" ) (("1" (propax) nil nil )) nil )"2" (expand "abs" ) (("2" (propax) 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 )"sequence[real]" power_series nil )IF const-decl "[boolean, T, T -> T]" if_def nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil exponent_props "reals/" )"nnreal" exponentiation nil )"(total_order?[real])" nil )nil real_props nil )"nnreal" nil )"sequence[real]" power_series_deriv_scafnil )"T" power_series_deriv_scaf nil )"nnreal" exponentiation nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil power_series_deriv_scaf nil )"[real -> boolean]" power_series_deriv_scaf nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"sequence[real]" series nil )"[T, T -> boolean]" equalities 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 reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil )nil 3352112910"" (skosimp*)"" (rewrite "apow_rew" )"" (rewrite "apow_rew" )"" (expand "apowerseq" )"" (expand "abs" 1)"" (apply-extensionality 1 :hide? t)"1" (lift-if)"1" (ground)"1" "IF x!1 < 0 THEN -x!1 ELSE x!1 ENDIF = abs(x!1)" )"1" (rewrite "abs_mult" )"1" (rewrite "abs_hat" )"1" (flatten)"1" (replace -1)"1" (assert )"1" rewrite "abs_0" )"1" (assert ) nil )))))))))))))"2" (hide 3) (("2" (grind) nil )))))))))"2" (skosimp*)"2" "IF x!1 < 0 THEN -x!1 ELSE x!1 ENDIF = abs(x!1)" )"1" (assert )"1" (assert )"1" (assert )"1" (hide -1)"1" "abs(x!1) ^ k!1 >= x!1 ^ k!1" )"1" "abs(a!1(k!1)) >= a!1(k!1)" )"1" case "x!1 = 0" )"1" replace -1)"1" rewrite "abs_0" )"1" (assert ) nil )))))"2" "AA" "abs(x!1) ^ k!1" )"2" case "AA > 0" )"1" replace -2)"1" "1" "CC" "abs(a!1(k!1))" )"1" case "CC >= 0" )"1" replace -2)"1" "1" "1" assert )"1" nil )))"2" "2" assert )"2" replace "2" "1" replace "1" "1" "abs_expt" )"1" expand "^" )"1" "k!1" "x!1" )"1" replace "1" "1" "expt" )nil )))))))))))))))"2" replace "2" "2" "abs_expt" )"2" expand "^" )"2" "k!1" "x!1" )"2" replace "2" "2" "expt" )nil )))))))))))))))))))))))))))))"2" (assert ) nil )))))))))"2" assert )"2" replace -1 + :dir rl)"2" "2" "abs_expt" )"2" expand "^" )"2" "k!1" "x!1" )"2" assert )"2" replace "2" "2" "expt_eq_0" )"2" expand "^" )"2" "2" assert )nil )))))))))))))))))))))))))))))))"2" (hide 3) (("2" (assert ) nil )))))"2" (hide 3)"2" assert )"2" rewrite "abs_hat" :dir rl)"1" (assert ) nil )"2" "2" replace -1)"2" rewrite "abs_0" )"2" assert )nil )))))))))))))))))))))))"2" (hide 3) (("2" (grind) nil )))))))"3" (skosimp*) (("3" (assert ) (("3" (assert ) nil )))))"4" (skosimp*)"4" (lift-if) (("4" (ground) nil ))))))))))))))))nil )nil nil )nil 3352094498"" (skosimp*)"" (rewrite "apow_rew" )"" (rewrite "apow_rew" )"" (expand "apowerseq" )"" (expand "abs" 1)"" (apply-extensionality 1 :hide? t)"1" (lift-if)"1" (ground)"1" "IF x!1 < 0 THEN -x!1 ELSE x!1 ENDIF = abs(x!1)" )"1" (rewrite "abs_mult" )"1" (rewrite "abs_hat" )"1" (flatten)"1" (replace -1)"1" (assert )"1" rewrite "abs_0" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3) (("2" (grind) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" "IF x!1 < 0 THEN -x!1 ELSE x!1 ENDIF = abs(x!1)" )"1" (assert )"1" (assert )"1" (assert )"1" (hide -1)"1" "abs(x!1) ^ k!1 >= x!1 ^ k!1" )"1" "abs(a!1(k!1)) >= a!1(k!1)" )"1" case "x!1 = 0" )"1" replace -1)"1" rewrite "abs_0" )"1" (assert ) nil nil ))nil ))nil )"2" "AA" "abs(x!1) ^ k!1" )"2" case "AA > 0" )"1" replace -2)"1" "1" "CC" "abs(a!1(k!1))" )"1" case "CC >= 0" )"1" replace -2)"1" "1" "1" "1" "1" "1" replace "1" "1" nil nil ))nil ))nil )"2" replace "2" "2" rewrite "abs_hat" )"1" rewrite "abs_hat" )"1" rewrite "abs_abs" )"1" assert )nil nil ))nil ))nil )"2" "2" "abs_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" rewrite "abs_hat" :dir rl)"2" assert )"2" replace -1 * rl)"2" "2" "expt_pos" )"2" "1" "abs_eq_0" )"1" "1" assert )nil nil ))nil ))nil )"2" "abs_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil )"2" (hide 3)"2" rewrite "abs_hat" :dir rl)"1" (assert ) nil nil )"2" "2" replace -1)"2" rewrite "abs_0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3) (("2" (grind) nil nil )) nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"sequence[real]" series nil )nil exponent_props "reals/" )nil power_series nil )"sequence[real]" power_series nil )nil power_series nil ))nil )nil 3299581520"" (skosimp*)"" (expand "powerseq" )"" (expand "abs" 1)"" (apply-extensionality 1 :hide? t)"1" (lift-if)"1" (ground)"1" "IF x!1 < 0 THEN -x!1 ELSE x!1 ENDIF = abs(x!1)" )"1" (rewrite "abs_mult" )"1" (rewrite "abs_hat" )"1" (flatten)"1" (replace -1)"1" (assert )"1" (rewrite "zero_hat" )"1" (rewrite "abs_0" )"1" assert )"1" rewrite "zero_hat" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3)"2" (ground) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" "IF x!1 < 0 THEN -x!1 ELSE x!1 ENDIF = abs(x!1)" )"1" (assert )"1" (assert )"1" (assert )"1" (hide -1)"1" "abs(x!1) ^ k!1 >= x!1 ^ k!1" )"1" "abs(a!1(k!1)) >= a!1(k!1)" )"1" (case "x!1 = 0" )"1" (replace -1)"1" rewrite "abs_0" )"1" assert )"1" rewrite "zero_hat" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (name "AA" "abs(x!1) ^ k!1" )"2" case "AA > 0" )"1" replace -2)"1" "1" "CC" "abs(a!1(k!1))" )"1" case "CC >= 0" )"1" replace -2)"1" "1" "1" "1" "1" "1" replace -1 * rl)"1" "1" nil nil ))nil ))nil )"2" replace -2 * rl)"2" "2" rewrite "abs_hat" )"1" rewrite "abs_hat" )"1" rewrite "abs_abs" )"1" assert )nil nil ))nil ))nil )"2" "2" "abs_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" rewrite "abs_hat" :dir rl)"2" assert )"2" replace -1 * rl)"2" "2" "expt_pos" )"2" "1" "abs_eq_0" )"1" "1" assert )nil nil ))nil ))nil )"2" "abs_eq_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3) (("2" (grind) nil nil )) nil ))nil )"2" (hide 3)"2" (rewrite "abs_hat" :dir rl)"1" (assert ) nil nil )"2" (flatten)"2" replace -1)"2" rewrite "abs_0" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 3) (("2" (grind) nil nil )) nil ))nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"sequence[real]" series nil )nil exponent_props "reals/" )nil exponent_props "reals/" )"sequence[real]" power_series nil ))nil ))"asdf" 3352094804"" (skosimp*)"" (name "ALPH" "max(abs(x!1), abs(xp!1))" )"" (case "ALPH /= 0" )"1" (case "T_pred(ALPH)" )"1" (flatten)"1" (expand "A2seq" )"1" (replace -2)"1" (hide -2)"1" (lemma "conv_derivseq" )"1" (inst - "derivseq(a!1)" )"1" (split -1)"1" (lemma "conv_series_shift" )"1" "2" "(LAMBDA (k): IF k < 2 THEN k") "1" (assert )"1" "end_series_conv" )"1" "1" assert )"1" "1" "end_series_conv" )"1" "1" assert )"1" "1" "3" )"1" "powerseries_abs_conv" )"1" "fseq(a!1)" )"1" "1" "ALPH" )"1" "abs(powerseq(fseq(a!1),ALPH)) = powerseq((LAMBDA n: ") "1" "1" "abs(ALPH) = ALPH" )"1" rewrite "apow_rew" )"1" expand "apowerseq" )"1" assert )"1" "(LAMBDA (k: nat): IF k = 0 THEN abs(1) * abs(2) * abs(a!1(2))LAMBDA n:") "1" "1" "end_series_conv" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" replace "1" assert )nil nil ))nil )"2" "2" rewrite "abs_mult" )"2" assert )"2" rewrite "abs_hat" )"2" "abs(ALPH) = ALPH" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "fseq" )"2" rewrite "A2_conv_scaf" )"2" "abs((LAMBDA n: (1 + n) * (2 + n) * a!1(2 + n))) = (LAMBDA n: abs(1 + n) * abs(2 + n) * abs(a!1(2 + n)))" )"1" "1" assert )nil nil ))nil )"2" "2" "abs((LAMBDA n: (1 + n) * (2 + n) * a!1(2 + n))) = abs(fseq(a!1))" )"1" "1" "1" expand "abs" "1" assert )"1" expand "fseq" )"1" "(2 * a!1(2 + x!2) + 3 * (a!1(2 + x!2) * x!2) + ") "1" rewrite "abs_mult" )"1" "1" "a!1(2 + x!2) + a!1(2 + x!2) * x!2 = (1+x!2)*a!1(2 + x!2)" )"1" rewrite "abs_mult" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "fseq" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "conv_powerseries?" )"2" "2" expand "derivseq" )"2" expand "fseq" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) nil nil ))nil ))nil )"2" (assert )"2" (hide 4)"2" (lemma "conv_derivseq" )"2" "a!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "ball" )"2" (inst - "x!1" )"2" (lemma "ball" )"2" (inst - "xp!1" )"2" (hide -5 3) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (hide -3 2) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil power_series_deriv_scaf nil )"[real -> boolean]" power_series_deriv_scaf nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"{z: nonneg_real | z >= x AND z >= y}" real_defs nil )"nnreal" exponentiation nil )"real" reals nil )"real" power_series_deriv_scaf nil )"sequence[real]" power_series_derivseq nil )nil sequences nil )nil naturalnumbers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil series nil )"posint" nil )"{j: posint | j >= i}" nil )"[numfield, numfield -> numfield]" number_fields nil )nil power_series_conv nil )"sequence[real]" power_series nil )"sequence[real]" series nil )"sequence[real]" power_series nil )nil real_types nil )"{r: posrat | r >= q}" nil )nil exponentiation nil )"even_int" integersnil )"odd_int" integers nil )nil real_props nil )nil reals nil )nil exponent_props "reals/" )nil power_series nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"even_int" integersnil )"real" reals nil )nil power_series_deriv_scaf nil )"bool" power_series_conv nil )"real" power_series_deriv_scaf nil )nil series nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"{z: nonneg_real | z >= abs(x!1) AND z >= abs(xp!1)}" nil )"T" power_series_deriv_scaf nil )"T" power_series_deriv_scaf nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )NOT const-decl "[bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"int" integers nil )"nnreal" nil )"posint" nil )nil power_series_derivseq nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )"{j: nonneg_int | j >= i}" nil )nil power_series_deriv_scaf nil )"boolean" notequal nil ))nil )"asdf" 3299581548"" (skosimp*)"" (name "ALPH" "max(abs(x!1), abs(xp!1))" )"" (case "ALPH /= 0" )"1" (case "T_pred(ALPH)" )"1" (flatten)"1" (expand "A2seq" )"1" (replace -2)"1" (hide -2)"1" (lemma "conv_derivseq" )"1" (inst - "derivseq(a!1)" )"1" (split -1)"1" (lemma "conv_series_shift" )"1" "2" "(LAMBDA (k): IF k < 2 THEN k") "1" (assert )"1" "end_series_conv" )"1" "1" assert )"1" "1" "end_series_conv" )"1" "1" assert )"1" "1" "3" )"1" "powerseries_abs_conv" )"1" "fseq(a!1)" )"1" "1" "ALPH" )"1" "abs(powerseq(fseq(a!1),ALPH)) = powerseq((LAMBDA n: ") "1" "1" "abs(ALPH) = ALPH" )"1" expand "powerseq" )"1" assert )"1" "(LAMBDA (k: nat): IF k = 0 THEN abs(1) * abs(2) * abs(a!1(2))LAMBDA n:") "1" "1" "end_series_conv" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" replace "1" assert )nil nil ))nil )"2" "2" rewrite "abs_mult" )"2" assert )"2" rewrite "abs_hat" )"2" "abs(ALPH) = ALPH" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "fseq" )"2" rewrite "A2_conv_scaf" )"2" "abs((LAMBDA n: (1 + n) * (2 + n) * a!1(2 + n))) = (LAMBDA n: abs(1 + n) * abs(2 + n) * abs(a!1(2 + n)))" )"1" "1" assert )nil nil ))nil )"2" "2" "abs((LAMBDA n: (1 + n) * (2 + n) * a!1(2 + n))) = abs(fseq(a!1))" )"1" "1" "1" expand "abs" "1" assert )"1" expand "fseq" )"1" "(2 * a!1(2 + x!2) + 3 * (a!1(2 + x!2) * x!2) + ") "1" rewrite "abs_mult" )"1" "1" "a!1(2 + x!2) + a!1(2 + x!2) * x!2 = (1+x!2)*a!1(2 + x!2)" )"1" rewrite "abs_mult" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "fseq" )"2" nil nil ))nil ))nil )"3" "3" assert )"3" assert )"3" "3" expand "abs" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "4" assert )"4" expand "abs" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "conv_powerseries?" )"2" "2" expand "derivseq" )"2" expand "fseq" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) nil nil ))nil ))nil )"2" (assert )"2" (hide 4)"2" (lemma "conv_derivseq" )"2" "a!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "ball" )"2" (inst - "x!1" )"2" (lemma "ball" )"2" (inst - "xp!1" )"2" (hide -5 3) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (hide -3 2) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"sequence[real]" power_series_derivseq nil )nil series nil )nil power_series_conv nil )"sequence[real]" power_series nil )"sequence[real]" series nil )nil exponent_props "reals/" )nil series nil )nil power_series_derivseq nil ))nil )"asdf" 3299574319"" (skosimp*)"" (name "ALPH" "max(abs(x!1), abs(xp!1))" )"" (case "ALPH /= 0" )"1" (case "T_pred(ALPH)" )"1" (flatten)"1" (expand "A2seq" )"1" (replace -2)"1" (hide -2)"1" (lemma "conv_derivseq" )"1" (inst - "derivseq(a!1)" )"1" (split -1)"1" (lemma "conv_series_shift" )"1" "2" "(LAMBDA (k): IF k < 2 THEN k") "1" (assert )"1" "end_series_conv" )"1" "1" assert )"1" "1" "end_series_conv" )"1" "1" assert )"1" "1" "3" )"1" "powerseries_abs_conv" )"1" "fseq(a!1)" )"1" "1" "ALPH" )"1" "abs(powerseq(fseq(a!1),ALPH)) = powerseq((LAMBDA n: ") "1" "1" "abs(ALPH) = ALPH" )"1" expand "powerseq" )"1" assert )"1" "(LAMBDA (k: nat): IF k = 0 THEN abs(1) * abs(2) * abs(a!1(2))LAMBDA n:") "1" "1" "end_series_conv" )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "2" "2" "1" replace "1" assert )nil nil ))nil )"2" "2" rewrite "abs_mult" )"2" assert )"2" rewrite "abs_hat" )"2" "abs(ALPH) = ALPH" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "fseq" )"2" rewrite "ABC_LEM" )"2" "abs((LAMBDA n: (1 + n) * (2 + n) * a!1(2 + n))) = (LAMBDA n: abs(1 + n) * abs(2 + n) * abs(a!1(2 + n)))" )"1" "1" assert )nil nil ))nil )"2" "2" "abs((LAMBDA n: (1 + n) * (2 + n) * a!1(2 + n))) = abs(fseq(a!1))" )"1" "1" "1" expand "abs" "1" assert )"1" expand "fseq" )"1" "(2 * a!1(2 + x!2) + 3 * (a!1(2 + x!2) * x!2) + ") "1" rewrite "abs_mult" )"1" "1" "a!1(2 + x!2) + a!1(2 + x!2) * x!2 = (1+x!2)*a!1(2 + x!2)" )"1" rewrite "abs_mult" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "fseq" )"2" nil nil ))nil ))nil )"3" "3" assert )"3" assert )"3" "3" expand "abs" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" "4" "4" assert )"4" expand "abs" )"4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "conv_powerseries?" )"2" "2" expand "derivseq" )"2" expand "fseq" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) nil nil ))nil ))nil )"2" (assert )"2" (hide 4)"2" (lemma "conv_derivseq" )"2" "a!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "ball" )"2" (inst - "x!1" )"2" (lemma "ball" )"2" (inst - "xp!1" )"2" (hide -5 3) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (assert )"2" (hide -3 2) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil series nil )nil power_series_conv nil )"sequence[real]" power_series nil )"sequence[real]" series nil )nil exponent_props "reals/" )nil series nil ))nil )"asdf" 3299574158"" (skosimp*)"" (name "ALPH" "max(abs(x!1), abs(xp!1))" )"" (case "ALPH /= 0" )"1" (flatten)"1" (expand "A2seq" )"1" (replace -1)"1" (hide -1)"1" (lemma "conv_derivseq" )"1" (inst - "derivseq(a!1)" )"1" (split -1)"1" (lemma "conv_series_shift" )"1" "2" "(LAMBDA (k): IF k < 2 THEN k") "1" (assert )"1" (lemma "end_series_conv" )"1" "1" assert )"1" "1" "A2_prep" )"1" "a!1" "ALPH" )"1" "1" "abs(powerseq((LAMBDA LAMBDA ") "1" "1" "abs(ALPH) = ALPH" )"1" assert )"1" "(LAMBDA (k: nat): IF k = 0 THEN abs(1) * abs(2) * abs(a!1(2))LAMBDA n:") "1" "1" "1" "abs(ALPH) = ALPH" )"1" "1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" (postpone) nil nil ))nil )"2" (postpone) nil nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (postpone) nil nil ))nil ))nil ))nil )nil nil )"asdf" 3299518193"" (skosimp*)"" (name "ALPH" "max(abs(x!1), abs(xp!1))" )"" (case "ALPH /= 0" )"1" (flatten)"1" (expand "A2seq" )"1" (replace -1)"1" (hide -1)"1" (lemma "conv_derivseq" )"1" (inst - "derivseq(a!1)" )"1" (split -1)"1" (lemma "conv_series_shift" )"1" "2" "(LAMBDA (k): IF k < 2 THEN k") "1" (assert )"1" (lemma "end_series_conv" )"1" "1" assert )"1" "1" "A2_prep" )"1" "a!1" "ALPH" )"1" (postpone) nil nil )"2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) nil nil ))nil ))nil )"2" (assert )"2" (hide 4)"2" (lemma "conv_derivseq" )"2" (inst - "a!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (flatten)"2" (hide -3 2) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil nil )"asdf" 3299518171"" (skosimp*)"" (name "ALPH" "max(abs(x!1), abs(xp!1))" )"" (case "ALPH /= 0" )"1" (flatten)"1" (expand "A2seq" )"1" (replace -1)"1" (hide -1)"1" (lemma "conv_derivseq" )"1" (inst - "derivseq(a!1)" )"1" (split -1)"1" (lemma "conv_series_shift" )"1" "2" "(LAMBDA (k): IF k < 2 THEN k") "1" (assert )"1" (lemma "end_series_conv" )"1" "1" assert )"1" "1" "A2_prep" )"1" "a!1" "ALPH" )"1" "powerseries_conv_abs" )"1" "(LAMBDA n: (1 + n) * (2 + n) * a!1(2 + n))" )"1" "1" (postpone) nil nil )"2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) nil nil ))nil ))nil )"2" (assert )"2" (hide 4)"2" (lemma "conv_derivseq" )"2" (inst - "a!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (flatten)"2" (hide -3 2) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil shostak)nil 3299500900"" (skosimp*)"" (name "ALPH" "max(abs(x!1), abs(xp!1))" )"" (case "ALPH /= 0" )"1" (flatten)"1" (expand "A2seq" )"1" (replace -1)"1" (hide -1)"1" (lemma "conv_derivseq" )"1" (inst - "derivseq(a!1)" )"1" (split -1)"1" (lemma "conv_series_shift" )"1" "2" "(LAMBDA (k): IF k < 2 THEN k") "1" (assert )"1" (lemma "end_series_conv" )"1" "1" assert )"1" "1" "A2_prep" )"1" "a!1" "ALPH" )"1" "powerseries_conv_abs" )"1" "(LAMBDA n: (1 + n) * (2 + n) * a!1(2 + n))" )"1" "1" "ALPH" )"1" "abs(powerseq((LAMBDA LAMBDA ") "1" "1" "abs(ALPH) = ALPH" )"1" expand "powerseq" )"1" assert )"1" "(LAMBDA (k: nat): IF k = 0 THEN abs(1) * abs(2) * abs(a!1(2))LAMBDA n:") "1" "1" "1" "1" replace "1" assert )nil nil ))nil )"2" "2" rewrite "abs_mult" )"2" assert )"2" rewrite "abs_hat" )"2" "abs(ALPH) = ALPH" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "ABC_LEM" )"2" "1" replace "1" "1" "abs((LAMBDA n: (1 + n) * (2 + n) * a!1(2 + n))) = (LAMBDA n: abs(1 + n) * abs(2 + n) * abs(a!1(2 + n)))" )"1" "1" "abs((LAMBDA n: (1 + n) * (2 + n) * a!1(2 + n))) = abs(fseq(a!1))" )"1" "1" "1" expand "abs" "1" assert )"1" "fseq(a!1)(x!2) = (1 + x!2) * (2 + x!2) * a!1(2 + x!2)" )"1" rewrite "abs_mult" )"1" "1" "2 + x!2 + (x!2 * x!2 + 2 * x!2) = (2+x!2)*(1+x!2)" )"1" rewrite "abs_mult" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" expand "fseq" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "fseq" )"2" nil nil ))nil ))nil )"3" "3" assert )"3" "3" nil nil ))nil ))nil ))nil )"4" "4" "4" assert )"4" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "ball" )"2" "x!1" )"2" assert )"2" "ball" )"2" "xp!1" )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -3)"2" "2" "x!2" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (postpone) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) nil nil ))nil ))nil )"2" (assert )"2" (hide 4)"2" (lemma "conv_derivseq" )"2" (inst - "a!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (flatten)"2" (hide -3 2) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil shostak))nil 3445341743"" (skosimp*)"" (expand "conv_series?" )"" (expand "Gseq" )"" case "FORALL (k: above(1)): abs(x!1 - GET_tk(x!1, h!1, k)) < abs(h!1)" )"1" (lemma "comparison_test_gen" )"1" (name "ALPH" "max(abs(x!1),abs(x!1+h!1))" )"1" (lemma "end_series_conv" )"1" (inst?)"1" (assert )"1" (hide 2)"1" (assert )"1" "(LAMBDA (k): IF k < 2 THEN k * a!1(k)" "(LAMBDA (k): IF k < 2 THEN 0 ELSE abs(h!1*k)*abs(k-1)*abs(a!1(k)*ALPH^(k-2)) ENDIF)" )"1" (assert )"1" (hide 1)"1" "1" "1" "(LAMBDA (k): IF k < 2 THEN 0LAMBDA (k): abs(h!1)*IF k < 2 THEN 0") "1" "1" "conv_scaf0" )"1" "1" "ALPH" )"1" assert )"1" "conv_series_scal" )"1" "1" "abs(h!1)" )"1" assert )"1" rewrite "series_scal" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" replace -1 * rl)"2" "2" "h!1" )"2" expand "A" )"2" assert )"2" "ball" )"2" "(h!1 + x!1)" )"2" "ball" )"2" "(x!1)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" rewrite "abs_mult" )"2" rewrite "abs_mult" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "3" )"2" "2" "2" "2" "n!1" )"2" "TK" "GET_tk(x!1, h!1, n!1)" )"2" case "(EXISTS (PKM1: between[T](x!1,TK)): ") "1" "1" replace -2)"1" case "abs(PKM1!1) <= abs(ALPH)" )"1" case "abs(a!1(n!1) * TK ^(n!1 - 1) * n!1 - ") "1" replace -1)"1" "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" "abs_0" )"1" "ALPH = 0" )"1" "1" nil nil ))nil )"2" "abs(n!1)*abs(n!1-1)" )"1" "1" "abs_neg" )"1" "(x!1 ^ (n!1 - 1) - TK ^ (n!1 - 1))" )"1" assert )"1" replace "1" replace "1" "abs(n!1-1)" )"1" "1" "1" "both_sides_expt_pos_ge" )"1" "(n!1-2)" "abs(ALPH)" "abs(PKM1!1)" )"1" assert )"1" rewrite "abs_hat" "1" "abs(a!1(n!1))" )"1" "1" "PKM1!1 = 0" )"1" assert )nil nil )"2" assert )"2" case "abs(PKM1!1) /= 0" )"1" "1" rewrite "abs_hat" "1" "abs(a!1(n!1))" )"1" "1" "1" assert )nil nil )"2" "abs_abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "abs_eq_0" )"2" "PKM1!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "abs(PKM1!1) /= 0" )"1" "1" rewrite "abs_eq_0" )nil nil ))nil )"2" "2" "PKM1!1 = 0" )"1" "PKM1!1 = 0" )"1" assert )nil nil ))nil )"2" "abs_eq_0" )"2" "PKM1!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "a!1(n!1) * TK ^ (n!1 - 1) * n!1 - ") "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" "2" "2" "2" "abs(max(abs(x!1), abs(h!1 + x!1))) = (max(abs(x!1), abs(h!1 + x!1)))" )"1" "1" "1" "TK" )"1" "1" "PKM1!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "mean_value[T]" )"1" "TK" "x!1" "(LAMBDA (x:T): x^(n!1-1))" )"1" "deriv_x_to_n[T]" )"1" "(n!1-1)" "1" )"1" assert )"1" "1" "(LAMBDA (x: T): 1 * x ^ (n!1 - 1)) = (LAMBDA (x: T): x ^ (n!1 - 1))" )"1" "1" assert )"1" "1" "1" "c!1" )"1" "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = ") "1" "1" "1" "NM1" "n!1-1" )"1" replace "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "deriv_x_to_n[T]" )"2" assert )"2" "(n!1-1)" "1" )"2" "2" "(LAMBDA (x: T): 1 * x ^ (n!1 - 1)) = (LAMBDA (x: T): x ^ (n!1 - 1))" )"1" "1" replace "1" "1" assert )"1" expand "deriv" "1" assert )"1" "(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" "2" replace "2" nil nil ))nil ))nil )"3" "not_one_element" )"3" nil nil ))nil )"4" "4" "4" nil nil ))nil ))nil )"5" "5" expand "derivable?" "5" "5" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "x!1 = TK" )"1" assert )"1" rewrite "abs_0" )"1" assert )"1" "TK" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "mean_value[T]" )"2" "x!1" "TK" "(LAMBDA (x:T): x^(n!1-1))" )"2" assert )"2" "2" "c!1" )"1" "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = ") "1" "1" "1" "NM1" "n!1-1" )"1" "abs_neg" )"1" "(x!1 - TK)" )"1" replace "1" "TKMx" "(TK - x!1)" )"1" "1" "abs(x!1 ^ NM1 - TK ^ NM1) = abs(TK ^ NM1 - x!1 ^ NM1) " )"1" replace "1" "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "abs" )"2" "2" "2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = deriv(LAMBDA (x: T): x ^ (n!1 - 1))(c!1)" )"1" replace "1" assert )nil nil ))nil )"2" expand "deriv" "2" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" "connected_domain" )"2" "connected_deriv_domain[T]" )"2" replace "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "not_one_element" )"2" nil nil ))nil )"3" "connected_domain" )"3" nil nil ))nil ))nil ))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 )"4" (skosimp*) (("4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (typepred "GET_tk(x!1, h!1, k!1)" )"2" (name-replace "TK" "GET_tk(x!1, h!1, k!1)" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" series nil )"{tk: between[T](x, x + h) | ((x + h) ^ k - x ^ k) / h = k * tk ^ (k - 1)}" nil )"[numfield, numfield -> numfield]" number_fields nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil taylors "analysis/" )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"[bool, bool -> bool]" booleans nil )nil integers nil )nil integers nil )"setof[nzreal]" derivatives_def "analysis/" )nil defined_types nil )nil reals nil )"boolean" notequal nil )nil power_series_deriv_scaf nil )"[real -> boolean]" power_series_deriv_scaf nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"{z: nonneg_real | z >= x AND z >= y}" real_defs nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"int" integers nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )"T" power_series_deriv_scaf nil )"(A(x!1))" power_series_deriv_scaf nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sequences nil )"nnreal" nil )"nnreal" exponentiation nil )"(strict_total_order?[real])" real_props nil )"nzreal" real_typesnil )"nnrat" exponentiation nil )nil real_props nil )"real" reals nil )nil real_props nil )"{n: nonneg_real | n >= n!1 - 1 AND n >= -(n!1 - 1)}" nil )nil real_props nil )nil reals nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )"{n: nonneg_real | n >= n!1 - 1 AND n >= -(n!1 - 1)}" nil )nil exponentiation nil )nil extra_real_props nil )"nat" exponentiation nil )nil exponent_props "reals/" )nil abs_lems "reals/" )nil real_props nil )"nzreal" nil )nil real_props nil )nil abs_lems "reals/" )nil exponent_props "reals/" )"between[T](x!1, TK)" nil )"{tk: between[T](x!1, h!1 + x!1) | " nil )nil abs_lems "reals/" )"nat" power_series_deriv_scaf nil )nil real_types nil )nil real_props nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"bool" reals nil )nil derivative_props "analysis/" )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )nil derivatives "analysis/" )"bool" deriv_domain_def "analysis/" )"odd_int" integers nil )nil derivatives "analysis/" )"T" power_series_deriv_scaf nil )"real" derivatives_def "analysis/" )"bool" derivatives_def "analysis/" )"bool" derivatives "analysis/" )nil power_series_deriv_scaf nil )nil power_series_deriv_scaf nil )"[T -> real]" derivatives "analysis/" )"T" power_series_deriv_scaf nil )nil deriv_domain_def"analysis/" )nil power_series_deriv_scaf nil )"(total_order?[real])" nil )nil real_props nil )"(total_order?[real])" nil )"{j: nonneg_int | j >= i}" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil power_series_deriv_scaf nil )nil series nil )"{y: posreal | y >= x}" nil )nil series nil )"{z: nonneg_real | z >= abs(x!1) AND z >= abs(h!1 + x!1)}" nil )nil power_series_deriv_scaf nil )nil series nil )nil series nil )"real" exponentiation nil )"real" power_series_deriv_scaf nil )"real" reals nil )"real" reals nil ))nil )nil 3299840221"" (skosimp*)"" (expand "conv_series?" )"" (expand "Gseq" )"" case "FORALL (k: above(1)): abs(x!1 - GET_tk(x!1, h!1, k)) < abs(h!1)" )"1" (lemma "comparison_test_gen" )"1" (name "ALPH" "max(abs(x!1),abs(x!1+h!1))" )"1" (lemma "end_series_conv" )"1" (inst?)"1" (assert )"1" (hide 2)"1" (assert )"1" "(LAMBDA (k): IF k < 2 THEN k * a!1(k)" "(LAMBDA (k): IF k < 2 THEN 0 ELSE abs(h!1*k)*abs(k-1)*abs(a!1(k)*ALPH^(k-2)) ENDIF)" )"1" (assert )"1" (hide 1)"1" "1" "1" "(LAMBDA (k): IF k < 2 THEN 0LAMBDA (k): abs(h!1)*IF k < 2 THEN 0") "1" "1" "conv_scaf0" )"1" "1" "ALPH" )"1" assert )"1" "conv_series_scal" )"1" "1" "abs(h!1)" )"1" assert )"1" rewrite "series_scal" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" replace -1 * rl)"2" "2" "h!1" )"2" expand "A" )"2" assert )"2" "ball" )"2" "(h!1 + x!1)" )"2" "ball" )"2" "(x!1)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" rewrite "abs_mult" )"2" rewrite "abs_mult" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "3" )"2" "2" "2" "2" "n!1" )"2" "TK" "GET_tk(x!1, h!1, n!1)" )"2" case "(EXISTS (PKM1: between[T](x!1,TK)): ") "1" "1" replace -2)"1" case "abs(PKM1!1) <= abs(ALPH)" )"1" case "abs(a!1(n!1) * TK ^(n!1 - 1) * n!1 - ") "1" replace -1)"1" "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" "abs_0" )"1" "ALPH = 0" )"1" "1" nil nil ))nil )"2" "abs(n!1)*abs(n!1-1)" )"1" "1" "abs_neg" )"1" "(x!1 ^ (n!1 - 1) - TK ^ (n!1 - 1))" )"1" assert )"1" replace "1" replace "1" "abs(n!1-1)" )"1" "1" "1" "both_sides_expt_pos_ge" )"1" "(n!1-2)" "abs(ALPH)" "abs(PKM1!1)" )"1" assert )"1" rewrite "abs_hat" "1" "abs(a!1(n!1))" )"1" "1" "PKM1!1 = 0" )"1" assert )nil nil )"2" assert )"2" case "abs(PKM1!1) /= 0" )"1" "1" rewrite "abs_hat" "1" "abs(a!1(n!1))" )"1" "1" "1" assert )nil nil )"2" "abs_abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "abs_eq_0" )"2" "PKM1!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "abs(PKM1!1) /= 0" )"1" "1" rewrite "abs_eq_0" )nil nil ))nil )"2" "2" "PKM1!1 = 0" )"1" "PKM1!1 = 0" )"1" assert )nil nil ))nil )"2" "abs_eq_0" )"2" "PKM1!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "a!1(n!1) * TK ^ (n!1 - 1) * n!1 - ") "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" "2" "2" "2" "abs(max(abs(x!1), abs(h!1 + x!1))) = (max(abs(x!1), abs(h!1 + x!1)))" )"1" "1" "1" "TK" )"1" "1" "PKM1!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "mean_value[T]" )"1" "TK" "x!1" "(LAMBDA (x:T): x^(n!1-1))" )"1" "deriv_x_to_n[T]" )"1" "(n!1-1)" "1" )"1" assert )"1" "1" "(LAMBDA (x: T): 1 * x ^ (n!1 - 1)) = (LAMBDA (x: T): x ^ (n!1 - 1))" )"1" "1" assert )"1" "1" "1" "c!1" )"1" "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = ") "1" "1" "1" "NM1" "n!1-1" )"1" replace "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "deriv_x_to_n[T]" )"2" assert )"2" "(n!1-1)" "1" )"2" "2" "(LAMBDA (x: T): 1 * x ^ (n!1 - 1)) = (LAMBDA (x: T): x ^ (n!1 - 1))" )"1" "1" replace "1" "1" assert )"1" expand "deriv" "1" assert )"1" "(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" "2" replace "2" nil nil ))nil ))nil )"3" "not_one_element" )"3" nil nil ))nil )"4" "connected_domain" )"4" nil nil ))nil )"5" "5" expand "derivable" "5" "5" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "x!1 = TK" )"1" assert )"1" rewrite "abs_0" )"1" assert )"1" "TK" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "mean_value[T]" )"2" "x!1" "TK" "(LAMBDA (x:T): x^(n!1-1))" )"2" assert )"2" "2" "c!1" )"1" "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = ") "1" "1" "1" "NM1" "n!1-1" )"1" "abs_neg" )"1" "(x!1 - TK)" )"1" replace "1" "TKMx" "(TK - x!1)" )"1" "1" "abs(x!1 ^ NM1 - TK ^ NM1) = abs(TK ^ NM1 - x!1 ^ NM1) " )"1" replace "1" "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "abs" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = deriv(LAMBDA (x: T): x ^ (n!1 - 1))(c!1)" )"1" replace "1" assert )nil nil ))nil )"2" expand "deriv" "2" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "not_one_element" )"2" nil nil ))nil )"3" "connected_domain" )"3" nil nil ))nil ))nil ))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 )"4" (skosimp*) (("4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (typepred "GET_tk(x!1, h!1, k!1)" )"2" (name-replace "TK" "GET_tk(x!1, h!1, k!1)" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil series nil )nil series nil )nil series nil )nil series nil )"[T -> real]" derivatives "analysis/" )"real" derivatives_def "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivative_props "analysis/" )nil power_series nil )nil exponent_props "reals/" )"setof[nzreal]" derivatives_def "analysis/" )nil taylors "analysis/" ))nil )nil 3298994988"" (skosimp*)"" (expand "conv_series?" )"" (expand "Gseq" )"" case "FORALL (k: above(1)): abs(x!1 - GET_tk(x!1, h!1, k)) < abs(h!1)" )"1" (lemma "comparison_test_gen" )"1" (name "ALPH" "max(abs(x!1),abs(x!1+h!1))" )"1" (lemma "end_series_conv" )"1" (inst?)"1" (assert )"1" (hide 2)"1" (assert )"1" "(LAMBDA (k): IF k < 2 THEN k * a!1(k)" "(LAMBDA (k): IF k < 2 THEN 0 ELSE abs(h!1*k)*abs(k-1)*abs(a!1(k)*ALPH^(k-2)) ENDIF)" )"1" (assert )"1" (hide 1)"1" "1" "1" "(LAMBDA (k): IF k < 2 THEN 0LAMBDA (k): abs(h!1)*IF k < 2 THEN 0") "1" "1" "conv_scaf0" )"1" "1" "ALPH" )"1" assert )"1" "convergent_scal" )"1" "1" "abs(h!1)" )"1" assert )"1" rewrite "series_scal" )"1" assert )"1" expand "*" )"1" nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" replace -1 * rl)"2" "2" "h!1" )"2" expand "A" )"2" assert )"2" "ball" )"2" "(h!1 + x!1)" )"2" "ball" )"2" "(x!1)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1" "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" (ground) nil nil ))nil )"2" "2" "2" replace -1 * rl)"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil )"3" "3" (assert ) nil nil ))nil ))nil ))nil )"2" "3" )"2" "2" "2" "2" "n!1" )"2" "TK" "GET_tk(x!1, h!1, n!1)" )"2" case "(EXISTS (PKM1: between[T](x!1,TK)): ") "1" "1" replace -2)"1" case "abs(PKM1!1) <= abs(ALPH)" )"1" case "abs(a!1(n!1) * TK ^(n!1 - 1) * n!1 - ") "1" replace -1)"1" "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" "abs_0" )"1" "ALPH = 0" )"1" "1" nil nil ))nil )"2" "abs(n!1)*abs(n!1-1)" )"1" "1" "abs_neg" )"1" "(x!1 ^ (n!1 - 1) - TK ^ (n!1 - 1))" )"1" assert )"1" replace "1" replace "1" "abs(n!1-1)" )"1" "1" "1" "both_sides_expt_pos_ge" )"1" "(n!1-2)" "abs(ALPH)" "abs(PKM1!1)" )"1" assert )"1" rewrite "abs_hat" "1" "abs(a!1(n!1))" )"1" "1" "PKM1!1 = 0" )"1" assert )"1" rewrite "zero_hat" )"1" assert )nil nil ))nil ))nil )"2" "abs_eq_0" )"2" "PKM1!1" )"2" assert )"2" rewrite "abs_hat" "2" "abs(a!1(n!1))" )"2" "2" "1" assert )nil nil )"2" "abs_abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "abs_eq_0" )"2" "PKM1!1" )"2" assert )"2" replace "2" assert )"2" rewrite "zero_hat" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "a!1(n!1) * TK ^ (n!1 - 1) * n!1 - ") "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" "2" "2" "2" "abs(max(abs(x!1), abs(h!1 + x!1))) = (max(abs(x!1), abs(h!1 + x!1)))" )"1" "1" "1" "TK" )"1" "1" "PKM1!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "mean_value[T]" )"1" "TK" "x!1" "(LAMBDA (x:T): x^(n!1-1))" )"1" "deriv_x_to_n[T]" )"1" "(n!1-1)" "1" )"1" assert )"1" "1" "(LAMBDA (x: T): 1 * x ^ (n!1 - 1)) = (LAMBDA (x: T): x ^ (n!1 - 1))" )"1" "1" assert )"1" "1" "1" "c!1" )"1" "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = ") "1" "1" "1" "NM1" "n!1-1" )"1" replace "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "deriv_x_to_n[T]" )"2" assert )"2" "(n!1-1)" "1" )"2" "2" "(LAMBDA (x: T): 1 * x ^ (n!1 - 1)) = (LAMBDA (x: T): x ^ (n!1 - 1))" )"1" "1" replace "1" "1" assert )"1" expand "deriv" "1" assert )"1" "(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" "2" replace "2" nil nil ))nil ))nil )"3" "not_one_element" )"3" nil nil ))nil )"4" "connected_domain" )"4" nil nil ))nil )"5" "5" expand "derivable" "5" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "derivable" "3" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil )"2" "x!1 = TK" )"1" assert )"1" rewrite "abs_0" )"1" assert )"1" "TK" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "mean_value[T]" )"2" "x!1" "TK" "(LAMBDA (x:T): x^(n!1-1))" )"2" assert )"2" "2" "c!1" )"1" "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = ") "1" "1" "1" "NM1" "n!1-1" )"1" "abs_neg" )"1" "(x!1 - TK)" )"1" replace "1" "TKMx" "(TK - x!1)" )"1" "1" "abs(x!1 ^ NM1 - TK ^ NM1) = abs(TK ^ NM1 - x!1 ^ NM1) " )"1" replace "1" "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "abs" )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" replace "3" assert )nil nil ))nil ))nil ))nil )"4" "4" replace "4" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = deriv(LAMBDA (x: T): x ^ (n!1 - 1))(c!1)" )"1" replace "1" assert )nil nil ))nil )"2" expand "deriv" "2" nil nil ))nil )"3" expand "derivable" "3" nil nil ))nil ))nil )"3" expand "derivable" "3" nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "not_one_element" )"2" nil nil ))nil )"3" "connected_domain" )"3" nil nil ))nil ))nil ))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 )"4" (skosimp*) (("4" (assert ) nil nil ))nil )"5" (skosimp*) (("5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (typepred "GET_tk(x!1, h!1, k!1)" )"2" (name-replace "TK" "GET_tk(x!1, h!1, k!1)" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil taylors "analysis/" )nil exponent_props "reals/" )nil exponent_props "reals/" )nil derivative_props "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" derivatives "analysis/" )"[T -> real]" derivatives "analysis/" )nil series nil )nil convergence_ops "analysis/" )nil series nil )nil series nil ))nil )nil 3298987688"" (skosimp*)"" (expand "conv_series?" )"" (expand "Gseq" )"" case "FORALL (k: above(1)): abs(x!1 - GET_tk(x!1, h!1, k)) < abs(h!1)" )"1" (lemma "comparison_test_gen" )"1" (name "ALPH" "max(abs(x!1),abs(x!1+h!1))" )"1" (lemma "end_series_conv" )"1" (inst?)"1" (assert )"1" (hide 2)"1" (assert )"1" "(LAMBDA (k): IF k < 2 THEN k * a!1(k)" "(LAMBDA (k): IF k < 2 THEN 0 ELSE abs(h!1*k)*abs(k-1)*abs(a!1(k)*ALPH^(k-2)) ENDIF)" )"1" (assert )"1" (hide 1)"1" "1" (postpone) nil nil )"2" "3" )"2" "2" "2" "2" "n!1" )"2" "TK" "GET_tk(x!1, h!1, n!1)" )"2" case "(EXISTS (PKM1: between[T](x!1,TK)): ") "1" "1" replace -2)"1" case "abs(PKM1!1) <= abs(ALPH)" )"1" case "abs(a!1(n!1) * TK ^(n!1 - 1) * n!1 - ") "1" replace -1)"1" "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )"1" "abs_0" )"1" "ALPH = 0" )"1" "1" nil nil ))nil )"2" "abs(n!1)*abs(n!1-1)" )"1" "1" "abs_neg" )"1" "(x!1 ^ (n!1 - 1) - TK ^ (n!1 - 1))" )"1" assert )"1" replace "1" replace "1" "abs(n!1-1)" )"1" "1" "1" "both_sides_expt_pos_ge" )"1" "(n!1-2)" "abs(ALPH)" "abs(PKM1!1)" )"1" assert )"1" rewrite "abs_hat" "1" "abs(a!1(n!1))" )"1" "1" "PKM1!1 = 0" )"1" assert )"1" rewrite "zero_hat" )"1" assert )nil nil ))nil ))nil )"2" "abs_eq_0" )"2" "PKM1!1" )"2" assert )"2" rewrite "abs_hat" "2" "abs(a!1(n!1))" )"2" "2" "1" assert )nil nil )"2" "abs_abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "abs_eq_0" )"2" "PKM1!1" )"2" assert )"2" replace "2" assert )"2" rewrite "zero_hat" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "a!1(n!1) * TK ^ (n!1 - 1) * n!1 - ") "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace "2" "2" "2" "2" "abs(max(abs(x!1), abs(h!1 + x!1))) = (max(abs(x!1), abs(h!1 + x!1)))" )"1" "1" "1" "TK" )"1" "1" "PKM1!1" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "mean_value[T]" )"1" "x!1" "TK" "(LAMBDA (x:T): x^(n!1-1))" )"1" "deriv_x_to_n[T]" )"1" "(n!1-1)" "1" )"1" assert )"1" "1" "(LAMBDA (x: T): 1 * x ^ (n!1 - 1)) = (LAMBDA (x: T): x ^ (n!1 - 1))" )"1" "1" assert )"1" "1" "1" "c!1" )"1" "deriv((LAMBDA (x: T): x ^ (n!1 - 1)), c!1) = ") "1" "abs_neg" )"1" "x!1 ^ (n!1 - 1) - TK ^ (n!1 - 1)" )"1" assert )"1" replace "1" nil nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" nil nil ))nil ))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 )"4" (skosimp*) (("4" (assert ) nil nil ))nil )"5" (skosimp*) (("5" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (typepred "GET_tk(x!1, h!1, k!1)" )"2" (name-replace "TK" "GET_tk(x!1, h!1, k!1)" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3298986947"" (skosimp*)"" (expand "conv_series?" )"" (expand "Gseq" )"" case "FORALL (k: above(1)): abs(x!1 - GET_tk(x!1, h!1, k)) < abs(h!1)" )"1" (lemma "comparison_test_gen" )"1" (name "ALPH" "max(abs(x!1),abs(x!1+h!1))" )"1" (lemma "end_series_conv" )"1" (inst?)"1" (assert )"1" (hide 2)"1" "(LAMBDA (k): IF k < 2 THEN k * a!1(k)" "(LAMBDA (k): abs(h!1*k)*abs(k-1)*abs(a!1(k)*ALPH^k-2))" )"1" (assert )"1" (hide 1)"1" (split +)"1" (postpone) nil nil )"2" "2" )"2" "2" "2" "2" "n!1" )"2" "TK" "GET_tk(x!1, h!1, n!1)" )"2" case "(EXISTS (PKM1: between[T](x!1,TK)): ") "1" "1" replace -2)"1" case "abs(PKM1!1) <= abs(ALPH)" )"1" case "abs(a!1(n!1) * TK ^ (n!1 - 1) * n!1 - ") "1" replace -1)"1" "1" rewrite "abs_mult" )"1" nil nil ))nil ))nil ))nil )"2" "2" "a!1(n!1) * TK ^ (n!1 - 1) * n!1 - ") "1" rewrite "abs_mult" )"1" rewrite "abs_mult" )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil )"2" (postpone) nil 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 )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (typepred "GET_tk(x!1, h!1, k!1)" )"2" (name-replace "TK" "GET_tk(x!1, h!1, k!1)" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil nil )nil 3298804872"" (skosimp*)"" (expand "conv_series?" )"" (expand "Gseq" )"" case "FORALL (k: above(1)): abs(x!1 - GET_tk(x!1, h!1, k)) < abs(h!1)" )"1" (lemma "comparison_test_gen" )"1" (name "ALPH" "max(abs(x!1),abs(x!1+h!1))" )"1" (lemma "end_series_conv" )"1" (inst?)"1" (assert )"1" (hide 2)"1" "(LAMBDA (k): IF k < 2 THEN k * a!1(k)" "(LAMBDA (k): abs(h!1*k*(k-1))*abs(a!1(k)*ALPH^k-2))" )"1" (assert )"1" (hide 1)"1" (split +)"1" (postpone) nil nil )"2" "2" )"2" "2" "2" "2" "n!1" )"2" "TK" "GET_tk(x!1, h!1, n!1)" )"2" case "(EXISTS (PKM1: between[T](x!1,TK)): ") "1" "1" replace -2)"1" case "abs(PKM1!1) <= abs(ALPH)" )"1" nil nil )"2" nil nil ))nil ))nil ))nil )"2" (postpone) nil 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 )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*) (("2" (assert ) nil nil )) nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil )"4" (skosimp*) (("4" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (typepred "GET_tk(x!1, h!1, k!1)" )"2" (name-replace "TK" "GET_tk(x!1, h!1, k!1)" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3471698183"" (skosimp*)"" (expand "conv_series?" )"" (expand "Gseq" )"" case "FORALL (k: above(1)): abs(x!1 - GET_tk(x!1, h!1, k)) < abs(h!1)" )"1" (lemma "comparison_test_gen" )"1" (name "ALPH" "max(abs(x!1),abs(x!1+h!1))" )"1" (lemma "end_series_conv" )"1" (inst?)"1" (assert )"1" (hide 2)"1" (assert )"1" "abs(LAMBDA (k): IF k < 2 THEN k * a!1(k)" "(LAMBDA (k): IF k < 2 THEN 0 ELSE abs(h!1*k)*abs(k-1)*abs(a!1(k)*ALPH^(k-2)) ENDIF)" )"1" (assert )"1" (hide 1)"1" "1" "1" "(LAMBDA (k): IF k < 2 THEN 0LAMBDA (k): abs(h!1)*IF k < 2 THEN 0") "1" "1" "conv_scaf0" )"1" "1" "ALPH" )"1" assert )"1" "conv_series_scal" )"1" "1" "abs(h!1)" )"1" assert )"1" rewrite "series_scal" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" replace -1 * rl)"2" "2" "h!1" )"2" expand "A" )"2" assert )"2" "ball" )"2" "(h!1 + x!1)" )"2" "ball" )"2" "(x!1)" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" rewrite "abs_mult" )"2" rewrite "abs_mult" )"2" (ground) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "3" )"2" "2" "2" "2" "n!1" )"2" expand "abs" 2 2)"2" rewrite "abs_abs" )"2" "TK" "GET_tk(x!1, h!1, n!1)" )
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.0.833Bemerkung:
(vorverarbeitet am 2026-04-27)
¤ *Bot Zugriff
