(youngnil 3432615617 ("" (subtype-tcc) nil nil ) nil nil ))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" "deriv_scal_fun[posreal]" "b" "c!1" "ff" "I[posreal]" ))"1" (lemma "deriv_id_fun[posreal]" )"1" "deriv_const_fun[posreal]" ("b" "1-c!1" ))"1" "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" "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" "1" "minimum_derivative[posreal]" "g" "F" "x" "1" ))"1" replace -4)"1" "1" "p!1" )"1" "p!1" )"1" replace "1" "1" rewrite "real_expt_1a" )"1" assert )"1" "1" "1" assert )"1" "c!1" )"1" "y!1" )"1" "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" "1" case "y!1>1" )"1" "real_expt_lt1" "x" "y!1" "a" "c!1-1" ))"1" "1" "1" "1" "1" "negreal_times_negreal_is_posreal" "nx" "y!1 ^ (c!1 - 1) - 1" "ny" "1-y!1" ))"1" "posreal_times_posreal_is_posreal" "px" "(y!1 ^ (c!1 - 1) - 1) * (1 - y!1)" "py" "c!1" ))"1" 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" "1" "real_expt_gt1" "x" "y!1" "a" "c!1-1" ))"1" "posreal_times_posreal_is_posreal" "px" "y!1 ^ (c!1 - 1) - 1" "py" "1-y!1" ))"1" "posreal_times_posreal_is_posreal" "px" "(y!1 ^ (c!1 - 1) - 1) * (1 - y!1)" "py" "c!1" ))"1" nil nil )"2" assert )nil nil ))nil )"2" assert )nil nil )"3" assert )"3" "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" "(LAMBDA (x: posreal): 1 - x ^ c!1 - c!1 + c!1 * x)=F" )"1" "1" replace -3)"1" assert )nil nil ))nil ))nil )"2" expand "F" )"2" nil nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" "F=(LAMBDA (x: posreal): 1 - x ^ c!1 - c!1 + c!1 * x)" )"1" "1" "derivable_diff[posreal]" "ff1" "lambda (x:posreal): 1-c!1+c!1*x" "ff2" "(LAMBDA (y:posreal): y ^ c!1)" ))"1" expand "-" )"1" nil nil ))nil ))nil ))nil )"2" expand "F" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil )"3" assert )"3" "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" 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 )"nnreal" real_expt "power/" )OR const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"even_int" integersnil )nil ln_exp_def "power/" )"continuous_fun[T]" integral"analysis/" )"continuous_fun[T]" "analysis/" )"continuous_fun[T]" integral_step"analysis/" )"continuous_fun[T]" unif_cont_fun"analysis/" )"continuous_fun" "analysis/" )"continuous_fun[T]" "analysis/" )"deriv_fun" derivatives "analysis/" )"continuous_fun[T2]" "analysis/" )nil derivatives "analysis/" )"bool" derivatives "analysis/" )nil derivatives "analysis/" )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )"nnreal" nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )"[T -> real]" derivatives "analysis/" )nil derivative_props "analysis/" )"bool" deriv_domain_def "analysis/" )"(total_order?[real])" nil )"real" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )nil real_expt "power/" )nil real_expt "power/" )nil real_expt "power/" )NOT const-decl "[bool -> bool]" booleans nil )nil deriv_domain "analysis/" )nil deriv_domain "analysis/" )"odd_int" integers nil )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )"deriv_fun" derivatives"analysis/" )"(convergent?)" "analysis/" )"deriv_fun" derivatives"analysis/" )nil derivatives "analysis/" )"[posreal -> real]" young nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posreal" nil ))nil 3432615617 ("" (subtype-tcc) nil nil )"posreal" nil ))nil ))nil 3432615617 ("" (subtype-tcc) nil nil )"posreal" nil ))nil ))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" "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" "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" "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" "deriv_scal_fun[posreal]" "b" "1/p!1" "ff" "LAMBDA (y:posreal): y ^ p!1" ))"1" "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" "a!1^(1/q!1)*b!1^-(1/p!1)" )"1" "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" "1" "1" expand "F" )"1" rewrite "mult_real_expt" "1" rewrite "real_expt_times" "1" "a!1 ^ ((1 / q!1) * (-q!1))=1/a!1" )"1" "1" rewrite "real_expt_times" "1" rewrite "mult_real_expt" )"1" rewrite "real_expt_times" "1" rewrite "real_expt_times" "1" "b!1 ^ (-(1 / p!1) * p!1)=1/b!1" )"1" "1" "(-(1 / p!1) * (-q!1))=q!1-1" )"1" "((1 / q!1) * p!1)=p!1-1" )"1" "1" rewrite "real_expt_minus" "1" rewrite "real_expt_minus" "1" rewrite "real_expt_x1" )"1" rewrite "real_expt_x1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "1/q!1=1-1/p!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil )"2" "2" assert )"2" "1/p!1=1-1/q!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "^" )"2" rewrite "nnreal_expt_x1" )"2" "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" "2" expand "^" )"2" rewrite "nnreal_expt_x1" )"2" "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" nil nil ))nil )"2" rewrite "posreal_times_posreal_is_posreal" "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" "2" "minimum_derivative[posreal]" "g" "F" "x" "1" ))"2" replace -2)"2" "2" "t!1" )"2" "F(1)=1" )"1" "1/=t!1" )"1" "1" assert )nil nil )"2" "2" "2" replace -4)"2" assert )"2" "2" case "y!1>1" )"1" "real_expt_gt1" "x" "y!1" "a" "p!1-1" ))"1" assert )"1" "real_expt_lt1" "x" "y!1" "a" "-q!1-1" ))"1" assert )"1" "1" "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" "1" "real_expt_lt1" "x" "y!1" "a" "p!1-1" ))"1" assert )"1" "real_expt_gt1" "x" "y!1" "a" "-q!1-1" ))"1" assert )"1" "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" "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" "derivable_sum[posreal]" "ff1" "1 / p!1 * (LAMBDA (y: posreal): y ^ p!1)" "ff2" "1 / q!1 * (LAMBDA (y: posreal): y ^ -q!1)" ))"2" "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 )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"nnreal" nil )"posreal" nil )"nnreal" nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"(total_order?[real])" nil )"posreal" nil )nil real_types nil )OR const-decl "[bool, bool -> bool]" booleans nil )"nnreal" real_expt "power/" )"nnreal" nil )"(strict_total_order?[real])" real_props nil )nil real_expt "power/" )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_expt "power/" )AND const-decl "[bool, bool -> bool]" booleans nil )nil ln_exp_def "power/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )"odd_int" integers nil )"even_int" integersnil )"bool" reals nil )nil real_props nil )nil real_expt "power/" )"nzreal" nil )"real" reals nil )"posreal" nil )"real" reals nil )nil real_expt "power/" )nil real_expt "power/" )"real" reals nil )nil nnreal_expt "power/" )"nzreal" nil )nil real_expt "power/" )"[posreal -> nnreal]" young nil )"real" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" young nil )"{r | r > 1}" young nil )"nnreal" young nil )"{r | r > 1}" young nil )"(total_order?[real])" nil )nil derivative_props "analysis/" )"bool" deriv_domain_def "analysis/" )"(strict_total_order?[real])" real_props nil )nil real_expt "power/" )nil real_expt "power/" )"bool" reals nil )nil real_expt "power/" )"[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[T -> real]" derivatives "analysis/" )"real" reals nil )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def "analysis/" )nil derivatives "analysis/" )"bool" derivatives "analysis/" )nil derivatives "analysis/" )"nzreal" real_typesnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.37 Sekunden
(vorverarbeitet am 2026-04-26)
¤ *© Formatika GbR, Deutschland
