SSL ln_approx.prf
Interaktion und
(ln_approxnil 3296313954 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil 3296309969"" (expand "ln_le2_lb" )"" (expand "ln_le2_ub" )"" (skosimp*)"" (lift-if)"" (prop)"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (lemma "ln_taylors" ("xgm1" "x!1" "n" "2*n!1" ))"1" (skosimp*)"1" (typepred "c!1" )"1" (assert )"1" (hide -1 -3 -4)"1" (replace -2)"1" (hide -2)"1" (flatten)"1" "expt_plus" "n0x" "x!1/-c!1" "i" "1" "j" "2*n!1" ))"1" rewrite "expt_x1" )"1" "expt_times" "n0x" "x!1/-c!1" "i" "2" "j" "n!1" ))"1" case "(x!1 / -c!1) ^ 2 > 0" )"1" "expt_pos" "px" "(x!1 / -c!1) ^ 2" "i" "n!1" ))"1" case "((x!1 / -c!1) ^ (1 + 2 * n!1)) / (1 + 2 * n!1) < 0" )"1" (assert ) nil nil )"2" "2" rewrite "div_mult_pos_lt1" "2" "posreal_times_posreal_is_posreal" "px" "x!1" "py" "(x!1 / -c!1) ^ (2 * n!1)" ))"1" "both_sides_div_neg_lt1" "nz" "-c!1" ))"1" "x!1 * (x!1 / -c!1) ^ (2 * n!1)" "0" )"1" assert )"1" replace -6)"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "2" "both_sides_div_neg_lt1" "nz" "-c!1" "y" "0" "x" "x!1" ))"1" "negreal_times_negreal_is_posreal" "nx" "x!1/-c!1" "ny" "x!1/-c!1" ))"1" assert )"1" expand "^" 1)"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"4" (lemma "ln_taylors" ("xgm1" "x!1" "n" "1+2*n!1" ))"1" (skosimp*)"1" (replace -1)"1" (typepred "c!1" )"1" (assert )"1" (hide -1 -3 -4)"1" (flatten)"1" (hide -3)"1" case "0<((x!1 / -c!1) ^ (2 + 2 * n!1)) / (2 + 2 * n!1)" )"1" (assert ) nil nil )"2" "2" "expt_times" "n0x" "x!1/-c!1" "i" "2" "j" "1+n!1" ))"2" "expt_pos" "px" "(x!1 / -c!1) ^ 2" "i" "1+n!1" ))"1" assert )"1" "posreal_div_posreal_is_posreal" "px" "(x!1 / -c!1) ^ (2 + 2 * n!1)" "py" "2 + 2*n!1" ))"1" (assert ) nil nil ))nil ))nil )"2" "2" "both_sides_div_neg_lt1" "nz" "-c!1" "y" "0" "x" "x!1" ))"1" assert )"1" "negreal_times_negreal_is_posreal" "nx" "x!1/-c!1" "ny" "x!1/-c!1" ))"1" expand "^" )"1" expand "expt" )"1" expand "expt" )"1" expand "expt" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" ln_approx nil )"even_int" integersnil )"even_int" integersnil )"posint" nil )nil real_types nil )nil ln_series nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil ln_series nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )nil taylors "analysis/" )nil exponentiation nil )"boolean" notequal nil )nil reals nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil exponentiation nil )nil real_types nil )"real" exponentiation nil )nil exponentiation nil )nil real_types nil )nil real_types nil )"(total_order?[real])" nil )nil real_types nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_props nil )nil real_props nil )"real" reals nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil exponentiation nil )"odd_int" integers nil )"real" reals nil )"real" reals nil )"real" reals nil )"posint" nil )"odd_int" integers nil )"posint" nil )"odd_int" integers nil )"(total_order?[real])" nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" ln_approx nil ))nil 3321024764 ("" (subtype-tcc) nil nil ) nil nil ))nil 3558254741"" (skeep)"" (expand "ln_gt1_ub" )"" (case "log_nat(xgt1,2)`1 <= log_nat(ygt1,2)`1" )"1" (case "log_nat(xgt1,2)`1 < log_nat(ygt1,2)`1" )"1" (hide -2)"1" (copy -1)"1" (case "NOT ln_le2_ub(n, 1)>0" )"1" (hide 2)"1" (expand "ln_le2_ub" )"1" (lemma "ln_le2_bounds" )"1" (inst - "n" "1" )"1" (assert )"1" (flatten)"1" (expand "ln_le2_ub" )"1" case "ln(2) > 0" )"1" (assert ) nil nil )"2" "2" "ln_le2_bounds" )"2" "6" "1" )"2" assert )"2" "2" "2" expand "ln_le2_lb" )"2" expand "ln_estimate" )"2" "ln" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (mult-by -2 "ln_le2_ub(n, 1)" )"2" (assert )"2" (name "nx" "log_nat(xgt1,2)`1" )"2" (name "sx" "log_nat(xgt1,2)`2" )"2" (replace -1)"2" (replace -2)"2" (name "ny" "log_nat(ygt1,2)`1" )"2" replace -1)"2" "sy" "log_nat(ygt1,2)`2" )"2" replace -1)"2" "sx" )"2" "sy" )"2" replace -8)"2" replace -10)"2" case "ln_le2_ub(n,sx-1)<=ln_le2_ub(n,1) AND ln_le2_ub(n,0) <= ln_le2_ub(n,sy-1)" )"1" "1" case "nx+1<=ny" )"1" "ln_le2_ub(n,1)" )"1" assert )"1" case "ln_le2_ub(n,0) = 0" )"1" assert )nil nil )"2" "2" expand "ln_le2_ub" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" expand "ln_le2_ub" )"2" "1" assert )"1" "1" assert )"1" "1" nil nil )"2" "2" "ln_estimate_increasing_odd" )"2" "n" "sx-1" "1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "ln_estimate_increasing_odd" )"2" "n" "0" "sy-1" )"2" assert )"2" case "ln_estimate(0,1+2*n) = 0" )"1" assert )nil nil )"2" "2" expand "ln_estimate" )"2" rewrite "sigma_restrict_eq_0" )"1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" 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 )"2" (case "log_nat(xgt1,2)`1 = log_nat(ygt1,2)`1" )"1" (replace -1 :dir rl)"1" (case "log_nat(xgt1,2)`2 <= log_nat(ygt1,2)`2" )"1" (expand "ln_le2_ub" )"1" (assert )"1" (lemma "ln_estimate_increasing_odd" )"1" "n" "log_nat(xgt1, 2)`2 - 1" "log_nat(ygt1, 2)`2 - 1" )"1" (assert )"1" (case "ln_estimate(0,1+2*n) = 0" )"1" (assert )"1" "1" assert )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" "2" expand "ln_estimate" )"2" rewrite "sigma_restrict_eq_0" )"1" "1" "1" "1" (ground) nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (hide (2 3))"2" (hide -2)"2" (typepred "log_nat(xgt1,2)`2" )"2" (typepred "log_nat(ygt1,2)`2" )"2" (replace -7 :dir rl)"2" (mult-by 1 "2^log_nat(xgt1,2)`1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (typepred "log_nat(xgt1,2)`2" )"2" (typepred "log_nat(ygt1,2)`2" )"2" (assert )"2" (copy -7)"2" (replace -7 -1)"2" (replace -4 -1)"2" (mult-by -1 "2^(-log_nat(ygt1,2)`1)" )"2" (assert )"2" (lemma "expt_plus" )"2" (rewrite -1 :dir rl)"2" rewrite -1 :dir rl)"2" "2" "1/log_nat(xgt1,2)`2" )"1" case "log_nat(ygt1,2)`2/log_nat(xgt1,2)`2 < 2" )"1" case "FORALL (nn:nat): 2^(nn+1) >= 2" )"1" "(-log_nat(ygt1, 2)`1) + log_nat(xgt1, 2)`1-1" )"1" (assert ) nil nil ))nil )"2" "2" "nn" )"1" (grind) nil nil )"2" "2" assert )"2" expand "^" )"2" expand "expt" +)"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (cross-mult 1) nil nil ))nil )"2" (cross-mult 1) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posint" exponentiation nil )"real" ln_approx nil )"posrat" nil )"int" integers nil )"nzreal" exponentiation nil )nil reals nil )nil real_props nil )"real" reals nil )"posint" nil )"posrat" nil )"posnat" exponentiation nil )"odd_int" integers nil )nil naturalnumbers nil )nil defined_types nil )"int" integers nil )"nzreal" nil )nil real_props nil )"{x: posreal | x > 1}" ln_approx nil )"nzreal" nil )nil exponentiation nil )nil exponentiation nil )"int" integers nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )nil real_props nil )"nat" ln_approx nil )"(total_order?[real])" nil )"real" reals nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"[numfield, numfield -> numfield]" number_fields nil )nil extra_real_propsnil )"[bool, bool -> bool]" booleans nil )nil sigma "reals/" )nil sigma "reals/" )"[numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sigma "reals/" )"rat" rationals nil )"even_int" integers nil )nil exponent_props "reals/" )nil ln_series nil )nil ln_approx nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"odd_int" integers nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"real" ln_approx nil )"nzrat" rationalsnil )"real" reals nil )"nzint" integers nil )"nzint" integersnil )"odd_int" integers nil )"int" exponentiation nil )"nzreal" exponentiation nil )"real" sigma "reals/" )"real" exponentiation nil )"real" ln_series nil )"real" ln_exp nil )"real" ln_approx nil )NOT const-decl "[bool -> bool]" booleans nil )nil real_props nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil ) (>= const-decl "bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[T, T -> boolean]" equalities nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat"reals/" )nil real_types nil )nil real_types nil ))nil 3558280348"" (skeep)"" (case "n = 0" )"1" (replace -1) (("1" (grind) nil nil )) nil )"2" (label "npos" 1)"2" (hide "npos" )"2" (expand "ln_gt1_lb" )"2" (case "log_nat(xgt1,2)`1 <= log_nat(ygt1,2)`1" )"1" (case "log_nat(xgt1,2)`1 < log_nat(ygt1,2)`1" )"1" (hide -2)"1" (copy -1)"1" (case "NOT ln_le2_lb(n, 1)>0" )"1" (hide 2)"1" (lemma "ln_estimate_error_bound" )"1" (expand "ln_le2_lb" )"1" (inst - "2*n" "1" )"1" assert )"1" case "n > 0" )"1" case "ln(2) >1/(1+2*n)" )"1" "1" "ln" "ln_estimate" ))nil nil ))nil )"2" "2" case "ln(2) > 1/3 AND FORALL (k:nat): 1/(1+2*(k+1)) <= 1/3" )"1" "1" "n-1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil )"2" "1" "1" "1" "ln_le2_bounds" )"1" "6" "1" )"1" assert )"1" "1" "1" expand "ln_le2_lb" )"1" expand "ln_estimate" )"1" "ln" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "npos" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (mult-by -2 "ln_le2_lb(n, 1)" )"2" (assert )"2" (name "nx" "log_nat(xgt1,2)`1" )"2" (name "sx" "log_nat(xgt1,2)`2" )"2" replace -1)"2" replace -2)"2" "ny" "log_nat(ygt1,2)`1" )"2" replace -1)"2" "sy" "log_nat(ygt1,2)`2" )"2" replace -1)"2" "sx" )"2" "sy" )"2" replace -8)"2" replace -10)"2" case "ln_le2_lb(n,sx-1)<=ln_le2_lb(n,1) AND ln_le2_lb(n,0) <= ln_le2_lb(n,sy-1)" )"1" "1" case "nx+1<=ny" )"1" "ln_le2_lb(n,1)" )"1" assert )"1" case "ln_le2_lb(n,0) = 0" )"1" assert )nil nil )"2" "2" expand "ln_le2_lb" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" expand "ln_le2_lb" )"2" "1" assert )"1" "1" assert )"1" "1" nil nil )"2" "2" "ln_estimate_increasing_even" )"2" "n" "sx-1" "1" )"1" assert )nil nil )"2" "2" nil nil ))nil )"3" expand "abs" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "ln_estimate_increasing_even" )"2" "n" "0" "sy-1" )"1" assert )"1" case "ln_estimate(0,2*n) = 0" )"1" assert )nil nil )"2" "2" expand "ln_estimate" )"2" rewrite "sigma_restrict_eq_0" )"1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" )"2" assert )nil nil ))nil )"3" assert )"3" "3" 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" (case "log_nat(xgt1,2)`1 = log_nat(ygt1,2)`1" )"1" (replace -1 :dir rl)"1" case "log_nat(xgt1,2)`2 <= log_nat(ygt1,2)`2" )"1" (expand "ln_le2_lb" )"1" (assert )"1" (lemma "ln_estimate_increasing_even" )"1" "n" "log_nat(xgt1, 2)`2 - 1" "log_nat(ygt1, 2)`2 - 1" )"1" assert )"1" case "ln_estimate(0,2*n) = 0" )"1" assert )"1" "1" assert )"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "ln_estimate" )"2" rewrite "sigma_restrict_eq_0" )"1" "1" "1" "1" nil nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "abs" )"2" (assert ) nil nil ))nil ))nil ))nil )"3" expand "abs" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (hide (2 3))"2" (hide -2)"2" (typepred "log_nat(xgt1,2)`2" )"2" "log_nat(ygt1,2)`2" )"2" replace -7 :dir rl)"2" "2^log_nat(xgt1,2)`1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide 2)"2" (typepred "log_nat(xgt1,2)`2" )"2" (typepred "log_nat(ygt1,2)`2" )"2" (assert )"2" (copy -7)"2" (replace -7 -1)"2" (replace -4 -1)"2" (mult-by -1 "2^(-log_nat(ygt1,2)`1)" )"2" assert )"2" "expt_plus" )"2" rewrite -1 :dir rl)"2" rewrite -1 :dir rl)"2" "2" "1/log_nat(xgt1,2)`2" )"1" case "log_nat(ygt1,2)`2/log_nat(xgt1,2)`2 < 2" )"1" case "FORALL (nn:nat): 2^(nn+1) >= 2" )"1" "(-log_nat(ygt1, 2)`1) + log_nat(xgt1, 2)`1-1" )"1" assert )nil nil ))nil )"2" "2" "nn" )"1" nil nil )"2" "2" assert )"2" expand "^" )"2" expand "expt" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"real" exponentiation nil )"real" exponentiation nil )"real" sigma "reals/" )"real" ln_series nil )"real" ln_approx nil )"real" ln_approx nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"nzrat" rationalsnil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"posint" exponentiation nil )"(total_order?[real])" nil )nil real_types nil )nil real_types nil )"[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat"reals/" )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"bool" reals nil ) (<= const-decl "bool" reals nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil ln_series nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"nzint" integers nil )"nzint" integersnil )"odd_int" integers nil )"int" exponentiation nil )"nzreal" exponentiation nil )nil ln_approx nil )nil reals nil )nil real_props nil )"odd_int" integers nil )"posint" nil )nil real_props nil )nil real_props nil )"int" integers nil )"nat" ln_approx nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"real" ln_exp nil )nil exponentiation nil )"posint" nil )"even_int" integersnil )"posrat" nil )"posint" nil )"odd_int" integers nil )"odd_int" integers nil )nil ln_series nil )nil ln_series nil )"{y | y < 2 AND xgt1 = 2 ^ log_nat(xgt1, 2)`1 * y}" ln_approx nil )"{x: posreal | x > 1}" ln_approx nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )"{j: posint | j >= i}" nil )"{j: nonneg_int | j >= i}" nil )"{r: posrat | r >= q}" nil )"{x: posreal | x > 1}" ln_approx nil )"{y | y < 2 AND ygt1 = 2 ^ log_nat(ygt1, 2)`1 * y}" ln_approx nil )nil exponent_props "reals/" )"even_int" integers nil )"rat" rationals nil )nil sigma "reals/" )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sigma "reals/" )nil sigma "reals/" )"[bool, bool -> bool]" booleans nil )nil extra_real_propsnil )nil real_props nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"int" integers nil )nil exponentiation nil )nil exponentiation nil )"nzreal" nil )nil real_props nil )"nzreal" nil )nil defined_types nil )nil naturalnumbers nil )"posnat" exponentiation nil )"real" reals nil )nil real_props nil )nil reals nil )"nzreal" exponentiation nil )"posrat" nil ))nil ))nil 3296313957 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3296313957 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil 3321025214"" (skosimp*)"" (expand "ln_gt1_lb" )"" (expand "ln_gt1_ub" )"" (typepred "log_nat(x!1,2)`2" )"1" (name-replace "m" "log_nat(x!1,2)`1" )"1" (name-replace "y" "log_nat(x!1,2)`2" )"1" (replaces -3)"1" (rewrite "ln_mult" )"1" (rewrite "ln_expt" )"1" (lemma "ln_le2_bounds" )"1" (inst -1 "n!1" "1" )"1" (assert )"1" (flatten)"1" (case "m=0" )"1" "1" rewrite "expt_x0" )"1" assert )"1" "ln_le2_bounds" )"1" "n!1" "y-1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" "m" )"2" "m" )"2" case "y=1" )"1" "1" rewrite "ln_1" )"1" expand "ln_le2_lb" )"1" expand "ln_le2_ub" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" "ln_le2_bounds" )"2" "n!1" "y-1" )"2" assert )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"posint" exponentiation nil )"real" reals nil )"real" ln_approx nil )"[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat"reals/" )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil naturalnumbers nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )nil real_types nil )nil ln_exp nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil ln_approx nil )"real" reals nil )"(total_order?[real])" nil )nil exponentiation nil )"[numfield, numfield -> numfield]" number_fields nil )"real" ln_approx nil )"posint" nil )"odd_int" integers nil )"posint" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )nil ln_exp nil )"nat" ln_approx nil )"real" ln_exp nil )"real" ln_approx nil )nil real_props nil )nil ln_exp nil )nil integers nil )"real" ln_approx nil ))nil ))nil 3296503304"" (skosimp)"" (rewrite "div_mult_pos_gt1" ) (("" (assert ) nil nil )) nil ))nil )nil extra_real_props nil )nil numbers nil )nil booleans 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 )"bool" reals nil )nil real_types nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil 3296503304 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil ))nil 3558342713"" (skeep)"" (expand "ln_lb" )"" case "FORALL (xx:posreal): (xx>1 IMPLIES ln_gt1_ub(n, xx) >= 0)" )"1" (case "px<1 IFF 1/px >1" )"1" (case "py<1 IFF 1/py >1" )"1" (case "1/py <= 1/px" )"1" (inst-cp - "px" )"1" (inst-cp - "py" )"1" (inst-cp - "1/px" )"1" (inst - "1/py" )"1" case "FORALL (xx:posreal): (xx>1 IMPLIES ln_gt1_lb(n, xx) >= 0)" )"1" (inst-cp - "px" )"1" (inst-cp - "py" )"1" (inst-cp - "1/px" )"1" "1/py" )"1" "1" "1" "1" "1" "1" assert )"1" "1" "1" "1" "1" assert )"1" "ln_gt1_ub_increasing" )"1" "n" "1/py" "1/px" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" "1" assert )"1" "1" nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "ln_gt1_lb_increasing" )"2" "n" "px" "py" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skeep)"2" (expand "ln_gt1_lb" )"2" case "ln_le2_lb(n,1)>=0 AND ln_le2_lb(n,0) = 0" )"1" "1" "log_nat(xx,2)`1" )"1" expand "ln_le2_lb" )"1" "1" "1" "ln_estimate_increasing_even" )"1" "n" "0" "log_nat(xx, 2)`2 - 1" )"1" assert )"1" case "ln_estimate(0, 2*n) = 0" )"1" assert )nil nil )"2" "2" expand "ln_estimate" )"2" rewrite "sigma_restrict_eq_0" )"1" "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "log_nat(xx,2)`2" )"2" "log_nat" )nil nil ))nil ))nil )"3" assert )"3" expand "abs" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ln_le2_lb" )"2" "ln_estimate_increasing_even" )"2" "n" "0" "1" )"1" assert )"1" case "ln_estimate(0, 2*n) = 0" )"1" (assert ) nil nil )"2" "2" expand "ln_estimate" )"2" rewrite "sigma_restrict_eq_0" )"1" "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil )"2" (hide-all-but 1)"2" (ground)"1" (cross-mult 1) nil nil )"2" (cross-mult -1) nil nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (ground)"1" (cross-mult 1) nil nil )"2" (cross-mult -1) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide-all-but 1)"2" (skeep)"2" (expand "ln_gt1_ub" )"2" (case "ln_le2_ub(n,1)>=0 AND ln_le2_ub(n,0) = 0" )"1" (flatten)"1" (mult-by -1 "log_nat(xx,2)`1" )"1" (expand "ln_le2_ub" )"1" (lift-if)"1" (ground)"1" (lemma "ln_estimate_increasing_odd" )"1" "n" "0" "log_nat(xx, 2)`2 - 1" )"1" assert )"1" case "ln_estimate(0, 1+2*n) = 0" )"1" (assert ) nil nil )"2" "2" expand "ln_estimate" )"2" rewrite "sigma_restrict_eq_0" )"1" "1" (grind) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "ln_le2_ub" )"2" (lemma "ln_estimate_increasing_odd" )"2" (inst - "n" "0" "1" )"2" (assert )"2" (case "ln_estimate(0, 1+2*n) = 0" )"1" (assert ) nil nil )"2" "2" expand "ln_estimate" )"2" rewrite "sigma_restrict_eq_0" )"1" "1" (grind) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" ln_approx nil )"real" ln_approx nil )nil ln_series nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"odd_int" integers nil )"posreal" nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil extra_real_props nil )"bool" reals nil )"posint" exponentiation nil )"{j: posint | j >= i}" nil )"{r: posrat | r >= q}" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" reals nil )"real" reals nil )"real" reals nil )"{j: nonneg_int | j >= i}" nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" ln_approx nil )nil ln_series nil )"real" ln_series nil )nil integers nil )nil exponent_props "reals/" )"even_int" integers nil )"rat" rationals nil )nil sigma "reals/" )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sigma "reals/" )nil sigma "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"posrat" nil )"posnat" exponentiation nil )nil ln_series nil )"[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat"reals/" )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )nil extra_real_propsnil )"[T, T -> boolean]" equalities nil )"real" ln_approx nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"(total_order?[real])" nil )nil ln_approx nil )nil ln_approx nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" ln_approx nil )nil real_props nil )nil reals nil )nil real_props nil )nil real_props nil )"posreal" nil )nil numbers nil )nil booleans 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 )"bool" reals nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"real" ln_approx nil ))nil 3558348180"" (skeep)"" (expand "ln_ub" )"" case "FORALL (xx:posreal): (xx>1 IMPLIES ln_gt1_ub(n, xx) >= 0)" )"1" (case "px<1 IFF 1/px >1" )"1" (case "py<1 IFF 1/py >1" )"1" (case "1/py <= 1/px" )"1" (inst-cp - "px" )"1" (inst-cp - "py" )"1" (inst-cp - "1/px" )"1" (inst - "1/py" )"1" case "FORALL (xx:posreal): (xx>1 IMPLIES ln_gt1_lb(n, xx) >= 0)" )"1" (inst-cp - "px" )"1" (inst-cp - "py" )"1" (inst-cp - "1/px" )"1" "1/py" )"1" "1" "1" "1" "1" "1" assert )"1" "1" "1" "1" "1" assert )"1" "ln_gt1_lb_increasing" )"1" "n" "1/py" "1/px" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" "1" assert )nil nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "1" "1" assert )"1" "1" nil nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "ln_gt1_ub_increasing" )"2" "n" "px" "py" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (skeep)"2" (expand "ln_gt1_lb" )"2" case "ln_le2_lb(n,1)>=0 AND ln_le2_lb(n,0) = 0" )"1" "1" "log_nat(xx,2)`1" )"1" expand "ln_le2_lb" )"1" "1" "1" "ln_estimate_increasing_even" )"1" "n" "0" "log_nat(xx, 2)`2 - 1" )"1" assert )"1" case "ln_estimate(0, 2*n) = 0" )"1" assert )nil nil )"2" "2" expand "ln_estimate" )"2" rewrite "sigma_restrict_eq_0" )"1" "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "log_nat(xx,2)`2" )"2" "log_nat" )nil nil ))nil ))nil )"3" assert )"3" expand "abs" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "ln_le2_lb" )"2" "ln_estimate_increasing_even" )"2" "n" "0" "1" )"1" assert )"1" case "ln_estimate(0, 2*n) = 0" )"1" (assert ) nil nil )"2" "2" expand "ln_estimate" )"2" rewrite "sigma_restrict_eq_0" )"1" "1" nil nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" (grind) nil nil ))nil )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (cross-mult 1) (("2" (assert ) nil nil )) nil ))nil )"2" (hide-all-but 1)"2" (ground)"1" (cross-mult 1) nil nil )"2" (cross-mult -1) nil nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (ground)"1" (cross-mult 1) nil nil )"2" (cross-mult -1) nil nil ))nil ))nil ))nil )"2" (hide 2)"2" (hide-all-but 1)"2" (skeep)"2" (expand "ln_gt1_ub" )"2" (case "ln_le2_ub(n,1)>=0 AND ln_le2_ub(n,0) = 0" )"1" (flatten)"1" (mult-by -1 "log_nat(xx,2)`1" )"1" (expand "ln_le2_ub" )"1" (lift-if)"1" (ground)"1" (lemma "ln_estimate_increasing_odd" )"1" "n" "0" "log_nat(xx, 2)`2 - 1" )"1" assert )"1" case "ln_estimate(0, 1+2*n) = 0" )"1" (assert ) nil nil )"2" "2" expand "ln_estimate" )"2" rewrite "sigma_restrict_eq_0" )"1" "1" (grind) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (expand "ln_le2_ub" )"2" (lemma "ln_estimate_increasing_odd" )"2" (inst - "n" "0" "1" )"2" (assert )"2" (case "ln_estimate(0, 1+2*n) = 0" )"1" (assert ) nil nil )"2" "2" expand "ln_estimate" )"2" rewrite "sigma_restrict_eq_0" )"1" "1" (grind) nil nil ))nil )"2" "2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" ln_approx nil )"real" ln_approx nil )nil ln_series nil )"[numfield, numfield -> numfield]" number_fields nil )"posint" nil )"odd_int" integers nil )"posreal" nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil extra_real_props nil )"bool" reals nil )"posint" exponentiation nil )"{j: posint | j >= i}" nil )"{r: posrat | r >= q}" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" reals nil )"real" reals nil )"real" reals nil )"{j: nonneg_int | j >= i}" nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" ln_approx nil )nil ln_series nil )"real" ln_series nil )nil integers nil )nil exponent_props "reals/" )"even_int" integers nil )"rat" rationals nil )nil sigma "reals/" )IF const-decl "[boolean, T, T -> T]" if_def nil )nil sigma "reals/" )nil sigma "reals/" )NOT const-decl "[bool -> bool]" booleans nil )"posrat" nil )"posnat" exponentiation nil )nil ln_series nil )"[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat"reals/" )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )nil extra_real_propsnil )"[T, T -> boolean]" equalities nil )"real" ln_approx nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" reals nil )"(total_order?[real])" nil )nil ln_approx nil )nil ln_approx nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"real" ln_approx nil )nil real_props nil )nil reals nil )nil real_props nil )nil real_props nil )"posreal" nil )nil numbers nil )nil booleans 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 )"bool" reals nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )"real" ln_approx nil ))nil ))nil 3296503392"" (expand "ln_ub" )"" (expand "ln_lb" )"" (skosimp*)"" (case-replace "px!1 < 1" )"1" (lemma "ln_gt1_bounds" ("x" "1/px!1" "n" "n!1" ))"1" "div_mult_pos_lt2" ("py" "px!1" "x" "1" "z" "1" ))"1" (assert )"1" (flatten)"1" (lemma "ln_div" ("px" "1" "py" "px!1" ))"1" (rewrite "ln_1" )"1" "both_sides_times_neg_lt1" ("nz" "-1" ))"1" "ln(px!1)" "-ln_gt1_ub(n!1, 1 / px!1)" )"1" "-ln_gt1_lb(n!1, 1 / px!1)" "ln(px!1)" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case-replace "px!1=1" )"1" (rewrite "ln_1" ) (("1" (assert ) nil nil )) nil )"2" (assert )"2" (lemma "ln_gt1_bounds" ("n" "n!1" "x" "px!1" ))"2" (assert )"2" (flatten) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" ln_approx nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil ) (>= const-decl "bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil real_props nil )nil ln_exp nil )"odd_int" integers nil )"real" ln_approx nil )"real" ln_exp nil )"real" reals nil )"real" reals nil )"real" ln_approx nil )"[numfield -> numfield]" number_fields nil )nil real_types nil )nil real_types nil )"bool" reals nil )nil real_props nil )nil ln_exp nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"(total_order?[real])" nil )"real" reals nil )"posreal" nil )nil ln_approx nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"real" ln_approx nil ))nil 3543148487"" (subtype-tcc) nil nil ) nil nil ))nil 3543148487"" (skeep)"" (typepred "np" )"" (lemma "exp_ln" )"" (inst?)"" (replace -4)"" (rewrite "exp_0" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )nil integers nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil real_types nil )nil real_types nil )nil ln_exp nil )nil ln_exp nil ))nil ))nil 3543148360"" (skeep)"" (typepred "xp" )"" (typepred "np" )"" (hide -1)"" (invoke (name "lp" "%1" ) (! 1 1 1))"" (replace -1)"" (label "lpname" -1)"" (case "lp >= 0" )"1" (invoke (name "mm" "%1" ) (! 1 1))"1" (replace -1)"1" (case "mm >= 0" )"1" (label "mmname" -2)"1" (invoke (name "nn" "%1" ) (! 1 2))"1" (replace -1)"1" "nnname" -1)"1" "log_nat_bounds" )"1" case "np ^ mm <= xp AND xp < np ^ (mm + 1)" )"1" "1" assert )"1" replace "nnname" )"1" "1" case "mm > nn" )"1" "both_sides_expt_gt1_lt_aux" )"1" "np" "nn" "mm-1" )"1" expand "^" )"1" assert )nil nil ))nil )"2" case "nn=mm-1" )"1" replace -1)"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" assert )"2" case "nn > mm" )"1" "both_sides_expt_gt1_lt_aux" )"1" "np" "mm" "nn-1" )"1" expand "^" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "2" "floor_def" )"2" "2" replace "mmname" )"2" "2" "ln_strict_increasing" )"2" "1" expand "strict_increasing?" )"1" "xp" "np^mm" )"1" assert )"1" "ln_expt" )"1" "1" replace "1" case "ln(np) > 0" )"1" case "mm > lp" )"1" assert )nil nil )"2" expand "lp" "2" "2" assert )nil nil ))nil ))nil ))nil )"2" "ln_gt_0" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "ln_increasing" )"2" expand "increasing?" )"2" "np^(mm+1)" "xp" )"2" assert )"2" "ln_expt" )"2" "2" replace "2" "2" case "1+mm <= lp" )"1" assert )nil nil )"2" expand "lp" "2" case "ln(np) > 0" )"1" nil nil )"2" "ln_gt_0" )"2" "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" (assert ) nil nil ))nil ))nil ))nil )"2" (case "ln(np) > 0" )"1" (expand "lp" +)"1" (cross-mult 1)"1" (lemma "ln_ge_0" )"1" (inst?) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (lemma "ln_gt_0" )"2" (inst?) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil log_nat "reals/" )nil ln_exp nil )nil ln_exp nil )nil extra_real_props nil )"{np: posnat | np > 1}" ln_approx nil )"real" reals nil )"bool" real_fun_preds "reals/" )"bool" real_fun_preds "reals/" )nil real_props nil )nil ln_exp nil )nil ln_exp nil )nil floor_ceil nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" ln_approx nil )"{i | i <= lp & lp < 1 + i}" ln_approx nil )"posint" nil )"posnat" exponentiation nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"(strict_total_order?[real])" real_props nil )"[bool, bool -> bool]" booleans nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"(total_order?[real])" nil )"int" integers nil )nil integers nil )nil naturalnumbers nil )"[numfield, numfield -> numfield]" number_fields nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat"reals/" )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil ln_exp nil )nil real_props nil )"real" ln_exp nil )nil real_types nil )nil real_types nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"(total_order?[real])" nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )nil integers nil )"posint" exponentiation nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.0.173Bemerkung:
(vorverarbeitet am 2026-04-30)
¤ *Bot Zugriff
2026-05-26
