|
(taylors
(deriv_domain 0
(deriv_domain-2 nil 3472399633
("" (lemma "connected_deriv_domain[T]")
(("" (lemma not_one_element)
(("" (lemma "connected_domain") (("" (assert) nil nil)) nil))
nil))
nil)
((not_one_element formula-decl nil taylors nil)
(connected_domain formula-decl nil taylors nil)
(connected_deriv_domain formula-decl nil deriv_domain_def 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]" taylors nil)
(T formal-subtype-decl nil taylors nil))
nil)
(deriv_domain-1 nil 3471607174
("" (skosimp*)
(("" (lemma "connected_domain")
(("" (lemma "connected_deriv_domain[T]")
(("1" (replace -2) (("1" (inst?) nil nil)) nil)
("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil))
nil))
nil))
nil)
nil nil))
(sigma_derivable_TCC1 0
(sigma_derivable_TCC1-1 nil 3255192119
("" (skosimp*)
(("" (lemma "deriv_domain") (("" (inst?) nil nil)) nil)) nil)
((deriv_domain formula-decl nil taylors nil)) nil))
(sigma_derivable_TCC2 0
(sigma_derivable_TCC2-1 nil 3255192119
("" (skolem!)
(("" (lemma "not_one_element") (("" (propax) nil nil)) nil)) nil)
((not_one_element formula-decl nil taylors nil)) nil))
(sigma_derivable_TCC3 0
(sigma_derivable_TCC3-1 nil 3374341760 ("" (subtype-tcc) nil nil)
((derivable? const-decl "bool" derivatives nil)) nil))
(sigma_derivable 0
(sigma_derivable-1 nil 3255192119
("" (induct "n" 1)
(("1" (skosimp*)
(("1" (expand "sigma")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (skosimp*)
(("2" (expand "sigma" 1)
(("2"
(case-replace
"(LAMBDA aa: g!1(aa, 1 + j!1) + sigma(0, j!1, LAMBDA m: g!1(aa, m))) = (LAMBDA aa: g!1(aa, 1 + j!1)) + (LAMBDA aa: sigma(0, j!1, LAMBDA m: g!1(aa, m)))")
(("1" (hide -1)
(("1" (inst - "g!1")
(("1" (split -1)
(("1" (inst - "1+j!1")
(("1"
(lemma "sum_derivable_fun[T]"
("f1" "LAMBDA aa: g!1(aa, 1 + j!1)" "f2"
"LAMBDA aa: sigma(0, j!1, LAMBDA m: g!1(aa, m))"))
(("1" (assert) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (skosimp*) (("2" (inst - "ii!1") nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "+
")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((+ const-decl "[T -> real]" real_fun_ops "reals/")
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(sum_derivable_fun formula-decl nil derivatives nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sigma_0_neg formula-decl nil sigma_nat "reals/")
(nat_induction formula-decl nil naturalnumbers nil)
(sigma def-decl "real" sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(derivable? const-decl "bool" derivatives nil)
(subrange type-eq-decl nil integers nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(T formal-subtype-decl nil taylors nil)
(T_pred const-decl "[real -> boolean]" taylors nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(tay1_TCC1 0
(tay1_TCC1-1 nil 3255192119
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(tay1 0
(tay1-1 nil 3255192119
("" (skosimp*)
(("" (case "derivable?[T](LAMBDA x: (bb!1 - x) ^ n!1)")
(("1"
(lemma "scal_derivable_fun[T]"
("f" "LAMBDA x: (bb!1 - x) ^ n!1" "b" "1/ factorial(n!1)"))
(("1" (assert)
(("1" (expand "*") (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (hide 2)
(("2" (case "n!1=0")
(("1" (replace -1)
(("1" (expand "^")
(("1" (expand "expt")
(("1" (lemma "const_derivable_fun[T]" ("b" "1"))
(("1" (expand "const_fun") (("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "const_derivable_fun[T]" ("b" "bb!1"))
(("2" (lemma "identity_derivable_fun[T]")
(("2" (expand "I")
(("2" (expand "const_fun")
(("2"
(lemma "diff_derivable_fun[T]"
("f1" "LAMBDA (x: T): bb!1" "f2"
"LAMBDA (x: T): x"))
(("2" (expand "-")
(("2" (assert)
(("2"
(lemma "deriv_exp_fun[T]"
("f" "LAMBDA (x_1: T): bb!1 - x_1" "n"
"n!1"))
(("2" (assert)
(("2" (flatten -1)
(("2"
(expand "^" -1)
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nat nonempty-type-eq-decl nil naturalnumbers nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(^ const-decl "real" exponentiation nil)
(>= const-decl "bool" reals nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" 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)
(derivable? const-decl "bool" derivatives nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-subtype-decl nil taylors nil)
(T_pred const-decl "[real -> boolean]" taylors 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)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(scal_derivable_fun formula-decl nil derivatives 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 "[T, T -> boolean]" equalities nil)
(const_derivable_fun formula-decl nil derivatives nil)
(expt def-decl "real" exponentiation nil)
(identity_derivable_fun formula-decl nil derivatives nil)
(diff_derivable_fun formula-decl nil derivatives nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(^ const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_exp_fun formula-decl nil derivatives nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(I const-decl "(bijective?[T, T])" identity nil))
nil))
(tay2 0
(tay2-1 nil 3255192119
("" (skosimp*)
(("" (lemma "const_derivable_fun[T]" ("b" "bb!1"))
(("" (lemma "deriv_const_fun[T]" ("b" "bb!1"))
(("" (lemma "identity_derivable_fun[T]")
(("" (lemma "deriv_id_fun[T]")
(("" (expand "I")
(("" (expand "const_fun")
((""
(lemma "diff_derivable_fun[T]"
("f1" "LAMBDA (x: T): bb!1" "f2"
"LAMBDA (x: T): x"))
(("" (expand "-" -1)
(("" (assert)
((""
(lemma "deriv_diff_fun[T]"
("ff1" "LAMBDA (x: T): bb!1" "ff2"
"LAMBDA (x: T): x"))
(("" (replace -5)
(("" (replace -3)
(("" (expand "-" -1)
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-subtype-decl nil taylors nil)
(T_pred const-decl "[real -> boolean]" taylors 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)
(const_derivable_fun formula-decl nil derivatives nil)
(identity_derivable_fun formula-decl nil derivatives nil)
(I const-decl "(bijective?[T, T])" identity nil)
(diff_derivable_fun formula-decl nil derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(derivable? const-decl "bool" derivatives nil)
(bool nonempty-type-eq-decl nil booleans nil)
(deriv_diff_fun formula-decl nil derivatives nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(deriv_id_fun formula-decl nil derivatives nil)
(deriv_const_fun formula-decl nil derivatives nil))
nil))
(tay3_TCC1 0
(tay3_TCC1-1 nil 3255192119
("" (skosimp*) (("" (assert) nil nil)) nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(tay3 0
(tay3-1 nil 3255192119
("" (skosimp*)
(("" (lemma "tay1" ("bb" "bb!1" "n" "n!1+1"))
(("" (lemma "tay2" ("bb" "bb!1"))
(("" (flatten -1)
(("" (replace -3 1)
((""
(lemma "deriv_exp_fun[T]"
("f" "LAMBDA x: (bb!1 - x)" "n" "n!1+1"))
(("" (assert)
(("" (flatten -1)
(("" (replace -4)
(("" (expand "^" -2)
(("" (expand "const_fun")
(("" (expand "*" -2)
((""
(lemma "deriv_scal_fun[T]"
("ff"
"LAMBDA (t: T): (bb!1 - t) ^ (1 + n!1)"
"b" "1/factorial(1+n!1)"))
(("1" (replace -3 -1)
(("1"
(expand "*" -1)
(("1"
(replace -1 1)
(("1"
(lemma
"extensionality"
("f"
"(LAMBDA (x: T):
-1 * ((bb!1 - x) ^ n!1 * (1 / factorial(1 + n!1))) -
(bb!1 - x) ^ n!1 * (1 / factorial(1 + n!1)) * n!1)"
"g"
"-(LAMBDA x: (bb!1 - x) ^ n!1 / factorial(n!1))"))
(("1"
(split -1)
(("1" (assert) nil nil)
("2"
(hide-all-but 1)
(("2"
(skosimp*)
(("2"
(expand "-")
(("2"
(case
"-1 * ((bb!1 - x!1) ^ n!1) *(1+n!1)/factorial(1 + n!1) = -1 * ((bb!1 - x!1) ^ n!1)/factorial(n!1)")
(("1" (assert) nil nil)
("2"
(hide 2)
(("2"
(case
"(1 + n!1) / factorial(1 + n!1) = 1/factorial(n!1)")
(("1"
(assert)
nil
nil)
("2"
(hide 2)
(("2"
(expand
"factorial"
1
1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(expand "^" -1)
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(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)
(T formal-subtype-decl nil taylors nil)
(T_pred const-decl "[real -> boolean]" taylors 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)
(tay1 formula-decl nil taylors nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(deriv_exp_fun formula-decl nil derivatives nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(^ const-decl "[T -> real]" real_fun_ops "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(= const-decl "[T, T -> boolean]" equalities nil)
(minus_real_is_real application-judgement "real" reals nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(- const-decl "[numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(extensionality formula-decl nil functions nil)
(^ const-decl "real" exponentiation nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(deriv_fun type-eq-decl nil derivatives nil)
(derivable? const-decl "bool" derivatives nil)
(factorial def-decl "posnat" factorial "ints/")
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(deriv_scal_fun formula-decl nil derivatives nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(derivable_const application-judgement "deriv_fun" derivatives nil)
(const_fun_continuous application-judgement "continuous_fun"
continuous_functions nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(tay2 formula-decl nil taylors nil))
nil))
(deriv_sigma_TCC1 0
(deriv_sigma_TCC1-1 nil 3255192119
("" (skosimp*)
(("" (lemma "sigma_derivable" ("g" "FF!1" "n" "n1!1"))
(("" (replace -2 -1) (("" (propax) nil nil)) nil)) nil))
nil)
((T formal-subtype-decl nil taylors nil)
(T_pred const-decl "[real -> boolean]" taylors 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)
(sigma_derivable formula-decl nil taylors nil))
nil))
(deriv_sigma_TCC2 0
(deriv_sigma_TCC2-1 nil 3255192119
("" (skosimp*) (("" (inst - "ii1!1") (("" (assert) nil nil)) nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(subrange type-eq-decl nil integers nil)
(n!1 skolem-const-decl "nat" taylors nil)
(ii1!1 skolem-const-decl "nat" taylors nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(deriv_sigma 0
(deriv_sigma-2 nil 3303660794
("" (induct "n1")
(("1" (skosimp*)
(("1" (expand "sigma" 1)
(("1" (inst - "0")
(("1"
(lemma "extensionality"
("f" "deriv(LAMBDA x: FF!1(x, 0))" "g"
"(LAMBDA x: deriv(LAMBDA xx: FF!1(xx, 0))(x))"))
(("1" (split -1)
(("1" (assert) nil nil)
("2" (hide 2) (("2" (skosimp*) nil nil)) nil))
nil)
("2" (skosimp*) nil nil) ("3" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst - "FF!1")
(("2" (split -1)
(("1" (expand "sigma" 1)
(("1"
(lemma "deriv_sum_fun[T]"
("ff1" "LAMBDA x: FF!1(x, 1 + j!1)" "ff2"
"LAMBDA x: sigma(0, j!1, LAMBDA n: FF!1(x, n))"))
(("1" (replace -2 -1)
(("1" (expand "+" -1)
(("1" (replace -1 1)
(("1" (hide -1 -2)
(("1"
(lemma "extensionality"
("f" "(LAMBDA (x_1: T):
deriv(LAMBDA x: FF!1(x, 1 + j!1))(x_1) +
sigma(0, j!1,
LAMBDA ii:
IF ii > j!1 THEN 0
ELSE deriv(LAMBDA xx: FF!1(xx, ii))(x_1)
ENDIF))" "g" "(LAMBDA x:
deriv(LAMBDA xx: FF!1(xx, 1 + j!1))(x) +
sigma(0, j!1,
LAMBDA ii:
IF ii > 1 + j!1 THEN 0
ELSE deriv(LAMBDA xx: FF!1(xx, ii))(x)
ENDIF))"))
(("1" (split -1)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (skosimp*)
(("2"
(lemma
"sigma_eq[nat]"
("low"
"0"
"high"
"j!1"
"F"
"LAMBDA ii:
IF ii > j!1 THEN 0
ELSE deriv(LAMBDA xx: FF!1(xx, ii))(x!1)
ENDIF"
"G"
"LAMBDA ii:
IF ii > 1 + j!1 THEN 0
ELSE deriv(LAMBDA xx: FF!1(xx, ii))(x!1)
ENDIF"))
(("1"
(split -1)
(("1" (assert) nil nil)
("2"
(hide 2)
(("2"
(skosimp*)
(("2"
(typepred "n!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(skosimp*)
(("2"
(inst - "ii!1")
(("2" (assert) nil nil))
nil))
nil))
nil)
("3"
(hide 2)
(("3"
(skosimp*)
(("3"
(inst - "ii!1")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (inst - "ii!1")
(("2" (assert) nil nil)) nil))
nil))
nil)
("3" (skosimp*)
(("3" (hide 3)
(("3" (inst - "ii!1")
(("3" (assert) nil nil)) nil))
nil))
nil)
("4" (hide 2)
(("4" (skosimp*)
(("4" (inst - "1+j!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 2)
(("2" (lemma "sigma_derivable" ("g" "FF!1" "n" "j!1"))
(("2" (assert)
(("2" (hide 2)
(("2" (skosimp*) (("2" (inst - "ii!1") nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (inst - "1+j!1") nil nil))
nil))
nil)
("2" (skosimp*) (("2" (inst - "ii!1") nil nil)) nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (skosimp*)
(("3" (inst - "ii1!1") (("3" (assert) nil nil)) nil)) nil))
nil)
("4" (hide 2)
(("4" (skosimp*)
(("4" (lemma "sigma_derivable" ("g" "FF!1" "n" "n1!2"))
(("4" (replace -2) (("4" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((ii1!1 skolem-const-decl "nat" taylors nil)
(n1!2 skolem-const-decl "nat" taylors nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(deriv_sum_fun formula-decl nil derivatives nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(ii!1 skolem-const-decl "nat" taylors nil)
(ii!1 skolem-const-decl "nat" taylors nil)
(ii!1 skolem-const-decl "nat" taylors nil)
(ii!1 skolem-const-decl "nat" taylors nil)
(j!1 skolem-const-decl "nat" taylors nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sigma_eq formula-decl nil sigma "reals/")
(sigma_derivable formula-decl nil taylors nil)
(sigma_0_neg formula-decl nil sigma_nat "reals/")
(extensionality formula-decl nil functions nil)
(nat_induction formula-decl nil naturalnumbers nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(deriv const-decl "[T -> real]" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(pred type-eq-decl nil defined_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(> const-decl "bool" 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)
(T_pred const-decl "[real -> boolean]" taylors nil)
(T formal-subtype-decl nil taylors nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(subrange type-eq-decl nil integers nil)
(derivable? const-decl "bool" derivatives nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(sigma def-decl "real" sigma "reals/"))
nil)
(deriv_sigma-1 nil 3255192119
("" (induct "n")
(("1" (skosimp*)
(("1" (expand "sigma" 1)
(("1" (inst - "0")
(("1"
(lemma "extensionality"
("f" "deriv(LAMBDA x: FF!1(x, 0))" "g"
"(LAMBDA x: deriv(LAMBDA xx: FF!1(xx, 0))(x))"))
(("1" (split -1)
(("1" (propax) nil nil)
("2" (hide 2) (("2" (skosimp*) nil nil)) nil))
nil)
("2" (skosimp*) nil nil) ("3" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (inst - "FF!1")
(("2" (split -1)
(("1" (expand "sigma" 1)
(("1"
(lemma "deriv_sum_fun[T]"
("ff1" "LAMBDA x: FF!1(x, 1 + j!1)" "ff2"
"LAMBDA x: sigma(0, j!1, LAMBDA n: FF!1(x, n))"))
(("1" (replace -2 -1)
(("1" (expand "+" -1)
(("1" (replace -1 1)
(("1" (hide -1 -2)
(("1"
(lemma "extensionality"
("f" "(LAMBDA (x_1: T):
deriv(LAMBDA x: FF!1(x, 1 + j!1))(x_1) +
sigma(0, j!1,
LAMBDA ii:
IF ii > j!1 THEN 0
ELSE deriv(LAMBDA xx: FF!1(xx, ii))(x_1)
ENDIF))" "g" "(LAMBDA x:
deriv(LAMBDA xx: FF!1(xx, 1 + j!1))(x) +
sigma(0, j!1,
LAMBDA ii:
IF ii > 1 + j!1 THEN 0
ELSE deriv(LAMBDA xx: FF!1(xx, ii))(x)
ENDIF))"))
(("1" (split -1)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (skosimp*)
(("2"
(lemma
"sigma_eq[nat]"
("low"
"0"
"high"
"j!1"
"F"
"LAMBDA ii:
IF ii > j!1 THEN 0
ELSE deriv(LAMBDA xx: FF!1(xx, ii))(x!1)
ENDIF"
"G"
"LAMBDA ii:
IF ii > 1 + j!1 THEN 0
ELSE deriv(LAMBDA xx: FF!1(xx, ii))(x!1)
ENDIF"))
(("1"
(split -1)
(("1" (assert) nil nil)
("2"
(hide 2)
(("2"
(skosimp*)
(("2"
(typepred "n!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(skosimp*)
(("2"
(inst - "ii!1")
(("2" (assert) nil nil))
nil))
nil))
nil)
("3"
(hide 2)
(("3"
(skosimp*)
(("3"
(inst - "ii!1")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (inst - "ii!1")
(("2" (assert) nil nil)) nil))
nil))
nil)
("3" (skosimp*)
(("3" (hide 3)
(("3" (inst - "ii!1")
(("3" (assert) nil nil)) nil))
nil))
nil)
("4" (hide 2)
(("4" (skosimp*)
(("4" (inst - "1+j!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 2)
(("2"
(lemma "sigma_derivable[T]" ("g" "FF!1" "n" "j!1"))
(("2" (assert)
(("2" (hide 2)
(("2" (skosimp*) (("2" (inst - "ii!1") nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (inst - "1+j!1") nil nil))
nil))
nil)
("2" (skosimp*) (("2" (inst - "ii!1") nil nil)) nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (skosimp*)
(("3" (inst - "ii1!1") (("3" (assert) nil nil)) nil)) nil))
nil)
("4" (hide 2)
(("4" (skosimp*)
(("4" (lemma "sigma_derivable[T]" ("g" "FF!1" "n" "n!2"))
(("4" (replace -2) (("4" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((deriv_sum_fun formula-decl nil derivatives nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(sigma_eq formula-decl nil sigma "reals/")
(deriv const-decl "[T -> real]" derivatives nil)
(deriv_fun type-eq-decl nil derivatives nil)
(sigma def-decl "real" sigma "reals/"))
nil))
(nderiv_term_derivable_TCC1 0
(nderiv_term_derivable_TCC1-1 nil 3255192119
("" (skosimp*)
(("" (lemma "derivable_n_times_lem[T]")
(("" (inst - "f!1" "n!1" "n!1+1") (("" (assert) nil nil)) nil))
nil))
nil)
((T formal-subtype-decl nil taylors nil)
(T_pred const-decl "[real -> boolean]" taylors 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)
(derivable_n_times_lem formula-decl nil nth_derivatives nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil))
(nderiv_term_derivable 0
(nderiv_term_derivable-1 nil 3255192119
("" (skosimp*)
(("" (case "n!1=0")
(("1" (replace -1)
(("1" (expand "derivable_n_times?")
(("1" (flatten -2) (("1" (rewrite "eta" 1) nil nil)) nil))
nil))
nil)
("2" (assert)
(("2"
(lemma "nderiv_derivable[T]" ("f" "f!1" "n" "n!1" "m" "n!1"))
(("2" (assert)
(("2" (lemma "tay1" ("bb" "bb!1" "n" "n!1"))
(("2"
(lemma "prod_derivable_fun[T]"
("f1" "nderiv(n!1, f!1)" "f2"
"LAMBDA x: (bb!1 - x) ^ n!1 / factorial(n!1)"))
(("1" (assert)
(("1" (expand "*") (("1" (assert) nil nil)) nil))
nil)
("2"
(lemma "derivable_n_times_lem[T]"
("f" "f!1" "n" "1+n!1" "m" "n!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(derivable_n_times? def-decl "bool" nth_derivatives nil)
(T formal-subtype-decl nil taylors nil)
(T_pred const-decl "[real -> boolean]" taylors nil)
(eta formula-decl nil functions nil)
(nderiv_derivable formula-decl nil nth_derivatives nil)
(tay1 formula-decl nil taylors nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(prod_derivable_fun formula-decl nil derivatives nil)
(nderiv_fun type-eq-decl nil nth_derivatives nil)
(nderiv def-decl "[T -> real]" nth_derivatives nil)
(numfield nonempty-type-eq-decl nil 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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "real" exponentiation nil)
(- const-decl "[numfield, numfield -> 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/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_times_real_is_real application-judgement "real" reals nil))
nil))
(taylor_derivable_TCC1 0
(taylor_derivable_TCC1-1 nil 3255192119
("" (skosimp*) (("" (inst + "0") (("" (assert) 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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(taylor_derivable_TCC2 0
(taylor_derivable_TCC2-1 nil 3255192119
("" (skosimp*)
(("" (lemma "derivable_n_times_lem[T]")
(("" (inst - "f!1" "nn!1" "n!1+1") (("" (assert) nil nil)) nil))
nil))
nil)
((T formal-subtype-decl nil taylors nil)
(T_pred const-decl "[real -> boolean]" taylors 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)
(derivable_n_times_lem formula-decl nil nth_derivatives nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(+ 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)
(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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil))
(taylor_derivable_TCC3 0
(taylor_derivable_TCC3-1 nil 3374341760
("" (skosimp*)
(("" (lemma "derivable_n_times_lem[T]")
(("" (inst - "f!1" "nn!1" "n!1+1") (("" (assert) nil nil)) nil))
nil))
nil)
((T formal-subtype-decl nil taylors nil)
(T_pred const-decl "[real -> boolean]" taylors 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)
(derivable_n_times_lem formula-decl nil nth_derivatives nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(+ const-decl "[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)
(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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil))
(taylor_derivable 0
(taylor_derivable-2 nil 3306748084
("" (skosimp*)
(("" (lemma "const_derivable_fun[T]" ("b" "f!1(bb!1)"))
(("" (expand "const_fun")
((""
(lemma "nderiv_term_derivable"
("f" "f!1" "n" "n!1" "bb" "bb!1"))
(("" (replace -3)
((""
(lemma "sigma_derivable"
("g" "LAMBDA (aa: T, nn:nat):IF nn > n!1 THEN 0
ELSIF nn = 0 THEN f!1(aa)
ELSE nderiv(nn, f!1)(aa) * (bb!1 - aa) ^ nn /
factorial(nn)
ENDIF" "n" "n!1"))
(("1" (split -1)
(("1" (simplify -1)
(("1"
(lemma "diff_derivable_fun[T]"
("f1" "LAMBDA (x: T): f!1(bb!1)" "f2"
"LAMBDA (aa_1: T):
sigma(0, n!1,
LAMBDA m:
IF m > n!1 THEN 0
ELSIF m = 0 THEN f!1(aa_1)
ELSE nderiv(m, f!1)(aa_1) * (bb!1 - aa_1) ^ m /
factorial(m)
ENDIF)"))
(("1" (assert)
(("1" (expand "-" -1) (("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (typepred "ii!1")
(("2" (assert)
(("2"
(lemma "derivable_n_times_lem[T]"
("f" "f!1" "n" "1+n!1" "m" "ii!1+1"))
(("2" (assert)
(("2"
(lemma "nderiv_term_derivable"
("f" "f!1" "n" "ii!1" "bb" "bb!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2"
(lemma "derivable_n_times_lem[T]"
("f" "f!1" "n" "n!1+1" "m" "nn!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-subtype-decl nil taylors nil)
(T_pred const-decl "[real -> boolean]" taylors 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)
(const_derivable_fun formula-decl nil derivatives nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sigma def-decl "real" sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(<= const-decl "bool" reals nil)
(diff_derivable_fun formula-decl nil derivatives nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(derivable_n_times_lem formula-decl nil nth_derivatives nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(subrange type-eq-decl nil integers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sigma_derivable formula-decl nil taylors nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(> const-decl "bool" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(derivable_n_times? def-decl "bool" nth_derivatives nil)
(nderiv_fun type-eq-decl nil nth_derivatives nil)
(nderiv def-decl "[T -> real]" nth_derivatives nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "real" exponentiation nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(factorial def-decl "posnat" factorial "ints/")
(nderiv_term_derivable formula-decl nil taylors 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))
nil)
(taylor_derivable-1 nil 3255192119
("" (skosimp*)
(("" (lemma "const_derivable_fun[T]" ("b" "f!1(bb!1)"))
(("" (expand "const_fun")
((""
(lemma "nderiv_term_derivable[T]"
("f" "f!1" "n" "n!1" "bb" "bb!1"))
(("" (replace -3)
((""
(lemma "sigma_derivable[T]"
("g" "LAMBDA (aa: T, nn:nat):IF nn > n!1 THEN 0
ELSIF nn = 0 THEN f!1(aa)
ELSE nderiv(nn, f!1)(aa) * (bb!1 - aa) ^ nn /
factorial(nn)
ENDIF" "n" "n!1"))
(("1" (split -1)
(("1" (simplify -1)
(("1"
(lemma "diff_derivable_fun[T]"
("f1" "LAMBDA (x: T): f!1(bb!1)" "f2"
"LAMBDA (aa_1: T):
sigma(0, n!1,
LAMBDA m:
IF m > n!1 THEN 0
ELSIF m = 0 THEN f!1(aa_1)
ELSE nderiv(m, f!1)(aa_1) * (bb!1 - aa_1) ^ m /
factorial(m)
ENDIF)"))
(("1" (assert)
(("1" (expand "-" -1) (("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp*)
(("2" (typepred "ii!1")
(("2" (assert)
(("2"
(lemma "derivable_n_times_lem[T]"
("f" "f!1" "n" "1+n!1" "m" "ii!1+1"))
(("2" (assert)
(("2"
(lemma "nderiv_term_derivable[T]"
("f" "f!1" "n" "ii!1" "bb" "bb!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2"
(lemma "derivable_n_times_lem[T]"
("f" "f!1" "n" "n!1+1" "m" "nn!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((const_derivable_fun formula-decl nil derivatives nil)
(nderiv def-decl "[T -> real]" nth_derivatives nil)
(nderiv_fun type-eq-decl nil nth_derivatives nil)
(derivable_n_times_lem formula-decl nil nth_derivatives nil)
(sigma def-decl "real" sigma "reals/")
(diff_derivable_fun formula-decl nil derivatives nil)
(const_fun const-decl "[T -> real]" real_fun_ops "reals/"))
nil))
(deriv_nderiv_TCC1 0
(deriv_nderiv_TCC1-1 nil 3255192119
("" (skosimp*)
((""
(lemma "derivable_n_times_lem" ("f" "f!1" "n" "n!1+1" "m" "n!1"))
(("" (assert) nil nil)) nil))
nil)
((T formal-subtype-decl nil taylors nil)
(T_pred const-decl "[real -> boolean]" taylors 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)
(+ 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)
(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)
(derivable_n_times_lem formula-decl nil nth_derivatives nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(deriv_nderiv_TCC2 0
(deriv_nderiv_TCC2-1 nil 3255192119
("" (skosimp*)
(("" (lemma "nderiv_derivable_eqv[T]" ("f" "f!1" "n" "n!1"))
(("" (replace -2 -1)
(("" (flatten -1)
((""
(lemma "extensionality"
("f" "nderiv(n!1, f!1)" "g"
"LAMBDA xx: (nderiv[T](n!1, f!1)(xx))"))
(("1" (split -1)
(("1" (replace -1 1 rl) (("1" (propax) nil nil)) nil)
("2" (hide 2) (("2" (skosimp*) nil nil)) nil))
nil)
("2" (skosimp*) nil nil) ("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
((T formal-subtype-decl nil taylors nil)
(T_pred const-decl "[real -> boolean]" taylors 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)
(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)
(nderiv_derivable_eqv formula-decl nil nth_derivatives nil)
(extensionality formula-decl nil functions nil)
(derivable_n_times? def-decl "bool" nth_derivatives nil)
(nderiv_fun type-eq-decl nil nth_derivatives nil)
(nderiv def-decl "[T -> real]" nth_derivatives nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(deriv_nderiv_TCC3 0
(deriv_nderiv_TCC3-1 nil 3255192119
("" (skosimp*) (("" (assert) nil nil)) nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil))
(deriv_nderiv 0
(deriv_nderiv-1 nil 3255192119
("" (skosimp*)
(("" (lemma "nderiv_derivable_aux" ("f" "f!1" "n" "n!1"))
(("" (assert)
(("" (replace -1 1)
((""
(lemma "extensionality"
("f" "LAMBDA xx: (nderiv(n!1, f!1)(xx))" "g"
"nderiv(n!1, f!1)"))
(("1" (split -1)
(("1" (replace -1) (("1" (propax) nil nil)) nil)
("2" (hide 2) (("2" (skosimp*) nil nil)) nil))
nil)
("2" (hide 2)
(("2"
(lemma "derivable_n_times_lem[T]"
("f" "f!1" "n" "n!1+1" "m" "n!1"))
(("2" (assert) nil nil)) nil))
nil)
("3" (skosimp*)
(("3"
(lemma "derivable_n_times_lem[T]"
("f" "f!1" "n" "n!1+1" "m" "n!1"))
(("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-subtype-decl nil taylors nil)
(T_pred const-decl "[real -> boolean]" taylors 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)
(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)
(nderiv_derivable_aux formula-decl nil nth_derivatives nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(extensionality formula-decl nil functions nil)
(derivable_n_times? def-decl "bool" nth_derivatives nil)
(nderiv_fun type-eq-decl nil nth_derivatives nil)
(nderiv def-decl "[T -> real]" nth_derivatives nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil))
(term_by_term_deriv_TCC1 0
(term_by_term_deriv_TCC1-1 nil 3255192119
("" (skosimp*) (("" (inst + "0") (("" (assert) 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)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(term_by_term_deriv_TCC2 0
(term_by_term_deriv_TCC2-1 nil 3255192119
("" (skosimp*)
(("" (lemma "derivable_n_times_lem[T]")
(("" (inst - "f!1" "ii!1" "n!1+1") (("" (assert) nil nil)) nil))
nil))
nil)
((T formal-subtype-decl nil taylors nil)
(T_pred const-decl "[real -> boolean]" taylors 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)
(derivable_n_times_lem formula-decl nil nth_derivatives nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil))
(term_by_term_deriv_TCC3 0
(term_by_term_deriv_TCC3-1 nil 3255192119
("" (skosimp*)
(("" (case "ii!1=0")
(("1" (propax) nil nil)
("2" (assert)
(("2" (expand "derivable_n_times?")
(("2"
(lemma "extensionality"
("f" "f!1" "g" "LAMBDA xx: f!1(xx)"))
(("2" (split -1)
(("1" (skosimp*)
(("1" (assert)
(("1"
(lemma "nderiv_derivable[T]"
("f" "f!1" "n" "n!1" "m" "ii!1"))
(("1" (assert)
(("1" (lemma "identity_derivable_fun[T]")
(("1" (expand "I")
(("1" (assert)
(("1" (hide -2)
(("1"
(lemma
"derivable_n_times_lem[T]"
("f" "f!1" "n" "1+n!1" "m" "ii!1"))
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
[ Dauer der Verarbeitung: 0.80 Sekunden
(vorverarbeitet)
]
|
