| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/vectors/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle sigma_fseq_3D.prf Sprache: Lisp |
|||||||||
|
(sigma_fseq_3D
(sigma_TCC1 0 (sigma_TCC1-1 nil 3563272396 ("" (subtype-tcc) nil nil) nil nil)) (sigma_TCC2 0 (sigma_TCC2-1 nil 3563272396 ("" (subtype-tcc) nil nil) ((int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (sigma_TCC3 0 (sigma_TCC3-1 nil 3563272396 ("" (assuming-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil))) ¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28