Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: function_image_extra.prf Sprache: Lisp

Original von: PVS^©

(function_image_extra
(image_singleton 0
  (image_singleton-1 nil 3318609248 ("" (grind-with-ext) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (R formal-type-decl nil function_image_extra nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (finite_image application-judgement "finite_set[R]"
     function_image_aux nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (singleton? const-decl "bool" sets nil)
    (image const-decl "set[R]" function_image nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (D formal-type-decl nil function_image_extra nil)
    (singleton const-decl "(singleton?)" sets nil))
   shostak))
(image_add 0
  (image_add-1 nil 3318609300
   ("" (skolem!)
    (("" (rewrite "add_as_union")
      (("" (rewrite "add_as_union")
        (("" (rewrite "image_union")
          (("" (rewrite "image_singleton") nil nil)) nil))
        nil))
      nil))
    nil)
   ((add_as_union formula-decl nil sets_lemmas nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (D formal-type-decl nil function_image_extra nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (nonempty_union2 application-judgement "(nonempty?)" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (image_union formula-decl nil function_image nil)
    (finite_image application-judgement "finite_set[R]"
     function_image_aux nil)
    (image_singleton formula-decl nil function_image_extra nil)
    (R formal-type-decl nil function_image_extra nil)
    (image const-decl "set[R]" function_image nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.16 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.