Quelle taylor_series.prf
Sprache: unbekannt
|
|
(taylor_series
(T_pred_0 0
(T_pred_0-1 nil 3298383901
("" (name "XX" "choose({X:T | TRUE})")
(("1" (lemma "ball")
(("1" (inst - "XX")
(("1" (assert)
(("1" (lemma "connected_domain")
(("1" (expand "connected?")
(("1" (case "XX >= 0")
(("1" (inst - "-XX" "XX" "0") (("1" (assert) nil nil))
nil)
("2" (inst - "XX" "-XX" "0") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (expand "member") (("2" (propax) nil nil)) nil)) nil))
nil))
nil)
((member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(ball formula-decl nil taylor_series nil)
(minus_real_is_real application-judgement "real" reals nil)
(connected? const-decl "bool" deriv_domain_def "analysis/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(>= const-decl "bool" reals nil)
(connected_domain formula-decl nil taylor_series nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(T formal-nonempty-subtype-decl nil taylor_series nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil)
(TRUE const-decl "bool" booleans nil))
nil))
(IMP_power_series_deriv_TCC1 0
(IMP_power_series_deriv_TCC1-1 nil 3298366313
("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
((connected_domain formula-decl nil taylor_series nil)) shostak))
(IMP_power_series_deriv_TCC2 0
(IMP_power_series_deriv_TCC2-1 nil 3298366313
("" (skosimp*)
(("" (lemma "not_one_element") (("" (inst?) nil nil)) nil)) nil)
((not_one_element formula-decl nil taylor_series nil)) shostak))
(IMP_power_series_deriv_TCC3 0
(IMP_power_series_deriv_TCC3-1 nil 3298366313
("" (skosimp*) (("" (lemma "open") (("" (inst?) nil nil)) nil)) nil)
((open formula-decl nil taylor_series nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(T formal-nonempty-subtype-decl nil taylor_series nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(IMP_power_series_deriv_TCC4 0
(IMP_power_series_deriv_TCC4-1 nil 3298366313
("" (lemma "ball")
(("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil)
((minus_real_is_real application-judgement "real" reals nil)
(T formal-nonempty-subtype-decl nil taylor_series nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(ball formula-decl nil taylor_series nil))
shostak))
(deriv_domain 0
(deriv_domain-1 nil 3472466626
("" (lemma connected_domain)
(("" (lemma not_one_element)
(("" (lemma connected_deriv_domain[T]) (("" (assert) nil nil))
nil))
nil))
nil)
((not_one_element formula-decl nil taylor_series nil)
(connected_deriv_domain formula-decl nil deriv_domain_def
"analysis/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(T formal-nonempty-subtype-decl nil taylor_series nil)
(connected_domain formula-decl nil taylor_series nil))
shostak))
(Inf_sum_0_TCC1 0
(Inf_sum_0_TCC1-1 nil 3298366313
("" (skosimp*)
(("" (name "XX" "epsilon({X:T | TRUE})")
(("" (lemma "ball")
(("" (inst - "XX")
(("" (assert)
(("" (lemma "connected_domain")
(("" (expand "connected?")
(("" (case "XX >= 0")
(("1" (inst - "-XX" "XX" "0")
(("1" (assert) nil nil)) nil)
("2" (inst - "XX" "-XX" "0")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((TRUE const-decl "bool" booleans nil)
(epsilon const-decl "T" epsilons nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-nonempty-subtype-decl nil taylor_series nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(connected_domain formula-decl nil taylor_series nil)
(>= const-decl "bool" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(connected? const-decl "bool" deriv_domain_def "analysis/")
(minus_real_is_real application-judgement "real" reals nil)
(ball formula-decl nil taylor_series nil))
shostak))
(Inf_sum_0 0
(Inf_sum_0-1 nil 3298299936
("" (skosimp*)
(("" (expand "Inf_sum")
(("" (assert)
(("" (expand "powerseries")
(("" (expand "powerseq")
((""
(case-replace "(LAMBDA (k: nat): a!1(k) * 0 ^ k) =
(LAMBDA (k: nat):
IF k = 0 THEN a!1(0) ELSE 0 ENDIF)")
(("1" (hide -1)
(("1" (expand "series")
(("1" (lemma "sigma_first[nat]")
(("1" (inst?)
(("1"
(case-replace "(LAMBDA (n: nat):
sigma(0, n,
(LAMBDA (k: nat): IF k = 0 THEN a!1(0) ELSE 0 ENDIF))) =
(LAMBDA (n: nat): a!1(0) )")
(("1" (lemma "limit_const")
(("1" (inst - "a!1(0)")
(("1" (assert)
(("1"
(expand "const_fun")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (apply-extensionality 1 :hide? t)
(("2" (lemma "sigma_first[nat]")
(("2"
(inst?)
(("2"
(assert)
(("2"
(case-replace "x!1 = 0")
(("1"
(expand "sigma" 1)
(("1"
(expand "sigma")
(("1" (propax) nil nil))
nil))
nil)
("2"
(assert)
(("2"
(replace -1)
(("2"
(hide -1)
(("2"
(rewrite
"sigma_restrict_to")
(("2"
(expand "restrict")
(("2"
(lemma "sigma_const")
(("2"
(inst?)
(("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" (apply-extensionality 1 :hide? t)
(("2" (lift-if)
(("2" (ground) (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Inf_sum const-decl "real" power_series_conv nil)
(powerseries const-decl "sequence[real]" power_series nil)
(real_times_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sequence type-eq-decl nil sequences nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(series const-decl "sequence[real]" series nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(T_low type-eq-decl nil sigma "reals/")
(<= const-decl "bool" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(restrict const-decl "[T -> real]" sigma "reals/")
(sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
(sigma_nat application-judgement "nat" sigma_nat "reals/")
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(sigma_const formula-decl nil sigma "reals/")
(sigma_restrict_to formula-decl nil sigma "reals/")
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(limit_const formula-decl nil convergence_ops "analysis/")
(constant_seq1 application-judgement "(convergent?)"
convergence_ops "analysis/")
(derivable_const application-judgement "deriv_fun" derivatives
"analysis/")
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(T_high type-eq-decl nil sigma "reals/")
(sigma def-decl "real" sigma "reals/")
(sigma_first formula-decl nil sigma "reals/")
(nat_exp application-judgement "nat" exponentiation nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(zero_hat formula-decl nil exponent_props "reals/")
(nat_expt application-judgement "nat" exponentiation nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(expt def-decl "real" exponentiation nil)
(powerseq const-decl "sequence[real]" power_series nil))
shostak))
(nderivseq_lem 0
(nderivseq_lem-1 nil 3298373671
("" (skosimp*)
(("" (expand "nderivseq")
(("" (apply-extensionality 1 :hide? t)
(("" (rewrite "factorial_plus1")
(("" (assert)
(("" (expand "derivseq")
(("" (name-replace "FNX" "factorial(n!1 + x!1)")
(("" (field 1) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nderivseq const-decl "sequence[real]" taylor_series nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(factorial_plus1 formula-decl nil factorial "ints/")
(int_minus_int_is_int application-judgement "int" integers nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(odd_plus_odd_is_even application-judgement "even_int" integers
nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(factorial def-decl "posnat" factorial "ints/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(sequence type-eq-decl nil sequences nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(T formal-nonempty-subtype-decl nil taylor_series nil)
(derivseq const-decl "sequence[real]" power_series_derivseq nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(conv_nderivseq 0
(conv_nderivseq-1 nil 3298367015
("" (induct "n")
(("1" (skosimp*)
(("1" (expand "nderivseq")
(("1"
(case-replace
"(LAMBDA (k: nat): factorial(k) / factorial(k) * a!1(k)) = a!1")
(("1" (apply-extensionality 1 :hide? t) nil nil)) nil))
nil))
nil)
("2" (skosimp*)
(("2" (rewrite "nderivseq_lem")
(("2" (inst?)
(("2" (assert)
(("2" (hide 2) (("2" (rewrite "conv_derivseq") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((derivseq const-decl "sequence[real]" power_series_derivseq nil)
(conv_derivseq formula-decl nil power_series_derivseq nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nderivseq_lem formula-decl nil taylor_series nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(factorial def-decl "posnat" factorial "ints/")
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(nat_induction formula-decl nil naturalnumbers nil)
(nderivseq const-decl "sequence[real]" taylor_series nil)
(conv_powerseries? const-decl "bool" power_series_conv nil)
(T formal-nonempty-subtype-decl nil taylor_series nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(sequence type-eq-decl nil sequences nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(Inf_sum_derivable_n_times_TCC1 0
(Inf_sum_derivable_n_times_TCC1-1 nil 3471697763
("" (skosimp*)
(("" (lemma "deriv_domain") (("" (inst?) nil nil)) nil)) nil)
((deriv_domain formula-decl nil taylor_series nil)) nil))
(Inf_sum_derivable_n_times 0
(Inf_sum_derivable_n_times-1 nil 3298373838
("" (induct "n")
(("1" (skosimp*)
(("1" (expand "derivable_n_times?") (("1" (propax) nil nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "derivable_n_times?" 1)
(("2" (rewrite "Inf_sum_derivable")
(("2" (inst - "derivseq(a!1)")
(("2" (rewrite "conv_derivseq")
(("2" (rewrite "deriv_Inf_sum") nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (lemma "not_one_element") (("3" (skosimp*) nil nil)) nil))
nil)
("4" (hide 2)
(("4" (lemma "connected_domain") (("4" (skosimp*) nil nil)) nil))
nil))
nil)
((Inf_sum_derivable formula-decl nil power_series_deriv nil)
(conv_derivseq formula-decl nil power_series_derivseq nil)
(deriv_Inf_sum formula-decl nil power_series_deriv nil)
(derivseq const-decl "sequence[real]" power_series_derivseq nil)
(nat_induction formula-decl nil naturalnumbers nil)
(Inf_sum const-decl "real" power_series_conv nil)
(derivable_n_times? def-decl "bool" nth_derivatives "analysis/")
(conv_powerseries? const-decl "bool" power_series_conv nil)
(T formal-nonempty-subtype-decl nil taylor_series nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(sequence type-eq-decl nil sequences nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(nderiv_Inf_sum_TCC1 0
(nderiv_Inf_sum_TCC1-1 nil 3298366314
("" (skosimp*) (("" (rewrite "Inf_sum_derivable_n_times") nil nil))
nil)
((Inf_sum_derivable_n_times formula-decl nil taylor_series nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sequence type-eq-decl nil sequences nil))
shostak))
(nderiv_Inf_sum_TCC2 0
(nderiv_Inf_sum_TCC2-1 nil 3298366314
("" (skosimp*)
(("" (lemma " conv_nderivseq")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil)
((conv_nderivseq formula-decl nil taylor_series nil)
(sequence type-eq-decl nil sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(nderiv_Inf_sum 0
(nderiv_Inf_sum-1 nil 3298302128
("" (induct "n")
(("1" (skosimp*)
(("1" (expand "nderiv")
(("1" (expand "nderivseq")
(("1"
(case-replace
"(LAMBDA (k: nat): factorial(k) / factorial(k) * a!1(k)) = a!1")
(("1" (hide 2)
(("1" (apply-extensionality 1 :hide? t) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "nderiv" 1)
(("2" (lemma "deriv_Inf_sum")
(("2" (inst?)
(("2" (assert)
(("2" (replace -1)
(("2" (hide -1)
(("2" (inst?)
(("2" (rewrite "conv_derivseq")
(("2" (replace -1)
(("2" (hide -1)
(("2"
(case-replace
"nderivseq(j!1, derivseq(a!1)) = nderivseq(1 + j!1, a!1)")
(("2" (hide 2)
(("2"
(expand "nderivseq")
(("2"
(expand "derivseq")
(("2"
(apply-extensionality 1 :hide? t)
(("2"
(name-replace
"AA"
"a!1(1 + j!1 + x!1)")
(("2"
(case-replace
"factorial(1 + j!1 + x!1) = (1 + j!1 + x!1)*factorial(j!1 + x!1)")
(("1"
(name-replace
"FF"
"factorial(j!1 + x!1)")
(("1" (field 1) nil nil))
nil)
("2"
(hide 2)
(("2"
(expand "factorial" 1 1)
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (skosimp*) (("3" (rewrite "conv_nderivseq") nil nil)) nil))
nil)
("4" (hide 2)
(("4" (skosimp*)
(("4" (rewrite "Inf_sum_derivable_n_times") nil nil)) nil))
nil))
nil)
((Inf_sum_derivable_n_times formula-decl nil taylor_series nil)
(conv_nderivseq formula-decl nil taylor_series nil)
(deriv_Inf_sum formula-decl nil power_series_deriv nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(conv_derivseq formula-decl nil power_series_derivseq nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posint nonempty-type-eq-decl nil integers nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(div_cancel2 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(both_sides_times1 formula-decl nil real_props nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(even_minus_odd_is_odd application-judgement "odd_int" integers
nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(derivseq const-decl "sequence[real]" power_series_derivseq nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(factorial def-decl "posnat" factorial "ints/")
(nat_induction formula-decl nil naturalnumbers nil)
(nderiv def-decl "[T -> real]" nth_derivatives "analysis/")
(nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
(= const-decl "[T, T -> boolean]" equalities nil)
(pred type-eq-decl nil defined_types nil)
(nderivseq const-decl "sequence[real]" taylor_series nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sequence type-eq-decl nil sequences nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(T formal-nonempty-subtype-decl nil taylor_series nil)
(conv_powerseries? const-decl "bool" power_series_conv nil)
(derivable_n_times? def-decl "bool" nth_derivatives "analysis/")
(Inf_sum const-decl "real" power_series_conv nil))
shostak))
(Taylor_expansion 0
(Taylor_expansion-1 nil 3298298896
("" (skosimp*)
(("" (replace -2)
(("" (lemma "nderiv_Inf_sum")
(("" (inst?)
(("" (assert)
(("" (replace -1)
(("" (hide -1)
(("" (lemma "Inf_sum_0")
(("" (rewrite "Inf_sum_0")
(("1" (lemma "Inf_sum_derivable_n_times")
(("1" (inst?)
(("1" (assert)
(("1" (expand "nderivseq")
(("1" (expand "factorial" 1 3)
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (rewrite "conv_nderivseq") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sequence type-eq-decl nil sequences nil)
(Inf_sum_0 formula-decl nil taylor_series nil)
(conv_nderivseq formula-decl nil taylor_series nil)
(Inf_sum_derivable_n_times formula-decl nil taylor_series nil)
(factorial def-decl "posnat" factorial "ints/")
(real_times_real_is_real application-judgement "real" reals nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nderivseq const-decl "sequence[real]" taylor_series nil)
(nderiv_Inf_sum formula-decl nil taylor_series nil))
shostak))
(Taylor_seq_TCC1 0
(Taylor_seq_TCC1-1 nil 3298631644
("" (skosimp*) (("" (rewrite "T_pred_0") nil nil)) nil)
((T_pred_0 formula-decl nil taylor_series nil)) shostak))
(Taylor_seq_TCC2 0
(Taylor_seq_TCC2-1 nil 3298631644
("" (skosimp*)
(("" (typepred "f!1")
(("" (expand "inf_deriv_fun?") (("" (inst?) nil nil)) nil)) nil))
nil)
((inf_deriv_fun? const-decl "bool" taylors "analysis/")
(T formal-nonempty-subtype-decl nil taylor_series nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil))
shostak))
(Taylor_seq_TCC3 0
(Taylor_seq_TCC3-1 nil 3471697763
("" (skosimp*)
(("" (lemma "deriv_domain") (("" (inst?) nil nil)) nil)) nil)
((deriv_domain formula-decl nil taylor_series nil)) nil))
(Taylor_seq_term_TCC1 0
(Taylor_seq_term_TCC1-1 nil 3298631644
("" (skosimp*) (("" (rewrite "T_pred_0") nil nil)) nil)
((T_pred_0 formula-decl nil taylor_series nil)) shostak))
(Taylor_seq_term_TCC2 0
(Taylor_seq_term_TCC2-1 nil 3298631644
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(Taylor_seq_term_TCC3 0
(Taylor_seq_term_TCC3-1 nil 3298631644
("" (skosimp*) (("" (rewrite "T_pred_0") nil nil)) nil)
((T_pred_0 formula-decl nil taylor_series nil)) shostak))
(Taylor_seq_term 0
(Taylor_seq_term-1 nil 3298383588
("" (skosimp*)
(("" (apply-extensionality 1 :hide? t)
(("1" (expand "Taylor_seq")
(("1" (expand "Taylor_term")
(("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
nil)
("2" (rewrite "T_pred_0") nil nil)
("3" (rewrite "T_pred_0") (("3" (skosimp*) nil nil)) nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(Taylor_term const-decl "real" taylors "analysis/")
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(Taylor_seq const-decl "real" taylor_series nil)
(inf_deriv_fun? const-decl "bool" taylors "analysis/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(T formal-nonempty-subtype-decl nil taylor_series nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
shostak))
(GET_C_TCC1 0
(GET_C_TCC1-1 nil 3298631645
("" (skosimp*)
(("" (typepred "f!1")
(("" (expand "inf_deriv_fun?") (("" (inst?) nil nil)) nil)) nil))
nil)
((inf_deriv_fun? const-decl "bool" taylors "analysis/")
(T formal-nonempty-subtype-decl nil taylor_series nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
shostak))
(GET_C_TCC2 0
(GET_C_TCC2-1 nil 3298631645
("" (skosimp*) (("" (rewrite "T_pred_0") nil nil)) nil)
((T_pred_0 formula-decl nil taylor_series nil)) shostak))
(GET_C_TCC3 0
(GET_C_TCC3-3 nil 3306575811
(""
(inst + "(LAMBDA (f:(inf_deriv_fun?[T]), x:T, k: nat):
choose({c: between[T](0, x) |
powerseries(Taylor_seq(f))(x)(k) =
f(x) -
Taylor_rem(k, f, 0, x, c)}))")
(("1" (skosimp*)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (lemma "Taylors_inf[T]")
(("1" (inst - "0" "x!1" "f!1" "k!1")
(("1" (assert)
(("1" (skosimp*)
(("1" (inst - "c!1")
(("1" (lemma "Taylor_seq_term")
(("1" (inst?)
(("1" (assert)
(("1" (replace -2)
(("1"
(assert)
(("1"
(expand "powerseries")
(("1"
(expand "powerseq")
(("1"
(replace -1 * rl)
(("1"
(hide -1)
(("1"
(expand "series")
(("1"
(case-replace
"(LAMBDA (k: nat): Taylor_seq(f!1)(k) * x!1 ^ k
) = (LAMBDA n:
IF n = 0 THEN f!1(0) ELSE Taylor_seq(f!1)(n) * x!1 ^ n ENDIF)")
(("1"
(hide 2)
(("1"
(apply-extensionality
1
:hide?
t)
(("1"
(lift-if)
(("1"
(ground)
(("1"
(expand
"Taylor_seq")
(("1"
(expand
"nderiv")
(("1"
(assert)
(("1"
(replace
-1)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "T_pred_0") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*) (("2" (rewrite "T_pred_0") nil nil)) nil)
("3" (skosimp*)
(("3" (typepred "f!1")
(("3" (expand "inf_deriv_fun?") (("3" (inst?) nil nil)) nil))
nil))
nil))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(empty? const-decl "bool" sets nil)
(Taylors_inf formula-decl nil taylors "analysis/")
(T_pred_0 formula-decl nil taylor_series nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(series const-decl "sequence[real]" series nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(factorial_0 formula-decl nil factorial "ints/")
(expt_x0 formula-decl nil exponentiation nil)
(nderiv def-decl "[T -> real]" nth_derivatives "analysis/")
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(powerseq const-decl "sequence[real]" power_series nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(Taylor_seq_term formula-decl nil taylor_series nil)
(member const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(Taylor_rem const-decl "real" taylors "analysis/")
(nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(derivable_n_times? def-decl "bool" nth_derivatives "analysis/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(Taylor_seq const-decl "real" taylor_series nil)
(powerseries const-decl "sequence[real]" power_series nil)
(sequence type-eq-decl nil sequences nil)
(between type-eq-decl nil taylors "analysis/")
(= const-decl "[T, T -> boolean]" equalities nil)
(< const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(inf_deriv_fun? const-decl "bool" taylors "analysis/")
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-nonempty-subtype-decl nil taylor_series nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil)
(GET_C_TCC3-2 nil 3298627880
(""
(inst + "(LAMBDA (f:(inf_deriv_fun?[T]), x:T, k: nat):
choose({c: between[T](0, x) |
powerseries(Taylor_seq[T](f))(x)(k) =
f(x) -
Taylor_rem[T](k, f, 0, x, c)}))")
(("1" (skosimp*)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (lemma "Taylors_inf[T]")
(("1" (inst - "0" "x!1" "f!1" "k!1")
(("1" (assert)
(("1" (skosimp*)
(("1" (inst - "c!1")
(("1" (lemma "Taylor_seq_term")
(("1" (inst?)
(("1" (assert)
(("1" (replace -2)
(("1"
(assert)
(("1"
(expand "powerseries")
(("1"
(expand "powerseq")
(("1"
(replace -1 * rl)
(("1"
(hide -1)
(("1"
(expand "series")
(("1"
(case-replace
"(LAMBDA (k: nat):
IF k = 0 THEN Taylor_seq[T](f!1)(0)
ELSE Taylor_seq[T](f!1)(k) * x!1 ^ k
ENDIF) = (LAMBDA n:
IF n = 0 THEN f!1(0) ELSE Taylor_seq(f!1)(n) * x!1 ^ n ENDIF)")
(("1"
(hide 2)
(("1"
(apply-extensionality
1
:hide?
t)
(("1"
(lift-if)
(("1"
(ground)
(("1"
(expand
"Taylor_seq")
(("1"
(expand
"nderiv")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "T_pred_0")
nil
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite "T_pred_0")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "T_pred_0") 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)
("2" (lemma "not_one_element") (("2" (skosimp*) nil nil)) nil)
("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil)
("4" (skosimp*) (("4" (rewrite "T_pred_0") nil nil)) nil)
("5" (skosimp*)
(("5" (typepred "f!1")
(("5" (expand "inf_deriv_fun?") (("5" (inst?) nil nil)) nil))
nil))
nil)
("6" (lemma "not_one_element") (("6" (skosimp*) nil nil)) nil)
("7" (lemma "connected_domain") (("7" (skosimp*) nil nil)) nil))
nil)
((Taylors_inf formula-decl nil taylors "analysis/")
(nderiv def-decl "[T -> real]" nth_derivatives "analysis/")
(powerseq const-decl "sequence[real]" power_series nil)
(Taylor_rem const-decl "real" taylors "analysis/")
(nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
(between type-eq-decl nil taylors "analysis/")
(inf_deriv_fun? const-decl "bool" taylors "analysis/"))
nil)
(GET_C_TCC3-1 nil 3298627046
(""
(inst + "(LAMBDA (f:(inf_deriv_fun?[T]), x:T, k: nat):
choose({c: between[T](0, x) |
powerseries(Taylor_seq[T](f))(x)(k) =
f(x) -
Taylor_rem[T](1 + k, f, 0, x, c)}))")
(("1" (skosimp*)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (lemma "Taylors_inf[T]")
(("1" (inst - "0" "x!1" "f!1" "k!1")
(("1" (assert)
(("1" (skosimp*)
(("1" (inst - "c!1")
(("1" (lemma "Taylor_seq_term")
(("1" (inst?)
(("1" (assert) (("1" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (postpone) nil nil))
nil)
("2" (postpone) nil nil) ("3" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "not_one_element") (("2" (skosimp*) nil nil)) nil)
("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil)
("4" (skosimp*) (("4" (rewrite "T_pred_0") nil nil)) nil)
("5" (skosimp*)
(("5" (typepred "f!1")
(("5" (expand "inf_deriv_fun?") (("5" (inst?) nil nil)) nil))
nil))
nil)
("6" (lemma "not_one_element") (("6" (skosimp*) nil nil)) nil)
("7" (lemma "connected_domain") (("7" (skosimp*) nil nil)) nil))
nil)
nil shostak))
(is_taylor_prep_TCC1 0
(is_taylor_prep_TCC1-1 nil 3298631645
("" (skosimp*)
(("" (expand "inf_deriv_fun?") (("" (inst?) nil nil)) nil)) nil)
((inf_deriv_fun? const-decl "bool" taylors "analysis/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
shostak))
(is_taylor_prep 0
(is_taylor_prep-3 nil 3306575640
("" (skosimp*)
(("" (expand "conv_powerseries?")
(("" (skosimp*)
((""
(case-replace "powerseries(Taylor_seq(f!1))(x!1) = (LAMBDA n:
f!1(x!1) - Taylor_rem(n, f!1, 0, x!1, GET_C(f!1,x!1,n)))")
(("1" (hide -1)
(("1" (inst?)
(("1" (lemma "convergent_diff")
(("1"
(inst - "(LAMBDA n: f!1(x!1))"
"(LAMBDA n: Taylor_rem(n, f!1, 0, x!1, GET_C(f!1, x!1, n)))")
(("1" (assert)
(("1" (expand "-")
(("1" (assert)
(("1" (hide 2)
(("1" (lemma "convergent_const")
(("1" (expand "const_fun")
(("1" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "T_pred_0") nil nil)
("3" (skosimp*)
(("3" (expand "inf_deriv_fun?")
(("3" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (apply-extensionality 1 :hide? t)
(("1" (rewrite "T_pred_0") nil nil)
("2" (skosimp*)
(("2" (expand "inf_deriv_fun?") (("2" (inst?) nil nil))
nil))
nil))
nil))
nil)
("3" (rewrite "T_pred_0") nil nil)
("4" (skosimp*)
(("4" (expand "inf_deriv_fun?") (("4" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((conv_powerseries? const-decl "bool" power_series_conv nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sequence type-eq-decl nil sequences nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(powerseries const-decl "sequence[real]" power_series nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(T formal-nonempty-subtype-decl nil taylor_series nil)
(inf_deriv_fun? const-decl "bool" taylors "analysis/")
(Taylor_seq const-decl "real" taylor_series nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(derivable_n_times? def-decl "bool" nth_derivatives "analysis/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(Taylor_rem const-decl "real" taylors "analysis/")
(between type-eq-decl nil taylors "analysis/")
(GET_C const-decl "{c: between[T](0, x) |
powerseries(Taylor_seq(f))(x)(k) =
f(x) - Taylor_rem(k, f, 0, x, c)}" taylor_series nil)
(f!1 skolem-const-decl "[T -> real]" taylor_series nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(convergent_const formula-decl nil convergence_ops "analysis/")
(T_pred_0 formula-decl nil taylor_series nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(convergent_diff formula-decl nil convergence_ops "analysis/"))
nil)
(is_taylor_prep-2 nil 3298631567
("" (skosimp*)
(("" (expand "conv_powerseries?")
(("" (skosimp*)
((""
(case-replace
"powerseries(Taylor_seq[T](f!1))(x!1) = (LAMBDA n:
f!1(x!1) - Taylor_rem(n, f!1, 0, x!1, GET_C(f!1,x!1,n)))")
(("1" (hide -1)
(("1" (inst?)
(("1" (lemma "convergent_diff")
(("1"
(inst - "(LAMBDA n: f!1(x!1))"
"(LAMBDA n: Taylor_rem(n, f!1, 0, x!1, GET_C(f!1, x!1, n)))")
(("1" (assert)
(("1" (expand "-")
(("1" (assert)
(("1" (hide 2)
(("1" (lemma "convergent_const")
(("1" (expand "const_fun")
(("1" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "T_pred_0") nil nil)
("3" (skosimp*)
(("3" (expand "inf_deriv_fun?")
(("3" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (apply-extensionality 1 :hide? t)
(("1" (rewrite "T_pred_0") nil nil)
("2" (skosimp*)
(("2" (expand "inf_deriv_fun?") (("2" (inst?) nil nil))
nil))
nil))
nil))
nil)
("3" (rewrite "T_pred_0") nil nil)
("4" (skosimp*)
(("4" (expand "inf_deriv_fun?") (("4" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((convergent_diff formula-decl nil convergence_ops "analysis/")
(convergent_const formula-decl nil convergence_ops "analysis/")
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(Taylor_rem const-decl "real" taylors "analysis/")
(between type-eq-decl nil taylors "analysis/")
(nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
(inf_deriv_fun? const-decl "bool" taylors "analysis/"))
nil)
(is_taylor_prep-1 nil 3298379071
("" (skosimp*)
(("" (expand "conv_powerseries?")
(("" (skosimp*)
(("" (lemma "convergent_diff")
((""
(inst - "(LAMBDA (k: nat): f!1(x!1))"
"(LAMBDA k: Taylor_rem(k+1, f!1, 0, x!1, GET_C(f!1,x!1,k)))")
(("1" (expand "-")
(("1" (expand "powerseries")
(("1" (lemma "Taylor_seq_term")
(("1" (inst?)
(("1" (expand "powerseq")
(("1" (inst - "x!1")
(("1" (assert) (("1" (postpone) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "T_pred_0") nil nil)
("3" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil)
nil shostak))
(is_taylor_TCC1 0
(is_taylor_TCC1-1 nil 3298374726
("" (skosimp*)
(("" (lemma "is_taylor_prep")
(("" (inst?)
(("" (assert)
(("" (hide 2)
(("" (skosimp*)
(("" (inst?)
(("" (expand "convergent?") (("" (inst + "0") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((is_taylor_prep formula-decl nil taylor_series nil)
(convergent? const-decl "bool" convergence_sequences "analysis/")
(T formal-nonempty-subtype-decl nil taylor_series nil)
(T_pred const-decl "[real -> boolean]" taylor_series nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(is_taylor 0
(is_taylor-2 "sdf" 3298630239
("" (skosimp*)
(("" (apply-extensionality 1 :hide? t)
(("1" (expand "Inf_sum")
(("1" (expand "powerseries")
(("1" (lemma "limit_def")
(("1" (inst?)
--> --------------------
--> maximum size reached
--> --------------------
[ zur Elbe Produktseite wechseln0.23Quellennavigators
Analyse erneut starten
]
|
2026-03-28
|
