|
(continuity_of_max_min
(IMP_continuity_ms_def_TCC1 0
(IMP_continuity_ms_def_TCC1-1 nil 3462092975
("" (lemma "fullset_metric_space") (("" (propax) nil nil)) nil)
((fullset_metric_space formula-decl nil continuity_of_max_min nil))
nil))
(IMP_continuity_ms_def_TCC2 0
(IMP_continuity_ms_def_TCC2-1 nil 3462092975
("" (lemma "real_metric_space")
(("" (inst - "fullset[real]") nil nil)) 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)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
(real_metric_space formula-decl nil real_metric_space nil))
nil))
(max_min_fun_convert 0
(max_min_fun_convert-1 nil 3462093337
("" (skosimp*)
(("" (expand "max_fun")
(("" (expand "min_fun")
(("" (expand "min")
(("" (expand "max")
(("" (prop)
(("1" (apply-extensionality)
(("1" (expand "-")
(("1" (lift-if) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (apply-extensionality)
(("2" (expand "-")
(("2" (lift-if) (("2" (assert) nil nil)) nil)) nil))
nil)
("3" (apply-extensionality)
(("3" (expand "-")
(("3" (lift-if) (("3" (assert) nil nil)) nil)) nil))
nil)
("4" (apply-extensionality)
(("4" (expand "-")
(("4" (lift-if) (("4" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((max_fun const-decl "real" continuity_of_max_min nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(< const-decl "bool" reals nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(> const-decl "bool" reals 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)
(T formal-nonempty-type-decl nil continuity_of_max_min nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(min_fun const-decl "real" continuity_of_max_min nil))
shostak))
(max_fun_continuous 0
(max_fun_continuous-1 nil 3462093051
("" (skosimp*)
(("" (expand "continuous?")
(("" (skosimp*)
(("" (inst - "x!1")
(("" (inst - "x!1")
(("" (expand "continuous_at?")
(("" (skosimp*)
(("" (inst - "epsilon!1/10")
(("" (inst - "epsilon!1/10")
(("" (skosimp*)
(("" (inst + "min(delta!1/10,delta!2/10)")
(("" (skosimp*)
(("" (expand "member")
(("" (inst - "y!1")
((""
(inst - "y!1")
((""
(expand "ball")
((""
(expand "real_dist")
((""
(expand "max_fun")
((""
(expand "max")
(("" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous? const-decl "bool" continuity_ms_def nil)
(T formal-nonempty-type-decl nil continuity_of_max_min nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(continuous_at? const-decl "bool" continuity_ms_def nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types 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)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(ball const-decl "set[T]" metric_spaces nil)
(max_fun const-decl "real" continuity_of_max_min nil)
(minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" 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)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(real_dist const-decl "nnreal" real_metric_space nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(member const-decl "bool" sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil))
shostak))
(min_fun_continuous 0
(min_fun_continuous-1 nil 3462093821
("" (expand "continuous?")
(("" (skosimp*)
(("" (inst - "x!1")
(("" (inst - "x!1")
(("" (expand "continuous_at?")
(("" (skosimp*)
(("" (inst - "epsilon!1/10")
(("" (inst - "epsilon!1/10")
(("" (skosimp*)
(("" (inst + "min(delta!1/10,delta!2/10)")
(("" (skosimp*)
(("" (inst - "y!1")
(("" (inst - "y!1")
(("" (expand "member")
((""
(expand "ball")
((""
(expand "real_dist")
((""
(expand "min_fun")
((""
(expand "min")
(("" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs 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)
(member const-decl "bool" sets nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_dist const-decl "nnreal" real_metric_space nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_lt_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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(min_fun const-decl "real" continuity_of_max_min nil)
(ball const-decl "set[T]" metric_spaces nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(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)
(number nonempty-type-decl nil numbers nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(continuous_at? const-decl "bool" continuity_ms_def nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil continuity_of_max_min nil)
(continuous? const-decl "bool" continuity_ms_def nil))
shostak)))
¤ Dauer der Verarbeitung: 0.18 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.
|
