|
(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)))
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
