|
(topology
(open_set_TCC1 0
(open_set_TCC1-1 nil 3324957210
("" (expand "open?")
(("" (typepred "S")
(("" (expand "topology?")
(("" (expand "topology_empty?") (("" (flatten) nil nil)) nil))
nil))
nil))
nil)
((S formal-const-decl "topology" topology 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 nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(topology_empty? const-decl "bool" topology_prelim nil)
(open? const-decl "bool" topology nil))
shostak))
(closed_set_TCC1 0
(closed_set_TCC1-1 nil 3324957210
("" (typepred "S")
(("" (expand "closed?")
(("" (rewrite "complement_emptyset")
(("" (expand "topology?")
(("" (expand "topology_full?") (("" (flatten) nil nil)) nil))
nil))
nil))
nil))
nil)
((closed? const-decl "bool" topology nil)
(topology_full? const-decl "bool" topology_prelim nil)
(complement_emptyset formula-decl nil sets_lemmas 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 nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(topology? const-decl "bool" topology_prelim nil)
(topology nonempty-type-eq-decl nil topology_prelim nil)
(S formal-const-decl "topology" topology nil))
shostak))
(clopen_set_TCC1 0
(clopen_set_TCC1-1 nil 3364196997
("" (expand "clopen?")
(("" (lemma "open_set_TCC1")
(("" (lemma "closed_set_TCC1") (("" (assert) nil nil)) nil))
nil))
nil)
((open_set_TCC1 subtype-tcc nil topology nil)
(closed_set_TCC1 subtype-tcc nil topology nil)
(clopen? const-decl "bool" topology nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil))
nil))
(compact_TCC1 0
(compact_TCC1-1 nil 3397736514
("" (expand "compact?")
(("" (expand "compact_subset?")
(("" (skosimp)
(("" (inst + "emptyset[set[T]]")
(("" (hide -1)
(("" (expand "finite_cover?")
(("" (rewrite "subset_emptyset")
(("" (expand "cover?")
(("" (rewrite "subset_emptyset") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((compact_subset? const-decl "bool" topology_prelim nil)
(T formal-type-decl nil topology 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)
(set type-eq-decl nil sets nil)
(emptyset const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_cover? const-decl "bool" topology_prelim nil)
(cover? const-decl "bool" topology_prelim nil)
(Union const-decl "set" sets nil)
(subset_emptyset formula-decl nil sets_lemmas nil)
(compact? const-decl "bool" topology nil))
nil))
(clopen_set_is_open 0
(clopen_set_is_open-1 nil 3364196997
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "clopen?") (("" (flatten) nil nil)) nil)) nil))
nil)
((clopen_set nonempty-type-eq-decl nil topology nil)
(clopen? const-decl "bool" topology nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil topology nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(clopen_set_is_closed 0
(clopen_set_is_closed-1 nil 3364196997
("" (skosimp)
(("" (typepred "x!1")
(("" (expand "clopen?") (("" (flatten) nil nil)) nil)) nil))
nil)
((clopen_set nonempty-type-eq-decl nil topology nil)
(clopen? const-decl "bool" topology nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil topology nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(open_complement 0
(open_complement-1 nil 3300504914
("" (expand "closed?")
(("" (expand "member")
(("" (expand "open?")
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((member const-decl "bool" sets nil)
(open? const-decl "bool" topology nil)
(closed? const-decl "bool" topology nil))
shostak))
(closed_complement 0
(closed_complement-1 nil 3300504937
("" (expand "closed?")
(("" (expand "open?")
(("" (skosimp)
(("" (rewrite "complement_complement") (("" (assert) nil nil))
nil))
nil))
nil))
nil)
((open? const-decl "bool" topology nil)
(complement_complement formula-decl nil sets_lemmas nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil topology nil)
(member const-decl "bool" sets nil)
(closed? const-decl "bool" topology nil))
shostak))
(open_emptyset 0
(open_emptyset-1 nil 3301114668
("" (expand "open?")
(("" (typepred "S")
(("" (expand "topology?")
(("" (flatten)
(("" (expand "topology_empty?") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((S formal-const-decl "topology" topology 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 nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(topology_empty? const-decl "bool" topology_prelim nil)
(open? const-decl "bool" topology nil))
shostak))
(open_fullset 0
(open_fullset-1 nil 3301114694
("" (expand "open?")
(("" (typepred "S")
(("" (expand "topology?")
(("" (flatten)
(("" (expand "topology_full?") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((S formal-const-decl "topology" topology 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 nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(topology_full? const-decl "bool" topology_prelim nil)
(open? const-decl "bool" topology nil))
shostak))
(open_Union 0
(open_Union-1 nil 3301114716
("" (skosimp)
(("" (typepred "S")
(("" (expand "topology?")
(("" (flatten)
(("" (expand "topology_Union?")
(("" (inst - "Y!1")
(("" (expand "open?")
(("" (split -3)
(("1" (propax) nil nil)
("2" (hide-all-but (-4 1))
(("2" (expand "subset?")
(("2" (skosimp)
(("2" (expand "every")
(("2" (expand "member")
(("2" (inst - "x!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((S formal-const-decl "topology" topology 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 nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(subset? const-decl "bool" sets nil)
(every const-decl "bool" sets nil)
(Y!1 skolem-const-decl "setofsets[T]" topology nil)
(x!1 skolem-const-decl "setof[T]" topology nil)
(member const-decl "bool" sets nil)
(open? const-decl "bool" topology nil)
(topology_Union? const-decl "bool" topology_prelim nil))
shostak))
(open_union 0
(open_union-1 nil 3301285730
("" (skosimp)
(("" (typepred "U1!1")
(("" (typepred "U2!1")
(("" (name "YY" "{a:set[T] | a = U1!1 OR a = U2!1}")
(("" (lemma "open_Union" ("Y" "YY"))
((""
(lemma "extensionality"
("a" "Union(YY)" "b" "union(U1!1,U2!1)"))
(("" (split -1)
(("1" (split -2)
(("1" (assert) nil nil)
("2" (replace -2 1 rl)
(("2" (hide -1 -2 2)
(("2" (expand "every")
(("2" (skosimp)
(("2" (typepred "x!1")
(("2" (split)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -2 1 rl)
(("2" (hide -1 -2 2)
(("2" (skosimp*)
(("2" (expand "Union")
(("2" (expand "union")
(("2" (assert)
(("2" (split 1)
(("1"
(skosimp*)
(("1"
(typepred "a!1")
(("1"
(split -1)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2"
(flatten)
(("2"
(split -1)
(("1" (inst + "U1!1") nil nil)
("2" (inst + "U2!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((open nonempty-type-eq-decl nil topology nil)
(open? const-decl "bool" topology nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil topology nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(extensionality formula-decl nil sets_lemmas nil)
(Union const-decl "set" sets nil) (union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(every const-decl "bool" sets nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(open_Union formula-decl nil topology nil))
shostak))
(open_intersection 0
(open_intersection-1 nil 3301114844
("" (skosimp)
(("" (typepred "U1!1")
(("" (typepred "U2!1")
(("" (expand "open?")
(("" (typepred "S")
(("" (expand "topology?")
(("" (flatten)
(("" (expand "topology_intersection?")
(("" (inst - "U1!1" "U2!1")
(("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((open nonempty-type-eq-decl nil topology nil)
(open? const-decl "bool" topology nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil topology nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(topology_intersection? const-decl "bool" topology_prelim nil)
(member const-decl "bool" sets nil)
(U2!1 skolem-const-decl "open" topology nil)
(U1!1 skolem-const-decl "open" topology nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(topology? const-decl "bool" topology_prelim nil)
(topology nonempty-type-eq-decl nil topology_prelim nil)
(S formal-const-decl "topology" topology nil))
shostak))
(open_Intersection 0
(open_Intersection-1 nil 3301282923
("" (skosimp)
(("" (name "N" "card(Y!1)")
(("1" (lemma "Intersection_finite" ("A" "Y!1" "P" "open?"))
(("1" (split -1)
(("1" (propax) nil nil)
("2" (rewrite "open_fullset") nil nil)
("3" (propax) nil nil)
("4" (expand "every") (("4" (propax) nil nil)) nil)
("5" (skosimp)
(("5" (lemma "open_intersection" ("U1" "a!1" "U2" "b!1"))
(("1" (propax) nil nil) ("2" (propax) nil nil)
("3" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil)
((setofsets type-eq-decl nil sets nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets 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)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-type-decl nil topology nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(open_fullset formula-decl nil topology nil)
(every const-decl "bool" sets nil)
(open_intersection formula-decl nil topology nil)
(open nonempty-type-eq-decl nil topology nil)
(open? const-decl "bool" topology nil)
(Intersection_finite formula-decl nil prelude_sets_aux nil))
shostak))
(closed_emptyset 0
(closed_emptyset-1 nil 3301114927
("" (rewrite "open_complement" 1 :dir rl)
(("" (rewrite "complement_emptyset")
(("" (rewrite "open_fullset") nil nil)) nil))
nil)
((complement_emptyset formula-decl nil sets_lemmas nil)
(open_fullset formula-decl nil topology nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset const-decl "set" sets 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-type-decl nil topology nil)
(open_complement formula-decl nil topology nil))
shostak))
(closed_fullset 0
(closed_fullset-1 nil 3301114973
("" (rewrite "open_complement" 1 :dir rl)
(("" (rewrite "complement_fullset")
(("" (rewrite "open_emptyset") nil nil)) nil))
nil)
((complement_fullset formula-decl nil sets_lemmas nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(open_emptyset formula-decl nil topology nil)
(fullset const-decl "set" sets 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-type-decl nil topology nil)
(open_complement formula-decl nil topology nil))
shostak))
(closed_Intersection 0
(closed_Intersection-1 nil 3301115017
("" (skosimp)
(("" (rewrite "open_complement" 1 :dir rl)
(("" (rewrite "Demorgan2")
(("" (lemma "open_Union" ("Y" "Complement(Y!1)"))
(("" (split)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (expand "every")
(("2" (skosimp)
(("2" (typepred "x!1")
(("2" (expand "Complement")
(("2" (skosimp)
(("2" (typepred "b!1")
(("2" (inst - "b!1")
(("2"
(rewrite "open_complement" -3 :dir rl)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((open_complement formula-decl nil topology nil)
(T formal-type-decl nil topology nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(Intersection const-decl "set" sets nil)
(Intersection_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(open_Union formula-decl nil topology nil)
(Complement const-decl "setofsets[T]" sets_lemmas nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(every const-decl "bool" sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(Complement_bijective name-judgement
"(bijective?[setofsets[T], setofsets[T]])" sets_lemmas nil)
(Demorgan2 formula-decl nil sets_lemmas nil))
shostak))
(closed_intersection 0
(closed_intersection-1 nil 3301287033
("" (skosimp)
(("" (typepred "V1!1")
(("" (typepred "V2!1")
(("" (rewrite "open_complement" :dir rl)
(("" (rewrite "open_complement" :dir rl)
(("" (rewrite "open_complement" :dir rl)
(("" (rewrite "demorgan2")
(("" (rewrite "open_union") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((closed nonempty-type-eq-decl nil topology nil)
(closed? const-decl "bool" topology nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil topology nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(open_complement formula-decl nil topology nil)
(intersection const-decl "set" sets nil)
(open_union formula-decl nil topology nil)
(open? const-decl "bool" topology nil)
(open nonempty-type-eq-decl nil topology nil)
(complement const-decl "set" sets nil)
(demorgan2 formula-decl nil sets_lemmas nil))
shostak))
(closed_union 0
(closed_union-1 nil 3301115491
("" (skosimp)
(("" (rewrite "open_complement" 1 :dir rl)
(("" (rewrite "demorgan1")
(("" (typepred "V1!1")
(("" (typepred "V2!1")
(("" (rewrite "open_complement" -1 :dir rl)
(("" (rewrite "open_complement" -2 :dir rl)
((""
(lemma "open_intersection"
("U1" "complement(V1!1)" "U2" "complement(V2!1)"))
(("1" (propax) nil nil) ("2" (propax) nil nil)
("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((open_complement formula-decl nil topology nil)
(T formal-type-decl nil topology nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil) (union const-decl "set" sets nil)
(closed? const-decl "bool" topology nil)
(closed nonempty-type-eq-decl nil topology nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(complement const-decl "set" sets nil)
(open nonempty-type-eq-decl nil topology nil)
(open? const-decl "bool" topology nil)
(open_intersection formula-decl nil topology nil)
(demorgan1 formula-decl nil sets_lemmas nil))
shostak))
(closed_Union 0
(closed_Union-1 nil 3301283172
("" (skosimp)
(("" (rewrite "open_complement" 1 :dir rl)
(("" (rewrite "Demorgan1")
(("" (lemma "open_Intersection" ("Y" "Complement(Y!1)"))
(("" (rewrite "finite_Complement")
(("" (split)
(("1" (propax) nil nil)
("2" (hide -1 2)
(("2" (expand "closed?")
(("2" (expand "Complement")
(("2" (expand "every")
(("2" (skosimp)
(("2" (typepred "x!1")
(("2" (skosimp)
(("2" (inst - "b!1")
(("2"
(expand "open?")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((open_complement formula-decl nil topology nil)
(T formal-type-decl nil topology nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(Union const-decl "set" sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(open_Intersection formula-decl nil topology nil)
(Complement const-decl "setofsets[T]" sets_lemmas nil)
(closed? const-decl "bool" topology nil)
(every const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(complement const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(open? const-decl "bool" topology nil)
(finite_Complement formula-decl nil prelude_sets_aux nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(Intersection_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(Complement_bijective name-judgement
"(bijective?[setofsets[T], setofsets[T]])" sets_lemmas nil)
(Demorgan1 formula-decl nil sets_lemmas nil))
shostak))
(complement_open_is_closed 0
(complement_open_is_closed-1 nil 3358736741
("" (skosimp)
(("" (typepred "U!1")
(("" (rewrite "closed_complement" -1 :dir rl) nil nil)) nil))
nil)
((open nonempty-type-eq-decl nil topology nil)
(open? const-decl "bool" topology nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil topology nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(closed_complement formula-decl nil topology nil))
nil))
(complement_closed_is_open 0
(complement_closed_is_open-1 nil 3358736741
("" (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 nil)
(set type-eq-decl nil sets nil)
(closed? const-decl "bool" topology nil)
(closed nonempty-type-eq-decl nil topology nil)
(member const-decl "bool" sets nil)
(open? const-decl "bool" topology nil))
nil))
(emptyset_is_open 0
(emptyset_is_open-1 nil 3358736741
("" (rewrite "open_emptyset") nil nil)
((open_emptyset formula-decl nil topology nil)) nil))
(fullset_is_open 0
(fullset_is_open-1 nil 3358736741
("" (rewrite "open_fullset") nil nil)
((open_fullset formula-decl nil topology nil)) nil))
(union_is_open 0
(union_is_open-1 nil 3358736741
("" (skosimp) (("" (rewrite "open_union") nil nil)) nil)
((open_union formula-decl nil topology nil)
(T formal-type-decl nil topology nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(open? const-decl "bool" topology nil)
(open nonempty-type-eq-decl nil topology nil))
nil))
(intersection_is_open 0
(intersection_is_open-1 nil 3358736741
("" (skosimp) (("" (rewrite "open_intersection") nil nil)) nil)
((open_intersection formula-decl nil topology nil)
(T formal-type-decl nil topology nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(open? const-decl "bool" topology nil)
(open nonempty-type-eq-decl nil topology nil))
nil))
(emptyset_is_closed 0
(emptyset_is_closed-1 nil 3358736741
("" (rewrite "closed_emptyset") nil nil)
((closed_emptyset formula-decl nil topology nil)) nil))
(fullset_is_closed 0
(fullset_is_closed-1 nil 3358736741
("" (rewrite "closed_fullset") nil nil)
((closed_fullset formula-decl nil topology nil)) nil))
(union_is_closed 0
(union_is_closed-1 nil 3358736741
("" (skosimp) (("" (rewrite "closed_union") nil nil)) nil)
((closed_union formula-decl nil topology nil)
(T formal-type-decl nil topology nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(closed? const-decl "bool" topology nil)
(closed nonempty-type-eq-decl nil topology nil))
nil))
(intersection_is_closed 0
(intersection_is_closed-1 nil 3358736741
("" (skosimp) (("" (rewrite "closed_intersection") nil nil)) nil)
((closed_intersection formula-decl nil topology nil)
(T formal-type-decl nil topology nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(closed? const-decl "bool" topology nil)
(closed nonempty-type-eq-decl nil topology nil))
nil))
(emptyset_is_clopen 0
(emptyset_is_clopen-1 nil 3364196997
("" (expand "clopen?") (("" (propax) nil nil)) nil)
((clopen? const-decl "bool" topology nil)
(emptyset_is_open name-judgement "open" topology nil)
(emptyset_is_closed name-judgement "closed" topology nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil))
nil))
(fullset_is_clopen 0
(fullset_is_clopen-1 nil 3364196997
("" (expand "clopen?") (("" (propax) nil nil)) nil)
((clopen? const-decl "bool" topology nil)
(fullset_is_open name-judgement "open" topology nil)
(fullset_is_closed name-judgement "closed" topology nil))
nil))
(indiscrete_subset 0
(indiscrete_subset-1 nil 3325049834
("" (skosimp)
(("" (typepred "t!1")
(("" (typepred "indiscrete_topology")
(("" (expand "subset?")
(("" (skosimp)
(("" (expand "member")
(("" (expand "indiscrete_topology")
(("" (expand "indiscrete_topology_set")
(("" (split -3)
(("1" (hide -2)
(("1" (rewrite "emptyset_is_empty?")
(("1" (replace -1)
(("1" (expand "topology?")
(("1" (flatten)
(("1"
(expand "topology_empty?")
(("1"
(expand "member")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "fullset_is_full?")
(("2" (replace -1)
(("2" (hide -1 -2)
(("2" (expand "topology?")
(("2" (flatten)
(("2"
(expand "topology_full?")
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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 nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(indiscrete_topology_set const-decl "setofsets[T]" topology_prelim
nil)
(fullset_is_full? formula-decl nil sets_lemmas nil)
(fullset_is_clopen name-judgement "clopen" topology nil)
(topology_full? const-decl "bool" topology_prelim nil)
(topology_empty? const-decl "bool" topology_prelim nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset_is_clopen name-judgement "clopen" topology nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(set type-eq-decl nil sets nil)
(indiscrete_topology const-decl "topology" topology_prelim nil))
shostak))
(discrete_subset 0
(discrete_subset-1 nil 3325049944
("" (skosimp)
(("" (typepred "t!1")
(("" (expand "subset?")
(("" (skosimp*)
(("" (expand "discrete_topology")
(("" (expand "discrete_topology_set")
(("" (expand "fullset")
(("" (expand "powerset")
(("" (expand "member")
(("" (expand "subset?")
(("" (skosimp*)
(("" (expand "member") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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 nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(discrete_topology_set const-decl "setofsets[T]" topology_prelim
nil)
(powerset const-decl "setofsets" sets nil)
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(discrete_topology const-decl "topology" topology_prelim nil)
(subset? const-decl "bool" sets nil))
shostak))
(open_def 0
(open_def-1 nil 3300477193
("" (skosimp)
(("" (expand "neighbourhood?")
(("" (expand "interior_point?")
(("" (expand "open?")
(("" (split)
(("1" (skosimp*)
(("1" (typepred "x!1")
(("1" (inst + "A!1")
(("1" (rewrite "subset_reflexive")
(("1" (expand "member") (("1" (propax) nil nil))
nil))
nil)
("2" (expand "open?") (("2" (propax) nil nil)) nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2"
(name "Ux"
"{a:set[T] | open?(a) & subset?(a,A!1) & EXISTS (x:(A!1)): a(x)}")
(("2" (case "A!1 = Union(Ux)")
(("1" (lemma "open_Union" ("Y" "Ux"))
(("1" (split -1)
(("1" (expand "open?") (("1" (assert) nil nil))
nil)
("2" (hide 2)
(("2" (expand "every")
(("2" (skosimp)
(("2" (typepred "x!1")
(("2"
(replace -3 -1 rl)
(("2"
(assert)
(("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "extensionality" 1)
(("2" (replace -1 1 rl)
(("2" (hide -1 2 3)
(("2" (skosimp)
(("2" (expand "Union")
(("2" (case-replace "A!1(x!1)")
(("1"
(inst - "x!1")
(("1"
(skosimp)
(("1"
(inst + "U!1")
(("1"
(assert)
(("1" (inst + "x!1") nil nil))
nil))
nil))
nil))
nil)
("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((neighbourhood? const-decl "bool" topology nil)
(open? const-decl "bool" topology nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(Union const-decl "set" sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(every const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(open_Union formula-decl nil topology nil)
(U!1 skolem-const-decl "open" topology nil)
(x!1 skolem-const-decl "T" topology nil)
(extensionality formula-decl nil functions nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(subset? const-decl "bool" sets nil)
(A!1 skolem-const-decl "set[T]" topology nil)
(open nonempty-type-eq-decl nil topology nil)
(member const-decl "bool" sets nil)
(subset_reflexive formula-decl nil sets_lemmas 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 nil)
(set type-eq-decl nil sets nil)
(interior_point? const-decl "bool" topology nil))
shostak))
(neighbourhood_intersection 0
(neighbourhood_intersection-1 nil 3300507815
("" (expand "neighbourhood?")
(("" (expand "interior_point?")
(("" (skosimp*)
(("" (expand "member")
(("" (inst + "intersection(U!1, U!2)")
(("1" (split)
(("1" (expand "subset?")
(("1" (expand "intersection")
(("1" (skosimp*)
(("1" (assert)
(("1" (inst - "x!2")
(("1" (inst - "x!2")
(("1" (flatten)
(("1" (assert) (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "intersection") (("2" (assert) nil nil))
nil))
nil)
("2" (expand "open?")
(("2" (assert)
(("2" (typepred "U!1")
(("2" (typepred "U!2")
(("2"
(lemma "open_intersection"
("U1" "U!1" "U2" "U!2"))
(("2" (expand "open?")
(("2" (expand "member")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((interior_point? const-decl "bool" topology nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(intersection const-decl "set" sets nil)
(open nonempty-type-eq-decl nil topology nil)
(open? const-decl "bool" topology 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-type-decl nil topology nil)
(intersection_is_open application-judgement "open" topology nil)
(neighbourhood? const-decl "bool" topology nil))
shostak))
(neighbourhood_subset 0
(neighbourhood_subset-1 nil 3300508120
("" (skosimp)
(("" (expand "neighbourhood?")
(("" (expand "interior_point?")
(("" (skosimp*)
(("" (inst + "U!1")
((""
(lemma "subset_transitive"
("a" "U!1" "b" "A!1" "c" "B!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((neighbourhood? const-decl "bool" topology nil)
(subset_transitive formula-decl nil sets_lemmas nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(member const-decl "bool" sets nil)
(open nonempty-type-eq-decl nil topology nil)
(open? const-decl "bool" topology 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-type-decl nil topology nil)
(interior_point? const-decl "bool" topology nil))
shostak))
(Cl_split1 0
(Cl_split1-1 nil 3300472637
("" (skosimp)
(("" (rewrite "extensionality")
(("" (hide 2)
(("" (skosimp)
(("" (expand "union")
(("" (expand "derived_set")
(("" (expand "limit_point?")
(("" (assert)
(("" (expand "Cl")
(("" (case-replace "A!1(x!1)")
(("1" (expand "adherent_point?")
(("1" (skosimp)
(("1" (expand "neighbourhood?")
(("1" (expand "interior_point?")
(("1"
(skosimp)
(("1"
(expand "nonempty?")
(("1"
(expand "intersection")
(("1"
(expand "empty?")
(("1"
(inst - "x!1")
(("1"
(assert)
(("1"
(expand "subset?")
(("1"
(inst - "x!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((extensionality formula-decl nil functions nil)
(set type-eq-decl nil sets nil) (union const-decl "set" sets nil)
(derived_set const-decl "set[T]" topology nil)
(Cl const-decl "set[T]" topology nil)
(T formal-type-decl nil topology nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(member const-decl "bool" sets nil)
(interior_point? const-decl "bool" topology nil)
(nonempty? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(neighbourhood? const-decl "bool" topology nil)
(adherent_point? const-decl "bool" topology nil)
(limit_point? const-decl "bool" topology nil))
shostak))
(Cl_split2 0
(Cl_split2-1 nil 3300473579
("" (expand "disjoint?")
(("" (expand "intersection")
(("" (expand "derived_set")
(("" (expand "limit_point?")
(("" (expand "empty?")
(("" (skosimp*)
(("" (assert) (("" (flatten) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((intersection const-decl "set" sets nil)
(limit_point? const-decl "bool" topology nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(derived_set const-decl "set[T]" topology nil)
(disjoint? const-decl "bool" sets nil))
shostak))
(subset_of_Cl 0
(subset_of_Cl-1 nil 3301285013
("" (expand "subset?")
(("" (expand "Cl")
(("" (skosimp*)
(("" (assert)
(("" (expand "adherent_point?")
(("" (expand "nonempty?")
(("" (skosimp*)
(("" (typepred "U!1")
(("" (expand "neighbourhood?")
(("" (expand "interior_point?")
(("" (expand "empty?")
(("" (skosimp)
(("" (typepred "U!2")
(("" (expand "subset?")
((""
(inst - "x!1")
((""
(assert)
((""
(inst - "x!1")
((""
(expand "intersection")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Cl const-decl "set[T]" topology nil)
(member const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(open nonempty-type-eq-decl nil topology nil)
(open? const-decl "bool" topology nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil topology nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(interior_point? const-decl "bool" topology nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(neighbourhood? const-decl "bool" topology nil)
(adherent_point? const-decl "bool" topology nil)
(subset? const-decl "bool" sets nil))
shostak))
(Cl_subset 0
(Cl_subset-1 nil 3301285299
("" (expand "Cl")
(("" (expand "subset?")
(("" (expand "member")
(("" (expand "adherent_point?")
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (skosimp*)
(("" (inst -2 "U!1")
(("" (assert)
(("" (skosimp)
(("" (inst - "x!2")
(("" (inst - "x!2")
(("" (expand "intersection")
((""
(flatten)
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset? const-decl "bool" sets nil)
(adherent_point? const-decl "bool" topology nil)
(empty? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(open nonempty-type-eq-decl nil topology nil)
(open? const-decl "bool" topology 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-type-decl nil topology nil)
(nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(Cl const-decl "set[T]" topology nil))
shostak))
(Cl_idempotent 0
(Cl_idempotent-1 nil 3301287365
("" (skosimp)
(("" (lemma "subset_of_Cl" ("A" "Cl(A!1)"))
(("" (case "subset?(Cl(Cl(A!1)), Cl(A!1))")
(("1"
(lemma "subset_antisymmetric"
("a" "Cl(A!1)" "b" "Cl(Cl(A!1))"))
(("1" (assert) nil nil)) nil)
("2" (hide 2)
(("2" (expand "subset?")
(("2" (expand "Cl")
(("2" (expand "adherent_point?")
(("2" (assert)
(("2" (skosimp*)
(("2" (inst - "U!1")
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (expand "intersection")
(("2" (assert)
(("2"
(expand "neighbourhood?")
(("2"
(expand "interior_point?")
(("2"
(assert)
(("2"
(skosimp*)
(("2"
(inst -2 "U!1")
(("2"
(hide -6)
(("2"
(split -2)
(("1" (propax) nil nil)
("2"
(inst + "U!1")
(("2"
(rewrite
"subset_reflexive")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Cl const-decl "set[T]" topology 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-type-decl nil topology nil)
(subset_of_Cl formula-decl nil topology nil)
(member const-decl "bool" sets nil)
(open nonempty-type-eq-decl nil topology nil)
(open? const-decl "bool" topology nil)
(empty? const-decl "bool" sets nil)
(interior_point? const-decl "bool" topology nil)
(subset_reflexive formula-decl nil sets_lemmas nil)
(neighbourhood? const-decl "bool" topology nil)
(intersection const-decl "set" sets nil)
(nonempty? const-decl "bool" sets nil)
(adherent_point? const-decl "bool" topology nil)
(subset_antisymmetric formula-decl nil sets_lemmas nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset? const-decl "bool" sets nil))
shostak))
(eq_Cl_is_closed 0
(eq_Cl_is_closed-1 nil 3301290171
("" (skosimp)
(("" (lemma "subset_of_Cl" ("A" "A!1"))
(("" (case-replace "subset?(Cl(A!1),A!1) IFF closed?(A!1)")
(("1" (rewrite "subset_antisymmetric" 1 :dir rl)
(("1" (assert) nil nil)) nil)
("2" (hide -1 2)
(("2" (rewrite "open_complement" :dir rl)
(("2" (rewrite "subset_complement" :dir rl)
(("2" (lemma "open_def" ("A" "complement(A!1)"))
(("2" (split 1)
(("1" (flatten 1)
(("1" (assert)
(("1" (skosimp)
(("1" (expand "neighbourhood?")
(("1" (expand "subset?")
(("1" (expand "Cl")
(("1"
(expand "interior_point?")
(("1"
(inst - "x!1")
(("1"
(assert)
(("1"
(expand "complement")
(("1"
(expand "member")
(("1"
(expand "adherent_point?")
(("1"
(skosimp*)
(("1"
(inst + "U!1")
(("1"
(assert)
(("1"
(expand
"neighbourhood?")
(("1"
(expand
"interior_point?")
(("1"
(skosimp*)
(("1"
(assert)
(("1"
(expand
"subset?")
(("1"
(inst-cp
-
"x!1")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(expand
"nonempty?")
(("1"
(expand
"empty?")
(("1"
(expand
"intersection")
(("1"
(inst
-4
"x!2")
(("1"
(assert)
(("1"
(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))
nil))
nil))
nil))
nil))
nil)
("2" (flatten 1)
(("2" (assert)
(("2" (expand "subset?")
(("2" (skosimp*)
(("2" (assert)
(("2" (inst - "x!1")
(("2"
(expand "Cl")
(("2"
(expand "complement")
(("2"
(assert)
(("2"
(expand "adherent_point?")
(("2"
(inst - "{x: T | NOT A!1(x)}")
(("2"
(assert)
(("2"
(expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(expand "intersection")
(("2"
(skosimp*)
(("2"
(assert)
(("2"
(flatten)
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)
((set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil topology nil)
(subset_of_Cl formula-decl nil topology nil)
(subset_complement formula-decl nil sets_lemmas nil)
(neighbourhood? const-decl "bool" topology nil)
(adherent_point? const-decl "bool" topology nil)
(open nonempty-type-eq-decl nil topology nil)
(open? const-decl "bool" topology nil)
(nonempty? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(interior_point? const-decl "bool" topology nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(complement const-decl "set" sets nil)
(open_def formula-decl nil topology nil)
(open_complement formula-decl nil topology nil)
(subset_antisymmetric formula-decl nil sets_lemmas nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(closed? const-decl "bool" topology nil)
(Cl const-decl "set[T]" topology nil)
(subset? const-decl "bool" sets nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil))
shostak))
(Cl_closed 0
(Cl_closed-1 nil 3300509409
("" (skosimp)
(("" (lemma "eq_Cl_is_closed" ("A" "Cl(A!1)"))
(("" (rewrite "Cl_idempotent") (("" (flatten) nil nil)) nil))
nil))
nil)
((Cl const-decl "set[T]" topology 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-type-decl nil topology nil)
(eq_Cl_is_closed formula-decl nil topology nil)
(Cl_idempotent formula-decl nil topology nil))
shostak))
(Cl_subset_closed 0
(Cl_subset_closed-1 nil 3301293173
("" (skosimp)
(("" (typepred "V!1")
(("" (rewrite "eq_Cl_is_closed" -1 :dir rl)
(("" (lemma "Cl_subset" ("A" "A!1" "B" "V!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((closed nonempty-type-eq-decl nil topology nil)
(closed? const-decl "bool" topology nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil topology nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Cl_subset formula-decl nil topology nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(eq_Cl_is_closed formula-decl nil topology nil))
shostak))
(Cl_union 0
(Cl_union-1 nil 3301293398
("" (skosimp)
(("" (lemma "subset_of_Cl" ("A" "A!1"))
(("" (lemma "subset_of_Cl" ("A" "B!1"))
(("" (lemma "Cl_closed" ("A" "A!1"))
(("" (lemma "Cl_closed" ("A" "B!1"))
(("" (lemma "closed_union" ("V1" "Cl(A!1)" "V2" "Cl(B!1)"))
(("1"
(lemma "union_upper_bound"
("a" "A!1" "b" "B!1" "c" "union(Cl(A!1), Cl(B!1))"))
(("1" (split -1)
(("1"
(lemma "Cl_subset_closed"
("A" "union(A!1,B!1)" "V"
"union(Cl(A!1),Cl(B!1))"))
(("1" (assert)
(("1"
(lemma "subset_antisymmetric"
("a" "Cl(union(A!1,B!1))" "b"
"union(Cl(A!1),Cl(B!1))"))
(("1" (assert)
(("1" (hide 2)
(("1" (expand "subset?")
(("1"
(expand "union")
(("1"
(skosimp*)
(("1"
(assert)
(("1"
(inst - "x!1")
(("1"
(inst - "x!1")
(("1"
(split -1)
(("1"
(expand "Cl")
(("1"
(hide-all-but (-1 1))
(("1"
(expand
"adherent_point?")
(("1"
(skosimp)
(("1"
(inst - "U!1")
(("1"
(assert)
(("1"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.94 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.
|
