|
(inverse_image_Union
(inverse_image_Union 0
(inverse_image_Union-1 nil 3389901218
("" (skosimp)
(("" (apply-extensionality :hide? t)
(("" (case-replace "inverse_image(f!1, Union(X!1))(x!1)")
(("1" (expand "Union")
(("1" (expand "inverse_image")
(("1" (expand "member")
(("1" (skosimp)
(("1" (typepred "a!1")
(("1" (inst + "inverse_image(f!1,a!1)")
(("1" (expand "inverse_image")
(("1" (assert)
(("1" (expand "member")
(("1" (propax) nil nil)) nil))
nil))
nil)
("2" (inst + "a!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (expand "Union" -1)
(("2" (skosimp)
(("2" (typepred "a!1")
(("2" (skosimp)
(("2" (replace -1)
(("2" (typepred "x!2")
(("2" (expand "inverse_image")
(("2" (expand "member")
(("2" (expand "Union")
(("2" (inst + "x!2") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((S formal-type-decl nil inverse_image_Union nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Union const-decl "set" sets nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(inverse_image const-decl "set[D]" function_image nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-type-decl nil inverse_image_Union nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(member const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(a!1 skolem-const-decl "(X!1)" inverse_image_Union nil)
(f!1 skolem-const-decl "[S -> T]" inverse_image_Union nil)
(X!1 skolem-const-decl "setofsets[T]" inverse_image_Union nil))
shostak)))
¤ Dauer der Verarbeitung: 0.18 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.
|
