|
(interval_taylor
(IMP_taylors_TCC1 0
(IMP_taylors_TCC1-2 nil 3304443847 ("" (grind) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers 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)
(Interval type-eq-decl nil interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_taylor nil)
(Xt type-eq-decl nil interval_deriv nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(|##| const-decl "bool" interval nil)
(connected? const-decl "bool" deriv_domain_def "analysis/"))
nil))
(IMP_taylors_TCC2 0
(IMP_taylors_TCC2-2 nil 3304443869
("" (expand "not_one_element?")
(("" (skeep :preds? t)
(("" (typepred "X")
(("" (expand "StrictInterval?")
(("" (inst 1 "if x=lb(X) then ub(X) else lb(X) endif")
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (grind) nil nil))
nil))
nil))
nil))
nil))
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)
(/= const-decl "boolean" notequal nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers 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)
(|##| const-decl "bool" interval nil)
(Xt type-eq-decl nil interval_deriv nil)
(x skolem-const-decl "Xt[X]" interval_taylor nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_taylor nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
nil))
(Taylor_TCC1 0
(Taylor_TCC1-2 nil 3320590025
("" (skeep :preds? t)
(("" (rewrite "Diffn_derivn")
(("" (rewrite "Diffn_derivn")
(("" (lemma "derivable_n_times_lem[Xt]")
(("" (inst -1 "f" "k" "n") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((Diffn_derivn formula-decl nil interval_deriv nil)
(number nonempty-type-decl nil numbers 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)
(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)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(|##| const-decl "bool" interval nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diffn? def-decl "bool" interval_deriv nil)
(real nonempty-type-from-decl nil reals nil)
(Interval type-eq-decl nil interval nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_taylor nil)
(derivable_n_times_lem formula-decl nil nth_derivatives
"analysis/")
(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_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil))
nil))
(Taylor 0
(Taylor-1 nil 3320589950
("" (skeep :preds? t)
(("" (case "n=0")
(("1" (replaces -1)
(("1" (expand "Sigma")
(("1" (expand "Sigma")
(("1" (assert)
(("1" (inst -6 "x")
(("1" (expand "Dn" -6) (("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "Taylors[Xt]")
(("2" (inst -1 "a" "x" "f" "n-1")
(("1" (rewrite "Diffn_derivn" :dir rl)
(("1" (assert)
(("1" (skeep -1)
(("1" (expand "Sigma" 2)
(("1" (rewrite "Add_comm")
(("1" (replaces -1)
(("1" (rewrite "Add_inclusion")
(("1" (hide 3)
(("1" (rewrite "Sigma_inclusion")
(("1" (hide 2)
(("1"
(skeep :preds? t)
(("1"
(lift-if)
(("1"
(split 1)
(("1"
(flatten)
(("1"
(replaces -1)
(("1"
(inst -7 "0")
(("1"
(expand "Dn" -7)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(rewrite "Div_inclusion")
(("1"
(rewrite "Mult_inclusion")
(("1"
(rewrite
"Dn_nderiv"
:dir
rl)
(("1"
(inst -7 "k_1")
nil
nil)
("2"
(rewrite "Diffn_derivn")
(("2"
(rewrite
"Diffn_derivn")
(("2"
(lemma
"derivable_n_times_lem[Xt]")
(("2"
(inst
-1
"f"
"k_1"
"n")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "Pow_inclusion")
(("2"
(rewrite "Sub_inclusion")
(("2"
(rewrite
"r2i_inclusion")
nil
nil))
nil))
nil))
nil)
("2"
(rewrite "r2i_inclusion")
nil
nil)
("3"
(rewrite "Pos_Zeroless")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(skeep)
(("2"
(rewrite "Diffn_derivn")
(("2"
(lemma "derivable_n_times_lem[Xt]")
(("2"
(inst -1 "f" "nn" "n")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (rewrite "Div_inclusion")
(("1" (hide 2)
(("1"
(rewrite "Mult_inclusion")
(("1"
(rewrite "Dn_nderiv" :dir rl)
(("1" (inst -6 "c") nil nil))
nil)
("2"
(rewrite "Pow_inclusion")
(("2"
(rewrite "Sub_inclusion")
(("2"
(rewrite "r2i_inclusion")
nil
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "r2i_inclusion") nil nil)
("3" (rewrite "Pos_Zeroless") nil nil))
nil))
nil)
("3" (hide 3)
(("3" (skeep)
(("3" (rewrite "Diffn_derivn")
(("3"
(lemma "derivable_n_times_lem[Xt]")
(("3"
(inst -1 "f" "nn" "n")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3) (("2" (assert) 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)
(Sigma def-decl "Interval" interval nil)
(r2i_Pos application-judgement "(Pos?)" interval nil)
(r2i_Nneg application-judgement "(NonNeg?)" interval nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(Proper_Sub application-judgement "ProperInterval" interval nil)
(Proper_Pow application-judgement "ProperInterval" interval nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Pow_0 formula-decl nil interval nil)
(Mult_1_r formula-decl nil interval nil)
(factorial_0 formula-decl nil factorial "ints/")
(Div_1 formula-decl nil interval nil)
(Add_0_r formula-decl nil interval nil)
(Dn def-decl "[Xt -> real]" interval_deriv nil)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_taylor nil)
(Xt type-eq-decl nil interval_deriv nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(n skolem-const-decl "nat" interval_taylor nil)
(Diffn? def-decl "bool" interval_deriv nil)
(real_div_nzreal_is_real application-judgement "real" reals 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)
(Pos? const-decl "bool" interval nil)
(Pos_Zeroless judgement-tcc nil interval nil)
(Mult_inclusion formula-decl nil interval nil)
(derivable_n_times_lem formula-decl nil nth_derivatives
"analysis/")
(Dn_nderiv formula-decl nil interval_deriv nil)
(Sub_inclusion formula-decl nil interval nil)
(r2i_inclusion formula-decl nil interval nil)
(Pow_inclusion formula-decl nil interval nil)
(Zeroless_Precondition name-judgement "(Precondition?)" interval
nil)
(Div_inclusion formula-decl nil interval nil)
(subrange type-eq-decl nil integers nil)
(below type-eq-decl nil naturalnumbers nil)
(Sigma_inclusion formula-decl nil interval 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)
(real_plus_real_is_real application-judgement "real" reals nil)
(between type-eq-decl nil taylors "analysis/")
(< const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(^ const-decl "real" exponentiation nil)
(nderiv def-decl "[T -> real]" nth_derivatives "analysis/")
(nderiv_fun type-eq-decl nil nth_derivatives "analysis/")
(derivable_n_times? def-decl "bool" nth_derivatives "analysis/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(IF const-decl "[boolean, T, T -> T]" if_def 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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(Add_inclusion formula-decl nil interval nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(Add_comm formula-decl nil interval nil)
(Div const-decl "Interval" interval nil)
(Mult const-decl "Interval" interval nil)
(Pow const-decl "Interval" interval nil)
(Sub const-decl "Interval" interval nil)
([\|\|] const-decl "Interval" interval 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/")
(int_plus_int_is_int application-judgement "int" integers nil)
(Diffn_derivn formula-decl nil interval_deriv nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(Taylors formula-decl nil taylors "analysis/"))
nil))
(Taylor1_Midpoint 0
(Taylor1_Midpoint-1 nil 3321284024
("" (skeep)
(("" (lemma "Taylor")
((""
(inst -1 "midpoint(X)" "1" "x" "f"
"LAMBDA(n:nat):IF n=0 THEN F(Midpoint) ELSE DF(X) ENDIF")
(("1" (expand "Sigma")
(("1" (expand "Sigma")
(("1" (expand "Sigma")
(("1" (assert)
(("1" (split -1)
(("1" (expand "Taylor1") (("1" (propax) nil nil))
nil)
("2" (skeep :preds? t)
(("2" (case "k=0")
(("1" (replaces -1)
(("1" (expand "Dn") (("1" (propax) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("3" (hide 2)
(("3" (expand "Dn")
(("3" (expand "Dn") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "Diffn?")
(("2" (expand "Diffn?") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((Taylor formula-decl nil interval_taylor nil)
(Sigma def-decl "Interval" interval nil)
(Taylor1 const-decl "Interval" interval_taylor nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(Dn def-decl "[Xt -> real]" interval_deriv nil)
(Add_0_r formula-decl nil interval nil)
(factorial_0 formula-decl nil factorial "ints/")
(Mult_1_r formula-decl nil interval nil)
(Pow_0 formula-decl nil interval nil)
(Div_1 formula-decl nil interval nil)
(factorial_1 formula-decl nil factorial "ints/")
(Pow_1 formula-decl nil interval nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
([\|\|] const-decl "Interval" interval nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(midpoint const-decl "real" interval 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)
(Interval type-eq-decl nil interval nil)
(|##| const-decl "bool" interval nil)
(StrictInterval? const-decl "bool" interval nil)
(StrictInterval type-eq-decl nil interval nil)
(X formal-const-decl "StrictInterval" interval_taylor nil)
(Xt type-eq-decl nil interval_deriv nil)
(Diffn? def-decl "bool" interval_deriv nil)
(Diff? const-decl "bool" interval_deriv nil)
(f skolem-const-decl "(Diff?)" interval_taylor nil)
(Proper_midpoint application-judgement "IntervalType(X)" interval
nil))
nil))
(Taylor2_Midpoint_TCC1 0
(Taylor2_Midpoint_TCC1-1 nil 3321310677
("" (skeep :preds? t)
(("" (expand "Diffn?") (("" (assert) nil nil)) nil)) nil)
((Diffn? def-decl "bool" interval_deriv nil)
(Proper_midpoint application-judgement "IntervalType(X)" interval
nil)
(r2i_Proper application-judgement "ProperInterval" interval nil))
nil))
(Taylor2_Midpoint_TCC2 0
(Taylor2_Midpoint_TCC2-1 nil 3321310936
("" (skeep :preds? t)
(("" (skeep)
(("" (expand "Diffn?")
(("" (expand "Diffn?") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((Proper_midpoint application-judgement "IntervalType(X)" interval
nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(Diffn? def-decl "bool" interval_deriv nil))
nil))
(Taylor2_Midpoint 0
(Taylor2_Midpoint-2 nil 3321317545
("" (skeep)
(("" (lemma "Taylor")
((""
(inst -1 "midpoint(X)" "2" "x" "f2"
"LAMBDA(n:nat):IF n=0 THEN F(Midpoint) ELSIF n=1 THEN DF(Midpoint) ELSE D2F(X) ENDIF")
(("" (expand "Sigma")
(("" (expand "Sigma")
(("" (expand "Sigma")
(("" (expand "Sigma")
(("" (assert)
(("" (split -1)
(("1" (rewrite "Pow2_Sq")
(("1" (expand "factorial")
(("1" (expand "factorial")
(("1" (expand "factorial")
(("1" (expand "Taylor2")
(("1"
(expand "Taylor1")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skeep :preds? t)
(("2" (case "k=0")
(("1" (replaces -1)
(("1" (expand "Dn") (("1" (propax) nil nil))
nil))
nil)
("2" (case "k=1")
(("1" (replaces -1)
(("1" (expand "Dn")
(("1"
(expand "Dn")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (expand "Dn")
(("3" (expand "Dn")
(("3" (expand "Dn") (("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Taylor formula-decl nil interval_taylor nil)
(Sigma def-decl "Interval" interval nil)
(r2i_Proper application-judgement "ProperInterval" interval nil)
(Pow_1 formula-decl nil interval nil)
(factorial_1 formula-decl nil factorial "ints/")
(Div_1 formula-decl nil interval nil)
(Pow_0 formula-decl nil interval nil)
(Mult_1_r formula-decl nil interval nil)
(factorial_0 formula-decl nil factorial "ints/")
(Add_0_r formula-decl nil interval nil)
(Dn def-decl "[Xt -> real]" interval_deriv nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(Sub const-decl "Interval" interval nil)
(Pow2_Sq formula-decl nil interval nil)
(Proper_Sub application-judgement "ProperInterval" interval nil)
(Strict_Sq application-judgement "StrictInterval" interval nil)
(Proper_Sq application-judgement "ProperInterval" interval nil)
(Taylor2 const-decl "Interval" interval_taylor nil)
(Taylor1 const-decl "Interval" interval_taylor nil)
(factorial def-decl "posnat" factorial "ints/")
([\|\|] const-decl "Interval" interval nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(Diffn? def-decl "bool" interval_deriv 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)
(midpoint const-decl "real" interval nil)
(Xt type-eq-decl nil interval_deriv nil)
(X formal-const-decl "StrictInterval" interval_taylor nil)
(StrictInterval type-eq-decl nil interval nil)
(StrictInterval? const-decl "bool" interval nil)
(|##| const-decl "bool" interval nil)
(bool nonempty-type-eq-decl nil booleans nil)
(Interval type-eq-decl nil interval 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)
(Proper_midpoint application-judgement "IntervalType(X)" interval
nil))
nil)))
¤ Dauer der Verarbeitung: 0.13 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.
|
