| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/lnexp/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 535 kB |
|
Quelle ln_exp_ineq.prf Sprache: Lisp |
|||||||||
|
(ln_exp_ineq
(ln_ineq1_TCC1 0 (ln_ineq1_TCC1-1 nil 3254127856 ("" (grind) nil nil) nil shostak)) (ln_ineq1_TCC2 0 (ln_ineq1_TCC2-1 nil 3254127856 ("" (grind) nil nil) nil shostak)) (ln_ineq1 0 (ln_ineq1-1 nil 3253817629 ("" (skolem + "x") (("" (name "z" "1+x") (("" (name "foo" "z-1") (("" (typepred "x") (("" (replace -4) (("" (replace -4 -3 rl) (("" (replace -3 (1 -1 -2)) (("" (replace -4) (("" (replace -3 (-1 -2 1) rl) (("" (hide -3 -4) (("" (simplify -2) (("" (assert) (("" (lemma "both_sides_plus_gt1" ("z" "1" "x" "z-1" "y" "-1")) (("" (replace -1 -3 rl) (("" (simplify -3) (("" (hide -1) (("" (name "F" "LAMBDA (x:posreal): x - 1 - ln(x)") (("" (name "G" "LAMBDA (x:posreal): ln(x) - (x-1)/x") (("" (case "FORALL (x, y: posreal), (z: real): x <= z AND z <= y IMPLIES z >= 0 AND z > 0") (("1" (case "FORALL (x: posreal): EXISTS (y: posreal): x /= y") (("1" (lemma "ln_derivable") (("1" (flatten -1) (("1" (lemma "const_derivable_fun[posreal]" ("b" "1")) (("1" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "diff_derivable_fun[posreal]") (("1" (inst-cp -1 "I[posreal]" "const_fun(1)") (("1" (inst-cp - "I[posreal] - const_fun(1)" "ln") (("1" (lemma "div_derivable_fun[posreal]" ("f" "I[posreal]-const_fun(1)" "g" "I[posreal]")) (("1" (inst - "ln" "(I[posreal]-const_fun(1))/I[posreal]") (("1" (lemma "deriv_const_fun[posreal]" ("b" "1")) (("1" (lemma "deriv_id_fun[posreal]") (("1" (lemma "deriv_diff_fun[posreal]") (("1" (replace -10) (("1" (replace -9) (("1" (replace -8) (("1" (replace -7) (("1" (replace -4) (("1" (expand "I") (("1" (expand "const_fun") (("1" (expand "-" (-4 -5 -6 -7)) (("1" (expand "/" (-4 -5)) (("1" (inst-cp - "LAMBDA (x: posreal): x" "LAMBDA (x: posreal): 1") (("1" (inst-cp - "LAMBDA (x:posreal): x - 1" "ln") (("1" (lemma "deriv_div_fun[posreal]" ("ff" "LAMBDA (x:posreal): x-1" "gg" "LAMBDA (x:posreal): x")) (("1" (inst - "ln" "LAMBDA (x:posreal): (x-1)/x") (("1" (expand "-" (-1 -2 -3 -4)) (("1" (expand "/") (("1" (expand "*") (("1" (replace -14) (("1" (replace -6) (("1" (replace -5) (("1" (simplify) (("1" (replace -4) (("1" (simplify -1) (("1" (replace -1) (("1" (simplify -2) (("1" (simplify -3) (("1" (replace -18) (("1" (replace -17) (("1" (hide-all-but (-2 -3 -8 -9 -15 -16 -17 -18 -19 -20 1)) (("1" (assert) (("1" (lemma "minimum_derivative[posreal]") (("1" (inst - "F" "1" "z") (("1" (lemma "minimum_derivative[posreal]") (("1" (inst - "G" "1" "z") (("1" (replace -3) (("1" (replace -4) (("1" (simplify -1) (("1" (simplify -2) (("1" (replace -9 -1 rl) (("1" (replace -10 -2 rl) (("1" (simplify -1) (("1" (simplify -2) (("1" (rewrite "ln_1") (("1" (simplify -2) (("1" (split -1) (("1" (split -2) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (rewrite "div_cancel1") (("2" (lemma "trich_lt" ("x" "y!1" "y" "1")) (("2" (split -1) (("1" (lemma "negreal_times_negreal_is_posreal" ("nx" "y!1-1" "ny" "y!1-1")) (("1" (lemma "both_sides_div_pos_gt1" ("x" "(y!1-1)*(y!1-1)" "y" "0" "pz" "y!1")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (propax) nil nil) ("3" (lemma "posreal_times_posreal_is_posreal" ("px" "y!1-1" "py" "y!1-1")) (("1" (lemma "both_sides_div_pos_gt1" ("x" "(y!1-1)*(y!1-1)" "y" "0" "pz" "y!1")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (rewrite "div_cancel1") (("2" (lemma "div_times" ("x" "y!1" "n0x" "1" "y" "1" "n0y" "y!1*y!1")) (("2" (replace -1 2) (("2" (simplify 2) (("2" (simplify 2) (("2" (lemma "div_cancel1" ("x" "1/y!1" "n0z" "y!1")) (("2" (rewrite "div_div2" -1) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "trich_lt" ("x" "y!1" "y" "1")) (("2" (split -1) (("1" (lemma "negreal_times_negreal_is_posreal" ("nx" "y!1-1" "ny" "y!1-1")) (("1" (lemma "both_sides_div_pos_gt1" ("pz" "y!1*y!1" "x" "(y!1-1)*(y!1-1)" "y" "0")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (propax) nil nil) ("3" (lemma "posreal_times_posreal_is_posreal" ("px" "y!1-1" "py" "y!1-1")) (("1" (lemma "both_sides_div_pos_gt1" ("pz" "y!1*y!1" "x" "(y!1-1)*(y!1-1)" "y" "0")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.29Bemerkung: (vorverarbeitet) ¤*Bot Zugriff |
|
2026-03-28