|
(deriv_domain_def
(connected_deriv_domain 0
(connected_deriv_domain-1 nil 3472397987
("" (flatten)
(("" (expand "connected?")
(("" (expand "not_one_element?")
(("" (expand "deriv_domain?")
(("" (skolem!)
(("" (inst -2 "x!1")
(("" (skosimp*)
(("" (case "abs(y!1 - x!1) < e!1")
(("1" (inst? 2) (("1" (assert) nil nil)) nil)
("2"
(inst 3
"if x!1 < y!1 then e!1/2 else -e!1/2 endif")
(("1" (grind) nil nil)
("2" (flatten)
(("2" (inst - "y!1" "x!1" "_")
(("2" (grind) nil nil)) nil))
nil)
("3" (inst - "x!1" "y!1" "_")
(("3" (inst?)
(("3" (flatten) (("3" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((connected? const-decl "bool" deriv_domain_def nil)
(deriv_domain? const-decl "bool" deriv_domain_def 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]" deriv_domain_def nil)
(T formal-subtype-decl nil deriv_domain_def nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(x!1 skolem-const-decl "T" deriv_domain_def nil)
(y!1 skolem-const-decl "T" deriv_domain_def nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_real_is_real application-judgement "real" reals nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(e!1 skolem-const-decl "posreal" deriv_domain_def nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(not_one_element? const-decl "bool" deriv_domain_def nil))
nil))
(del_neigh_all_lem 0
(del_neigh_all_lem-1 nil 3474887925
("" (flatten)
(("" (expand "deriv_domain?")
(("" (skosimp*)
(("" (expand "del_neigh_all?")
(("" (inst - "x!1")
(("" (skosimp*)
(("" (inst - "x!1 + min(del!1,e!1)/2")
(("" (split -1)
(("1" (inst + "min(del!1, e!1) / 2")
(("1" (grind) nil nil) ("2" (grind) nil nil)) nil)
("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((deriv_domain? const-decl "bool" deriv_domain_def nil)
(del_neigh_all? const-decl "bool" deriv_domain_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(x!1 skolem-const-decl "T" deriv_domain_def nil)
(e!1 skolem-const-decl "posreal" deriv_domain_def nil)
(del!1 skolem-const-decl "posreal" deriv_domain_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(T formal-subtype-decl nil deriv_domain_def nil)
(T_pred const-decl "[real -> boolean]" deriv_domain_def 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)
(real_plus_real_is_real application-judgement "real" reals nil))
nil)))
[ zur Elbe Produktseite wechseln0.15Quellennavigators
Analyse erneut starten
]
|
