|
(hausdorff_convergence
(unique_limit 0
(unique_limit-1 nil 3358828139
("" (skosimp)
(("" (typepred "S")
(("" (expand "hausdorff_space?")
(("" (flatten)
(("" (expand "hausdorff?")
(("" (expand "is_T2?")
(("" (inst - "l1!1" "l2!1")
(("" (assert)
(("" (skosimp)
(("" (expand "convergence?")
(("" (inst - "U!1")
(("1" (inst - "V!1")
(("1" (assert)
(("1" (skosimp*)
(("1"
(inst - "max(n!1,n!2)")
(("1"
(inst - "max(n!1,n!2)")
(("1"
(expand "disjoint?")
(("1"
(expand "empty?")
(("1"
(inst - "u!1(max(n!1, n!2))")
(("1"
(expand "intersection")
(("1"
(expand "member")
(("1"
(name-replace
"DRL1"
"u!1(max(n!1, n!2))")
(("1"
(hide-all-but
(-4 -5 1))
(("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "V!1")
(("2" (expand "open?")
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "open?")
(("2" (typepred "U!1")
(("2" (expand "member")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((S formal-const-decl "hausdorff" hausdorff_convergence nil)
(hausdorff nonempty-type-eq-decl nil topology_prelim nil)
(hausdorff_space? const-decl "bool" topology_prelim nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil hausdorff_convergence nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(is_T2? const-decl "bool" topology_prelim nil)
(member const-decl "bool" sets nil)
(convergence? const-decl "bool" topological_convergence nil)
(V!1 skolem-const-decl "(S)" hausdorff_convergence nil)
(empty? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(sequence type-eq-decl nil sequences nil)
(disjoint? const-decl "bool" sets 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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(max const-decl "{p: real | p >= m AND p >= n}" real_defs nil)
(nat_max application-judgement "{k: nat | i <= k AND j <= k}"
real_defs nil)
(nonneg_rat_max application-judgement
"{s: nonneg_rat | s >= q AND s >= r}" real_defs nil)
(open nonempty-type-eq-decl nil topology nil)
(U!1 skolem-const-decl "(S)" hausdorff_convergence nil)
(open? const-decl "bool" topology nil)
(set type-eq-decl nil sets nil)
(hausdorff? const-decl "bool" topology_prelim nil))
shostak))
(limit_def 0
(limit_def-1 nil 3358828249
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (replace -1 1 rl) (("1" (rewrite "limit_lemma") nil nil))
nil))
nil)
("2" (flatten)
(("2" (lemma "limit_lemma" ("v" "v!1"))
(("2"
(lemma "unique_limit"
("u" "v!1" "l1" "limit(v!1)" "l2" "l!1"))
(("1" (assert) nil nil)
("2" (typepred "S")
(("2" (expand "hausdorff_space?")
(("2" (flatten) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((S formal-const-decl "hausdorff" hausdorff_convergence nil)
(hausdorff nonempty-type-eq-decl nil topology_prelim nil)
(hausdorff_space? const-decl "bool" topology_prelim nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil hausdorff_convergence nil)
(convergent type-eq-decl nil topological_convergence nil)
(convergent? const-decl "bool" topological_convergence nil)
(sequence type-eq-decl nil sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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)
(limit_lemma formula-decl nil topological_convergence nil)
(unique_limit formula-decl nil hausdorff_convergence nil)
(limit const-decl "T" topological_convergence nil))
shostak))
(singleton_is_closed 0
(singleton_is_closed-1 nil 3364193951
("" (skosimp)
(("" (typepred "S")
(("" (expand "hausdorff_space?")
(("" (flatten)
(("" (expand "hausdorff?")
(("" (expand "is_T2?")
(("" (name "A" "{(U:(S)) | NOT U(x!1)}")
(("" (case "forall (x:T): Union(A)(x) IFF x /= x!1")
(("1" (lemma "open_Union" ("Y" "A"))
(("1" (split -1)
(("1"
(case-replace
"Union(extend[setof[T], (S), bool, FALSE](A)) = complement(singleton(x!1))")
(("1" (expand "closed?")
(("1" (expand "open?")
(("1" (propax) nil nil)) nil))
nil)
("2" (hide-all-but (-2 1))
(("2" (apply-extensionality 1 :hide? t)
(("2" (expand "singleton")
(("2"
(expand "complement")
(("2"
(expand "member")
(("2"
(inst - "x!2")
(("2"
(replace -1)
(("2"
(hide -1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "A")
(("2" (expand "extend")
(("2" (expand "open?")
(("2" (expand "every")
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (case-replace "x!2=x!1")
(("1" (assert)
(("1" (expand "extend")
(("1" (expand "A")
(("1"
(expand "Union")
(("1"
(skosimp)
(("1"
(typepred "a!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (expand "extend")
(("2" (expand "A")
(("2"
(expand "Union")
(("2"
(inst - "x!2" "x!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(inst + "U!1")
(("2"
(expand "disjoint?")
(("2"
(expand "intersection")
(("2"
(expand "empty?")
(("2"
(inst - "x!1")
(("2"
(assert)
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)
((S formal-const-decl "hausdorff" hausdorff_convergence nil)
(hausdorff nonempty-type-eq-decl nil topology_prelim nil)
(hausdorff_space? const-decl "bool" topology_prelim nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil hausdorff_convergence nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(is_T2? const-decl "bool" topology_prelim nil)
(/= const-decl "boolean" notequal nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(Union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(closed? const-decl "bool" topology nil)
(open? const-decl "bool" topology nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(singleton_is_compact application-judgement "compact"
hausdorff_convergence nil)
(complement const-decl "set" sets nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(every const-decl "bool" sets nil)
(A skolem-const-decl "[(S) -> bool]" hausdorff_convergence nil)
(open_Union formula-decl nil topology nil)
(disjoint? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(x!1 skolem-const-decl "T" hausdorff_convergence nil)
(U!1 skolem-const-decl "(S)" hausdorff_convergence nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(hausdorff? const-decl "bool" topology_prelim nil))
nil))
(compact_is_closed 0
(compact_is_closed-1 nil 3397556799
("" (skolem + ("X"))
(("" (typepred "X")
(("" (name "B" "difference(fullset[T],X)")
(("" (case "nonempty?(B)")
(("1"
(case "forall x: B(x) => EXISTS (U:open): U(x) & subset?(U,B)")
(("1"
(name "BB" "Union({U:set[T] | open?(U) & subset?(U,B)})")
(("1" (case-replace "BB=B")
(("1"
(lemma "open_Union"
("Y" "{U: set[T] | open?(U) & subset?(U, B)}"))
(("1" (replace -3)
(("1" (split -1)
(("1"
(lemma "difference_intersection"
("a" "fullset[T]" "b" "X"))
(("1" (replace -7)
(("1" (lemma "closed_complement" ("A" "B"))
(("1" (assert)
(("1"
(replace -2 -1)
(("1"
(rewrite "demorgan2")
(("1"
(rewrite "complement_complement")
(("1"
(rewrite "complement_fullset[T]")
(("1"
(rewrite "union_commutative")
(("1"
(rewrite "union_empty")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "every") (("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (apply-extensionality :hide? t)
(("2" (replace -1 1 rl)
(("2" (expand "Union")
(("2" (case-replace "B(x!1)")
(("1" (inst - "x!1")
(("1" (assert)
(("1"
(skosimp)
(("1" (inst + "U!1") nil nil))
nil))
nil))
nil)
("2" (replace 1 2)
(("2" (assert)
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2"
(expand "subset?")
(("2"
(inst - "x!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "S")
(("2" (expand "hausdorff_space?")
(("2" (flatten) nil nil)) nil))
nil))
nil)
("2" (case-replace "X=emptyset[T]")
(("1" (rewrite "emptyset_is_closed") nil nil)
("2" (case "nonempty?(X)")
(("1" (hide 1 3)
(("1" (skosimp)
(("1" (expand "compact?")
(("1" (expand "compact_subset?")
(("1"
(name "UV"
"lambda (y:(X)): choose({uv:[set[T],set[T]]| open?(uv`1) & open?(uv`2) & uv`1(x!1) & uv`2(y) & disjoint?(uv`1,uv`2)})")
(("1"
(inst -6
"{a:set[T] | exists (y:(X)): UV(y)`2 = a}")
(("1" (split -6)
(("1"
(skosimp)
(("1"
(case
"forall (v:(V!1)): exists (u: open): disjoint?(v,u) & u(x!1)")
(("1"
(expand "finite_cover?")
(("1"
(flatten)
(("1"
(case
"forall (v:(V!1)): nonempty?[open]({u: open | disjoint?(v, u) & u(x!1)})")
(("1"
(lemma
"finite_image[(V!1),open]"
("f"
"lambda (v: (V!1)): choose[open]({u:open | disjoint?(v, u) & u(x!1)})"
"S"
"V!1"))
(("1"
(lemma
"open_Intersection"
("Y"
"(image[(V!1), open]
(LAMBDA (v: (V!1)):
choose[open]({u: open | disjoint?(v, u) & u(x!1)}),
restrict[setof[T], ((V!1)), boolean](V!1)))"))
(("1"
(expand "restrict")
(("1"
(expand "image")
(("1"
(expand "extend")
(("1"
(split -1)
(("1"
(hide -2 -6 -8)
(("1"
(inst
+
"(Intersection(LAMBDA (t: setof[T]):
IF open?[T, S](t)
THEN EXISTS (x:
(LAMBDA (s: (((V!1)))): TRUE)):
t
=
choose[open]
({u_1: open
|
disjoint?(x, u_1) & u_1(x!1)})
ELSE FALSE
ENDIF))")
(("1"
(hide -1)
(("1"
(split)
(("1"
(expand
"Intersection")
(("1"
(skosimp)
(("1"
(typepred
"a!1")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(typepred
"x!2")
(("1"
(inst
-4
"x!2")
(("1"
(lemma
"choose_member[open]"
("a"
"{u_1: open | disjoint?(x!2, u_1) & u_1(x!1)}"))
(("1"
(expand
"nonempty?")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"Intersection")
(("2"
(expand
"subset?")
(("2"
(expand
"member")
(("2"
(skosimp*)
(("2"
(case
"X(x!2)")
(("1"
(expand
"cover?")
(("1"
(expand
"subset?")
(("1"
(inst
-6
"x!2")
(("1"
(assert)
(("1"
(expand
"Union"
-6)
(("1"
(skosimp)
(("1"
(typepred
"a!1")
(("1"
(inst
-
"choose[open]
({u_1: open |
disjoint?(a!1, u_1) & u_1(x!1)})")
(("1"
(lemma
"choose_member[open]"
("a"
"{u_1: open | disjoint?(a!1, u_1) & u_1(x!1)}"))
(("1"
(split
-1)
(("1"
(expand
"member")
(("1"
(flatten)
(("1"
(name-replace
"AA"
"choose({u_1: open | disjoint?(a!1, u_1) & u_1(x!1)})")
(("1"
(expand
"disjoint?")
(("1"
(expand
"empty?")
(("1"
(inst
-
"x!2")
(("1"
(expand
"intersection")
(("1"
(expand
"member")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst
-
"a!1")
nil
nil))
nil))
nil))
nil)
("2"
(inst
-
"a!1")
(("2"
(expand
"nonempty?")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(inst
+
"a!1")
nil
nil)
("3"
(inst
-
"a!1")
nil
nil)
("4"
(typepred
"S")
(("4"
(expand
"hausdorff_space?")
(("4"
(flatten)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"B"
2)
(("2"
(expand
"fullset")
(("2"
(expand
"difference")
(("2"
(expand
"member")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp)
nil
nil)
("3"
(skosimp)
(("3"
(skosimp)
(("3"
(typepred
"S")
(("3"
(expand
"hausdorff_space?")
(("3"
(flatten)
nil
nil))
nil))
nil))
nil))
nil)
("4"
(typepred
"S")
(("4"
(expand
"hausdorff_space?")
(("4"
(flatten)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-1 1))
(("2"
(expand
"is_finite")
(("2"
(skosimp)
(("2"
(inst
+
"N!1"
"f!1")
(("1"
(expand
"injective?")
(("1"
(skosimp)
(("1"
(inst
-
"x1!1"
"x2!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(skosimp)
(("2"
(case-replace
"open?[T, S](x2!1)")
(("1"
(split)
(("1"
(flatten)
nil
nil)
("2"
(flatten)
nil
nil))
nil)
("2"
(replace
1)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide -1 -5 -7 2)
(("3"
(expand
"every")
(("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "S")
(("2"
(expand
"hausdorff_space?")
(("2"
(flatten)
nil
nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3"
(hide-all-but (-4 1))
(("3"
(expand "restrict")
(("3"
(expand "is_finite")
(("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-1 1))
(("2"
(skosimp)
(("2"
(inst - "v!1")
(("2"
(skosimp)
(("2"
(expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(inst - "u!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(skosimp)
(("2"
(expand "subset?")
(("2"
(inst - "v!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(inst + "UV(y!1)`1")
(("1"
(typepred "UV(y!1)")
(("1"
(assert)
(("1"
(expand
"disjoint?")
(("1"
(rewrite
"intersection_commutative")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "UV(y!1)")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp)
(("3"
(typepred "S")
(("3"
(expand "hausdorff_space?")
(("3" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "open_cover?")
(("2"
(split)
(("1"
(expand "subset?")
(("1"
(expand "member")
(("1"
(skosimp)
(("1"
(skosimp)
(("1"
(typepred "UV(y!1)")
(("1"
(replace -6)
(("1"
(expand "open?")
(("1"
(expand "member")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "cover?")
(("2"
(expand "subset?")
(("2"
(expand "member")
(("2"
(skosimp)
(("2"
(expand "Union")
(("2"
(inst + "UV(x!2)`2")
(("1"
(typepred "UV(x!2)")
(("1"
(propax)
nil
nil))
nil)
("2"
(inst + "x!2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -5 2)
(("2" (skosimp)
(("2"
(typepred "y!1")
(("2"
(typepred "S")
(("2"
(expand "hausdorff_space?")
(("2"
(flatten)
(("2"
(expand "hausdorff?")
(("2"
(expand "is_T2?")
(("2"
(inst - "x!1" "y!1")
(("2"
(assert)
(("2"
(split -2)
(("1"
(skosimp)
(("1"
(expand
"nonempty?"
1)
(("1"
(expand
"empty?"
-6)
(("1"
(expand
"member")
(("1"
(inst
-
"(U!1,V!1)")
(("1"
(assert)
(("1"
(typepred
"U!1")
(("1"
(typepred
"V!1")
(("1"
(expand
"open?")
(("1"
(expand
"member")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(replace -6 -4 rl)
(("2"
(expand
"fullset")
(("2"
(expand
"difference")
(("2"
(expand
"member")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp)
(("3" (typepred "S")
(("3"
(expand "hausdorff_space?")
(("3" (flatten) nil nil))
nil))
nil))
nil)
("4" (skosimp)
(("4" (typepred "S")
(("4"
(expand "hausdorff_space?")
(("4" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "nonempty?")
(("2" (rewrite "emptyset_is_empty?") nil nil)) nil))
nil))
nil)
("3" (skosimp)
(("3" (typepred "S")
(("3" (expand "hausdorff_space?")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.102 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.
|
