Quelle  identity_borel.prf   Sprache: Lisp

(identity_borel
 (id_borel 0
  (id_borel-1 nil 3384890445
   ("" (expand "I")
    (("" (expand "borel_function?")
      (("" (skosimp)
        (("" (typepred "B!1")
          (("" (expand "inverse_image")
            (("" (expand "member")
              ((""
                (lemma "extensionality_postulate"
                 ("f" "B!1" "g" "{x_1: T | B!1(x_1)}"))
                (("" (flatten)
                  (("" (split -1)
                    (("1" (assert) nil nil) ("2" (skosimp) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((borel_function? const-decl "bool" borel_functions nil)
    (borel nonempty-type-eq-decl nil borel nil)
    (borel? const-decl "sigma_algebra" borel nil)
    (S formal-const-decl "topology" identity_borel nil)
    (topology nonempty-type-eq-decl nil topology_prelim "topology/")
    (topology? const-decl "bool" topology_prelim "topology/")
    (sigma_algebra nonempty-type-eq-decl nil subset_algebra_def nil)
    (sigma_algebra? const-decl "bool" subset_algebra_def nil)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (T formal-type-decl nil identity_borel nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (member const-decl "bool" sets nil)
    (extensionality_postulate formula-decl nil functions nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (I const-decl "(bijective?[T, T])" identity nil))
   shostak))
 (I_is_borel 0
  (I_is_borel-1 nil 3384890413 ("" (rewrite "id_borel") nil nil)
   ((id_borel formula-decl nil identity_borel nil)) nil)))