| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/analysis/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quelle Maybe.prf Sprache: Lisp |
|||||||||
|
(Maybe
(Maybe_none 0 (Maybe_none-1 nil 3561161978 ("" (grind) nil nil) nil shostak)) (Maybe_some 0 (Maybe_some-1 nil 3561161985 ("" (induct-and-simplify "a") nil nil) ((Maybe type-decl nil Maybe nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (some? adt-recognizer-decl "[Maybe -> boolean]" Maybe nil) (T formal-type-decl nil Maybe nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (val adt-accessor-decl "[(some?) -> T]" Maybe nil) (Some adt-constructor-decl "[T -> (some?)]" Maybe nil) (Maybe_induction formula-decl nil Maybe nil)) shostak)) (Maybe_or 0 (Maybe_or-1 nil 3561162049 ("" (grind) nil nil) nil shostak)) (Maybe_either_TCC1 0 (Maybe_either_TCC1-1 nil 3561067427 ("" (subtype-tcc) nil nil) nil nil)) (Maybe_either 0 (Maybe_either-1 nil 3561162065 ("" (induct-and-simplify "a") nil nil) ((some? adt-recognizer-decl "[Maybe -> boolean]" Maybe nil) (T formal-type-decl nil Maybe nil) (None adt-constructor-decl "(none?)" Maybe nil) (none? adt-recognizer-decl "[Maybe -> boolean]" Maybe nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (Maybe type-decl nil Maybe nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (val adt-accessor-decl "[(some?) -> T]" Maybe nil) (Some adt-constructor-decl "[T -> (some?)]" Maybe nil) (Maybe_induction formula-decl nil Maybe nil)) shostak))) ¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28