| products/Sources/formale Sprachen/Roqc/parsing/ Datei vom 15.8.2025 mit Größe 9 kB |
|
Quellcode-Bibliothek ln_exp_ineq.prfSprache: Lisp |
|||||||||||||||
|
(ln_exp_ineq (noa_posreal 0 (noa_posreal-1 nil 3477843693 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst + "x!1 + 1") (("" (assert) nil nil)) nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) shostak)) (conn_posreal 0 (conn_posreal-1 nil 3477843707 ("" (expand "connected?") (("" (skosimp*) (("" (assert) nil nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (connected? const-decl "bool" deriv_domain_def "analysis/")) shostak)) (ln_ineq1_TCC1 0 (ln_ineq1_TCC1-1 nil 3254127856 ("" (grind) nil nil) nil shostak)) (ln_ineq1_TCC2 0 (ln_ineq1_TCC2-1 nil 3254127856 ("" (grind) nil nil) nil shostak)) (ln_ineq1 0 (ln_ineq1-1 nil 3253817629 ("" (skolem + "x") (("" (name "z" "1+x") (("" (name "foo" "z-1") (("" (typepred "x") (("" (replace -4) (("" (replace -4 -3 rl) (("" (replace -3 (1 -1 -2)) (("" (replace -4) (("" (replace -3 (-1 -2 1) rl) (("" (hide -3 -4) (("" (simplify -2) (("" (assert) (("" (lemma "both_sides_plus_gt1" ("z" "1" "x" "z-1" "y" "-1")) (("" (replace -1 -3 rl) (("" (simplify -3) (("" (hide -1) (("" (name "F" "LAMBDA (x:posreal): x - 1 - ln(x)") (("" (name "G" "LAMBDA (x:posreal): ln(x) - (x-1)/x") (("" (case "FORALL (x, y: posreal), (z: real): x <= z AND z <= y IMPLIES z >= 0 AND z > 0") (("1" (case "FORALL (x: posreal): EXISTS (y: posreal): x /= y") (("1" (lemma "ln_derivable") (("1" (flatten -1) (("1" (lemma "const_derivable_fun[posreal]" ("b" "1")) (("1" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "diff_derivable_fun[posreal]") (("1" (inst-cp -1 "I[posreal]" "const_fun(1)") (("1" (inst-cp - "I[posreal] - const_fun(1)" "ln") (("1" (lemma "div_derivable_fun[posreal]" ("f" "I[posreal]-const_fun(1)" "g" "I[posreal]")) (("1" (inst - "ln" "(I[posreal]-const_fun(1))/I[posreal]") (("1" (lemma "deriv_const_fun[posreal]" ("b" "1")) (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "deriv_id_fun[posreal]") (("1" (lemma "deriv_diff_fun[posreal]") (("1" (replace -10) (("1" (replace -8) (("1" (expand "-" (-4 -5 -6 -7)) (("1" (expand "/" (-4 -5)) (("1" (inst-cp - "LAMBDA (x: posreal): x" "LAMBDA (x: posreal): 1") (("1" (inst-cp - "LAMBDA (x:posreal): x - 1" "ln") (("1" (lemma "deriv_div_fun[posreal]" ("ff" "LAMBDA (x:posreal): x-1" "gg" "LAMBDA (x:posreal): x")) (("1" (inst - "ln" "LAMBDA (x:posreal): (x-1)/x") (("1" (expand "-" (-1 -2 -3 -4)) (("1" (expand "/") (("1" (expand "*") (("1" (replace -14) (("1" (replace -6) (("1" (replace -5) (("1" (simplify) (("1" (replace -4) (("1" (simplify -1) (("1" (replace -1) (("1" (simplify -2) (("1" (simplify -3) (("1" (replace -18) (("1" (replace -17) (("1" (hide-all-but (-2 -3 -8 -9 -15 -16 -17 -18 -19 -20 1)) (("1" (assert) (("1" (lemma "minimum_derivative[posreal]") (("1" (inst - "F" "1" "z") (("1" (lemma "minimum_derivative[posreal]") (("1" (inst - "G" "1" "z") (("1" (replace -3) (("1" (replace -4) (("1" (simplify -1) (("1" (simplify -2) (("1" (replace -9 -1 rl) (("1" (replace -10 -2 rl) (("1" (simplify -1) (("1" (simplify -2) (("1" (rewrite "ln_1") (("1" (simplify -2) (("1" (split -1) (("1" (split -2) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (rewrite "div_cancel1") (("2" (lemma "trich_lt" ("x" "y!1" "y" "1")) (("2" (split -1) (("1" (lemma "negreal_times_negreal_is_posreal" ("nx" "y!1-1" "ny" "y!1-1")) (("1" (lemma "both_sides_div_pos_gt1" ("x" "(y!1-1)*(y!1-1)" "y" "0" "pz" "y!1")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (propax) nil nil) ("3" (lemma "posreal_times_posreal_is_posreal" ("px" "y!1-1" "py" "y!1-1")) (("1" (lemma "both_sides_div_pos_gt1" ("x" "(y!1-1)*(y!1-1)" "y" "0" "pz" "y!1")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (rewrite "div_cancel1") (("2" (lemma "div_times" ("x" "y!1" "n0x" "1" "y" "1" "n0y" "y!1*y!1")) (("2" (replace -1 2) (("2" (simplify 2) (("2" (simplify 2) (("2" (lemma "div_cancel1" ("x" "1/y!1" "n0z" "y!1")) (("2" (rewrite "div_div2" -1) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "trich_lt" ("x" "y!1" "y" "1")) (("2" (split -1) (("1" (lemma "negreal_times_negreal_is_posreal" ("nx" "y!1-1" "ny" "y!1-1")) (("1" (lemma "both_sides_div_pos_gt1" ("pz" "y!1*y!1" "x" "(y!1-1)*(y!1-1)" "y" "0")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (propax) nil nil) ("3" (lemma "posreal_times_posreal_is_posreal" ("px" "y!1-1" "py" "y!1-1")) (("1" (lemma "both_sides_div_pos_gt1" ("pz" "y!1*y!1" "x" "(y!1-1)*(y!1-1)" "y" "0")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -9) (("2" (propax) 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) ("2" (propax) nil nil) ("3" (lemma "deriv_domain_posreal") (("3" (propax) nil 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) ((nzreal_gt_m1 nonempty-type-eq-decl nil ln_exp_ineq nil) (- const-decl "[numfield -> numfield]" 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_plus_real_is_real application-judgement "real" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_div_nzreal_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) (identity_derivable_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (I const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (div_derivable_fun formula-decl nil derivatives "analysis/") (deriv_const_fun formula-decl nil derivatives "analysis/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (div_div2 formula-decl nil real_props nil) (div_times formula-decl nil real_props nil) (trich_lt formula-decl nil real_props nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (negreal_times_negreal_is_posreal judgement-tcc nil real_types nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_div_pos_gt1 formula-decl nil real_props nil) (div_cancel1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (ln_1 formula-decl nil ln_exp nil) (connected? const-decl "bool" deriv_domain_def "analysis/") (minimum_derivative formula-decl nil derivative_props "analysis/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (nz_deriv_fun type-eq-decl nil derivatives "analysis/") (deriv_div_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_id_fun formula-decl nil derivatives "analysis/") (/ const-decl "[T -> real]" real_fun_ops "reals/") (derivable_diff application-judgement "deriv_fun" derivatives "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (id_fun_continuous name-judgement "continuous_fun[T2]" lim_of_composition "analysis/") (derivable_id name-judgement "deriv_fun" derivatives "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" indefinite_integral "analysis/") (id_fun_continuous name-judgement "continuous_fun" continuous_functions "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" unif_cont_fun "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral_step "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral_split_scaf "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral "analysis/") (derivable_const application-judgement "deriv_fun" derivatives "analysis/") (constant_seq2 application-judgement "(convergent_nz?)" convergence_ops "analysis/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (const_derivable_fun formula-decl nil derivatives "analysis/") (ln_derivable formula-decl nil ln_exp nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (both_sides_plus_gt1 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) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals 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-6 nil 3566561050 ("" (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" (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" (flatten) (("1" (hide -1) (("1" (split -1) (("1" (inst -1 "x!1") (("1" (replace -1) (("1" (lemma "div_mult_pos_lt2" ("z" "1" "x" "3/2" "py" "1-x!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (replaces -5) (("2" (decompose-equality) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst-cp + "2/3") (("2" (inst-cp + "3/4") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (lemma "deriv_domain_open") (("3" (inst - "1/3" "1") (("3" (expand "deriv_domain?") (("3" (skosimp*) (("3" (inst - "e!1" "x!3") (("3" (skosimp*) (("3" (inst + "y!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "derivable?" -6) (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "connected?") (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst-cp + "3/4") (("2" (inst-cp + "2/3") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (lemma "deriv_domain_open") (("3" (inst - "1/3" "1") (("3" (assert) (("3" (expand "deriv_domain?") (("3" (skosimp*) (("3" (inst - "e!1" "x!1") (("3" (skosimp*) (("3" (inst + "y!1") nil nil)) nil)) nil)) nil)) nil)) nil)) 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" (propax) 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" (assert) (("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" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (grind) 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) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (ln_1 formula-decl nil ln_exp nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_plus_lt1 formula-decl nil real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (ln const-decl "real" ln_exp nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (div_mult_pos_le1 formula-decl nil real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_neg_le1 formula-decl nil real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_gt_m1 nonempty-type-eq-decl nil ln_exp_ineq nil) (nzreal nonempty-type-eq-decl nil reals nil) (ln_ineq1 formula-decl nil ln_exp_ineq nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (deriv_id_fun formula-decl nil derivatives "analysis/") (deriv_const_fun formula-decl nil derivatives "analysis/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (ln_derivable formula-decl nil ln_exp nil) (composition_derivable_fun formula-decl nil chain_rule "analysis/") (O const-decl "T3" function_props nil) (sum_derivable_fun formula-decl nil derivatives "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (negative_derivative formula-decl nil derivative_props "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (NOT const-decl "[bool -> bool]" booleans nil) (extensionality_postulate formula-decl nil functions nil) (derivable? const-decl "bool" derivatives_def "analysis/") (deriv const-decl "real" derivatives_def "analysis/") (div_mult_pos_lt2 formula-decl nil real_props nil) (deriv_domain_open formula-decl nil deriv_domain "analysis/") (open_interval type-eq-decl nil intervals_real "reals/") (deriv const-decl "[T -> real]" derivatives "analysis/") (deriv_sum_fun formula-decl nil derivatives "analysis/") (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (deriv_comp_fun formula-decl nil chain_rule "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (deriv_scal_fun formula-decl nil derivatives "analysis/") (scal_derivable_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (I const-decl "(bijective?[T, T])" identity nil) (const_derivable_fun formula-decl nil derivatives "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (G skolem-const-decl "[{x: posreal | 1/3 < x & x < 1} -> real]" ln_exp_ineq nil) (strict_decreasing? const-decl "bool" real_fun_preds "reals/") (minus_even_is_even application-judgement "even_int" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (real_gtm1_le1 nonempty-type-eq-decl nil ln_exp_series_alt nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (expt_times formula-decl nil exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (^ const-decl "real" exponentiation nil) (ln_estimate const-decl "real" ln_exp_series_alt nil) (expt_plus formula-decl nil exponentiation nil) (odd_minus_even_is_odd application-judgement "odd_int" integers nil) (even_minus_even_is_even application-judgement "even_int" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (sigma_0_neg formula-decl nil sigma_nat "reals/") (even_plus_even_is_even application-judgement "even_int" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (expt def-decl "real" exponentiation nil) (expt_x1 formula-decl nil exponentiation nil) (sigma def-decl "real" sigma "reals/") (minus_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (posrat_expt application-judgement "posrat" exponentiation nil) (rat_exp application-judgement "rat" exponentiation nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (rat_plus_rat_is_rat application-judgement "rat" rationals nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}" real_defs nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (nzrat_times_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (posrat_exp application-judgement "posrat" exponentiation nil) (ln_estimate_bnd formula-decl nil ln_exp_series_alt nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (inverse_add formula-decl nil number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (px!1 skolem-const-decl "posreal" ln_exp_ineq nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (ln_strict_increasing formula-decl nil ln_exp nil)) nil) (ln_ineq3-5 nil 3566560344 ("" (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" (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" (split -1) (("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" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst-cp + "2/3") (("2" (inst-cp + "3/4") (("2" (flatten) (("2" (assert) nil))))))))))))) ("3" (hide-all-but 1) (("3" (lemma "deriv_domain_open") (("3" (inst - "1/3" "1") (("3" (expand "deriv_domain?") (("3" (skosimp*) (("3" (inst - "e!1" "x!3") (("3" (skosimp*) (("3" (inst + "y!1") nil))))))))))))))) ("4" (expand "derivable?" -6) (("4" (propax) nil))))))))))))))) ("2" (assert) (("2" (expand "connected?") (("2" (skosimp*) (("2" (assert) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst-cp + "3/4") (("2" (inst-cp + "2/3") (("2" (assert) nil))))))))) ("3" (assert) (("3" (lemma "deriv_domain_open") (("3" (inst - "1/3" "1") (("3" (assert) (("3" (expand "deriv_domain?") (("3" (skosimp*) (("3" (inst - "e!1" "x!1") (("3" (skosimp*) (("3" (inst + "y!1") 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))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("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-4 nil 3445353896 ("" (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" (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" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst-cp + "2/3") (("2" (inst-cp + "3/4") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (lemma "deriv_domain_open") (("3" (inst - "1/3" "1") (("3" (expand "deriv_domain?") (("3" (skosimp*) (("3" (inst - "e!1" "x!3") (("3" (skosimp*) (("3" (inst + "y!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "derivable?" -6) (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "connected?") (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst-cp + "3/4") (("2" (inst-cp + "2/3") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (lemma "deriv_domain_open") (("3" (inst - "1/3" "1") (("3" (assert) (("3" (expand "deriv_domain?") (("3" (skosimp*) (("3" (inst - "e!1" "x!1") (("3" (skosimp*) (("3" (inst + "y!1") nil nil)) nil)) nil)) nil)) nil)) nil)) 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)) --> -------------------- --> maximum size reached --> --------------------
¤ 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.699Bemerkung: (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-01) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26