|
(real_intervals_aux
(bounded_open_interval_def 0
(bounded_open_interval_def-1 nil 3471584778
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (expand "bounded_open_interval?")
(("1" (expand "bounded_interval?")
(("1" (expand "bounded?")
(("1" (flatten)
(("1" (split -2)
(("1" (propax) nil nil)
("2" (flatten)
(("2" (expand "empty?")
(("2" (skosimp)
(("2" (expand "member")
(("2" (name "LO" "inf(A!1)")
(("1" (name "HI" "sup(A!1)")
(("1"
(typepred "sup(A!1)")
(("1"
(typepred "inf(A!1)")
(("1"
(replace -3)
(("1"
(replace -4)
(("1"
(expand "least_upper_bound")
(("1"
(expand
"greatest_lower_bound")
(("1"
(flatten)
(("1"
(expand "lower_bound")
(("1"
(expand "upper_bound")
(("1"
(hide -5 -6 -7 -8 -9)
(("1"
(case "LO)
(("1"
(inst
+
"(HI+LO)/2"
"(HI-LO)/2")
(("1"
(apply-extensionality
:hide?
t)
(("1"
(case-replace
"A!1(x!2)")
(("1"
(hide -9)
(("1"
(expand
"metric_open?")
(("1"
(inst
-8
"x!2")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(expand
"subset?")
(("1"
(inst-cp
-8
"x!2-r!1/2")
(("1"
(inst
-8
"x!2+r!1/2")
(("1"
(assert)
(("1"
(split
-8)
(("1"
(split
-9)
(("1"
(inst
-5
"x!2 - r!1 / 2")
(("1"
(inst
-7
"r!1 / 2 + x!2")
(("1"
(hide
-6
-8
-9)
(("1"
(grind)
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand
"ball")
(("2"
(case
"LO)
(("1"
(flatten)
(("1"
(hide
-3)
(("1"
(inst
-5
"x!2")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(typepred
"z!1")
(("1"
(case
"z!1)
(("1"
(hide
2)
(("1"
(inst
-8
"x!2")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(case
"x!2)
(("1"
(hide
2)
(("1"
(typepred
"z!2")
(("1"
(expand
"interval?")
(("1"
(inst
-10
"z!1"
"z!2"
"x!2")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-1
-2
1))
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(hide 2)
(("2"
(expand
"metric_open?")
(("2"
(inst
-6
"x!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(expand
"subset?")
(("2"
(inst
-6
"x!1+r!1/2")
(("2"
(assert)
(("2"
(split
-6)
(("1"
(inst
-2
"x!1")
(("1"
(inst
-4
"x!1+r!1/2")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "bounded_open_interval?")
(("2" (expand "bounded_interval?")
(("2" (expand "bounded?")
(("2" (split -1)
(("1" (assert)
(("1" (rewrite "emptyset_is_empty?")
(("1" (replace -1)
(("1" (hide -1)
(("1" (split)
(("1" (grind) nil nil)
("2" (expand "metric_open?")
(("2" (expand "emptyset")
(("2"
(expand "subset?")
(("2"
(expand "member")
(("2"
(skosimp)
(("2"
(skosimp)
(("2"
(inst - "x!1")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (split)
(("1" (replace -1)
(("1" (hide -1) (("1" (grind) nil nil)) nil))
nil)
("2" (replace -1)
(("2" (hide -1)
(("2" (flatten)
(("2" (expand "nonempty?")
(("2" (assert)
(("2"
(split)
(("1"
(expand "above_bounded")
(("1"
(inst + "x!1+r!1")
(("1" (grind) nil nil))
nil))
nil)
("2"
(expand "below_bounded")
(("2"
(inst + "x!1-r!1")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (replace -1)
(("3" (hide -1)
(("3"
(lemma "metric_open_ball"
("x" "x!1" "r" "r!1"))
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bounded_open_interval? const-decl "bool" real_topology
"metric_space/")
(bounded? const-decl "bool" real_topology "metric_space/")
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(above_bounded const-decl "bool" bounded_reals "reals/")
(sup_set type-eq-decl nil bounded_reals "reals/")
(least_upper_bound const-decl "bool" bound_defs "reals/")
(sup const-decl "{x | least_upper_bound(<=)(x, Su)}" bounded_reals
"reals/")
(lower_bound const-decl "bool" bound_defs "reals/")
(r!1 skolem-const-decl "posreal" real_intervals_aux nil)
(x!1 skolem-const-decl "real" real_intervals_aux nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(>= const-decl "bool" reals 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(A!1 skolem-const-decl "set[real]" real_intervals_aux nil)
(HI skolem-const-decl
"{x | least_upper_bound[real, real](<=)(x, A!1)}"
real_intervals_aux nil)
(LO skolem-const-decl
"{x | greatest_lower_bound[real, real](<=)(x, A!1)}"
real_intervals_aux nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_open? const-decl "bool" metric_space_def "metric_space/")
(subset? const-decl "bool" sets nil)
(x!2 skolem-const-decl "real" real_intervals_aux nil)
(r!1 skolem-const-decl "posreal" real_intervals_aux nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(interval? const-decl "bool" real_topology "metric_space/")
(real_plus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(ball const-decl "set[T]" metric_space_def "metric_space/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil)
(upper_bound const-decl "bool" bound_defs "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(nonempty? const-decl "bool" sets nil)
(setof type-eq-decl nil defined_types nil)
(below_bounded const-decl "bool" bounded_reals "reals/")
(inf_set type-eq-decl nil bounded_reals "reals/")
(pred type-eq-decl nil defined_types nil)
(greatest_lower_bound const-decl "bool" bound_defs "reals/")
(<= const-decl "bool" reals nil)
(inf const-decl "{x | greatest_lower_bound(<=)(x, Sl)}"
bounded_reals "reals/")
(bounded_interval? const-decl "bool" real_topology "metric_space/")
(metric_open_ball formula-decl nil metric_space "metric_space/")
(emptyset const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(emptyset_is_clopen name-judgement
"clopen[real, (metric_induced_topology)]" real_topology
"metric_space/")
(emptyset_is_compact name-judgement
"compact[real, (metric_induced_topology)]" real_topology
"metric_space/")
(emptyset_is_empty? formula-decl nil sets_lemmas nil))
shostak))
(unbounded_open_interval_def 0
(unbounded_open_interval_def-1 nil 3471587044
("" (skosimp)
(("" (expand "unbounded?")
(("" (split)
(("1" (flatten)
(("1" (expand "bounded?")
(("1" (flatten)
(("1" (expand "nonempty?")
(("1" (assert)
(("1" (case-replace "above_bounded[real](A!1)")
(("1" (hide 4 3)
(("1" (typepred "sup(A!1)")
(("1" (name-replace "HI" "sup(A!1)")
(("1" (expand "least_upper_bound")
(("1" (flatten)
(("1"
(expand "upper_bound")
(("1"
(inst + "HI")
(("1"
(apply-extensionality 3 :hide? t)
(("1"
(expand "inf_open")
(("1"
(case-replace "A!1(x!1)")
(("1"
(expand "open_interval?")
(("1"
(flatten)
(("1"
(expand "metric_open?")
(("1"
(inst -6 "x!1")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(expand
"subset?")
(("1"
(inst
-6
"x!1+r!1/2")
(("1"
(split -6)
(("1"
(assert)
(("1"
(inst
-3
"r!1 / 2 + x!1")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(inst -3 "x!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(case "x!1)
(("1"
(typepred "z!1")
(("1"
(hide 2)
(("1"
(expand
"below_bounded")
(("1"
(inst
+
"x!1")
(("1"
(expand
"lower_bound")
(("1"
(skosimp)
(("1"
(case
"z!2)
(("1"
(hide
3)
(("1"
(expand
"open_interval?")
(("1"
(flatten)
(("1"
(expand
"interval?")
(("1"
(inst
-7
"z!2"
"z!1"
"x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "nonempty?")
(("2" (propax) nil nil)) nil))
nil))
nil)
("2" (case-replace "below_bounded[real](A!1)")
(("1" (hide 3 6 4)
(("1" (typepred "inf(A!1)")
(("1" (name-replace "LO" "inf(A!1)")
(("1" (inst + "LO")
(("1"
(expand "open_inf")
(("1"
(expand "greatest_lower_bound")
(("1"
(expand "lower_bound")
(("1"
(apply-extensionality 3 :hide? t)
(("1"
(case-replace "A!1(x!1)")
(("1"
(flatten)
(("1"
(expand "open_interval?")
(("1"
(flatten)
(("1"
(expand "metric_open?")
(("1"
(inst -6 "x!1")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(expand
"subset?")
(("1"
(inst
-6
"x!1-r!1/2")
(("1"
(split -6)
(("1"
(expand
"member")
(("1"
(inst
-3
"x!1 - r!1 / 2")
(("1"
(assert)
(("1"
(hide-all-but
(-3
1))
(("1"
(typepred
"r!1")
(("1"
(expand
"<="
-3)
(("1"
(split)
(("1"
(assert)
(("1"
(typepred
"reals.<")
(("1"
(expand
"strict_total_order?")
(("1"
(expand
"strict_order?")
(("1"
(flatten)
(("1"
(expand
"transitive?")
(("1"
(inst
-
"LO"
"x!1 - r!1 / 2"
"x!1")
(("1"
(split
-2)
(("1"
(propax)
nil
nil)
("2"
(propax)
nil
nil)
("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
1)
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(flatten)
(("2"
(inst -3 "x!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "z!1")
(("2"
(case "z!1)
(("1"
(hide 2)
(("1"
(expand
"above_bounded")
(("1"
(inst
+
"x!1")
(("1"
(expand
"upper_bound")
(("1"
(skosimp)
(("1"
(case
"x!1)
(("1"
(typepred
"z!2")
(("1"
(expand
"open_interval?")
(("1"
(flatten)
(("1"
(expand
"interval?")
(("1"
(inst
-8
"z!1"
"z!2"
"x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "nonempty?")
(("2" (propax) nil nil)) nil))
nil))
nil)
("2" (hide 4 6 7)
(("2" (apply-extensionality 4 :hide? t)
(("2" (expand "fullset")
(("2" (expand "open_interval?")
(("2"
(flatten)
(("2"
(expand "below_bounded")
(("2"
(inst + "x!1")
(("2"
(expand "above_bounded")
(("2"
(inst + "x!1")
(("2"
(expand "upper_bound")
(("2"
(expand "lower_bound")
(("2"
(skosimp*)
(("2"
(case "z!1)
(("1"
(case "x!1)
(("1"
(expand
"interval?")
(("1"
(inst
-
"z!1"
"z!2"
"x!1")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (split)
(("1" (replace -1)
(("1" (hide -1)
(("1" (split)
(("1" (expand "bounded?")
(("1" (split)
(("1" (grind) nil nil)
("2" (flatten)
(("2" (expand "above_bounded")
(("2" (skosimp)
(("2" (expand "upper_bound")
(("2"
(inst - "n!1+1")
(("1" (assert) nil nil)
("2"
(expand "fullset")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "open_interval?")
(("2" (split)
(("1" (grind) nil nil)
("2" (expand "metric_open?")
(("2" (expand "fullset")
(("2" (expand "subset?")
(("2" (expand "member")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (replace -1)
(("2" (hide -1)
(("2" (split)
(("1" (expand "bounded?")
(("1" (split)
(("1" (expand "open_inf")
(("1" (expand "empty?")
(("1" (expand "member")
(("1"
(inst - "a!1+1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "open_inf")
(("2" (expand "above_bounded")
(("2"
(skosimp)
(("2"
(expand "upper_bound")
(("2"
(inst - "max(a!1+1,n!1+1)")
(("1" (grind) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "open_inf")
(("2" (expand "open_interval?")
(("2" (split)
(("1" (grind) nil nil)
("2" (expand "metric_open?")
(("2" (skosimp)
(("2"
(expand "subset?")
(("2"
(expand "member")
(("2"
(case-replace "a!1)
(("1"
(assert)
(("1"
(inst + "x!1-a!1")
(("1"
(skosimp)
(("1" (grind) nil nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(skosimp)
(("2"
(inst - "x!1")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp)
(("3" (replace -1)
(("3" (hide -1)
(("3" (assert)
(("3" (split)
(("1" (expand "inf_open")
(("1" (expand "bounded?")
(("1" (split)
(("1" (expand "empty?")
(("1"
(expand "member")
(("1"
(inst - "a!1-1")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.207 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.
|
