| products/Sources/formale Sprachen/PVS/exact_real_arith/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: hyperbolic.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(div
(div_lemma 0 (div_lemma-1 nil 3251044650 ("" (skosimp*) (("" (lemma "inv_lemma" ("nzx" "nzy!1" "nzcx" "nzcy!1")) (("" (assert) (("" (lemma "mul_lemma" ("x" "x!1" "cx" "cx!1" "y" "1/nzy!1" "cy" "cauchy_inv(nzcy!1)")) (("" (assert) (("" (expand "cauchy_div") (("" (name-replace "CZ" "cauchy_mul(cx!1, cauchy_inv(nzcy!1))") (("" (rewrite "div_def" -1) (("" (rewrite "div_def" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonzero_real nonempty-type-eq-decl nil reals nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal nil) (cauchy_nzreal nonempty-type-eq-decl nil cauchy nil) (cauchy_nzreal? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (inv_lemma formula-decl nil inv nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (cauchy_inv const-decl "cauchy_nzreal" inv nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (mul_lemma formula-decl nil mul nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (cauchy_div const-decl "cauchy_real" div nil) (div_def formula-decl nil number_fields nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (cauchy_mul const-decl "cauchy_real" mul nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) shostak))) ¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
