| products/sources/formale Sprachen/PVS/exact_real_arith/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: max.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(max (cauchy_max_TCC1 0
(cauchy_max_TCC1-1 nil 3251054936 ("" (expand "cauchy_real?") (("" (skosimp*) (("" (typepred "cx!1") (("" (typepred "cy!1") (("" (expand "cauchy_real?") (("" (skosimp*) (("" (inst + "max(x!2,x!1)") (("" (expand "cauchy_prop") (("" (skosimp*) (("" (lemma "expt_pos" ("px" "2" "i" "p!1")) (("" (inst - "p!1") (("" (inst - "p!1") (("" (case "cx!1(p!1) < cy!1(p!1)") (("1" (lemma "both_sides_times_pos_lt1" ("x" "x!1" "y" "x!2" "pz" "2^p!1")) (("1" (grind) nil nil)) nil) ("2" (lemma "both_sides_times_pos_lt1" ("x" "x!2" "y" "x!1" "pz" "2^p!1")) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_exp application-judgement "posint" exponentiation nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (cauchy_prop const-decl "bool" cauchy nil) (expt_pos formula-decl nil exponentiation nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posnat_expt application-judgement "posnat" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs 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) (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil)) shostak)) (max_lemma 0 (max_lemma-1 nil 3251054748 ("" (expand "cauchy_max") (("" (expand "cauchy_prop") (("" (skosimp*) (("" (inst - "p!1") (("" (inst - "p!1") (("" (lemma "expt_pos" ("px" "2" "i" "p!1")) (("" (case "cx!1(p!1) < cy!1(p!1)") (("1" (lemma "both_sides_times_pos_lt1" ("x" "y!1" "y" "x!1" "pz" "2^p!1")) (("1" (grind) nil nil)) nil) ("2" (lemma "both_sides_times_pos_lt1" ("x" "x!1" "y" "y!1" "pz" "2^p!1")) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posint_exp application-judgement "posint" exponentiation nil) (int_max application-judgement "{k: int | i <= k AND j <= k}" real_defs nil) (rat_max application-judgement "{s: rat | s >= q AND s >= r}" real_defs nil) (cauchy_prop const-decl "bool" cauchy 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) (expt_pos formula-decl nil exponentiation nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (real_minus_real_is_real application-judgement "real" reals nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posnat_expt application-judgement "posnat" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (< const-decl "bool" reals nil) (cauchy_max const-decl "cauchy_real" max nil)) shostak))) ¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
