Quelle epsilon_lemmas.prf
Sprache: Lisp
(epsilon_lemmasnil 3253549178"" (skosimp)"" (lemma "triangle" )"" (inst -1 "(x1!1 - y1!1) * x2!1" "(x2!1 - y2!1) * y1!1" )"" (auto-rewrite "abs_mult" )"" (do-rewrite)"" (assert )"" case "abs(x2!1 - y2!1) * abs(y1!1) <= e2!1 * abs(y1!1)" )"1" case "abs(x1!1 - y1!1) * abs(x2!1) < e1!1 * (abs(y2!1) + e2!1)" )"1" (assert ) nil nil )"2" (delete -1 -2 2)"2" (rewrite "lt_times_lt_pos1" 1)"2" (lemma "abs_diff" )"2" (inst -1 "x2!1" "y2!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (delete -1 2)"2" (rewrite "le_times_le_pos" 1) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_props nil )nil real_props nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil abs_lems "reals/" )nil abs_lems "reals/" )nil real_types nil )"bool" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil ) (<= const-decl "bool" reals nil )nil booleans nil )nil real_props nil )"(total_order?[real])" nil )"real" reals nil )"(total_order?[real])" nil )"nnreal" nil )"nnreal" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"posreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil ))nil ))nil 3253549178"" (skolem!)"" case "EXISTS (u, v, w : posreal) : and abs(y1!1) * v < e!1/3 and abs(y2!1) * w < e!1/3") "1" (skosimp)"1" (inst 1 "min(u!1, w!1)" "v!1" )"1" case "min(u!1, w!1) * v!1 <= u!1 * v!1 and abs(y2!1) * min(u!1, w!1) <= abs(y2!1) * w!1" )"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (delete -1 -2 -3 2)"2" (split)"1" (rewrite "both_sides_times_pos_le1" )"1" (assert ) nil nil )) nil )"2" (rewrite "le_times_le_pos" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (delete 2)"2" (name "f" "e!1/3" )"2" (replace -1)"2" case "FORALL (x : nonneg_real) : x * (f / (x+1)) < f" )"1" (inst-cp -1 "abs(y1!1)" )"1" (inst -1 "abs(y2!1)" )"1" "abs(y1!1) + 1" "f / (abs(y1!1) + 1)" "f / (abs(y2!1) + 1)" )"1" (split)"1" (rewrite "div_cancel1" )"1" (assert ) nil nil )) nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (delete -1 2)"2" (skolem!)"2" (rewrite "times_div1" )"2" (rewrite "div_mult_pos_lt1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"nnreal" nil )"posreal" nil )"posreal" nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil real_props nil )nil real_props nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"nnreal" nil )"[T, T -> boolean]" equalities nil )"posreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil real_props nil )nil reals nil )nil real_props nil )"nnreal" nil )nil real_props nil ))nil ))nil 3253549178"" (skosimp)"" (rewrite "zero_times3" ) (("" (assert ) nil nil )) nil )) nil )nil real_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil ))nil ))nil 3253549178"" (skosimp)"" (assert )"" (lemma "abs_eq_0" ("x" "x1!1" ))"" (replace 1)"" (ground)"" (auto-rewrite "zero_times3" )"" case "abs(1 / x1!1 - 1 / y1!1) = abs(x1!1 - y1!1) / (abs(y1!1) * abs(x1!1))" )"1" (lemma "lt_div_lt_pos2" )"1" "abs(x1!1 - y1!1)" "abs(y1!1) * (abs(y1!1) - e1!1)" "abs(y1!1) * abs(x1!1)" "e1!1" )"1" (split)"1" (assert )"1" (replace -2) (("1" (propax) nil nil ))nil ))nil )"2" (propax) nil nil )"3" (delete -1 5)"3" (rewrite "both_sides_times_pos_le2" )"3" "abs_diff" ("x" "y1!1" "y" "x1!1" ))"3" (rewrite "abs_diff_commute" -2)"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (delete -1 5)"2" (case "abs(y1!1) * (abs(y1!1) - e1!1) > 0" )"1" (assert ) nil nil )"2" (delete 2)"2" (rewrite "pos_times_gt" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (delete 5 -1)"2" "minus_div1" "abs_div" "abs_mult" )"2" (assert )"2" (rewrite "abs_diff_commute" 1)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )"(total_order?[real])" nil )nil abs_lems "reals/" )"odd_int" integers nil )nil abs_lems "reals/" )"posreal" epsilon_lemmas nil )nil real_types nil )"bool" reals nil )"real" epsilon_lemmas nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"[T, T -> boolean]" equalities nil )nil booleans nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil abs_lems "reals/" )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"nzreal" nil )"real" reals nil ))nil ))nil 3253549178"" (skosimp)"" (lemma "abs_eq_0" ("x" "y1!1" ))"" (assert )"" (case "EXISTS (c : posreal) : c < e!1 / (1 + e!1)" )"1" (skolem!)"1" (inst 3 "abs(y1!1) * c!1" )"1" (split)"1" "both_sides_times_pos_lt2" "pz" "abs(y1!1)" "x" "c!1" "y" "1" ))"1" (assert )"1" case "e!1 / (1 + e!1) < (1 + e!1) / (1 + e!1)" )"1" (rewrite "div_simp" )"1" (assert ) nil nil )) nil )"2" (rewrite "both_sides_div_pos_lt1" ) nil nil ))nil ))nil ))nil )"2" (lemma "both_sides_times_pos_lt2" )"2" (inst -1 "abs(y1!1)" "c!1" "e!1 * (1 - c!1)" )"2" (assert )"2" (delete 2)"2" (rewrite "div_mult_pos_lt2" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "pos_times_gt" ) nil nil ))nil ))nil )"2" (delete 2 3 4)"2" (inst 1 "e!1 / (2 + e!1)" )"2" (rewrite "both_sides_div_pos_lt2" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil abs_lems "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"posreal" nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"[numfield, numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" epsilon_lemmas nil )"posreal" epsilon_lemmas nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil real_props nil )"real" reals nil )nil real_props nil )nil reals nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil real_props nil )"posreal" nil )"nnreal" nil )"(total_order?[real])" nil ))nil ))nil 3253549178"" (skosimp*)"" (rewrite "zero_times3" ) (("" (assert ) nil nil )) nil )) nil )"real" reals nil )nil real_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3253549178"" (skosimp)"" (lemma "abs_eq_0" ("x" "y1!1" ))"" (assert )"" (lemma "inv_epsilon1" ("y1" "y1!1" "e" "e!1 * abs(y1!1)" ))"1" (assert )"1" (skosimp)"1" (inst 3 "e1!1" )"1" (assert )"1" (rewrite "div_mult_pos_lt1" )"1" (delete -2 4)"1" "posreal_mult_closed" "x" "abs(y1!1)" "y" "abs(y1!1) - e1!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "posreal_mult_closed" ) nil nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil abs_lems "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil epsilon_lemmas nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil real_axioms nil )"nzreal" nil )"real" reals nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" nil )"real" reals nil )"(total_order?[real])" nil ))nil ))nil 3461939779"" (skosimp)"" (split)"1" (grind) nil nil )"2" (flatten)"2" (lemma "archimedean" ("px" "x!1-y!1" ))"1" (skosimp)"1" (inst - "1/n!1" ) (("1" (assert ) nil nil )) nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posrat" nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )nil integers nil )"(strict_total_order?[real])" real_props nil )"real" reals nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
