Quelle function_image_nonempty.prf Sprache: Lisp

(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)))

quality100%

¤ Dauer der Verarbeitung: 0.16 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.