Quelle connected_space.prf
Sprache: unbekannt
|
|
(connected_space
(clopen_def 0
(clopen_def-1 nil 3364197290
("" (skosimp)
(("" (expand "clopen?")
(("" (typepred "S")
(("" (expand "connected_space?")
(("" (flatten)
(("" (expand "connected?")
(("" (split 1)
(("1" (flatten)
(("1" (expand "open?")
(("1" (expand "closed?")
(("1" (expand "member")
(("1" (inst - "A!1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (hide -3)
(("2" (split)
(("1" (replace -1)
(("1" (assert)
(("1" (rewrite "open_emptyset")
(("1" (rewrite "closed_emptyset") nil nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (rewrite "closed_fullset")
(("2" (rewrite "open_fullset") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((clopen? const-decl "bool" topology nil)
(connected? const-decl "bool" topology_prelim nil)
(closed_emptyset formula-decl nil topology nil)
(open_emptyset formula-decl nil topology nil)
(closed_fullset formula-decl nil topology nil)
(open_fullset formula-decl nil topology nil)
(closed? const-decl "bool" topology nil)
(set type-eq-decl nil sets nil)
(A!1 skolem-const-decl "set[T]" connected_space nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset_is_clopen name-judgement "clopen" connected_space nil)
(emptyset_is_compact name-judgement "compact" connected_space nil)
(fullset_is_clopen name-judgement "clopen" connected_space nil)
(member const-decl "bool" sets nil)
(open? const-decl "bool" topology 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 connected_space nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(connected_space? const-decl "bool" topology_prelim nil)
(connected_space nonempty-type-eq-decl nil topology_prelim nil)
(S formal-const-decl "connected_space" connected_space nil))
shostak)))
[ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet)
]
|
2026-03-28
|
