|
|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
ln_exp_ineq.prf
Sprache: Lisp
Original von: PVS©
|
|
|
(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
--> --------------------
¤ 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.
|
|
|
|
|
|
