Quelle  hausdorff_borel.prf   Sprache: Lisp

(hausdorff_borel
 (singleton_is_borel 0
  (singleton_is_borel-1 nil 3384849802
   ("" (skosimp)
    (("" (assert)
      (("" (lemma "closed_is_borel" ("Y" "singleton(x!1)"))
        (("" (propax) nil nil)) nil))
      nil))
    nil)
   ((singleton_is_compact application-judgement "compact[T, S]"
     hausdorff_borel nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" countable_props "sets_aux/")
    (closed_is_borel formula-decl nil borel nil)
    (set type-eq-decl nil sets nil)
    (closed? const-decl "bool" topology "topology/")
    (closed nonempty-type-eq-decl nil topology "topology/")
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (T formal-type-decl nil hausdorff_borel 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)
    (hausdorff_space? const-decl "bool" topology_prelim "topology/")
    (hausdorff nonempty-type-eq-decl nil topology_prelim "topology/")
    (S formal-const-decl "hausdorff" hausdorff_borel nil))
   shostak)))