|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
yts805.cob
Sprache: Isabelle
Original von: PVS©
|
|
|
(function_image_nonempty
(nonempty_image 0
(nonempty_image-1 nil 3368875322
("" (skosimp*)
(("" (typepred "S!1")
(("" (rewrite "nonempty_exists")
(("" (rewrite "nonempty_exists")
(("" (skosimp*)
(("" (inst + "f!1(x!1)")
(("" (expand "image") (("" (inst + "x!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(D formal-type-decl nil function_image_nonempty nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(image const-decl "set[R]" function_image nil)
(R formal-type-decl nil function_image_nonempty nil)
(x!1 skolem-const-decl "(S!1)" function_image_nonempty nil)
(S!1 skolem-const-decl "(nonempty?[D])" function_image_nonempty
nil)
(f!1 skolem-const-decl "[D -> R]" function_image_nonempty nil)
(nonempty_exists formula-decl nil sets_lemmas nil))
nil))
(nonempty_finite_image 0
(nonempty_finite_image-2 nil 3368875625
("" (skosimp*)
(("" (use "nonempty_image")
(("" (expand "nonempty?") (("" (propax) nil nil)) nil)) nil))
nil)
((nonempty_image judgement-tcc nil function_image_nonempty nil)
(R formal-type-decl nil function_image_nonempty nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(D formal-type-decl nil function_image_nonempty nil)
(nonempty_image application-judgement "(nonempty?[R])"
function_image_nonempty nil)
(finite_image application-judgement "finite_set[R]"
function_image_aux nil))
nil)
(nonempty_finite_image-1 nil 3368875322 ("" (judgement-tcc) nil nil)
nil nil)))
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
|
|
|
|
|
