|
(topology_prelim
(discrete_topology_lem 0
(discrete_topology_lem-1 nil 3302350397 ("" (grind) nil nil)
((discrete_topology_set const-decl "setofsets[T]" topology_prelim
nil)
(emptyset const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(powerset const-decl "setofsets" sets nil)
(topology_empty? const-decl "bool" topology_prelim nil)
(topology_full? const-decl "bool" topology_prelim nil)
(Union const-decl "set" sets nil)
(topology_Union? const-decl "bool" topology_prelim nil)
(intersection const-decl "set" sets nil)
(topology_intersection? const-decl "bool" topology_prelim nil)
(topology? const-decl "bool" topology_prelim nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(nonempty_powerset application-judgement "(nonempty?[set[T]])"
sets_lemmas nil))
shostak))
(indiscrete_topology_lem 0
(indiscrete_topology_lem-1 nil 3302350598
("" (expand "indiscrete_topology_set")
(("" (expand "empty?")
(("" (expand "full?")
(("" (expand "topology?")
(("" (split)
(("1" (grind) nil nil) ("2" (grind) nil nil)
("3" (expand "topology_Union?")
(("3" (skosimp*)
(("3" (expand "member")
(("3" (flatten)
(("3" (skosimp*)
(("3" (expand "subset?")
(("3" (expand "Union")
(("3" (skosimp)
(("3" (typepred "a!1")
(("3"
(inst - "a!1")
(("3"
(expand "member")
(("3"
(split)
(("1" (inst - "x!1") nil nil)
("2"
(inst - "x!2")
(("2" (inst + "a!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "topology_intersection?")
(("4" (skosimp*)
(("4" (typepred "A!1")
(("4" (typepred "B!1")
(("4" (expand "intersection")
(("4" (expand "member")
(("4" (flatten)
(("4" (skosimp*)
(("4" (split -1)
(("1" (inst - "x!1") nil nil)
("2"
(inst - "x!2")
(("2"
(assert)
(("2"
(split -2)
(("1" (inst - "x!1") nil nil)
("2" (inst - "x!2") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(topology? const-decl "bool" topology_prelim nil)
(topology_intersection? const-decl "bool" topology_prelim nil)
(set type-eq-decl nil sets nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(intersection const-decl "set" sets nil)
(topology_Union? const-decl "bool" topology_prelim nil)
(Union const-decl "set" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil topology_prelim nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(subset? const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(topology_full? const-decl "bool" topology_prelim nil)
(member const-decl "bool" sets nil)
(emptyset const-decl "set" sets nil)
(topology_empty? const-decl "bool" topology_prelim nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(full? const-decl "bool" sets nil)
(indiscrete_topology_set const-decl "setofsets[T]" topology_prelim
nil))
shostak))
(topology_TCC1 0
(topology_TCC1-1 nil 3324957564
("" (lemma "discrete_topology_lem") (("" (propax) nil nil)) nil)
((discrete_topology_lem formula-decl nil topology_prelim nil))
shostak))
(indiscrete_topology_TCC1 0
(indiscrete_topology_TCC1-1 nil 3325047594
("" (lemma "indiscrete_topology_lem") (("" (propax) nil nil)) nil)
((indiscrete_topology_lem formula-decl nil topology_prelim nil))
shostak))
(T0_topology_TCC1 0
(T0_topology_TCC1-1 nil 3330396254
("" (expand "T0_space?")
(("" (expand "is_T0?")
(("" (skosimp)
(("" (inst + "singleton(x!1)")
(("1" (grind) nil nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((is_T0? const-decl "bool" topology_prelim nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(x!1 skolem-const-decl "T" topology_prelim nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(discrete_topology const-decl "topology" topology_prelim nil)
(topology nonempty-type-eq-decl nil topology_prelim nil)
(topology? 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 topology_prelim nil)
(member const-decl "bool" sets nil)
(discrete_topology_set const-decl "setofsets[T]" topology_prelim
nil)
(fullset const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(powerset const-decl "setofsets" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(nonempty_powerset application-judgement "(nonempty?[set[T]])"
sets_lemmas nil)
(T0_space? const-decl "bool" topology_prelim nil))
shostak))
(T1_topology_TCC1 0
(T1_topology_TCC1-1 nil 3330396254
("" (expand "T1_space?")
(("" (expand "is_T1?")
(("" (skosimp)
(("" (inst + "singleton(x!1)")
(("1" (grind) nil nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((is_T1? const-decl "bool" topology_prelim nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(x!1 skolem-const-decl "T" topology_prelim nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(discrete_topology const-decl "topology" topology_prelim nil)
(topology nonempty-type-eq-decl nil topology_prelim nil)
(topology? 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 topology_prelim nil)
(member const-decl "bool" sets nil)
(discrete_topology_set const-decl "setofsets[T]" topology_prelim
nil)
(fullset const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(powerset const-decl "setofsets" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(nonempty_powerset application-judgement "(nonempty?[set[T]])"
sets_lemmas nil)
(T1_space? const-decl "bool" topology_prelim nil))
shostak))
(T2_topology_TCC1 0
(T2_topology_TCC1-1 nil 3330396254
("" (expand "T2_space?")
(("" (expand "is_T2?")
(("" (skosimp)
(("" (inst + "singleton(x!1)" "singleton(y!1)")
(("1" (grind) nil nil)
("2" (hide 2) (("2" (grind) nil nil)) nil)
("3" (hide 2) (("3" (grind) nil nil)) nil))
nil))
nil))
nil))
nil)
((is_T2? const-decl "bool" topology_prelim nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(x!1 skolem-const-decl "T" topology_prelim nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(discrete_topology const-decl "topology" topology_prelim nil)
(topology nonempty-type-eq-decl nil topology_prelim nil)
(topology? 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 topology_prelim nil)
(y!1 skolem-const-decl "T" topology_prelim nil)
(finite_intersection1 application-judgement "finite_set"
finite_sets nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(discrete_topology_set const-decl "setofsets[T]" topology_prelim
nil)
(fullset const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(powerset const-decl "setofsets" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(nonempty_powerset application-judgement "(nonempty?[set[T]])"
sets_lemmas nil)
(T2_space? const-decl "bool" topology_prelim nil))
shostak))
(hausdorff_TCC1 0
(hausdorff_TCC1-1 nil 3324957564
("" (lemma "discrete_topology_lem")
(("" (expand "hausdorff_space?")
(("" (expand "hausdorff?")
(("" (lemma "T2_topology_TCC1")
(("" (expand "T2_space?") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((hausdorff_space? const-decl "bool" topology_prelim nil)
(T2_topology_TCC1 subtype-tcc nil topology_prelim nil)
(T2_space? const-decl "bool" topology_prelim nil)
(hausdorff? const-decl "bool" topology_prelim nil)
(discrete_topology_lem formula-decl nil topology_prelim nil))
shostak))
(T0_is_topology 0
(T0_is_topology-1 nil 3330396877
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "T1_space?") (("" (flatten) nil nil)) nil)) nil))
nil)
((T1_topology nonempty-type-eq-decl nil topology_prelim nil)
(T1_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 topology_prelim nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(T1_is_T0 0
(T1_is_T0-1 nil 3330396689
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "T1_space?")
(("" (expand "T0_space?")
(("" (flatten)
(("" (assert)
(("" (expand "is_T0?")
(("" (expand "is_T1?")
(("" (skosimp)
(("" (expand "member")
(("" (inst - "x!2" "y!1")
(("" (assert)
(("" (skosimp)
(("" (inst + "U!1") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T1_topology nonempty-type-eq-decl nil topology_prelim nil)
(T1_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 topology_prelim nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T0_space? const-decl "bool" topology_prelim nil)
(is_T1? const-decl "bool" topology_prelim nil)
(member const-decl "bool" sets nil)
(is_T0? const-decl "bool" topology_prelim nil))
shostak))
(T2_is_T1 0
(T2_is_T1-1 nil 3330396531
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "T2_space?")
(("" (flatten)
(("" (expand "T1_space?")
(("" (assert)
(("" (expand "is_T1?")
(("" (expand "is_T2?")
(("" (hide -1)
(("" (skosimp)
(("" (inst - "x!2" "y!1")
(("" (assert)
(("" (skosimp)
(("" (inst + "U!1")
((""
(expand "disjoint?")
((""
(expand "empty?")
((""
(replace -2)
((""
(inst - "y!1")
(("" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T2_topology nonempty-type-eq-decl nil topology_prelim nil)
(T2_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 topology_prelim 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)
(empty? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(disjoint? const-decl "bool" sets nil)
(is_T1? const-decl "bool" topology_prelim nil)
(T1_space? const-decl "bool" topology_prelim nil))
shostak))
(hausdorff_is_T2 0
(hausdorff_is_T2-1 nil 3330400662
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "hausdorff_space?")
(("" (expand "T2_space?")
(("" (expand "hausdorff?") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
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 topology_prelim nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T2_space? const-decl "bool" topology_prelim nil)
(hausdorff? const-decl "bool" topology_prelim nil))
shostak))
(T2_is_hausdorff 0
(T2_is_hausdorff-1 nil 3330400662
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "T2_space?")
(("" (expand "hausdorff_space?")
(("" (expand "hausdorff?") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((T2_topology nonempty-type-eq-decl nil topology_prelim nil)
(T2_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 topology_prelim nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(hausdorff_space? const-decl "bool" topology_prelim nil)
(hausdorff? const-decl "bool" topology_prelim nil))
shostak))
(compact_space_TCC1 0
(compact_space_TCC1-1 nil 3330397116
("" (expand "compact_space?")
(("" (expand "compact_subset?")
(("" (skosimp)
(("" (expand "finite_cover?")
(("" (expand "open_cover?")
(("" (flatten)
(("" (expand "indiscrete_topology")
(("" (inst + "U!1")
(("" (split)
(("1" (grind) nil nil)
("2" (hide -2)
(("2" (expand "subset?")
(("2" (expand "indiscrete_topology_set")
(("2" (expand "member")
(("2"
(lemma "finite_subset[set[T]]"
("s"
"U!1"
"A"
"{A | empty?(A) OR full?(A)}"))
(("1"
(assert)
(("1"
(expand "subset?")
(("1"
(expand "member")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(expand "is_finite")
(("2"
(inst
+
"2"
"lambda (x: {A | empty?[T](A) OR full?[T](A)}): if empty?(x) then 0 else 1 endif")
(("2"
(expand "injective?")
(("2"
(skosimp)
(("2"
(typepred "x1!1")
(("2"
(case-replace
"empty?[T](x1!1)")
(("1"
(lift-if)
(("1"
(prop)
(("1"
(rewrite
"emptyset_is_empty?")
(("1"
(rewrite
"emptyset_is_empty?")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(typepred "x2!1")
(("2"
(case-replace
"empty?[T](x2!1)")
(("1"
(lift-if)
(("1"
(assert)
nil
nil))
nil)
("2"
(assert)
(("2"
(rewrite
"fullset_is_full?")
(("2"
(rewrite
"fullset_is_full?")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((compact_subset? const-decl "bool" topology_prelim nil)
(finite_cover? const-decl "bool" topology_prelim nil)
(T formal-type-decl nil topology_prelim nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(finite_subset formula-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(set type-eq-decl nil sets nil)
(injective? const-decl "bool" functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(fullset_is_full? formula-decl nil sets_lemmas nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals 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)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(full? const-decl "bool" sets nil)
(indiscrete_topology_set const-decl "setofsets[T]" topology_prelim
nil)
(Union const-decl "set" sets nil)
(cover? const-decl "bool" topology_prelim nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(indiscrete_topology const-decl "topology" topology_prelim nil)
(open_cover? const-decl "bool" topology_prelim nil)
(compact_space? const-decl "bool" topology_prelim nil))
shostak))
(compact_space_is_topology 0
(compact_space_is_topology-1 nil 3330397116
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "compact_space?") (("" (flatten) nil nil)) nil))
nil))
nil)
((compact_space nonempty-type-eq-decl nil topology_prelim nil)
(compact_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 topology_prelim nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(compact_hausdorff_is_topology 0
(compact_hausdorff_is_topology-1 nil 3382168325
("" (judgement-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil topology_prelim nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(compact_hausdorff? const-decl "bool" topology_prelim nil)
(compact_hausdorff type-eq-decl nil topology_prelim nil)
(/= const-decl "boolean" notequal nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(is_T2? const-decl "bool" topology_prelim nil)
(hausdorff? const-decl "bool" topology_prelim nil)
(Union const-decl "set" sets nil)
(cover? const-decl "bool" topology_prelim nil)
(open_cover? const-decl "bool" topology_prelim nil)
(injective? const-decl "bool" functions nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_cover? const-decl "bool" topology_prelim nil)
(compact_subset? const-decl "bool" topology_prelim nil)
(compact_space? const-decl "bool" topology_prelim nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(member const-decl "bool" sets nil)
(topology_empty? const-decl "bool" topology_prelim nil)
(topology_full? const-decl "bool" topology_prelim nil)
(subset? const-decl "bool" sets nil)
(topology_Union? const-decl "bool" topology_prelim nil)
(topology_intersection? const-decl "bool" topology_prelim nil)
(topology? const-decl "bool" topology_prelim nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil))
nil))
(compact_hausdorff_is_hausdorff 0
(compact_hausdorff_is_hausdorff-1 nil 3382168325
("" (judgement-tcc) nil nil)
((compact_hausdorff type-eq-decl nil topology_prelim nil)
(compact_hausdorff? 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 topology_prelim nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(compact_space? const-decl "bool" topology_prelim nil)
(compact_subset? const-decl "bool" topology_prelim nil)
(finite_cover? const-decl "bool" topology_prelim nil)
(is_finite const-decl "bool" finite_sets nil)
(injective? const-decl "bool" functions nil)
(open_cover? const-decl "bool" topology_prelim nil)
(cover? const-decl "bool" topology_prelim nil)
(Union const-decl "set" sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(member const-decl "bool" sets nil)
(topology_empty? const-decl "bool" topology_prelim nil)
(topology_full? const-decl "bool" topology_prelim nil)
(subset? const-decl "bool" sets nil)
(topology_Union? const-decl "bool" topology_prelim nil)
(topology_intersection? const-decl "bool" topology_prelim nil)
(topology? const-decl "bool" topology_prelim nil)
(/= const-decl "boolean" notequal nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(disjoint? const-decl "bool" sets nil)
(is_T2? const-decl "bool" topology_prelim nil)
(hausdorff? const-decl "bool" topology_prelim nil)
(hausdorff_space? const-decl "bool" topology_prelim nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil))
nil))
(compact_hausdorff_is_compact_space 0
(compact_hausdorff_is_compact_space-1 nil 3382168325
("" (judgement-tcc) nil nil)
((compact_hausdorff type-eq-decl nil topology_prelim nil)
(compact_hausdorff? 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 topology_prelim nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(hausdorff? const-decl "bool" topology_prelim nil)
(is_T2? const-decl "bool" topology_prelim nil)
(disjoint? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(/= const-decl "boolean" notequal nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(member const-decl "bool" sets nil)
(topology_empty? const-decl "bool" topology_prelim nil)
(topology_full? const-decl "bool" topology_prelim nil)
(subset? const-decl "bool" sets nil)
(topology_Union? const-decl "bool" topology_prelim nil)
(topology_intersection? const-decl "bool" topology_prelim nil)
(topology? const-decl "bool" topology_prelim nil)
(Union const-decl "set" sets nil)
(cover? const-decl "bool" topology_prelim nil)
(open_cover? const-decl "bool" topology_prelim nil)
(injective? const-decl "bool" functions nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_cover? const-decl "bool" topology_prelim nil)
(compact_subset? const-decl "bool" topology_prelim nil)
(compact_space? const-decl "bool" topology_prelim nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil))
nil))
(connected_space_TCC1 0
(connected_space_TCC1-1 nil 3330401564
("" (expand "connected_space?")
(("" (expand "connected?")
(("" (skosimp)
(("" (typepred "A!1")
(("" (expand "indiscrete_topology")
(("" (expand "indiscrete_topology_set")
(("" (rewrite "emptyset_is_empty?")
(("" (rewrite "emptyset_is_empty?")
(("" (rewrite "fullset_is_full?")
(("" (rewrite "fullset_is_full?")
(("" (split -1)
(("1" (propax) nil nil) ("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((connected? const-decl "bool" topology_prelim nil)
(indiscrete_topology const-decl "topology" topology_prelim nil)
(topology nonempty-type-eq-decl nil topology_prelim nil)
(topology? 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 topology_prelim nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(indiscrete_topology_set const-decl "setofsets[T]" topology_prelim
nil)
(complement const-decl "set" sets nil)
(fullset_is_full? formula-decl nil sets_lemmas nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(set type-eq-decl nil sets nil)
(connected_space? const-decl "bool" topology_prelim nil))
shostak))
(connected_space_is_topology 0
(connected_space_is_topology-1 nil 3330401565
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "connected_space?") (("" (flatten) nil nil)) nil))
nil))
nil)
((connected_space nonempty-type-eq-decl nil topology_prelim nil)
(connected_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 topology_prelim nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak)))
¤ Dauer der Verarbeitung: 0.51 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.
|
