|
(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
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.26Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
