|
(continuity_ms
(IMP_continuity_ms_def_TCC1 0
(IMP_continuity_ms_def_TCC1-1 nil 3459678538
("" (rewrite "fullset_metric_space1") nil nil)
((fullset_metric_space1 formula-decl nil continuity_ms nil)) nil))
(IMP_continuity_ms_def_TCC2 0
(IMP_continuity_ms_def_TCC2-1 nil 3459678538
("" (rewrite "fullset_metric_space2") nil nil)
((fullset_metric_space2 formula-decl nil continuity_ms nil)) nil))
(image_inverse_image 0
(image_inverse_image-1 nil 3293835710
("" (skosimp*)
(("" (expand "restrict")
(("" (expand "subset?")
(("" (expand "image")
(("" (expand "inverse_image")
(("" (expand "extend")
(("" (expand "member")
(("" (skosimp*)
(("" (typepred "x!2")
(("" (replace -5 -2)
(("" (simplify -2) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((restrict const-decl "R" restrict nil)
(image const-decl "set[R]" function_image nil)
(extend const-decl "R" extend nil) (set type-eq-decl nil sets nil)
(T1 formal-nonempty-type-decl nil continuity_ms nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(inverse_image const-decl "set[D]" function_image nil)
(subset? const-decl "bool" sets nil))
shostak))
(inverse_image_image 0
(inverse_image_image-1 nil 3293835874
("" (expand "subset?")
(("" (expand "extend")
(("" (expand "inverse_image")
(("" (expand "member")
(("" (expand "image")
(("" (skosimp*)
(("" (inst -1 "x!1")
(("" (assert)
(("" (inst - "f!1(x!1)")
(("" (case-replace "T!1(f!1(x!1))")
(("1" (replace -3)
(("1" (assert)
(("1" (inst + "x!1")
(("1" (expand "restrict")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((extend const-decl "R" extend nil)
(member const-decl "bool" sets nil)
(x!1 skolem-const-decl "T1" continuity_ms nil)
(X!1 skolem-const-decl "set[T1]" continuity_ms nil)
(S!1 skolem-const-decl "set[T1]" continuity_ms nil)
(restrict const-decl "R" restrict nil)
(T2 formal-nonempty-type-decl nil continuity_ms nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(T1 formal-nonempty-type-decl nil continuity_ms nil)
(image const-decl "set[R]" function_image nil)
(inverse_image const-decl "set[D]" function_image nil)
(subset? const-decl "bool" sets nil))
shostak))
(continuous_open_sets 0
(continuous_open_sets-3 nil 3459689578
("" (skosimp*)
(("" (prop)
(("1" (expand "continuous?")
(("1" (expand "continuous_at?")
(("1" (skeep)
(("1" (expand "open_in?")
(("1" (prop)
(("1" (skosimp*)
(("1" (case "inverse_image(f!1,Y)(s!1)")
(("1" (expand "subset?")
(("1" (expand "member")
(("1" (expand "intersection")
(("1" (expand "member")
(("1" (expand "ball")
(("1"
(expand "inverse_image")
(("1"
(expand "member")
(("1"
(inst - "s!1")
(("1"
(expand "open?")
(("1"
(expand "interior")
(("1"
(expand "interior_point?")
(("1"
(expand "subset?")
(("1"
(expand "ball")
(("1"
(decompose-equality)
(("1"
(expand "member")
(("1"
(inst - "f!1(s!1)")
(("1"
(iff)
(("1"
(prop)
(("1"
(skosimp*)
(("1"
(copy -5)
(("1"
(inst
-
"r!1")
(("1"
(skosimp*)
(("1"
(inst
+
"delta!1")
(("1"
(skosimp*)
(("1"
(prop)
(("1"
(inst
-
"x!1")
(("1"
(prop)
(("1"
(inst
-
"f!1(x!1)")
(("1"
(prop)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "s!1")
(("2"
(expand "inverse_image")
(("2"
(expand "intersection")
(("2"
(expand "member")
(("2" (prop) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "s!1")
(("2" (expand "intersection")
(("2" (expand "member") (("2" (prop) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "subset?")
(("2" (expand "member")
(("2" (expand "intersection")
(("2" (expand "member")
(("2" (skosimp*) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "continuous?")
(("2" (skosimp*)
(("2" (typepred "x!1")
(("2" (expand "continuous_at?")
(("2" (expand "member")
(("2" (expand "ball")
(("2" (expand "open_in?")
(("2" (expand "subset?")
(("2" (expand "intersection")
(("2" (expand "inverse_image")
(("2" (expand "member")
(("2" (expand "ball")
(("2"
(skosimp*)
(("2"
(case
"open?[T2,d2](ball[T2,d2](f!1(x!1),epsilon!1))")
(("1"
(inst
-
"ball[T2,d2](f!1(x!1),epsilon!1)")
(("1"
(prop)
(("1"
(inst - "x!1")
(("1"
(skosimp*)
(("1"
(inst + "r!1")
(("1"
(skosimp*)
(("1"
(inst - "y!1")
(("1"
(prop)
(("1"
(expand "ball")
(("1"
(propax)
nil
nil))
nil)
("2"
(typepred "y!1")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "inverse_image")
(("2"
(expand "intersection")
(("2"
(expand "member")
(("2"
(expand "ball")
(("2"
(lemma
"fullset_metric_space2")
(("2"
(expand
"metric_space?")
(("2"
(expand
"space_zero?")
(("2"
(prop)
(("2"
(inst
-
"f!1(x!1)"
"f!1(x!1)")
(("1"
(prop)
(("1"
(assert)
nil
nil))
nil)
("2"
(expand
"fullset")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "ball_open[T2,d2]")
(("2"
(inst - "epsilon!1" "f!1(x!1)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous_at? const-decl "bool" continuity_ms_def nil)
(open_in? const-decl "bool" metric_spaces nil)
(subset? const-decl "bool" sets nil)
(ball const-decl "set[T]" metric_spaces nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(open? const-decl "bool" metric_spaces nil)
(interior_point? const-decl "bool" metric_spaces nil)
(x!1 skolem-const-decl "T1" continuity_ms nil)
(d2 formal-const-decl "[T2, T2 -> nnreal]" continuity_ms nil)
(nnreal type-eq-decl nil real_types nil)
(< const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(interior const-decl "set[T]" metric_spaces nil)
(s!1 skolem-const-decl "(intersection(inverse_image(f!1, Y), S!1))"
continuity_ms nil)
(Y skolem-const-decl "set[T2]" continuity_ms nil)
(f!1 skolem-const-decl "[T1 -> T2]" continuity_ms nil)
(S!1 skolem-const-decl "set[T1]" continuity_ms nil)
(member const-decl "bool" sets nil)
(T1 formal-nonempty-type-decl nil continuity_ms nil)
(T2 formal-nonempty-type-decl nil continuity_ms nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(inverse_image const-decl "set[D]" function_image nil)
(intersection const-decl "set" sets nil)
(continuous? const-decl "bool" continuity_ms_def nil)
(fullset_metric_space2 formula-decl nil continuity_ms nil)
(space_zero? const-decl "bool" metric_spaces_def nil)
(fullset const-decl "set" sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(metric_space? const-decl "bool" metric_spaces_def nil)
(epsilon!1 skolem-const-decl "posreal" continuity_ms nil)
(x!1 skolem-const-decl "(S!1)" continuity_ms nil)
(ball_open formula-decl nil metric_spaces nil))
nil)
(continuous_open_sets-2 nil 3459689494
("" (skosimp*)
(("" (prop)
(("1" (expand "continuous?")
(("1" (expand "continuous_at?")
(("1" (skeep)
(("1" (expand "open?" +)
(("1" (expand "interior")
(("1" (apply-extensionality)
(("1" (hide 2)
(("1" (case "inverse_image(f!1,Y)(x!1)")
(("1" (assert)
(("1" (expand "interior_point?")
(("1" (expand "subset?")
(("1" (expand "member")
(("1"
(inst - "x!1")
(("1"
(expand "inverse_image")
(("1"
(expand "member")
(("1"
(expand "open?")
(("1"
(expand "interior")
(("1"
(decompose-equality)
(("1"
(inst - "f!1(x!1)")
(("1"
(assert)
(("1"
(expand
"interior_point?")
(("1"
(skosimp*)
(("1"
(inst - "r!1")
(("1"
(skosimp*)
(("1"
(inst
+
"delta!1")
(("1"
(skosimp*)
(("1"
(expand
"ball")
(("1"
(inst
-
"x!2")
(("1"
(assert)
(("1"
(expand
"subset?")
(("1"
(expand
"member")
(("1"
(inst
-
"f!1(x!2)")
(("1"
(assert)
nil)))))))))
("2"
(expand
"fullset[T1]")
(("2"
(propax)
nil)))))))))))))))))))))))))))))))))
("2"
(expand "fullset[T1]")
(("2" (propax) nil)))))))))))))
("2" (assert) nil)))))
("2" (lemma fullset_metric_space1)
(("2" (propax) nil)))))))))))))))
("2" (expand "continuous?")
(("2" (expand "continuous_at?")
(("2" (expand "member")
(("2" (expand "ball")
(("2" (skosimp*)
(("2" (lemma "ball_open[T2,d2]")
(("2" (inst - "epsilon!1" "f!1(x!1)")
(("2"
("" (skosimp*) (prop)
(("1" (expand "continuous?")
(expand "continuous_at?") (skeep)
(expand "open_in?") (prop)
(("1" (skosimp*)
(case "inverse_image(f!1,Y)(s!1)")
(("1" (expand "subset?") (expand "member")
(expand "intersection") (expand "member")
(expand "ball") (expand "inverse_image")
(expand "member") (inst - "s!1")
(("1" (expand "open?") (expand "interior")
(expand "interior_point?")
(expand "subset?") (expand "ball")
(decompose-equality) (expand "member")
(inst - "f!1(s!1)") (iff) (prop)
(skosimp*) (copy -5) (inst - "r!1")
(skosimp*) (inst + "delta!1") (skosimp*)
(prop) (inst - "x!1") (prop)
(inst - "f!1(x!1)") (prop))
("2" (typepred "s!1")
(expand "inverse_image")
(expand "intersection")
(expand "member") (prop))))
("2" (typepred "s!1")
(expand "intersection") (expand "member")
(prop))))
("2" (expand "subset?") (expand "member")
(expand "intersection") (expand "member")
(skosimp*))))
("2" (expand "continuous?") (skosimp*)
(typepred "x!1") (expand "continuous_at?")
(expand "member") (expand "ball")
(expand "open_in?") (expand "subset?")
(expand "intersection")
(expand "inverse_image") (expand "member")
(expand "ball") (skosimp*)
(case "open?[T2,d2](ball[T2,d2](f!1(x!1),epsilon!1))")
(("1"
(inst - "ball[T2,d2](f!1(x!1),epsilon!1)")
(prop) (inst - "x!1")
(("1" (skosimp*) (inst + "r!1") (skosimp*)
(inst - "y!1") (prop)
(("1" (expand "ball") (propax))
("2" (typepred "y!1") (propax))))
("2" (expand "inverse_image")
(expand "intersection") (expand "member")
(expand "ball")
(lemma "fullset_metric_space2")
(expand "metric_space?")
(expand "space_zero?") (prop)
(inst - "f!1(x!1)" "f!1(x!1)")
(("1" (prop) (assert))
("2" (expand "fullset") (propax))))))
("2" (lemma "ball_open[T2,d2]")
(inst - "epsilon!1" "f!1(x!1)"))))))
nil))))))))))))))))))
nil)
nil nil)
(continuous_open_sets-1 nil 3459597870
("" (skosimp*)
(("" (prop)
(("1" (expand "continuous?")
(("1" (expand "continuous_at?")
(("1" (skeep)
(("1" (expand "open?" +)
(("1" (expand "interior")
(("1" (apply-extensionality)
(("1" (hide 2)
(("1" (case "inverse_image(f!1,Y)(x!1)")
(("1" (assert)
(("1" (expand "interior_point?")
(("1" (expand "subset?")
(("1" (expand "member")
(("1"
(inst - "x!1")
(("1"
(expand "inverse_image")
(("1"
(expand "member")
(("1"
(expand "open?")
(("1"
(expand "interior")
(("1"
(decompose-equality)
(("1"
(inst - "f!1(x!1)")
(("1"
(assert)
(("1"
(expand
"interior_point?")
(("1"
(skosimp*)
(("1"
(inst - "r!1")
(("1"
(skosimp*)
(("1"
(inst
+
"delta!1")
(("1"
(skosimp*)
(("1"
(expand
"ball")
(("1"
(inst
-
"x!2")
(("1"
(assert)
(("1"
(expand
"subset?")
(("1"
(expand
"member")
(("1"
(inst
-
"f!1(x!2)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"fullset[T1]")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "fullset[T1]")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (lemma fullset_metric_space1)
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "continuous?")
(("2" (expand "continuous_at?")
(("2" (expand "member")
(("2" (expand "ball")
(("2" (skosimp*)
(("2" (lemma "ball_open[T2,d2]")
(("2" (inst - "epsilon!1" "f!1(x!1)")
(("2" (inst - "ball[T2,d2](f!1(x!1),epsilon!1)")
(("2" (assert)
(("2" (hide -1)
(("2" (expand "open?")
(("2" (expand "interior")
(("2"
(expand "interior_point?")
(("2"
(expand "subset?")
(("2"
(expand "ball")
(("2"
(expand "member")
(("2"
(decompose-equality)
(("2"
(inst - "x!1")
(("2"
(expand "inverse_image")
(("2"
(expand "member")
(("2"
(lemma
"fullset_metric_space2")
(("2"
(expand
"metric_space?")
(("2"
(prop)
(("2"
(expand
"space_zero?")
(("2"
(inst
-
"f!1(x!1)"
"f!1(x!1)")
(("1"
(prop)
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(inst
+
"r!1")
(("1"
(skosimp*)
(("1"
(inst
-
"y!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"fullset")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((space_zero? const-decl "bool" metric_spaces_def nil)
(ball_open formula-decl nil metric_spaces nil)
(interior const-decl "set[T]" metric_spaces nil)
(ball const-decl "set[T]" metric_spaces nil)
(metric_space? const-decl "bool" metric_spaces_def nil)
(interior_point? const-decl "bool" metric_spaces nil)
(open? const-decl "bool" metric_spaces nil))
shostak))
(continuous_closed_sets 0
(continuous_closed_sets-1 nil 3293836724
("" (skosimp*)
(("" (lemma "continuous_open_sets")
(("" (inst - "S!1" "f!1")
(("" (replace -1)
(("" (hide -1)
(("" (prop)
(("1" (skosimp*)
(("1" (expand "closed?")
(("1" (expand "closed_in?")
(("1" (inst - "complement(Y!1)")
(("1" (prop)
(("1"
(case "inverse_image(f!1, complement(Y!1)) = complement(intersection
(inverse_image(f!1, Y!1), S!1))")
(("1" (replace -1) (("1" (propax) nil nil))
nil)
("2" (lemma "demorgan2[T1]")
(("2"
(inst - "inverse_image(f!1,Y!1)" "S!1")
(("2"
(replace -1)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil)
("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "closed?")
(("2" (expand "closed_in?")
(("2" (inst - "complement(Y!1)")
(("2" (lemma "complement_complement[T2]")
(("2" (inst - "Y!1")
(("2" (replace -1)
(("2" (prop)
(("2"
(hide -2 -3 -4 -5 -6 -7 -8 -9)
(("2"
(case
"intersection(complement(intersection
(inverse_image
(f!1, complement(Y!1)),
S!1)),
S!1) = intersection(inverse_image(f!1, Y!1), S!1)")
(("1"
(replace -1)
(("1" (propax) nil nil))
nil)
("2"
(hide-all-but 1)
(("2"
(apply-extensionality)
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((continuous_open_sets formula-decl nil continuity_ms nil)
(closed? const-decl "bool" metric_spaces nil)
(complement const-decl "set" sets nil)
(intersection const-decl "set" sets nil)
(inverse_image const-decl "set[D]" function_image nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(ball const-decl "set[T]" metric_spaces nil)
(union const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(open_in? const-decl "bool" metric_spaces nil)
(open? const-decl "bool" metric_spaces nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(s!1 skolem-const-decl
"(intersection(union(complement(inverse_image(f!1, Y!1)), complement(S!1)),
S!1))" continuity_ms nil)
(S!1 skolem-const-decl "set[T1]" continuity_ms nil)
(f!1 skolem-const-decl "[T1 -> T2]" continuity_ms nil)
(Y!1 skolem-const-decl "set[T2]" continuity_ms nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(demorgan2 formula-decl nil sets_lemmas nil)
(closed_in? const-decl "bool" metric_spaces nil)
(complement_complement formula-decl nil sets_lemmas nil)
(T2 formal-nonempty-type-decl nil continuity_ms nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-nonempty-type-decl nil continuity_ms nil))
shostak)))
¤ Dauer der Verarbeitung: 0.32 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.
|
