| products/Sources/formale Sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: matrix_diag.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(taylor_series
(T_pred_0 0 (T_pred_0-1 nil 3298383901 ("" (name "XX" "choose({X:T | TRUE})") (("1" (lemma "ball") (("1" (inst - "XX") (("1" (assert) (("1" (lemma "connected_domain") (("1" (expand "connected?") (("1" (case "XX >= 0") (("1" (inst - "-XX" "XX" "0") (("1" (assert) nil nil)) nil) ("2" (inst - "XX" "-XX" "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (ball formula-decl nil taylor_series nil) (minus_real_is_real application-judgement "real" reals nil) (connected? const-decl "bool" deriv_domain_def "analysis/") (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (connected_domain formula-decl nil taylor_series nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (T formal-nonempty-subtype-decl nil taylor_series nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (TRUE const-decl "bool" booleans nil)) nil)) (IMP_power_series_deriv_TCC1 0 (IMP_power_series_deriv_TCC1-1 nil 3298366313 ("" (lemma "connected_domain") (("" (propax) nil nil)) nil) ((connected_domain formula-decl nil taylor_series nil)) shostak)) (IMP_power_series_deriv_TCC2 0 (IMP_power_series_deriv_TCC2-1 nil 3298366313 ("" (skosimp*) (("" (lemma "not_one_element") (("" (inst?) nil nil)) nil)) nil) ((not_one_element formula-decl nil taylor_series nil)) shostak)) (IMP_power_series_deriv_TCC3 0 (IMP_power_series_deriv_TCC3-1 nil 3298366313 ("" (skosimp*) (("" (lemma "open") (("" (inst?) nil nil)) nil)) nil) ((open formula-decl nil taylor_series nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (T formal-nonempty-subtype-decl nil taylor_series nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (IMP_power_series_deriv_TCC4 0 (IMP_power_series_deriv_TCC4-1 nil 3298366313 ("" (lemma "ball") (("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (T formal-nonempty-subtype-decl nil taylor_series nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (ball formula-decl nil taylor_series nil)) shostak)) (deriv_domain 0 (deriv_domain-1 nil 3472466626 ("" (lemma connected_domain) (("" (lemma not_one_element) (("" (lemma connected_deriv_domain[T]) (("" (assert) nil nil)) nil)) nil)) nil) ((not_one_element formula-decl nil taylor_series nil) (connected_deriv_domain formula-decl nil deriv_domain_def "analysis/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (T formal-nonempty-subtype-decl nil taylor_series nil) (connected_domain formula-decl nil taylor_series nil)) shostak)) (Inf_sum_0_TCC1 0 (Inf_sum_0_TCC1-1 nil 3298366313 ("" (skosimp*) (("" (name "XX" "epsilon({X:T | TRUE})") (("" (lemma "ball") (("" (inst - "XX") (("" (assert) (("" (lemma "connected_domain") (("" (expand "connected?") (("" (case "XX >= 0") (("1" (inst - "-XX" "XX" "0") (("1" (assert) nil nil)) nil) ("2" (inst - "XX" "-XX" "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((TRUE const-decl "bool" booleans nil) (epsilon const-decl "T" epsilons nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (T formal-nonempty-subtype-decl nil taylor_series nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (connected_domain formula-decl nil taylor_series nil) (>= const-decl "bool" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (connected? const-decl "bool" deriv_domain_def "analysis/") (minus_real_is_real application-judgement "real" reals nil) (ball formula-decl nil taylor_series nil)) shostak)) (Inf_sum_0 0 (Inf_sum_0-1 nil 3298299936 ("" (skosimp*) (("" (expand "Inf_sum") (("" (assert) (("" (expand "powerseries") (("" (expand "powerseq") (("" (case-replace "(LAMBDA (k: nat): a!1(k) * 0 ^ k) = (LAMBDA (k: nat): IF k = 0 THEN a!1(0) ELSE 0 ENDIF)") (("1" (hide -1) (("1" (expand "series") (("1" (lemma "sigma_first[nat]") (("1" (inst?) (("1" (case-replace "(LAMBDA (n: nat): sigma(0, n, (LAMBDA (k: nat): IF k = 0 THEN a!1(0) ELSE 0 ENDIF))) = (LAMBDA (n: nat): a!1(0) )") (("1" (lemma "limit_const") (("1" (inst - "a!1(0)") (("1" (assert) (("1" (expand "const_fun") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (lemma "sigma_first[nat]") (("2" (inst?) (("2" (assert) (("2" (case-replace "x!1 = 0") (("1" (expand "sigma" 1) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (rewrite "sigma_restrict_to") (("2" (expand "restrict") (("2" (lemma "sigma_const") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("2" (lift-if) (("2" (ground) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Inf_sum const-decl "real" power_series_conv nil) (powerseries const-decl "sequence[real]" power_series nil) (real_times_real_is_real application-judgement "real" reals nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sequence type-eq-decl nil sequences nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (series const-decl "sequence[real]" series nil) (int_minus_int_is_int application-judgement "int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (T_low type-eq-decl nil sigma "reals/") (<= const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (restrict const-decl "[T -> real]" sigma "reals/") (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (sigma_nat application-judgement "nat" sigma_nat "reals/") (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (sigma_const formula-decl nil sigma "reals/") (sigma_restrict_to formula-decl nil sigma "reals/") (odd_minus_odd_is_even application-judgement "even_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (limit_const formula-decl nil convergence_ops "analysis/") (constant_seq1 application-judgement "(convergent?)" convergence_ops "analysis/") (derivable_const application-judgement "deriv_fun" derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_first formula-decl nil sigma "reals/") (nat_exp application-judgement "nat" exponentiation nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (zero_hat formula-decl nil exponent_props "reals/") (nat_expt application-judgement "nat" exponentiation nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (expt def-decl "real" exponentiation nil) (powerseq const-decl "sequence[real]" power_series nil)) shostak)) (nderivseq_lem 0 (nderivseq_lem-1 nil 3298373671 ("" (skosimp*) (("" (expand "nderivseq") (("" (apply-extensionality 1 :hide? t) (("" (rewrite "factorial_plus1") (("" (assert) (("" (expand "derivseq") (("" (name-replace "FNX" "factorial(n!1 + x!1)") (("" (field 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nderivseq const-decl "sequence[real]" taylor_series nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (factorial_plus1 formula-decl nil factorial "ints/") (int_minus_int_is_int application-judgement "int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (real_plus_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_times_real_is_real application-judgement "real" reals nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (factorial def-decl "posnat" factorial "ints/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sequence type-eq-decl nil sequences nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (T formal-nonempty-subtype-decl nil taylor_series nil) (derivseq const-decl "sequence[real]" power_series_derivseq nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (conv_nderivseq 0 (conv_nderivseq-1 nil 3298367015 ("" (induct "n") (("1" (skosimp*) (("1" (expand "nderivseq") (("1" (case-replace "(LAMBDA (k: nat): factorial(k) / factorial(k) * a!1(k)) = a!1") (("1" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "nderivseq_lem") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (rewrite "conv_derivseq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((derivseq const-decl "sequence[real]" power_series_derivseq nil) (conv_derivseq formula-decl nil power_series_derivseq nil) (int_minus_int_is_int application-judgement "int" integers nil) (nderivseq_lem formula-decl nil taylor_series nil) (numfield nonempty-type-eq-decl nil number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (factorial def-decl "posnat" factorial "ints/") (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_times_real_is_real application-judgement "real" reals nil) (nat_induction formula-decl nil naturalnumbers nil) (nderivseq const-decl "sequence[real]" taylor_series nil) (conv_powerseries? const-decl "bool" power_series_conv nil) (T formal-nonempty-subtype-decl nil taylor_series nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sequence type-eq-decl nil sequences nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (Inf_sum_derivable_n_times_TCC1 0 (Inf_sum_derivable_n_times_TCC1-1 nil 3471697763 ("" (skosimp*) (("" (lemma "deriv_domain") (("" (inst?) nil nil)) nil)) nil) ((deriv_domain formula-decl nil taylor_series nil)) nil)) (Inf_sum_derivable_n_times 0 (Inf_sum_derivable_n_times-1 nil 3298373838 ("" (induct "n") (("1" (skosimp*) (("1" (expand "derivable_n_times?") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "derivable_n_times?" 1) (("2" (rewrite "Inf_sum_derivable") (("2" (inst - "derivseq(a!1)") (("2" (rewrite "conv_derivseq") (("2" (rewrite "deriv_Inf_sum") nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (lemma "not_one_element") (("3" (skosimp*) nil nil)) nil)) nil) ("4" (hide 2) (("4" (lemma "connected_domain") (("4" (skosimp*) nil nil)) nil)) nil)) nil) ((Inf_sum_derivable formula-decl nil power_series_deriv nil) (conv_derivseq formula-decl nil power_series_derivseq nil) (deriv_Inf_sum formula-decl nil power_series_deriv nil) (derivseq const-decl "sequence[real]" power_series_derivseq nil) (nat_induction formula-decl nil naturalnumbers nil) (Inf_sum const-decl "real" power_series_conv nil) (derivable_n_times? def-decl "bool" nth_derivatives "analysis/") (conv_powerseries? const-decl "bool" power_series_conv nil) (T formal-nonempty-subtype-decl nil taylor_series nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (sequence type-eq-decl nil sequences nil) (pred type-eq-decl nil defined_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (nderiv_Inf_sum_TCC1 0 (nderiv_Inf_sum_TCC1-1 nil 3298366314 ("" (skosimp*) (("" (rewrite "Inf_sum_derivable_n_times") nil nil)) nil) ((Inf_sum_derivable_n_times formula-decl nil taylor_series nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sequence type-eq-decl nil sequences nil)) shostak)) (nderiv_Inf_sum_TCC2 0 (nderiv_Inf_sum_TCC2-1 nil 3298366314 ("" (skosimp*) (("" (lemma " conv_nderivseq") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((conv_nderivseq formula-decl nil taylor_series nil) (sequence type-eq-decl nil sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (nderiv_Inf_sum 0 (nderiv_Inf_sum-1 nil 3298302128 ("" (induct "n") (("1" (skosimp*) (("1" (expand "nderiv") (("1" (expand "nderivseq") (("1" (case-replace "(LAMBDA (k: nat): factorial(k) / factorial(k) * a!1(k)) = a!1") (("1" (hide 2) (("1" (apply-extensionality 1 :hide? t) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "nderiv" 1) (("2" (lemma "deriv_Inf_sum") (("2" (inst?) (("2" (assert) (("2" (replace -1) (("2" (hide -1) (("2" (inst?) (("2" (rewrite "conv_derivseq") (("2" (replace -1) (("2" (hide -1) (("2" (case-replace "nderivseq(j!1, derivseq(a!1)) = nderivseq(1 + j!1, a!1)") (("2" (hide 2) (("2" (expand "nderivseq") (("2" (expand "derivseq") (("2" (apply-extensionality 1 :hide? t) (("2" (name-replace "AA" "a!1(1 + j!1 + x!1)") (("2" (case-replace "factorial(1 + j!1 + x!1) = (1 + j!1 + x!1)*factorial(j!1 + x!1)") (("1" (name-replace "FF" "factorial(j!1 + x!1)") (("1" (field 1) nil nil)) nil) ("2" (hide 2) (("2" (expand "factorial" 1 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (rewrite "conv_nderivseq") nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (rewrite "Inf_sum_derivable_n_times") nil nil)) nil)) nil)) nil) ((Inf_sum_derivable_n_times formula-decl nil taylor_series nil) (conv_nderivseq formula-decl nil taylor_series nil) (deriv_Inf_sum formula-decl nil power_series_deriv nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (conv_derivseq formula-decl nil power_series_derivseq nil) (real_minus_real_is_real application-judgement "real" reals nil) (posint nonempty-type-eq-decl nil integers nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (div_cancel2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (both_sides_times1 formula-decl nil real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (derivseq const-decl "sequence[real]" power_series_derivseq nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_times_real_is_real application-judgement "real" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (factorial def-decl "posnat" factorial "ints/") (nat_induction formula-decl nil naturalnumbers nil) (nderiv def-decl "[T -> real]" nth_derivatives "analysis/") (nderiv_fun type-eq-decl nil nth_derivatives "analysis/") (= const-decl "[T, T -> boolean]" equalities nil) (pred type-eq-decl nil defined_types nil) (nderivseq const-decl "sequence[real]" taylor_series nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sequence type-eq-decl nil sequences nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (T formal-nonempty-subtype-decl nil taylor_series nil) (conv_powerseries? const-decl "bool" power_series_conv nil) (derivable_n_times? def-decl "bool" nth_derivatives "analysis/") (Inf_sum const-decl "real" power_series_conv nil)) shostak)) (Taylor_expansion 0 (Taylor_expansion-1 nil 3298298896 ("" (skosimp*) (("" (replace -2) (("" (lemma "nderiv_Inf_sum") (("" (inst?) (("" (assert) (("" (replace -1) (("" (hide -1) (("" (lemma "Inf_sum_0") (("" (rewrite "Inf_sum_0") (("1" (lemma "Inf_sum_derivable_n_times") (("1" (inst?) (("1" (assert) (("1" (expand "nderivseq") (("1" (expand "factorial" 1 3) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "conv_nderivseq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (sequence type-eq-decl nil sequences nil) (Inf_sum_0 formula-decl nil taylor_series nil) (conv_nderivseq formula-decl nil taylor_series nil) (Inf_sum_derivable_n_times formula-decl nil taylor_series nil) (factorial def-decl "posnat" factorial "ints/") (real_times_real_is_real application-judgement "real" reals nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nderivseq const-decl "sequence[real]" taylor_series nil) (nderiv_Inf_sum formula-decl nil taylor_series nil)) shostak)) (Taylor_seq_TCC1 0 (Taylor_seq_TCC1-1 nil 3298631644 ("" (skosimp*) (("" (rewrite "T_pred_0") nil nil)) nil) ((T_pred_0 formula-decl nil taylor_series nil)) shostak)) (Taylor_seq_TCC2 0 (Taylor_seq_TCC2-1 nil 3298631644 ("" (skosimp*) (("" (typepred "f!1") (("" (expand "inf_deriv_fun?") (("" (inst?) nil nil)) nil)) nil)) nil) ((inf_deriv_fun? const-decl "bool" taylors "analysis/") (T formal-nonempty-subtype-decl nil taylor_series nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil)) shostak)) (Taylor_seq_TCC3 0 (Taylor_seq_TCC3-1 nil 3471697763 ("" (skosimp*) (("" (lemma "deriv_domain") (("" (inst?) nil nil)) nil)) nil) ((deriv_domain formula-decl nil taylor_series nil)) nil)) (Taylor_seq_term_TCC1 0 (Taylor_seq_term_TCC1-1 nil 3298631644 ("" (skosimp*) (("" (rewrite "T_pred_0") nil nil)) nil) ((T_pred_0 formula-decl nil taylor_series nil)) shostak)) (Taylor_seq_term_TCC2 0 (Taylor_seq_term_TCC2-1 nil 3298631644 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (Taylor_seq_term_TCC3 0 (Taylor_seq_term_TCC3-1 nil 3298631644 ("" (skosimp*) (("" (rewrite "T_pred_0") nil nil)) nil) ((T_pred_0 formula-decl nil taylor_series nil)) shostak)) (Taylor_seq_term 0 (Taylor_seq_term-1 nil 3298383588 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("1" (expand "Taylor_seq") (("1" (expand "Taylor_term") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (rewrite "T_pred_0") nil nil) ("3" (rewrite "T_pred_0") (("3" (skosimp*) nil nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Taylor_term const-decl "real" taylors "analysis/") (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (Taylor_seq const-decl "real" taylor_series nil) (inf_deriv_fun? const-decl "bool" taylors "analysis/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (T formal-nonempty-subtype-decl nil taylor_series nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (= const-decl "[T, T -> boolean]" equalities nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) shostak)) (GET_C_TCC1 0 (GET_C_TCC1-1 nil 3298631645 ("" (skosimp*) (("" (typepred "f!1") (("" (expand "inf_deriv_fun?") (("" (inst?) nil nil)) nil)) nil)) nil) ((inf_deriv_fun? const-decl "bool" taylors "analysis/") (T formal-nonempty-subtype-decl nil taylor_series nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil)) shostak)) (GET_C_TCC2 0 (GET_C_TCC2-1 nil 3298631645 ("" (skosimp*) (("" (rewrite "T_pred_0") nil nil)) nil) ((T_pred_0 formula-decl nil taylor_series nil)) shostak)) (GET_C_TCC3 0 (GET_C_TCC3-3 nil 3306575811 ("" (inst + "(LAMBDA (f:(inf_deriv_fun?[T]), x:T, k: nat): choose({c: between[T](0, x) | powerseries(Taylor_seq(f))(x)(k) = f(x) - Taylor_rem(k, f, 0, x, c)}))") (("1" (skosimp*) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (lemma "Taylors_inf[T]") (("1" (inst - "0" "x!1" "f!1" "k!1") (("1" (assert) (("1" (skosimp*) (("1" (inst - "c!1") (("1" (lemma "Taylor_seq_term") (("1" (inst?) (("1" (assert) (("1" (replace -2) (("1" (assert) (("1" (expand "powerseries") (("1" (expand "powerseq") (("1" (replace -1 * rl) (("1" (hide -1) (("1" (expand "series") (("1" (case-replace "(LAMBDA (k: nat): Taylor_seq(f!1)(k) * x!1 ^ k ) = (LAMBDA n: IF n = 0 THEN f!1(0) ELSE Taylor_seq(f!1)(n) * x!1 ^ n ENDIF)") (("1" (hide 2) (("1" (apply-extensionality 1 :hide? t) (("1" (lift-if) (("1" (ground) (("1" (expand "Taylor_seq") (("1" (expand "nderiv") (("1" (assert) (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "T_pred_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "T_pred_0") nil nil)) nil) ("3" (skosimp*) (("3" (typepred "f!1") (("3" (expand "inf_deriv_fun?") (("3" (inst?) nil nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (empty? const-decl "bool" sets nil) (Taylors_inf formula-decl nil taylors "analysis/") (T_pred_0 formula-decl nil taylor_series nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (series const-decl "sequence[real]" series nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (factorial_0 formula-decl nil factorial "ints/") (expt_x0 formula-decl nil exponentiation nil) (nderiv def-decl "[T -> real]" nth_derivatives "analysis/") (real_times_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (NOT const-decl "[bool -> bool]" booleans nil) (powerseq const-decl "sequence[real]" power_series nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (Taylor_seq_term formula-decl nil taylor_series nil) (member const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (nonempty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (Taylor_rem const-decl "real" taylors "analysis/") (nderiv_fun type-eq-decl nil nth_derivatives "analysis/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (derivable_n_times? def-decl "bool" nth_derivatives "analysis/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (Taylor_seq const-decl "real" taylor_series nil) (powerseries const-decl "sequence[real]" power_series nil) (sequence type-eq-decl nil sequences nil) (between type-eq-decl nil taylors "analysis/") (= const-decl "[T, T -> boolean]" equalities nil) (< const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (inf_deriv_fun? const-decl "bool" taylors "analysis/") (bool nonempty-type-eq-decl nil booleans nil) (T formal-nonempty-subtype-decl nil taylor_series nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil) (GET_C_TCC3-2 nil 3298627880 ("" (inst + "(LAMBDA (f:(inf_deriv_fun?[T]), x:T, k: nat): choose({c: between[T](0, x) | powerseries(Taylor_seq[T](f))(x)(k) = f(x) - Taylor_rem[T](k, f, 0, x, c)}))") (("1" (skosimp*) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (lemma "Taylors_inf[T]") (("1" (inst - "0" "x!1" "f!1" "k!1") (("1" (assert) (("1" (skosimp*) (("1" (inst - "c!1") (("1" (lemma "Taylor_seq_term") (("1" (inst?) (("1" (assert) (("1" (replace -2) (("1" (assert) (("1" (expand "powerseries") (("1" (expand "powerseq") (("1" (replace -1 * rl) (("1" (hide -1) (("1" (expand "series") (("1" (case-replace "(LAMBDA (k: nat): IF k = 0 THEN Taylor_seq[T](f!1)(0) ELSE Taylor_seq[T](f!1)(k) * x!1 ^ k ENDIF) = (LAMBDA n: IF n = 0 THEN f!1(0) ELSE Taylor_seq(f!1)(n) * x!1 ^ n ENDIF)") (("1" (hide 2) (("1" (apply-extensionality 1 :hide? t) (("1" (lift-if) (("1" (ground) (("1" (expand "Taylor_seq") (("1" (expand "nderiv") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "T_pred_0") nil nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "T_pred_0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "T_pred_0") nil nil)) nil) ("2" (lemma "not_one_element") (("2" (propax) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element") (("2" (skosimp*) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil) ("4" (skosimp*) (("4" (rewrite "T_pred_0") nil nil)) nil) ("5" (skosimp*) (("5" (typepred "f!1") (("5" (expand "inf_deriv_fun?") (("5" (inst?) nil nil)) nil)) nil)) nil) ("6" (lemma "not_one_element") (("6" (skosimp*) nil nil)) nil) ("7" (lemma "connected_domain") (("7" (skosimp*) nil nil)) nil)) nil) ((Taylors_inf formula-decl nil taylors "analysis/") (nderiv def-decl "[T -> real]" nth_derivatives "analysis/") (powerseq const-decl "sequence[real]" power_series nil) (Taylor_rem const-decl "real" taylors "analysis/") (nderiv_fun type-eq-decl nil nth_derivatives "analysis/") (between type-eq-decl nil taylors "analysis/") (inf_deriv_fun? const-decl "bool" taylors "analysis/")) nil) (GET_C_TCC3-1 nil 3298627046 ("" (inst + "(LAMBDA (f:(inf_deriv_fun?[T]), x:T, k: nat): choose({c: between[T](0, x) | powerseries(Taylor_seq[T](f))(x)(k) = f(x) - Taylor_rem[T](1 + k, f, 0, x, c)}))") (("1" (skosimp*) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (lemma "Taylors_inf[T]") (("1" (inst - "0" "x!1" "f!1" "k!1") (("1" (assert) (("1" (skosimp*) (("1" (inst - "c!1") (("1" (lemma "Taylor_seq_term") (("1" (inst?) (("1" (assert) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (postpone) nil nil)) nil) ("2" (postpone) nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "not_one_element") (("2" (skosimp*) nil nil)) nil) ("3" (lemma "connected_domain") (("3" (skosimp*) nil nil)) nil) ("4" (skosimp*) (("4" (rewrite "T_pred_0") nil nil)) nil) ("5" (skosimp*) (("5" (typepred "f!1") (("5" (expand "inf_deriv_fun?") (("5" (inst?) nil nil)) nil)) nil)) nil) ("6" (lemma "not_one_element") (("6" (skosimp*) nil nil)) nil) ("7" (lemma "connected_domain") (("7" (skosimp*) nil nil)) nil)) nil) nil shostak)) (is_taylor_prep_TCC1 0 (is_taylor_prep_TCC1-1 nil 3298631645 ("" (skosimp*) (("" (expand "inf_deriv_fun?") (("" (inst?) nil nil)) nil)) nil) ((inf_deriv_fun? const-decl "bool" taylors "analysis/") (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (is_taylor_prep 0 (is_taylor_prep-3 nil 3306575640 ("" (skosimp*) (("" (expand "conv_powerseries?") (("" (skosimp*) (("" (case-replace "powerseries(Taylor_seq(f!1))(x!1) = (LAMBDA n: f!1(x!1) - Taylor_rem(n, f!1, 0, x!1, GET_C(f!1,x!1,n)))") (("1" (hide -1) (("1" (inst?) (("1" (lemma "convergent_diff") (("1" (inst - "(LAMBDA n: f!1(x!1))" "(LAMBDA n: Taylor_rem(n, f!1, 0, x!1, GET_C(f!1, x!1, n)))") (("1" (assert) (("1" (expand "-") (("1" (assert) (("1" (hide 2) (("1" (lemma "convergent_const") (("1" (expand "const_fun") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "T_pred_0") nil nil) ("3" (skosimp*) (("3" (expand "inf_deriv_fun?") (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("1" (rewrite "T_pred_0") nil nil) ("2" (skosimp*) (("2" (expand "inf_deriv_fun?") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("3" (rewrite "T_pred_0") nil nil) ("4" (skosimp*) (("4" (expand "inf_deriv_fun?") (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((conv_powerseries? const-decl "bool" power_series_conv nil) (real_minus_real_is_real application-judgement "real" reals nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sequence type-eq-decl nil sequences nil) (= const-decl "[T, T -> boolean]" equalities nil) (powerseries const-decl "sequence[real]" power_series nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (T formal-nonempty-subtype-decl nil taylor_series nil) (inf_deriv_fun? const-decl "bool" taylors "analysis/") (Taylor_seq const-decl "real" taylor_series nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (derivable_n_times? def-decl "bool" nth_derivatives "analysis/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nderiv_fun type-eq-decl nil nth_derivatives "analysis/") (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (Taylor_rem const-decl "real" taylors "analysis/") (between type-eq-decl nil taylors "analysis/") (GET_C const-decl "{c: between[T](0, x) | powerseries(Taylor_seq(f))(x)(k) = f(x) - Taylor_rem(k, f, 0, x, c)}" taylor_series nil) (f!1 skolem-const-decl "[T -> real]" taylor_series nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (convergent_const formula-decl nil convergence_ops "analysis/") (T_pred_0 formula-decl nil taylor_series nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (convergent_diff formula-decl nil convergence_ops "analysis/")) nil) (is_taylor_prep-2 nil 3298631567 ("" (skosimp*) (("" (expand "conv_powerseries?") (("" (skosimp*) (("" (case-replace "powerseries(Taylor_seq[T](f!1))(x!1) = (LAMBDA n: f!1(x!1) - Taylor_rem(n, f!1, 0, x!1, GET_C(f!1,x!1,n)))") (("1" (hide -1) (("1" (inst?) (("1" (lemma "convergent_diff") (("1" (inst - "(LAMBDA n: f!1(x!1))" "(LAMBDA n: Taylor_rem(n, f!1, 0, x!1, GET_C(f!1, x!1, n)))") (("1" (assert) (("1" (expand "-") (("1" (assert) (("1" (hide 2) (("1" (lemma "convergent_const") (("1" (expand "const_fun") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "T_pred_0") nil nil) ("3" (skosimp*) (("3" (expand "inf_deriv_fun?") (("3" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (apply-extensionality 1 :hide? t) (("1" (rewrite "T_pred_0") nil nil) ("2" (skosimp*) (("2" (expand "inf_deriv_fun?") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("3" (rewrite "T_pred_0") nil nil) ("4" (skosimp*) (("4" (expand "inf_deriv_fun?") (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((convergent_diff formula-decl nil convergence_ops "analysis/") (convergent_const formula-decl nil convergence_ops "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (Taylor_rem const-decl "real" taylors "analysis/") (between type-eq-decl nil taylors "analysis/") (nderiv_fun type-eq-decl nil nth_derivatives "analysis/") (inf_deriv_fun? const-decl "bool" taylors "analysis/")) nil) (is_taylor_prep-1 nil 3298379071 ("" (skosimp*) (("" (expand "conv_powerseries?") (("" (skosimp*) (("" (lemma "convergent_diff") (("" (inst - "(LAMBDA (k: nat): f!1(x!1))" "(LAMBDA k: Taylor_rem(k+1, f!1, 0, x!1, GET_C(f!1,x!1,k)))") (("1" (expand "-") (("1" (expand "powerseries") (("1" (lemma "Taylor_seq_term") (("1" (inst?) (("1" (expand "powerseq") (("1" (inst - "x!1") (("1" (assert) (("1" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "T_pred_0") nil nil) ("3" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (is_taylor_TCC1 0 (is_taylor_TCC1-1 nil 3298374726 ("" (skosimp*) (("" (lemma "is_taylor_prep") (("" (inst?) (("" (assert) (("" (hide 2) (("" (skosimp*) (("" (inst?) (("" (expand "convergent?") (("" (inst + "0") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((is_taylor_prep formula-decl nil taylor_series nil) (convergent? const-decl "bool" convergence_sequences "analysis/") (T formal-nonempty-subtype-decl nil taylor_series nil) (T_pred const-decl "[real -> boolean]" taylor_series nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (is_taylor 0 (is_taylor-2 "sdf" 3298630239 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("1" (expand "Inf_sum") (("1" (expand "powerseries") (("1" (lemma "limit_def") (("1" (inst?) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.193 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
