|
(young
(youngs_aux_TCC1 0
(youngs_aux_TCC1-1 nil 3432615617 ("" (subtype-tcc) nil nil) nil
nil))
(youngs_aux 0
(youngs_aux-1 nil 3432615617
("" (skolem + ("c!1" "_"))
(("" (name "F" "lambda r: (1 - c!1) + c!1 * r - r ^ c!1")
(("" (case "FORALL (p: {r | r > 1}): F(p)>0")
(("1" (skosimp)
(("1" (inst - "p!1")
(("1" (expand "F") (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (hide 2)
(("2" (case "F(1) = 0")
(("1" (lemma "real_expt_derivable" ("x" "c!1"))
(("1" (flatten)
(("1"
(lemma "deriv_scal_fun[posreal]"
("b" "c!1" "ff" "I[posreal]"))
(("1" (lemma "deriv_id_fun[posreal]")
(("1"
(lemma "deriv_const_fun[posreal]" ("b" "1-c!1"))
(("1"
(lemma "deriv_sum_fun[posreal]"
("ff1" "const_fun[posreal](1 - c!1)" "ff2"
"c!1 * I[posreal]"))
(("1" (replace -4)
(("1" (expand "I")
(("1" (expand "const_fun")
(("1"
(expand "*")
(("1"
(expand "+")
(("1"
(lemma
"deriv_diff_fun[posreal]"
("ff1"
"LAMBDA (x_1: posreal): 1 - c!1 + c!1 * x_1"
"ff2"
"LAMBDA (y:posreal): y ^ c!1"))
(("1"
(replace -7)
(("1"
(replace -2)
(("1"
(expand "-")
(("1"
(case
"derivable?[posreal](F)")
(("1"
(case
"deriv[posreal](F)=(LAMBDA (x: posreal): c!1 - c!1 * x ^ (c!1 - 1))")
(("1"
(hide-all-but
(-1 -2 -10 1))
(("1"
(lemma
"minimum_derivative[posreal]"
("g" "F" "x" "1"))
(("1"
(replace -4)
(("1"
(skosimp)
(("1"
(typepred
"p!1")
(("1"
(inst
-
"p!1")
(("1"
(replace
-5
-4)
(("1"
(simplify
-4)
(("1"
(rewrite
"real_expt_1a")
(("1"
(assert)
(("1"
(hide
2
-4
-5
-6
-1
-2)
(("1"
(skosimp)
(("1"
(assert)
(("1"
(typepred
"c!1")
(("1"
(typepred
"y!1")
(("1"
(case-replace
"y!1 ^ (c!1 - 1) * c!1 - y!1 ^ (c!1 - 1) * c!1 * y!1 - c!1 + y!1 * c!1= (y!1 ^ (c!1 - 1)-1)*(1-y!1)*c!1")
(("1"
(hide
-1)
(("1"
(case
"y!1>1")
(("1"
(lemma
"real_expt_lt1"
("x"
"y!1"
"a"
"c!1-1"))
(("1"
(flatten
-1)
(("1"
(hide
-1)
(("1"
(split
-1)
(("1"
(hide
1)
(("1"
(lemma
"negreal_times_negreal_is_posreal"
("nx"
"y!1 ^ (c!1 - 1) - 1"
"ny"
"1-y!1"))
(("1"
(lemma
"posreal_times_posreal_is_posreal"
("px"
"(y!1 ^ (c!1 - 1) - 1) * (1 - y!1)"
"py"
"c!1"))
(("1"
(propax)
nil
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(assert)
nil
nil)
("3"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(case
"y!1<1")
(("1"
(hide
1
2)
(("1"
(lemma
"real_expt_gt1"
("x"
"y!1"
"a"
"c!1-1"))
(("1"
(lemma
"posreal_times_posreal_is_posreal"
("px"
"y!1 ^ (c!1 - 1) - 1"
"py"
"1-y!1"))
(("1"
(lemma
"posreal_times_posreal_is_posreal"
("px"
"(y!1 ^ (c!1 - 1) - 1) * (1 - y!1)"
"py"
"c!1"))
(("1"
(propax)
nil
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(assert)
nil
nil)
("3"
(assert)
(("3"
(hide
2)
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case-replace
"(LAMBDA (x: posreal): 1 - x ^ c!1 - c!1 + c!1 * x)=F")
(("1"
(apply-extensionality
1
:hide?
t)
(("1"
(replace -3)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(expand "F")
(("2"
(propax)
nil
nil))
nil))
nil)
("3" (propax) nil nil))
nil)
("2"
(case-replace
"F=(LAMBDA (x: posreal): 1 - x ^ c!1 - c!1 + c!1 * x)")
(("1"
(hide 2)
(("1"
(lemma
"derivable_diff[posreal]"
("ff1"
"lambda (x:posreal): 1-c!1+c!1*x"
"ff2"
"(LAMBDA (y:posreal): y ^ c!1)"))
(("1"
(expand "-")
(("1"
(propax)
nil
nil))
nil))
nil))
nil)
("2"
(expand "F")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3"
(assert)
(("3"
(lemma
"derivable_sum[posreal]"
("ff1"
"const_fun[posreal](1-c!1)"
"ff2"
"c!1*I[posreal]"))
(("3"
(expand "*")
(("3"
(expand "+")
(("3"
(expand "const_fun")
(("3"
(expand "I")
(("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2 -1)
(("2" (expand "F")
(("2" (rewrite "real_expt_1a") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "nnreal" real_expt "power/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nnreal type-eq-decl nil real_types nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(< const-decl "bool" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(real_minus_real_is_real application-judgement "real" reals nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_expt_derivable formula-decl nil ln_exp_def "power/")
(id_fun_continuous name-judgement "continuous_fun[T]" integral
"analysis/")
(id_fun_continuous name-judgement "continuous_fun[T]"
integral_split_scaf "analysis/")
(id_fun_continuous name-judgement "continuous_fun[T]" integral_step
"analysis/")
(id_fun_continuous name-judgement "continuous_fun[T]" unif_cont_fun
"analysis/")
(id_fun_continuous name-judgement "continuous_fun"
continuous_functions "analysis/")
(id_fun_continuous name-judgement "continuous_fun[T]"
indefinite_integral "analysis/")
(derivable_id name-judgement "deriv_fun" derivatives "analysis/")
(id_fun_continuous name-judgement "continuous_fun[T2]"
lim_of_composition "analysis/")
(deriv_scal_fun formula-decl nil derivatives "analysis/")
(derivable? const-decl "bool" derivatives "analysis/")
(deriv_fun type-eq-decl nil derivatives "analysis/")
(bijective? const-decl "bool" functions nil)
(I const-decl "(bijective?[T, T])" identity nil)
(deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
(not_one_element? const-decl "bool" deriv_domain_def "analysis/")
(deriv_const_fun formula-decl nil derivatives "analysis/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(derivable_sum judgement-tcc nil derivatives "analysis/")
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(derivable_diff judgement-tcc nil derivatives "analysis/")
(deriv const-decl "[T -> real]" derivatives "analysis/")
(minimum_derivative formula-decl nil derivative_props "analysis/")
(connected? const-decl "bool" deriv_domain_def "analysis/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(negreal_times_negreal_is_posreal judgement-tcc nil real_types nil)
(<= const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(posreal_times_posreal_is_posreal judgement-tcc nil real_types nil)
(real_expt_lt1 formula-decl nil real_expt "power/")
(real_expt_gt1 formula-decl nil real_expt "power/")
(real_expt_1a formula-decl nil real_expt "power/")
(NOT const-decl "[bool -> bool]" booleans nil)
(deriv_domain_posreal formula-decl nil deriv_domain "analysis/")
(not_one_element_posreal formula-decl nil deriv_domain "analysis/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(deriv_diff_fun formula-decl nil derivatives "analysis/")
(* const-decl "[T -> real]" real_fun_ops "reals/")
(const_fun const-decl "[T -> real]" real_fun_ops "reals/")
(deriv_sum_fun formula-decl nil derivatives "analysis/")
(derivable_scal application-judgement "deriv_fun" derivatives
"analysis/")
(constant_seq1 application-judgement "(convergent?)"
convergence_ops "analysis/")
(derivable_const application-judgement "deriv_fun" derivatives
"analysis/")
(deriv_id_fun formula-decl nil derivatives "analysis/")
(F skolem-const-decl "[posreal -> real]" young nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil))
shostak))
(youngs_inequality_TCC1 0
(youngs_inequality_TCC1-1 nil 3432615617 ("" (subtype-tcc) nil nil)
((posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil))
nil))
(youngs_inequality_TCC2 0
(youngs_inequality_TCC2-1 nil 3432615617 ("" (subtype-tcc) nil nil)
((posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil))
nil))
(youngs_inequality 0
(youngs_inequality-1 nil 3432622712
("" (skosimp)
(("" (case-replace "a!1=0")
(("1" (rewrite "real_expt_0x")
(("1" (case-replace "b!1=0")
(("1" (rewrite "real_expt_0x") (("1" (assert) nil nil)) nil)
("2" (lemma "real_expt_pos" ("px" "b!1" "a" "q!1"))
(("1"
(lemma "posreal_div_posreal_is_posreal"
("px" "b!1 ^ q!1" "py" "q!1"))
(("1" (assert) nil nil) ("2" (propax) nil nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil)
("2" (case-replace "b!1=0")
(("1" (rewrite "real_expt_0x")
(("1" (lemma "real_expt_pos" ("px" "a!1" "a" "q!1"))
(("1"
(lemma "posreal_div_posreal_is_posreal"
("px" "a!1 ^ p!1" "py" "p!1"))
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
("2" (assert) nil nil))
nil))
nil)
("2" (case "a!1>0&b!1>0")
(("1" (flatten)
(("1" (hide 1 2)
(("1"
(name "F" "lambda (x:posreal): x^p!1/p!1+x^(-q!1)/q!1")
(("1" (lemma "real_expt_derivable" ("x" "p!1"))
(("1" (lemma "real_expt_derivable" ("x" "-q!1"))
(("1" (flatten)
(("1"
(lemma "deriv_scal_fun[posreal]"
("b" "1/p!1" "ff"
"LAMBDA (y:posreal): y ^ p!1"))
(("1"
(lemma "deriv_scal_fun[posreal]"
("b" "1/q!1" "ff"
"LAMBDA (y:posreal): y ^ -q!1"))
(("1"
(case "derivable?[posreal](F)&deriv[posreal](F) = lambda (x:posreal): x^(p!1-1)-x^(-q!1-1)")
(("1" (flatten)
(("1"
(case "deriv[posreal](F)(1)=0")
(("1"
(case "forall (t:posreal): 1<=F(t)")
(("1"
(inst - "a!1^(1/q!1)*b!1^-(1/p!1)")
(("1"
(lemma
"both_sides_times_pos_le1"
("pz"
"a!1*b!1"
"x"
"1"
"y"
"F(a!1 ^ (1 / q!1) * b!1 ^ -(1 / p!1))"))
(("1"
(assert)
(("1"
(replace -1 -2 rl)
(("1"
(hide -1)
(("1"
(hide-all-but
(-1 -12 -13 -14 1))
(("1"
(expand "F")
(("1"
(rewrite
"mult_real_expt"
-1)
(("1"
(rewrite
"real_expt_times"
-1
:dir
rl)
(("1"
(case-replace
"a!1 ^ ((1 / q!1) * (-q!1))=1/a!1")
(("1"
(hide -1)
(("1"
(rewrite
"real_expt_times"
-1
:dir
rl)
(("1"
(rewrite
"mult_real_expt")
(("1"
(rewrite
"real_expt_times"
-1
:dir
rl)
(("1"
(rewrite
"real_expt_times"
-1
:dir
rl)
(("1"
(case-replace
"b!1 ^ (-(1 / p!1) * p!1)=1/b!1")
(("1"
(hide
-1)
(("1"
(case-replace
"(-(1 / p!1) * (-q!1))=q!1-1")
(("1"
(case-replace
"((1 / q!1) * p!1)=p!1-1")
(("1"
(hide
-1
-2)
(("1"
(rewrite
"real_expt_minus"
-1)
(("1"
(rewrite
"real_expt_minus"
-1)
(("1"
(rewrite
"real_expt_x1")
(("1"
(rewrite
"real_expt_x1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-5
1))
(("2"
(case-replace
"1/q!1=1-1/p!1")
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(hide
-1
2)
(("2"
(assert)
(("2"
(case-replace
"1/p!1=1-1/q!1")
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-3
1))
(("2"
(expand
"^")
(("2"
(rewrite
"nnreal_expt_x1")
(("2"
(lemma
"posreal_div_posreal_is_posreal"
("px"
"1"
"py"
"b!1"))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-2 1))
(("2"
(expand "^")
(("2"
(rewrite
"nnreal_expt_x1")
(("2"
(lemma
"posreal_div_posreal_is_posreal"
("px"
"1"
"py"
"a!1"))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite
"real_expt_pos")
(("2"
(rewrite
"real_expt_pos")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite
"posreal_times_posreal_is_posreal"
1)
nil
nil))
nil)
("2"
(rewrite
"posreal_times_posreal_is_posreal"
1)
(("1"
(rewrite "real_expt_pos")
nil
nil)
("2"
(rewrite "real_expt_pos")
nil
nil))
nil)
("3" (assert) nil nil)
("4" (assert) nil nil))
nil)
("2"
(hide 2)
(("2"
(lemma
"minimum_derivative[posreal]"
("g" "F" "x" "1"))
(("2"
(replace -2)
(("2"
(skosimp)
(("2"
(inst - "t!1")
(("2"
(case-replace "F(1)=1")
(("1"
(case-replace "1/=t!1")
(("1"
(split -3)
(("1"
(assert)
nil
nil)
("2"
(skosimp)
(("2"
(hide 3 4)
(("2"
(replace -4)
(("2"
(assert)
(("2"
(hide-all-but
(-12
-13
-14
1
2))
(("2"
(case
"y!1>1")
(("1"
(lemma
"real_expt_gt1"
("x"
"y!1"
"a"
"p!1-1"))
(("1"
(assert)
(("1"
(lemma
"real_expt_lt1"
("x"
"y!1"
"a"
"-q!1-1"))
(("1"
(assert)
(("1"
(hide
1)
(("1"
(lemma
"posreal_times_posreal_is_posreal"
("px"
"y!1 ^ (p!1 - 1)-y!1 ^ (-q!1 - 1)"
"py"
"y!1-1"))
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(case
"y!1<1")
(("1"
(hide
1
2)
(("1"
(lemma
"real_expt_lt1"
("x"
"y!1"
"a"
"p!1-1"))
(("1"
(assert)
(("1"
(lemma
"real_expt_gt1"
("x"
"y!1"
"a"
"-q!1-1"))
(("1"
(assert)
(("1"
(lemma
"posreal_times_posreal_is_posreal"
("px"
"y!1 ^ (-q!1 - 1)-y!1 ^ (p!1 - 1)"
"py"
"1-y!1"))
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(hide-all-but
(-12 -13 -14 1))
(("2"
(expand "F")
(("2"
(rewrite
"real_expt_1a")
(("2"
(rewrite
"real_expt_1a")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace -2)
(("2"
(assert)
(("2"
(rewrite "real_expt_1a")
(("2"
(rewrite "real_expt_1a")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "derivable_sum[posreal]"
("ff1"
"1 / p!1 * (LAMBDA (y: posreal): y ^ p!1)"
"ff2"
"1 / q!1 * (LAMBDA (y: posreal): y ^ -q!1)"))
(("2"
(lemma
"deriv_sum_fun[posreal]"
("ff1"
"1 / p!1 * (LAMBDA (y: posreal): y ^ p!1)"
"ff2"
"1 / q!1 * (LAMBDA (y: posreal): y ^ -q!1)"))
(("2"
(replace -3)
(("2"
(replace -4)
(("2"
(replace -6)
(("2"
(replace -8)
(("2"
(expand "*")
(("2"
(expand "+")
(("2"
(expand "F" 1)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal judgement-tcc nil real_types nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.116 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.
|
