(interval_chainnil 3304701211"" (lemma "deriv_domain_Xt[X]" ) (("" (propax) nil nil )) nil )nil interval_deriv nil )nil reals nil )nil interval nil )nil booleans nil )nil booleans nil )"bool" interval nil )"(StrictInterval?)" interval_chain nil ))nil 3304701423"" (expand "not_one_element?" )"" (skeep)"" (typepred "x" )"" (typepred "X" )"" (expand "StrictlyProper?" )"" (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 ))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 )"[T, T -> boolean]" equalities nil )"XT" interval_chain 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 )"bool" interval nil )"(StrictInterval?)" interval_chain nil )nil interval_chain nil )"bool" deriv_domain_def "analysis/" ))nil ))nil 3304701483"" (lemma "deriv_domain_Xt[Y]" ) (("" (propax) nil nil )) nil )nil interval_deriv nil )nil reals nil )nil interval nil )nil booleans nil )nil booleans nil )"bool" interval nil )"(StrictInterval?)" interval_chain nil ))nil 3304701436"" (expand "not_one_element?" )"" (skeep)"" (typepred "x" )"" (typepred "Y" )"" (expand "StrictlyProper?" )"" (inst 1 "if x=lb(Y) then ub(Y) else lb(Y) endif" )"1" (grind) nil nil ) ("2" (grind) nil nil )"3" (grind) nil 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 )"[T, T -> boolean]" equalities nil )"YT" interval_chain 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 )"bool" interval nil )"(StrictInterval?)" interval_chain nil )nil interval_chain nil )"bool" deriv_domain_def "analysis/" ))nil ))nil 3319158888"" (skosimp :preds? t) (("" (inst -2 "t!1" ) nil 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 )"bool" interval nil )"(StrictInterval?)" interval_chain nil )nil interval_deriv nil )"bool" interval_deriv nil )nil interval_chain nil )"(StrictInterval?)" interval_chain nil ))nil ))nil 3319159473"" (skosimp :preds? t)"" (expand "Diff?" )"" (lemma "composition_derivable_fun" )"" (inst -1 "f!1" "g!1" )"" (assert ) (("" (expand "o" ) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"(LAMBDA (f: (Diff?[X])): FORALL (t: XT): f(t) ## Y)" nil )"T3" function_props nil )nil interval_chain nil )nil chain_rule "analysis/" )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 )"bool" interval nil )"(StrictInterval?)" interval_chain nil )nil interval_deriv nil )"bool" interval_deriv nil )nil interval_chain nil )"(StrictInterval?)" interval_chain nil ))nil ))nil 3319158888"" (skosimp :preds? t) (("" (rewrite "Diff_comp" ) nil nil )) nil )nil interval_chain 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 )"bool" interval nil )"(StrictInterval?)" interval_chain nil )nil interval_deriv nil )"bool" interval_deriv nil )nil interval_chain nil )"(StrictInterval?)" interval_chain nil ))nil ))nil 3319159512"" (skosimp :preds? t)"" (expand * "Diff?" "D" )"" (lemma "deriv_comp_fun" )"" (inst -1 "f!1" "g!1" )"1" (expand "o" )"1" (assert )"1" (expand "*" ) (("1" (propax) nil nil )) nil )) nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"[Xt -> real]" interval_deriv nil )"bool" derivatives "analysis/" )"(Diff?[Y])" interval_chain nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(LAMBDA (f: (Diff?[X])): FORALL (t: XT): f(t) ## Y)" nil )"real" reals nil )"[T -> real]" real_fun_ops "reals/" )"T3" function_props nil )nil interval_chain nil )nil chain_rule "analysis/" )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 )"bool" interval nil )"(StrictInterval?)" interval_chain nil )nil interval_deriv nil )"bool" interval_deriv nil )nil interval_chain nil )"(StrictInterval?)" interval_chain nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.11 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
