| products/Sources/formale Sprachen/PVS/topology/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: SMLOriginal von: PVS© |
|
||||||
|
(lindelof
(lindelof 0 (lindelof-1 nil 3397754551 ("" (skosimp) (("" (typepred "S") (("" (expand "second_countable?") (("" (flatten) (("" (expand "has_countable_basis?") (("" (skosimp) (("" (expand "open_cover?") (("" (flatten) (("" (expand "cover?") (("" (lemma "synthetic_base_is_base" ("B" "B!1")) (("" (replace -5) (("" (expand "base?") (("" (flatten) (("" (expand "subcover?") (("" (expand "cover?" 1 1) (("" (assert) (("" (hide -3 -6 -5) (("" (name "UU" "{x:set[T] | U!1(x) & nonempty?(x)}") (("" (case "Union(U!1)=Union(UU)") (("1" (case "subset?(UU,S)") (("1" (case "EXISTS V: is_countable(V) AND cover?(V, fullset[T]) AND subset?(V, UU)") (("1" (skosimp) (("1" (inst + "V!1") (("1" (assert) (("1" (hide-all-but (-3 1)) (("1" (expand "UU") (("1" (expand "subset?") (("1" (skosimp) (("1" (expand "member") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (replace -2) (("2" (hide -2 -3 -7) (("2" (name "BB" "{x:set[T] | B!1(x) & exists (y:(UU)): subset?(x,y)}") (("2" (case "is_countable(BB)") (("1" (hide -6) (("1" (case "forall (x:(BB)): exists (y:(UU)): subset?(x,y)") (("1" (hide -3) (("1" (name "F" "lambda (x:(BB)): choose[set[T]]({y:set[T] | UU(y) & subset?(x, y)})") (("1" (case "forall (x: (BB)): UU(F(x)) & subset?(x,F(x))") (("1" (hide -2) (("1" (hide -2) (("1" (name "VV" "image[(BB),set[T]](F,BB)") (("1" (lemma "countable_image[(BB),set[T]]" ("S" "BB" "f" "F")) (("1" (expand "image" -1) (("1" (replace -2) (("1" (split -1) (("1" (inst + "VV") (("1" (split 1) (("1" (propax) nil nil) ("2" (expand "fullset") (("2" (expand "cover?") (("2" (expand "subset?" (-8 1)) (("2" (expand "member") (("2" (skosimp) (("2" (inst -8 "x!1") (("2" (expand "Union" (-8 1)) (("2" (skosimp) (("2" (typepred "a!1") (("2" (expand "subset?" -6) (("2" (inst -6 "a!1") (("2" (expand "member") (("2" (inst -8 "a!1") (("2" (skosimp) (("2" (copy -10) (("2" (replace -10 -1 rl) (("2" (expand "Union" -1) (("2" (skosimp) (("2" (typepred "a!2") (("2" (expand "subset?" -10) (("2" (inst -10 "a!2") (("2" (expand "member") (("2" (inst -6 "a!2") (("1" (flatten) (("1" (expand "subset?" -7) (("1" (inst -7 "x!1") (("1" (assert) (("1" (inst + "F(a!2)") (("1" (expand "VV") (("1" (expand "restrict") (("1" (expand "image") (("1" (inst + "a!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "BB" 1) (("2" (assert) (("2" (inst + "a!1") (("2" (replace -10 1 rl) (("2" (expand "subset?") (("2" (expand "member") (("2" (expand "Union") (("2" (skosimp) (("2" (inst + "a!2") 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)) nil)) nil)) nil)) nil) ("3" (expand "subset?" 1) (("3" (skolem!) (("3" (expand "member") (("3" (flatten) (("3" (expand "VV" -1) (("3" (expand "restrict" -1) (("3" (expand "image" -1) (("3" (skolem!) (("3" (typepred "x!2") (("3" (inst -5 "x!2") (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (expand "restrict") (("2" (expand "is_countable") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (skosimp) (("2" (expand "F") (("2" (typepred "choose[set[T]]({y: set[T] | UU(y) & subset?(x!1, y)})") (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "nonempty?") (("2" (inst - "x!1") (("2" (skosimp) (("2" (expand "empty?") (("2" (inst - "y!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp) (("2" (inst - "x!1") (("2" (skosimp) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (inst - "y!1") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "x!1") (("2" (expand "BB") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-5 1)) (("2" (expand "BB") (("2" (lemma "countable_subset[set[T]]" ("S" "{x: set[T] | B!1(x) & (EXISTS (y: (UU)): subset?(x, y))}" "Count" "B!1")) (("2" (split -1) (("1" (propax) nil nil) ("2" (hide -1 2) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -6)) (("2" (expand "UU") (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp) (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (expand "UU") (("2" (expand "Union") (("2" (case-replace "EXISTS (a: (U!1)): a(x!1)") (("1" (skosimp) (("1" (inst + "a!1") (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (inst - "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1 2) (("2" (assert) (("2" (skosimp) (("2" (typepred "a!1") (("2" (inst + "a!1") 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) ((S formal-const-decl "second_countable" lindelof nil) (second_countable type-eq-decl nil topology_def nil) (second_countable? const-decl "bool" topology_def nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil lindelof nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (synthetic_base_is_base formula-decl nil basis nil) (synthetic_base? const-decl "bool" basis nil) (synthetic_base type-eq-decl nil basis nil) (base? const-decl "bool" basis nil) (subcover? const-decl "bool" topology_prelim nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (fullset_is_clopen name-judgement "clopen" lindelof nil) (synthetic_basis_is_topology application-judgement "topology[T]" lindelof nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonempty? const-decl "bool" sets nil) (U!1 skolem-const-decl "setofsets[T]" lindelof nil) (a!1 skolem-const-decl "(U!1)" lindelof nil) (subset? const-decl "bool" sets nil) (choose const-decl "(p)" sets nil) (empty? const-decl "bool" sets nil) (image const-decl "set[R]" function_image nil) (restrict const-decl "R" restrict nil) (image const-decl "set[R]" function_image nil) (VV skolem-const-decl "set[set[T]]" lindelof nil) (F skolem-const-decl "[x: (BB) -> ({y: set[T] | UU(y) & subset?(x, y)})]" lindelof nil) (TRUE const-decl "bool" booleans nil) (a!2 skolem-const-decl "(V!1)" lindelof nil) (V!1 skolem-const-decl "setofsets[T]" lindelof nil) (BB skolem-const-decl "[set[T] -> boolean]" lindelof nil) (a!1 skolem-const-decl "(UU)" lindelof nil) (countable_image formula-decl nil countable_image "sets_aux/") (countable_set nonempty-type-eq-decl nil countability "sets_aux/") (countable_subset formula-decl nil countability "sets_aux/") (UU skolem-const-decl "[set[T] -> boolean]" lindelof nil) (member const-decl "bool" sets nil) (fullset const-decl "set" sets nil) (is_countable const-decl "bool" countability "sets_aux/") (Union const-decl "set" sets nil) (cover? const-decl "bool" topology_prelim nil) (open_cover? const-decl "bool" topology_prelim nil) (has_countable_basis? const-decl "bool" topology_def nil)) shostak))) ¤ Dauer der Verarbeitung: 0.117 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.Bot Zugriff |
