| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/numbers/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 165 kB |
|
Quelle sub.prf Sprache: Lisp |
|||||||||
|
(sub
(sub_lemma 0 (sub_lemma-1 nil 3251041975 ("" (skosimp*) (("" (expand "cauchy_sub") (("" (lemma "neg_lemma" ("x" "y!1" "cx" "cy!1")) (("" (lemma "add_lemma" ("x" "x!1" "y" "-y!1" "cx" "cx!1" "cy" "cauchy_neg(cy!1)")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((cauchy_sub const-decl "cauchy_real" sub nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (cauchy_neg const-decl "cauchy_real" neg nil) (add_lemma formula-decl nil add nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (neg_lemma formula-decl nil neg nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans 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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (cauchy_real? const-decl "bool" cauchy nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil)) shostak))) ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28