Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/structures/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 1 kB

Quelle const_fun_def.prf Sprache: Lisp

(const_fun_def
(image_const 0
  (image_const-1 nil 3461937620
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((T formal-type-decl nil const_fun_def nil)
    (boolean nonempty-type-decl nil booleans nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (emptyset const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (const_fun const-decl "[S -> T]" const_fun_def nil)
    (image const-decl "set[R]" function_image nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (S formal-type-decl nil const_fun_def nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (member const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   nil))
(inverse_image_const 0
  (inverse_image_const-1 nil 3461937640
   ("" (skosimp)
    (("" (apply-extensionality :hide? t) (("" (grind) nil nil)) nil))
    nil)
   ((S formal-type-decl nil const_fun_def nil)
    (boolean nonempty-type-decl nil booleans nil)
    (emptyset const-decl "set" sets nil)
    (fullset const-decl "set" sets nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (const_fun const-decl "[S -> T]" const_fun_def 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 const_fun_def nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (member const-decl "bool" sets nil))
   nil)))

quality100%

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