| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/exact_real_arith/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 7 kB |
|
Quelle min.prf Sprache: Lisp |
|||||||||
|
(min (cauchy_min_TCC1 0
(cauchy_min_TCC1-1 nil 3251054266 ("" (skosimp*) (("" (typepred "cx!1") (("" (typepred "cy!1") (("" (expand "cauchy_real?") (("" (skosimp*) (("" (inst + "min(x!1,x!2)") (("" (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" "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) ((cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (posnat_expt application-judgement "posnat" exponentiation nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (expt_pos formula-decl nil exponentiation nil) (cauchy_prop const-decl "bool" cauchy nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (posint_exp application-judgement "posint" exponentiation nil)) shostak)) (min_lemma 0 (min_lemma-1 nil 3251053661 ("" (expand "cauchy_min") (("" (expand "cauchy_prop") (("" (skosimp*) (("" (case "cx!1(p!1) (("1" (replace -1) (("1" (inst - "p!1") (("1" (inst - "p!1") (("1" (lemma "expt_pos" ("px" "2" "i" "p!1")) (("1" (lemma "both_sides_times_pos_lt1" ("x" "y!1" "y" "x!1" "pz" "2^p!1")) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace 1) (("2" (lemma "expt_pos" ("px" "2" "i" "p!1")) (("2" (inst - "p!1") (("2" (inst - "p!1") (("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)) nil) ((posint_exp application-judgement "posint" exponentiation nil) (int_min application-judgement "{k: int | k <= i AND k <= j}" real_defs nil) (cauchy_prop const-decl "bool" cauchy nil) (cauchy_real nonempty-type-eq-decl nil cauchy nil) (cauchy_real? const-decl "bool" cauchy nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (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) (min 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) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (expt_pos formula-decl nil exponentiation nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (cauchy_min const-decl "cauchy_real" min nil)) shostak))) ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28