| products/sources/formale Sprachen/PVS/analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Complex.thy Sprache: IsabelleOriginal von: PVS© |
|
||||||
|
(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) ((fullset const-decl "set" sets nil) (adh const-decl "setof[real]" convergence_functions nil) (NQ const-decl "real" derivatives_def nil) (convergence const-decl "bool" convergence_functions nil) (convergence const-decl "bool" lim_of_functions nil) (convergent? const-decl "bool" lim_of_functions nil) (derivable? const-decl "bool" derivatives_def nil) (derivable? const-decl "bool" derivatives nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals 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 a (("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" (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) (constant_seq2 application-judgement "(convergent_nz?)" convergence_ops 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) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.112 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
