|
(compact_spaces
(compact_closed_def 0
(compact_closed_def-1 nil 3406967481
("" (skosimp)
(("" (typepred "S")
(("" (rewrite "compact_def")
(("" (inst - "U!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((S formal-const-decl "compact_space" compact_spaces 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 compact_spaces nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Intersection_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(compact_def formula-decl nil topology nil))
shostak)))
¤ Dauer der Verarbeitung: 0.20 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.
|
