Quelle interval_taylor.prf
Sprache: Lisp
(interval_taylornil 3304443847 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil interval nil )"bool" interval nil )nil interval nil )"StrictInterval" interval_taylor nil )nil interval_deriv nil )"(total_order?[real])" nil )"bool" interval nil )"bool" deriv_domain_def "analysis/" ))nil ))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 )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"[bool, bool -> bool]" booleans nil )nil numbers nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"bool" interval nil )nil interval_deriv nil )"Xt[X]" interval_taylor nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil reals nil )nil interval nil )"bool" interval nil )nil interval nil )"StrictInterval" interval_taylor nil )"bool" deriv_domain_def "analysis/" ))nil ))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 )nil interval_deriv nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"bool" interval nil )nil interval_deriv nil )"bool" interval_deriv nil )nil reals nil )nil interval nil )nil booleans nil )nil booleans nil )"bool" interval nil )nil interval nil )"StrictInterval" interval_taylor nil )nil nth_derivatives"analysis/" )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil naturalnumbers nil )"bool" reals nil ))nil ))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" "1" "1" "1" "1" "1" "0" )"1" expand "Dn" -7)"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "Div_inclusion" )"1" rewrite "Mult_inclusion" )"1" rewrite "Dn_nderiv" "1" "k_1" )nil nil )"2" rewrite "Diffn_derivn" )"2" rewrite "Diffn_derivn" )"2" "derivable_n_times_lem[Xt]" )"2" "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" "2" rewrite "Diffn_derivn" )"2" "derivable_n_times_lem[Xt]" )"2" "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" "derivable_n_times_lem[Xt]" )"3" "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 )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"Interval" interval nil )"(Pos?)" interval nil )"(NonNeg?)" interval nil )"ProperInterval" interval nil )"ProperInterval" interval nil )"ProperInterval" interval nil )"(total_order?[real])" nil )nil interval nil )nil interval nil )nil factorial "ints/" )nil interval nil )nil interval nil )"[Xt -> real]" interval_deriv nil )nil interval nil )"bool" interval nil )"bool" interval nil )nil interval nil )"StrictInterval" interval_taylor nil )nil interval_deriv nil )"int" integers nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nat" interval_taylor nil )"bool" interval_deriv nil )"real" reals nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"bool" interval nil )nil interval nil )nil interval nil )nil nth_derivatives"analysis/" )nil interval_deriv nil )nil interval nil )nil interval nil )nil interval nil )"(Precondition?)" intervalnil )nil interval nil )nil integers nil )nil naturalnumbers nil )nil interval nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"real" reals nil )nil taylors "analysis/" )"bool" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"[T -> real]" nth_derivatives "analysis/" )nil nth_derivatives "analysis/" )"bool" nth_derivatives "analysis/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" sigma "reals/" )nil sigma "reals/" )nil sigma "reals/" )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil interval nil )"real" reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil interval nil )"Interval" interval nil )"Interval" interval nil )"Interval" interval nil )"Interval" interval nil )"Interval" interval nil )nil integers nil )"bool" reals nil )nil integers nil )"posnat" factorial "ints/" )"int" integers nil )nil interval_deriv nil )"[numfield, numfield -> numfield]" number_fields nil )nil taylors "analysis/" ))nil ))nil 3321284024"" (skeep)"" (lemma "Taylor" )"" "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 )nil interval_taylor nil )"Interval" interval nil )"Interval" interval_taylor nil )"bool" reals nil )nil naturalnumbers nil )"[Xt -> real]" interval_deriv nil )nil interval nil )nil factorial "ints/" )nil interval nil )nil interval nil )nil interval nil )nil factorial "ints/" )nil interval nil )"ProperInterval" interval nil )"Interval" interval nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"real" interval nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil naturalnumbers nil )nil interval nil )"bool" interval nil )"bool" interval nil )nil interval nil )"StrictInterval" interval_taylor nil )nil interval_deriv nil )"bool" interval_deriv nil )"bool" interval_deriv nil )"(Diff?)" interval_taylor nil )"IntervalType(X)" intervalnil ))nil ))nil 3321310677"" (skeep :preds? t)"" (expand "Diffn?" ) (("" (assert ) nil nil )) nil )) nil )"bool" interval_deriv nil )"IntervalType(X)" intervalnil )"ProperInterval" interval nil ))nil ))nil 3321310936"" (skeep :preds? t)"" (skeep)"" (expand "Diffn?" )"" (expand "Diffn?" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"IntervalType(X)" intervalnil )"ProperInterval" interval nil )"bool" interval_deriv nil ))nil ))nil 3321317545"" (skeep)"" (lemma "Taylor" )"" "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 )nil interval_taylor nil )"Interval" interval nil )"ProperInterval" interval nil )nil interval nil )nil factorial "ints/" )nil interval nil )nil interval nil )nil interval nil )nil factorial "ints/" )nil interval nil )"[Xt -> real]" interval_deriv nil )nil naturalnumbers nil )"bool" reals nil )"Interval" interval nil )nil interval nil )"ProperInterval" interval nil )"StrictInterval" interval nil )"ProperInterval" interval nil )"Interval" interval_taylor nil )"Interval" interval_taylor nil )"posnat" factorial "ints/" )"Interval" interval nil )"[T, T -> boolean]" equalities nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"bool" interval_deriv nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" interval nil )nil interval_deriv nil )"StrictInterval" interval_taylor nil )nil interval nil )"bool" interval nil )"bool" interval nil )nil booleans nil )nil interval nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"IntervalType(X)" intervalnil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
