|
(ln_exp_ineq
(noa_posreal 0
(noa_posreal-1 nil 3477843693
("" (expand "not_one_element?")
(("" (skosimp*)
(("" (inst + "x!1 + 1") (("" (assert) nil nil)) nil)) nil))
nil)
((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(>= 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)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
shostak))
(conn_posreal 0
(conn_posreal-1 nil 3477843707
("" (expand "connected?")
(("" (skosimp*) (("" (assert) nil nil)) nil)) nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(connected? const-decl "bool" deriv_domain_def "analysis/"))
shostak))
(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"
(expand
"I")
(("1"
(expand
"const_fun")
(("1"
(lemma
"deriv_id_fun[posreal]")
(("1"
(lemma
"deriv_diff_fun[posreal]")
(("1"
(replace
-10)
(("1"
(replace
-8)
(("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)
("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.31 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
