Quelle composition_borel.prf Sprache: Lisp

(composition_borel
(composition_borel 0
  (composition_borel-1 nil 3384890801
   ("" (skosimp)
    (("" (expand "o")
      (("" (expand "borel_function?")
        (("" (skosimp)
          (("" (inst - "B!1")
            (("" (inst - "inverse_image(f!1,B!1)")
              (("" (expand "inverse_image")
                (("" (expand "member") (("" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (B!1 skolem-const-decl "borel[T3, U]" composition_borel nil)
    (f!1 skolem-const-decl "[T2 -> T3]" composition_borel nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (set type-eq-decl nil sets nil)
    (T formal-const-decl "topology[T2]" composition_borel nil)
    (T2 formal-type-decl nil composition_borel nil)
    (member const-decl "bool" sets nil)
    (borel nonempty-type-eq-decl nil borel nil)
    (borel? const-decl "sigma_algebra" borel nil)
    (U formal-const-decl "topology[T3]" composition_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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil composition_borel nil)
    (borel_function? const-decl "bool" borel_functions nil))
   shostak))
(composition_is_borel 0
  (composition_is_borel-1 nil 3384890745
   ("" (skosimp)
    (("" (lemma "composition_borel" ("g" "G!1" "f" "F!1"))
      (("" (assert) nil nil)) nil))
    nil)
   ((S formal-const-decl "topology[T1]" composition_borel nil)
    (T1 formal-type-decl nil composition_borel nil)
    (borel_function type-eq-decl nil borel_functions nil)
    (borel_function? const-decl "bool" borel_functions nil)
    (U formal-const-decl "topology[T3]" composition_borel nil)
    (T formal-const-decl "topology[T2]" composition_borel nil)
    (topology nonempty-type-eq-decl nil topology_prelim "topology/")
    (topology? const-decl "bool" topology_prelim "topology/")
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil composition_borel nil)
    (T2 formal-type-decl nil composition_borel nil)
    (composition_borel formula-decl nil composition_borel nil))
   nil)))

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.