| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/lnexp/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 535 kB |
|
Quelle ln_exp_ineq.prfSprache: Lisp |
|||||||||||||||
|
(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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) 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) ("3" (propax) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((const_fun const-decl "[T -> real]" real_fun_ops "reals/") (ln_1 formula-decl nil ln_exp nil) (ln const-decl "real" ln_exp nil)) shostak)) (ln_ineq2_TCC1 0 (ln_ineq2_TCC1-1 nil 3254162049 ("" (grind) nil nil) nil shostak)) (ln_ineq2_TCC2 0 (ln_ineq2_TCC2-1 nil 3254162049 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (ln_ineq2 0 (ln_ineq2-1 nil 3254162404 ("" (skosimp*) (("" (typepred "xlt1!1") (("" (lemma "ln_ineq1" ("xgtm1" "-xlt1!1")) (("" (flatten) (("" (lemma "both_sides_times_neg_lt1" ("nz" "-1")) (("" (inst-cp - "-xlt1!1" "ln(1 + -xlt1!1)") (("" (inst - "ln(1 + -xlt1!1)" "-xlt1!1 / (1 + -xlt1!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nzreal_lt1 nonempty-type-eq-decl nil ln_exp_ineq nil) (< const-decl "bool" reals nil) (nzreal nonempty-type-eq-decl nil reals 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) (/= const-decl "boolean" notequal nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (ln const-decl "real" ln_exp nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (both_sides_times_neg_lt1 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (ln_ineq1 formula-decl nil ln_exp_ineq nil) (> const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nzreal_gt_m1 nonempty-type-eq-decl nil ln_exp_ineq nil)) shostak)) (ln_ineq3_TCC1 0 (ln_ineq3_TCC1-1 nil 3254162049 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (ln_ineq3 0 (ln_ineq3-3 nil 3322413185 ("" (skosimp) (("" (expand "abs") (("" (lemma "ln_strict_increasing") (("" (expand "strict_increasing?") (("" (inst - "1-px!1" "1") (("1" (rewrite "ln_1") (("1" (assert) (("1" (lemma "both_sides_plus_lt1" ("z" "ln(1-px!1)" "x" "-ln(1 - px!1)" "y" "3 * px!1 / 2")) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (simplify 1) (("1" (assert) (("1" (rewrite "inverse_add" 1) (("1" (case "px!1<=1/3") (("1" (lemma "ln_ineq1" ("xgtm1" "-px!1")) (("1" (flatten) (("1" (case "px!1/(1-px!1) <= 3*px!1/2") (("1" (assert) nil nil) ("2" (hide -1 -2 -4 -5 2) (("2" (lemma "both_sides_times_pos_le1" ("pz" "px!1" "x" "1/(1-px!1)" "y" "3/2")) (("2" (replace -1 1) (("2" (hide -1) (("2" (rewrite "div_mult_pos_le1" 1) (("2" (lemma "both_sides_times_neg_le1" ("nz" "-3/2")) (("2" (inst - "1/3" "px!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "1/3<px!1") (("1" (hide 1) (("1" (name "G" "lambda (x:{x:posreal| 1/3<x&x<1}): ln(1-x) + 3/2*x") (("1" (case "G(5828/10000)>0") (("1" (case "strict_decreasing?(G)") (("1" (expand "strict_decreasing?") (("1" (expand "<=" -6) (("1" (split -6) (("1" (inst - "px!1" "5828/10000") (("1" (assert) (("1" (expand "G" -2 2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "G" -3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2 -4) (("2" (lemma "identity_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]") (("1" (lemma "deriv_id_fun[{x: posreal | 1 / 3 < x & x < 1}]") (("1" (lemma "const_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("b" "1")) (("1" (lemma "deriv_const_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("b" "1")) (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "diff_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("f1" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 1" "f2" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): x")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_diff_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("ff1" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 1" "ff2" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): x")) (("1" (replace -5) (("1" (replace -3) (("1" (expand "-") (("1" (lemma "scal_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("f" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): x" "b" "3/2")) (("1" (assert) (("1" (lemma "deriv_scal_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("ff" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): x" "b" "3/2")) (("1" (replace -7) (("1" (expand "*") (("1" (lemma "ln_derivable") (("1" (flatten) (("1" (lemma "composition_derivable_fun[{x: posreal | 1 / 3 < x & x < 1},posreal]" ("f" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 1 - x" "g" "ln")) (("1" (assert) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: posreal | 1 / 3 < x & x < 1},posreal]" ("ff" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 1 - x" "gg" "ln")) (("1" (replace -4) (("1" (replace -7) (("1" (expand "o") (("1" (expand "*") (("1" (lemma "sum_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("f1" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): ln(1 - x)" "f2" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 3 / 2 * x")) (("1" (assert) (("1" (expand "+") (("1" (lemma "deriv_sum_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("ff1" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): ln(1 - x)" "ff2" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 3 / 2 * x")) (("1" (replace -3) (("1" (replace -7) (("1" (expand "+") (("1" (replace -15) (("1" (lemma "negative_derivative[{x: posreal | 1 / 3 < x & x < 1}]" ("g" "G")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "x!1") (("2" (expand "deriv" -5) (("2" (lemma "extensionality_postulate" ("f" "(LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): deriv(G, x))" "g" "(LAMBDA (x_1: {x: posreal | 1 / 3 < x & x < 1}): 3 / 2 + (1 / (1 - x_1)) * -1)")) (("1" (replace -1 -6 rl) (("1" (hide -1) (("1" (inst -5 "x!1") (("1" (replace -5) (("1" (hide-all-but (-1 -2 -3 -4 1)) (("1" (lemma "div_mult_pos_lt2" ("z" "1" "x" "3/2" "py" "1-x!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "x!3") (("2" (case-replace "x!3=1/2") (("1" (inst + "2/3") (("1" (assert) nil nil)) nil) ("2" (inst + "1/2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (expand "derivable" -6) (("4" (propax) 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" (skosimp) (("2" (inst + "2*x!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (case-replace "x!1=1/2") (("1" (inst + "2/3") (("1" (assert) nil nil)) nil) ("2" (inst + "1/2") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -3 -2 -4) (("2" (replace -1 1 rl) (("2" (assert) (("2" (hide -1) (("2" (lemma "ln_estimate_bnd") (("2" (inst - "19" "-5828/10000") (("2" (assert) (("2" (expand "abs" -1 2) (("2" (name-replace "DRL1" "ln(1-5828/10000)") (("2" (lemma "expt_times" ("n0x" "5828/10000" "i" "4" "j" "5")) (("2" (replace -1) (("2" (case "(5828 / 10000) ^ 4 = 1153660896461056 / 10000000000000000") (("1" (replace -1) (("1" (hide -2) (("1" (case-replace "(1153660896461056 / 10000000000000000) ^ 5 / (20 + 20 * (-5828 / 10000)) = (1153660896461056 / 10000000000000000) ^ 5 *10000/83440") (("1" (hide -1) (("1" (case-replace "(1153660896461056 / 10000000000000000) ^ 5 = 2043576321503877532268812309827579231198 (("1" (hide -1) (("1" (hide -1) (("1" (name "DRL2" "ln_estimate(-5828 / 10000, 19)") (("1" (replace -1) (("1" (case-replace "2043576321503877532268812309827579231198161568314157086599156544970504011776 / 10000000000000000000000000000000000000000000000000000000000000000000000000000000 * 10000 / 83440 = 2043576321503877532268812309827579231198161568314157086599156544970504011 /8344000000000000000000000000000000000000000000000000000000000000000000000000000 (("1" (hide -1) (("1" (expand "ln_estimate") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (case-replace "-(-5828 / 10000) = 5828/10000") (("1" (hide -1) (("1" (lemma "expt_times" ("n0x" "5828/10000")) (("1" (lemma "expt_plus" ("n0x" "5828/10000")) (("1" (rewrite "expt_x1" -3) (("1" (case "(5828 / 10000) ^ 2 = 33965584/100000000") (("1" (replace -1) (("1" (inst-cp - "1" "2") (("1" (lemma "expt_x1") (("1" (inst - "5828/10000") (("1" (replace -1) (("1" (replace -2) (("1" (replace -4) (("1" (case-replace "5828 / 10000 * (33965584 / 100000000) = 197951423552/1000000000000") (("1" (hide -1) (("1" (inst-cp - "2" "2") (("1" (replace -2) (("1" (case-replace "33965584 / 100000000 * (33965584 / 100000000) = 1153660896461056 / 10000000000000000") (("1" (hide -1) (("1" (replace -4) (("1" (inst-cp - "2" "3") (("1" (replace -2) (("1" (replace -6) (("1" (case-replace "33965584 / 100000000 * (197951423552 / 1000000000000) = 6723535704575034368/10000000000 (("1" (replace -5) (("1" (hide -1) (("1" (inst-cp - "3" "3") (("1" (replace -7) (("1" (case-replace "197951423552 / 1000000000000 * (197951423552 / 1000000000000) = 39184766086263300296704 (("1" (hide -1) (("1" (replace -4) (("1" (simplify -4) (("1" (simplify -5) (("1" (simplify -6) (("1" (simplify -7) (("1" (inst-cp - "3" "4") (("1" (replace -8) (("1" (replace -7) (("1" (simplify -4) (("1" (replace -4) (("1" (hide -9) (("1" (inst-cp - "4" "4") (("1" (replace -8) (("1" (replace -4) (("1" (inst-cp - "4" "5") (("1" (replace -8) (("1" (replace -9) (("1" (replace -4) (("1" (inst-cp - "5" "5") (("1" (replace -9) (("1" (replace -4) (("1" (inst-cp - "5" "6") (("1" (replace -9) (("1" (replace -10) (("1" (replace -4) (("1" (inst-cp - "6" "6") (("1" (replace -10) (("1" (replace -4) (("1" (case-replace "(197951423552 / 1000000000000 * (1153660896461056 / 10000000000000000)) = 228368816750742514129190912/10000000000000 (("1" (hide -1) (("1" (inst-cp - "6" "7") (("1" (replace -10) (("1" (replace -11) (("1" (replace -4) (("1" (inst-cp - "7" "7") (("1" (replace -11) (("1" (replace -4) (("1" (inst-cp - "7" "8") (("1" (replace -12) (("1" (replace -11) (("1" (replace -4) (("1" (inst-cp - "8" "8") (("1" (replace -12) (("1" (replace -4) (("1" (inst-cp - "8" "9") (("1" (replace -12) (("1" (replace -13) (("1" (replace -4) (("1" (inst-cp - "9" "9") (("1" (replace -13) (("1" (replace -4) (("1" (inst - "9" "10") (("1" (replace -12) (("1" (replace -13) (("1" (replace -3) (("1" (hide-all-but (-20 -21 1)) (("1" (expand "abs" -2) (("1" (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)) 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)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^" 1) (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (assert) nil nil)) nil)) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "^") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) 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)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((ln_strict_increasing formula-decl nil ln_exp nil) (ln_estimate_bnd formula-decl nil ln_exp_series_alt nil) (sigma def-decl "real" sigma "reals/") (ln_estimate const-decl "real" ln_exp_series_alt nil) (real_gtm1_le1 nonempty-type-eq-decl nil ln_exp_series_alt nil) (strict_decreasing? const-decl "bool" real_fun_preds "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (ln const-decl "real" ln_exp nil) (ln_1 formula-decl nil ln_exp nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/")) nil) (ln_ineq3-2 nil 3322412713 ("" (skosimp) (("" (expand "abs") (("" (lemma "ln_strict_increasing") (("" (expand "strict_increasing?") (("" (inst - "1-px!1" "1") (("1" (rewrite "ln_1") (("1" (assert) (("1" (lemma "both_sides_plus_lt1" ("z" "ln(1-px!1)" "x" "-ln(1 - px!1)" "y" "3 * px!1 / 2")) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (simplify 1) (("1" (assert) (("1" (rewrite "inverse_add" 1) (("1" (case "px!1<=1/3") (("1" (lemma "ln_ineq1" ("xgtm1" "-px!1")) (("1" (flatten) (("1" (case "px!1/(1-px!1) <= 3*px!1/2") (("1" (assert) nil) ("2" (hide -1 -2 -4 -5 2) (("2" (lemma "both_sides_times_pos_le1" ("pz" "px!1" "x" "1/(1-px!1)" "y" "3/2")) (("2" (replace -1 1) (("2" (hide -1) (("2" (rewrite "div_mult_pos_le1" 1) (("2" (lemma "both_sides_times_neg_le1" ("nz" "-3/2")) (("2" (inst - "1/3" "px!1") (("2" (assert) nil))))))))))))))))))))) ("2" (case "1/3<px!1") (("1" (hide 1) (("1" (name "G" "lambda (x:{x:posreal| 1/3<x&x<1}): ln(1-x) + 3/2*x") (("1" (case "G(5828/10000)>0") (("1" (case "strict_decreasing?(G)") (("1" (expand "strict_decreasing?") (("1" (expand "<=" -6) (("1" (split -6) (("1" (inst - "px!1" "5828/10000") (("1" (assert) (("1" (expand "G" -2 2) (("1" (assert) nil))))))) ("2" (replace -1) (("2" (expand "G" -3) (("2" (assert) nil))))))))))) ("2" (hide -1 2 -4) (("2" (lemma "identity_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]") (("1" (lemma "deriv_id_fun[{x: posreal | 1 / 3 < x & x < 1}]") (("1" (lemma "const_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("b" "1")) (("1" (lemma "deriv_const_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("b" "1")) (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "diff_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("f1" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 1" "f2" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): x")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_diff_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("ff1" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 1" "ff2" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): x")) (("1" (replace -5) (("1" (replace -3) (("1" (expand "-") (("1" (lemma "scal_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("f" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): x" "b" "3/2")) (("1" (assert) (("1" (lemma "deriv_scal_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("ff" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): x" "b" "3/2")) (("1" (replace -7) (("1" (expand "*") (("1" (lemma "ln_derivable") (("1" (flatten) (("1" (lemma "composition_derivable_fun[{x: posreal | 1 / 3 < x & x < 1},posreal]" ("f" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 1 - x" "g" "ln")) (("1" (assert) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: posreal | 1 / 3 < x & x < 1},posreal]" ("ff" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 1 - x" "gg" "ln")) (("1" (replace -4) (("1" (replace -7) (("1" (expand "o") (("1" (expand "*") (("1" (lemma "sum_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("f1" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): ln(1 - x)" "f2" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 3 / 2 * x")) (("1" (assert) (("1" (expand "+") (("1" (lemma "deriv_sum_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("ff1" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): ln(1 - x)" "ff2" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 3 / 2 * x")) (("1" (replace -3) (("1" (replace -7) (("1" (expand "+") (("1" (replace -15) (("1" (lemma "negative_derivative[{x: posreal | 1 / 3 < x & x < 1}]" ("g" "G")) (("1" (split -1) (("1" (propax) nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "x!1") (("2" (expand "deriv" -5) (("2" (lemma "extensionality_postulate" ("f" "(LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): deriv(G, x))" "g" "(LAMBDA (x_1: {x: posreal | 1 / 3 < x & x < 1}): 3 / 2 + (1 / (1 - x_1)) * -1)")) (("1" (replace -1 -6 rl) (("1" (hide -1) (("1" (inst -5 "x!1") (("1" (replace -5) (("1" (hide-all-but (-1 -2 -3 -4 1)) (("1" (lemma "div_mult_pos_lt2" ("z" "1" "x" "3/2" "py" "1-x!1")) (("1" (assert) nil))))))))))))) ("2" (skosimp*) (("2" (typepred "x!3") (("2" (case-replace "x!3=1/2") (("1" (inst + "2/3") (("1" (assert) nil))) ("2" (inst + "1/2") (("2" (assert) nil))))))))) ("3" (skosimp*) (("3" (assert) nil))) ("4" (expand "derivable" -6) (("4" (propax) nil))))))))))))))) ("2" (propax) nil))))))))))))))))))))))))))))))))) ("2" (skosimp) (("2" (inst + "2*x!1") (("2" (assert) nil))))) ("3" (skosimp) (("3" (assert) nil))))))))))))))))))))))))))))))))))))))))))) ("2" (skosimp) (("2" (case-replace "x!1=1/2") (("1" (inst + "2/3") (("1" (assert) nil))) ("2" (inst + "1/2") (("2" (assert) nil))))))) ("3" (skosimp) (("3" (assert) nil))))))))) ("2" (hide 2 -3 -2 -4) (("2" (replace -1 1 rl) (("2" (assert) (("2" (hide -1) (("2" (lemma "ln_estimate") (("2" (inst - "19" "-5828/10000") (("2" (assert) (("2" (expand "abs" -1 2) (("2" (name-replace "DRL1" "ln(1-5828/10000)") (("2" (lemma "expt_times" ("n0x" "5828/10000" "i" "4" "j" "5")) (("2" (replace -1) (("2" (case "(5828 / 10000) ^ 4 = 1153660896461056 / 10000000000000000") (("1" (replace -1) (("1" (hide -2) (("1" (case-replace "(1153660896461056 / 10000000000000000) ^ 5 / (20 + 20 * (-5828 / 10000)) = (1153660896461056 / 10000000000000000) ^ 5 *10000/83440") (("1" (hide -1) (("1" (case-replace "(1153660896461056 / 10000000000000000) ^ 5 = 2043576321503877532268812309827579231198 (("1" (hide -1) (("1" (hide -1) (("1" (name "DRL2" "ln_estimate(-5828 / 10000, 19)") (("1" (replace -1) (("1" (case-replace "2043576321503877532268812309827579231198161568314157086599156544970504011776 / 10000000000000000000000000000000000000000000000000000000000000000000000000000000 * 10000 / 83440 = 2043576321503877532268812309827579231198161568314157086599156544970504011 /8344000000000000000000000000000000000000000000000000000000000000000000000000000 (("1" (hide -1) (("1" (expand "ln_estimate") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (case-replace "-(-5828 / 10000) = 5828/10000") (("1" (hide -1) (("1" (lemma "expt_times" ("n0x" "5828/10000")) (("1" (lemma "expt_plus" ("n0x" "5828/10000")) (("1" (rewrite "expt_x1" -3) (("1" (case "(5828 / 10000) ^ 2 = 33965584/100000000") (("1" (replace -1) (("1" (inst-cp - "1" "2") (("1" (lemma "expt_x1") (("1" (inst - "5828/10000") (("1" (replace -1) (("1" (replace -2) (("1" (replace -4) (("1" (case-replace "5828 / 10000 * (33965584 / 100000000) = 197951423552/1000000000000") (("1" (hide -1) (("1" (inst-cp - "2" "2") (("1" (replace -2) (("1" (case-replace "33965584 / 100000000 * (33965584 / 100000000) = 1153660896461056 / 10000000000000000") (("1" (hide -1) (("1" (replace -4) (("1" (inst-cp - "2" "3") (("1" (replace -2) (("1" (replace -6) (("1" (case-replace "33965584 / 100000000 * (197951423552 / 1000000000000) = 6723535704575034368/10000000000 (("1" (replace -5) (("1" (hide -1) (("1" (inst-cp - "3" "3") (("1" (replace -7) (("1" (case-replace "197951423552 / 1000000000000 * (197951423552 / 1000000000000) = 39184766086263300296704 (("1" (hide -1) (("1" (replace -4) (("1" (simplify -4) (("1" (simplify -5) (("1" (simplify -6) (("1" (simplify -7) (("1" (inst-cp - "3" "4") (("1" (replace -8) (("1" (replace -7) (("1" (simplify -4) (("1" (replace -4) (("1" (hide -9) (("1" (inst-cp - "4" "4") (("1" (replace -8) (("1" (replace -4) (("1" (inst-cp - "4" "5") (("1" (replace -8) (("1" (replace -9) (("1" (replace -4) (("1" (inst-cp - "5" "5") (("1" (replace -9) (("1" (replace -4) (("1" (inst-cp - "5" "6") (("1" (replace -9) (("1" (replace -10) (("1" (replace -4) (("1" (inst-cp - "6" "6") (("1" (replace -10) (("1" (replace -4) (("1" (case-replace "(197951423552 / 1000000000000 * (1153660896461056 / 10000000000000000)) = 228368816750742514129190912/10000000000000 (("1" (hide -1) (("1" (inst-cp - "6" "7") (("1" (replace -10) (("1" (replace -11) (("1" (replace -4) (("1" (inst-cp - "7" "7") (("1" (replace -11) (("1" (replace -4) (("1" (inst-cp - "7" "8") (("1" (replace -12) (("1" (replace -11) (("1" (replace -4) (("1" (inst-cp - "8" "8") (("1" (replace -12) (("1" (replace -4) (("1" (inst-cp - "8" "9") (("1" (replace -12) (("1" (replace -13) (("1" (replace -4) (("1" (inst-cp - "9" "9") (("1" (replace -13) (("1" (replace -4) (("1" (inst - "9" "10") (("1" (replace -12) (("1" (replace -13) (("1" (replace -3) (("1" (hide-all-but (-20 -21 1)) (("1" (expand "abs" -2) (("1" (assert) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (assert) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (assert) nil))))))))))) ("2" (assert) nil))))))))))))) ("2" (assert) nil))))))))) ("2" (assert) nil))))))))))))))))) ("2" (expand "^" 1) (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (assert) nil))))))))))))))))))) ("2" (assert) nil))))))))))))))))))))))))))))))))))))))))))))))) ("2" (assert) nil))))))))))) ("2" (hide-all-but 1) (("2" (expand "^") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (assert) nil))))))))))))))))))))) ("2" (hide-all-but 1) (("2" (assert) nil))))))))) ("2" (hide-all-but 1) (("2" (grind) nil))))))))))))))))))))))))))))))))) ("2" (assert) nil))))))))))))))))))))) ("2" (assert) nil)))))))))) nil) nil nil) (ln_ineq3-1 nil 3254163549 ("" (skosimp) (("" (expand "abs") (("" (lemma "ln_strict_increasing") (("" (expand "strict_increasing?") (("" (inst - "1-px!1" "1") (("1" (rewrite "ln_1") (("1" (assert) (("1" (lemma "both_sides_plus_lt1" ("z" "ln(1-px!1)" "x" "-ln(1 - px!1)" "y" "3 * px!1 / 2")) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (simplify 1) (("1" (assert) (("1" (rewrite "inverse_add" 1) (("1" (case "px!1<=1/3") (("1" (lemma "ln_ineq1" ("xgtm1" "-px!1")) (("1" (flatten) (("1" (case "px!1/(1-px!1) <= 3*px!1/2") (("1" (assert) nil nil) ("2" (hide -1 -2 -4 -5 2) (("2" (lemma "both_sides_times_pos_le1" ("pz" "px!1" "x" "1/(1-px!1)" "y" "3/2")) (("2" (replace -1 1) (("2" (hide -1) (("2" (rewrite "div_mult_pos_le1" 1) (("2" (lemma "both_sides_times_neg_le1" ("nz" "-3/2")) (("2" (inst - "1/3" "px!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "1/3<px!1") (("1" (hide 1) (("1" (name "G" "lambda (x:{x:posreal| 1/3<x&x<1}): ln(1-x) + 3/2*x") (("1" (case "G(5828/10000)>0") (("1" (case "strict_decreasing?(G)") (("1" (expand "strict_decreasing?") (("1" (expand "<=" -6) (("1" (split -6) (("1" (inst - "px!1" "5828/10000") (("1" (assert) (("1" (expand "G" -2 2) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "G" -3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2 -4) (("2" (lemma "identity_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]") (("1" (lemma "deriv_id_fun[{x: posreal | 1 / 3 < x & x < 1}]") (("1" (lemma "const_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("b" "1")) (("1" (lemma "deriv_const_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("b" "1")) (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "diff_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("f1" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 1" "f2" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): x")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_diff_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("ff1" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 1" "ff2" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): x")) (("1" (replace -5) (("1" (replace -3) (("1" (expand "-") (("1" (lemma "scal_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("f" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): x" "b" "3/2")) (("1" (assert) (("1" (lemma "deriv_scal_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("ff" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): x" "b" "3/2")) (("1" (replace -7) (("1" (expand "*") (("1" (lemma "ln_derivable") (("1" (flatten) (("1" (lemma "composition_derivable_fun[{x: posreal | 1 / 3 < x & x < 1},posreal]" ("f" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 1 - x" "g" "ln")) (("1" (assert) (("1" (expand "o") (("1" (lemma "deriv_comp_fun[{x: posreal | 1 / 3 < x & x < 1},posreal]" ("ff" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 1 - x" "gg" "ln")) (("1" (replace -4) (("1" (replace -7) (("1" (expand "o") (("1" (expand "*") (("1" (lemma "sum_derivable_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("f1" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): ln(1 - x)" "f2" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 3 / 2 * x")) (("1" (assert) (("1" (expand "+") (("1" (lemma "deriv_sum_fun[{x: posreal | 1 / 3 < x & x < 1}]" ("ff1" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): ln(1 - x)" "ff2" "LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): 3 / 2 * x")) (("1" (replace -3) (("1" (replace -7) (("1" (expand "+") (("1" (replace -15) (("1" (lemma "negative_derivative[{x: posreal | 1 / 3 < x & x < 1}]" ("g" "G")) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp) (("2" (typepred "x!1") (("2" (expand "deriv" -5) (("2" (lemma "extensionality_postulate" ("f" "(LAMBDA (x: {x: posreal | 1 / 3 < x & x < 1}): deriv(G, x))" "g" "(LAMBDA (x_1: {x: posreal | 1 / 3 < x & x < 1}): 3 / 2 + (1 / (1 - x_1)) * -1)")) (("1" (replace -1 -6 rl) (("1" (hide -1) (("1" (inst -5 "x!1") (("1" (replace -5) (("1" (hide-all-but (-1 -2 -3 -4 1)) (("1" (lemma "div_mult_pos_lt2" ("z" "1" "x" "3/2" "py" "1-x!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "x!3") (("2" (case-replace "x!3=1/2") (("1" (inst + "2/3") (("1" (assert) nil nil)) nil) ("2" (inst + "1/2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (expand "derivable" -6) (("4" (propax) 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)) nil)) nil)) nil) ("2" (skosimp) (("2" (inst + "2*x!1") (("2" (assert) nil nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (case-replace "x!1=1/2") (("1" (inst + "2/3") (("1" (assert) nil nil)) nil) ("2" (inst + "1/2") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2 -3 -2 -4) (("2" (replace -1 1 rl) (("2" (assert) (("2" (hide -1) (("2" (lemma "ln_series") (("2" (inst - "19" "-5828/10000") (("2" (assert) (("2" (expand "abs" -1 2) (("2" (name-replace "DRL1" "ln(1-5828/10000)") (("2" (lemma "expt_times" ("n0x" "5828/10000" "i" "4" "j" "5")) (("2" (replace -1) (("2" (case "(5828 / 10000) ^ 4 = 1153660896461056 / 10000000000000000") (("1" (replace -1) (("1" (hide -2) (("1" (case-replace "(1153660896461056 / 10000000000000000) ^ 5 / (20 + 20 * (-5828 / 10000)) = (1153660896461056 / 10000000000000000) ^ 5 *10000/83440") (("1" (hide -1) (("1" (case-replace "(1153660896461056 / 10000000000000000) ^ 5 = 2043576321503877532268812309827579231198 (("1" (hide -1) (("1" (hide -1) (("1" (name "DRL2" "ln_estimate(-5828 / 10000, 19)") (("1" (replace -1) (("1" (case-replace "2043576321503877532268812309827579231198161568314157086599156544970504011776 / 10000000000000000000000000000000000000000000000000000000000000000000000000000000 * 10000 / 83440 = 2043576321503877532268812309827579231198161568314157086599156544970504011 /8344000000000000000000000000000000000000000000000000000000000000000000000000000 (("1" (hide -1) (("1" (expand "ln_estimate") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (expand "sigma") (("1" (case-replace "-(-5828 / 10000) = 5828/10000") (("1" (hide -1) (("1" (lemma "expt_times" ("n0x" "5828/10000")) (("1" (lemma "expt_plus" ("n0x" "5828/10000")) (("1" (rewrite "expt_x1" -3) (("1" (case "(5828 / 10000) ^ 2 = 33965584/100000000") (("1" (replace -1) (("1" (inst-cp - "1" "2") (("1" (lemma "expt_x1") (("1" (inst - "5828/10000") (("1" (replace -1) (("1" (replace -2) (("1" (replace -4) (("1" (case-replace "5828 / 10000 * (33965584 / 100000000) = 197951423552/1000000000000") (("1" (hide -1) (("1" (inst-cp - "2" "2") (("1" (replace -2) (("1" (case-replace "33965584 / 100000000 * (33965584 / 100000000) = 1153660896461056 / 10000000000000000") (("1" (hide -1) (("1" (replace -4) (("1" (inst-cp - "2" "3") (("1" (replace -2) (("1" (replace -6) (("1" (case-replace "33965584 / 100000000 * (197951423552 / 1000000000000) = 6723535704575034368/10000000000 (("1" (replace -5) (("1" (hide -1) (("1" (inst-cp - "3" "3") (("1" (replace -7) (("1" (case-replace "197951423552 / 1000000000000 * (197951423552 / 1000000000000) = 39184766086263300296704 (("1" (hide -1) (("1" (replace -4) (("1" (simplify -4) (("1" (simplify -5) (("1" (simplify -6) (("1" (simplify -7) (("1" (inst-cp - "3" "4") (("1" (replace -8) (("1" (replace -7) (("1" (simplify -4) (("1" (replace -4) (("1" (hide -9) (("1" (inst-cp - "4" "4") (("1" (replace -8) (("1" (replace -4) (("1" (inst-cp - "4" "5") (("1" (replace -8) (("1" (replace -9) (("1" (replace -4) (("1" (inst-cp - "5" "5") (("1" (replace -9) (("1" (replace -4) (("1" (inst-cp - "5" "6") (("1" (replace -9) (("1" (replace -10) (("1" (replace -4) (("1" (inst-cp - "6" "6") (("1" (replace -10) (("1" (replace -4) (("1" (case-replace "(197951423552 / 1000000000000 * (1153660896461056 / 10000000000000000)) = 228368816750742514129190912/10000000000000 (("1" (hide -1) (("1" (inst-cp - "6" "7") (("1" (replace -10) (("1" (replace -11) (("1" (replace -4) (("1" (inst-cp - "7" "7") (("1" (replace -11) (("1" (replace -4) (("1" (inst-cp - "7" "8") (("1" (replace -12) (("1" (replace -11) (("1" (replace -4) (("1" (inst-cp - "8" "8") (("1" (replace -12) (("1" (replace -4) (("1" (inst-cp - "8" "9") (("1" (replace -12) (("1" (replace -13) (("1" (replace -4) (("1" (inst-cp - "9" "9") (("1" (replace -13) (("1" (replace -4) (("1" (inst - "9" "10") (("1" (replace -12) (("1" (replace -13) (("1" (replace -3) (("1" (hide-all-but (-20 -21 1)) (("1" (expand "abs" -2) (("1" (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)) 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)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "^" 1) (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (assert) nil nil)) nil)) 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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "^") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (expand "expt") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) 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)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((ln_strict_increasing formula-decl nil ln_exp nil) (sigma def-decl "real" sigma "reals/") (strict_decreasing? const-decl "bool" real_fun_preds "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (ln const-decl "real" ln_exp nil) (ln_1 formula-decl nil ln_exp nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/")) shostak)) (ln_ineq4 0 (ln_ineq4-1 nil 3254161830 ("" (skosimp*) (("" (lemma "ln_ineq1" ("xgtm1" "px!1-1")) (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (case "px!1=1") (("1" (replace -1 2) (("1" (rewrite "ln_1") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzreal_gt_m1 nonempty-type-eq-decl nil ln_exp_ineq nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (> const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (nzreal nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.547 Sekunden (vorverarbeitet am 2026-04-28) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26