(subinterval_derivnil 3545779475"" (skosimp*)"" (typepred "X!1" )"" (expand "StrictInterval?" )"" (lemma "deriv_domain_closed" )"" (inst - "lb(X!1)" "ub(X!1)" )"" (assert )"" (expand "deriv_domain?" )"" (skosimp*)"" (inst - "e!1" "x!1" )"1" (skosimp*)"1" (inst + "y!1" ) (("1" (grind) nil nil ))nil ))nil )"2" (assert )"2" (hide 2)"2" (typepred "x!1" )"2" (expand "##" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" interval nil )nil interval nil )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil deriv_domain "analysis/" )"(strict_total_order?[real])" real_props nil )"{u: nzreal | lb(X!1) <= u + x!1 AND u + x!1 <= ub(X!1)}" nil )"boolean" notequal nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil intervals_real "reals/" )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"(StrictInterval?)" subinterval_deriv nil )"bool" interval nil )nil interval_deriv nil )"Xt[X!1]" subinterval_deriv nil )"(total_order?[real])" nil )"bool" deriv_domain_def "analysis/" )"real" reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil ))nil )nil 3472488092"" (skosimp*)"" (typepred "X!1" )"" (expand "StrictlyProper?" )"" (lemma "deriv_domain_closed" )"" (inst - "lb(X!1)" "ub(X!1)" )"" (assert )"" (expand "deriv_domain?" )"" (skosimp*)"" (inst - "e!1" "x!1" )"1" (skosimp*)"1" (inst + "y!1" ) (("1" (grind) nil nil ))nil ))nil )"2" (assert )"2" (hide 2)"2" (typepred "x!1" )"2" (expand "##" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil interval nil )nil deriv_domain "analysis/" )nil intervals_real "reals/" )nil interval_deriv nil )"bool" deriv_domain_def "analysis/" ))nil 3350435325 ("" (subtype-tcc) nil nil )"bool" interval nil )nil interval nil )nil reals nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil interval_deriv nil )"bool" interval nil )"set" sets nil )"setof[real]" convergence_functions "analysis/" )"real" derivatives_def "analysis/" )"bool" convergence_functions "analysis/" )"bool" lim_of_functions "analysis/" )"bool" lim_of_functions "analysis/" )"bool" derivatives_def "analysis/" )"bool" derivatives "analysis/" )"bool" interval_deriv nil )"real" reals nil )"real" reals nil )"bool" interval nil ))nil ))nil 3472488084"" (skeep :preds? t)"" (lemma "restrict2_derivable[Xt[Y],Xt[X]]" )"1" (inst -1 "f" )"1" (expand "restrict2" )"1" (expand "Diff?" 1)"1" (assert )"1" (lemma "restrict2_deriv[Xt[Y],Xt[X]]" )"1" (decompose-equality 1)"1" (inst -1 "x!1" f)"1" (expand "restrict2" )"1" (expand "D" )"1" (replaces -1 :dir rl) nil nil )) nil ))nil )"2" (expand "Diff?" ) (("2" (propax) nil nil ))nil ))nil )"2" (expand "Diff?" ) (("2" (propax) nil nil )) nil )"3" (hide-all-but (-5 1)) (("3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "Diff?" -4) (("2" (propax) nil nil )) nil ))nil )"2" (skeep)"2" (inst 1 "x" )"2" (typepred "x" )"2" (hide-all-but (-1 -4 1)) (("2" (grind) nil nil ))nil ))nil ))nil ))nil )"3" (hide -4 2)"3" (expand "not_one_element?" )"3" (skeep)"3" (case "x=lb(X)" )"1" (inst 1 "ub(X)" )"1" (grind) nil nil ) ("2" (grind) nil nil )) nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil )"4" (hide -4 2)"4" (expand "not_one_element?" )"4" (skeep)"4" (case "x=lb(Y)" )"1" (inst 1 "ub(Y)" )"1" (grind) nil nil ) ("2" (grind) nil nil )) nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil )"5" (hide -4 2) (("5" (rewrite "deriv_domain_Xt" ) nil nil ))nil )"6" (hide -4 2) (("6" (rewrite "deriv_domain_Xt" ) nil nil ))nil ))nil ))nil )nil interval_deriv 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 )nil restrict2_deriv "analysis/" )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )"[T, T -> boolean]" equalities nil )"[T1 -> real]" restrict2_deriv "analysis/" )"(StrictInterval?)" subinterval_deriv nil )"[Xt -> real]" interval_deriv nil )"(total_order?[real])" nil )"bool" interval nil )NOT const-decl "[bool -> bool]" booleans nil )nil restrict2_deriv "analysis/" )"bool" interval_deriv nil )nil derivatives "analysis/" )"(StrictInterval?)" subinterval_deriv nil )"bool" derivatives "analysis/" )"[Xt[X] -> real]" subinterval_deriv nil )"Xt[Y]" subinterval_deriv nil )"boolean" notequal nil )"(strict_total_order?[real])" real_props nil )nil subinterval_deriv nil ))nil )nil 3350435426"" (skeep :preds? t)"" (lemma "restrict2_derivable[Xt[Y],Xt[X]]" )"1" (inst -1 "f" )"1" (expand "restrict2" )"1" (expand "Diff?" 1)"1" (assert )"1" (lemma "restrict2_deriv[Xt[Y],Xt[X]]" )"1" (decompose-equality 1)"1" (inst -1 "x!1" f)"1" (expand "restrict2" )"1" (expand "D" )"1" (replaces -1 :dir rl) nil nil )) nil ))nil )"2" (expand "Diff?" ) (("2" (propax) nil nil ))nil ))nil )"2" (expand "Diff?" ) (("2" (propax) nil nil )) nil )"3" (hide-all-but (-5 1)) (("3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "Diff?" -4) (("2" (propax) nil nil )) nil ))nil )"2" (skeep)"2" (inst 1 "x" )"2" (typepred "x" )"2" (hide-all-but (-1 -4 1)) (("2" (grind) nil nil ))nil ))nil ))nil ))nil )"3" (hide -4 2)"3" (skeep)"3" (case "x=lb(X)" )"1" (inst 1 "ub(X)" )"1" (grind) nil nil ) ("2" (grind) nil nil )) nil )"2" (grind) nil nil ))nil ))nil ))nil )"4" (hide -4 2)"4" (skeep)"4" (case "x=lb(Y)" )"1" (inst 1 "ub(Y)" )"1" (grind) nil nil ) ("2" (grind) nil nil )) nil )"2" (grind) nil nil ))nil ))nil ))nil )"5" (hide -4 2) (("5" (rewrite "deriv_domain_XtY" ) nil nil ))nil )"6" (hide -4 2) (("6" (rewrite "deriv_domain_XtY" ) nil nil ))nil ))nil ))nil )"bool" derivatives "analysis/" )nil derivatives "analysis/" )"bool" interval_deriv nil )nil restrict2_deriv "analysis/" )"bool" interval nil )"[Xt -> real]" interval_deriv nil )"[T1 -> real]" restrict2_deriv "analysis/" )"bool" deriv_domain_def "analysis/" )nil restrict2_deriv "analysis/" )nil interval nil )nil interval_deriv nil ))nil 3350435325 ("" (subtype-tcc) 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 )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil interval nil )"bool" interval nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )nil interval_deriv nil )"bool" interval nil )"bool" interval nil ))nil ))nil 3350512779"" (induct "n" )"1" (skeep)"1" (expand "Diffn?" )"1" (expand "Dn" ) (("1" (propax) nil nil )) nil )) nil ))nil )"2" (skeep)"2" (skeep)"2" (expand "Diffn?" 1)"2" (expand "Dn" 1)"2" (expand "Diffn?" -3)"2" (flatten)"2" (inst -1 "X" "Y" "D(f)" )"2" (assert )"2" (flatten)"2" (lemma "subinterval_deriv" )"2" (inst -1 "X" "Y" "f" )"2" (assert )"2" (flatten) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide 2)"3" (skeep) (("3" (hide -1 -3) (("3" (grind) nil nil )) nil ))nil ))nil )"4" (hide 2)"4" (skeep)"4" (match "Diffn?" step (hide $1n)) (("4" (grind) nil nil ))nil ))nil ))nil ))nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"[Xt -> real]" interval_deriv nil )"bool" interval_deriv nil )nil subinterval_deriv nil )nil naturalnumbers nil )"[Xt -> real]" interval_deriv nil )"[T, T -> boolean]" equalities nil )nil defined_types 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_deriv nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" interval nil )"bool" interval_deriv nil ))quality 100%
¤ Dauer der Verarbeitung: 0.5 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
