(nn_root0 1 nil 3427098022 "" (skosimp) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil ))nil ))0 1 nil 3427098022 "" (skosimp) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil ))nil ))0 1 nil 3427098023 "" (induct "pn" )"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (skosimp*)"3" (case -replace "j!1=0" )"1" (inst + "epsilon!1" )"1" (skosimp)"1" (rewrite "expt_x1" )"1" (rewrite "expt_x1" ) nil nil )) nil ))nil ))nil )"2" (case -replace "j!1>0" )"1" (hide -3 1 )"1" case "forall (f:[nnreal->nnreal]): (FORALL (epsilon: posreal, x1: nnreal): ") "1" (inst - "lambda x: x^j!1" )"1" (replace -3 -1 )"1" (hide -3 )"1" (inst - "epsilon!1" "x1!1" )"1" (skosimp)"1" (inst + "delta!1" )"1" (skosimp)"1" (inst - "x2!1" )"1" assert )"1" expand "^" )"1" expand "expt" +)"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1 )"2" (skosimp*)"2" (inst - "_" "x1!2" )"2" (name-replace "F0" "f!1(x1!2)" )"2" (inst - "epsilon!2/(2*x1!2+4)" )"2" (skosimp)"2" "min(delta!1,min(1/4,epsilon!2 / (2*(abs(F0) + 1))))" )"2" (skosimp)"2" "x2!1" )"2" 1 )"1" case "abs(x1!2 - x2!1) <1/4" )"1" case "abs(x1!2 - x2!1) <epsilon!2 / (2 * (abs(F0) + 1))" )"1" 4 )"1" case "abs(x1!2*F0-x2!1*F0) < epsilon!2/2" )"1" 2 )"1" case "abs(x2!1*F0-x2!1*f!1(x2!1))<epsilon!2/2" )"1" 3 -4 )"1" "triangle" "x" "x1!2 * F0 - x2!1 * F0" "y" "x2!1 * F0 - x2!1 * f!1(x2!1)" ))"1" assert )nil nil ))nil ))nil )"2" 1 2 )"2" "abs_mult" "x" "x2!1" "y" "F0-f!1(x2!1)" ))"2" replace -1 )"2" 1 )"2" expand "abs" 1 )"2" "div_mult_pos_lt2" "x" "abs(F0 - f!1(x2!1))" "z" "epsilon!2 / 2" "py" "x1!2 + 2" ))"2" rewrite "div_div2" )"2" replace 1 )"2" 1 )"2" case -replace "abs(F0 - f!1(x2!1))=0" )"1" assert )nil nil )"2" "both_sides_times_pos_lt1" "pz" "abs(F0 - f!1(x2!1))" "x" "x2!1" "y" "x1!2+2" ))"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 1 1 ))"2" "div_mult_pos_lt2" "py" "abs(F0)+1" "x" "abs(x1!2 - x2!1)" "z" "epsilon!2 / 2" ))"2" rewrite "div_div2" )"2" replace -1 )"2" 1 )"2" assert )"2" rewrite "abs_mult" 1 "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" 3 1 ))"2" (grind) nil nil ))nil ))nil )"2" 2 1 ))"2" (grind) nil nil ))nil ))nil )"2" 2 )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"nnreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" exponentiation nil )"posint" nil )"real" exponentiation nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"odd_int" integers nil )nil real_props nil )"(total_order?[real])" nil )"real" reals nil )"nnreal" nil )nil real_props nil )nil real_props nil )nil real_props nil )nil real_props nil )eq -decl nil reals nil )"real" reals nil )"real" reals nil )"nzreal" nil )"bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"posreal" nil )"posrat" nil )"posreal" nil )"{z: posreal | z <= x AND z <= y}" real_defs nil )eq -decl nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"posreal" nil )"posreal" nil )nil exponentiation nil )"[T, T -> boolean]" equalities nil )"(strict_total_order?[real])" real_props nil )eq -decl nil integers nil )eq -decl nil integers nil )nil naturalnumbers nil )"real" reals nil )"nnreal" exponentiation nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )eq -decl nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil real_types nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )eq -decl nil defined_types nil )eq -decl nil naturalnumbers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))0 1 nil 3427106954 "" (skosimp) (("" (assert ) nil nil )) nil )"(total_order?[real])" nil ))nil ))0 1 nil 3427106955 "" (skosimp)"" case "forall (f:[nnreal->nnreal]): f(0) = 0 AND AND AND ") "1" (inst - "LAMBDA x: x ^ pn!1" )"1" (assert )"1" (hide 2 )"1" (split)"1" (expand "^" )"1" (expand "expt" ) (("1" (assert ) nil nil )) nil ))nil )"2" (skosimp)"2" (inst + "y!1+1" )"2" (case -replace "y!1=0" )"1" (rewrite "expt_1i" ) (("1" (assert ) nil nil ))nil )"2" "both_sides_expt_gt1_le" "gt1x" "y!1+1" "i" "1" "j" "pn!1" ))"1" (rewrite "expt_x1" )"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" (skolem + ("x!1" "y!1" ))"3" (flatten)"3" (case -replace "x!1=0" )"1" (expand "^" 1 1 )"1" (expand "expt" )"1" "expt_pos" ("px" "y!1" "i" "pn!1" ))"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" "both_sides_expt_pos_lt" "px" "x!1" "py" "y!1" "pm" "pn!1" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" (skosimp)"4" "continuous_alt_hat" "epsilon" "epsilon!1" "x1" "x1!1" "pn" "pn!1" ))"4" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 )"2" (skosimp*)"2" (expand "bijective?" )"2" (split)"1" (expand "injective?" )"1" (skosimp)"1" (lemma "trich_lt" ("x" "x1!1" "y" "x2!1" ))"1" (split -1 )"1" (inst -5 "x1!1" "x2!1" )"1" (assert ) nil nil )) nil )"2" (propax) nil nil )"3" (inst -5 "x2!1" "x1!1" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "surjective?" )"2" (skosimp)"2" (name "BELOW" "{x:real| 0<= x & f!1(x)<= y!1}" )"1" (case "nonempty?(BELOW)" )"1" (case "bounded_above?(BELOW)" )"1" (lemma "lub_exists" ("SA" "BELOW" ))"1" (skosimp)"1" "lub_lem" "x" "x!1" "SA" "BELOW" ))"1" assert )"1" case "x!1>=0" )"1" "x!1" )"1" expand "least_upper_bound?" )"1" "1" expand "upper_bound?" )"1" "trich_lt" "x" "f!1(x!1)" "y" "y!1" ))"1" 1 )"1" expand "abs" -12 )"1" 12 "x!1" "y!1-f!1(x!1)" )"1" "1" 12 "x!1+delta!1/2" )"1" 11 "x!1" "x!1+delta!1/2" )"1" assert )"1" 4 "delta!1 / 2 + x!1" )"1" assert )nil nil )"2" expand "BELOW" )"2" nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" (propax) nil nil )"3" 1 )"3" "y!1" )"3" expand ">=" -3 )"3" expand "<=" -3 )"3" 3 )"1" 13 "x!1" "f!1(x!1)-y!1" )"1" "1" 13 "max(x!1/2,x!1-delta!1/2)" )"1" case "max(x!1 / 2, x!1 - delta!1 / 2)>0 & x!1>max(x!1 / 2, x!1 - delta!1 / 2) & x!1 - max(x!1 / 2, x!1 - delta!1 / 2)<delta!1" )"1" "1" expand "abs" )"1" assert )"1" 15 " max(x!1 / 2, x!1 - delta!1 / 2)" "x!1" )"1" assert )"1" 9 "max(x!1 / 2, x!1 - delta!1 / 2)" )"1" assert )"1" "1" "s!1" )"1" expand "BELOW" )"1" "1" 16 "max(x!1 / 2, x!1 - delta!1 / 2)" "s!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "max" )"2" case -replace "x!1 / 2 < x!1 - delta!1 / 2" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil )"2" expand "max" )"2" case -replace "x!1 / 2 < x!1 - delta!1 / 2" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil )"2" replace 1 "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "least_upper_bound?" )"2" "2" expand "upper_bound?" )"2" "0" )"1" (assert ) nil nil )"2" expand "BELOW" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" (hide 2 )"2" (expand "bounded_above?" )"2" (expand "upper_bound?" )"2" 4 "y!1" )"2" "2" "x!1" )"2" "2" "s!1" )"2" expand "BELOW" )"2" "2" 7 "x!1" "s!1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (propax) nil nil ))nil )"2" (hide-all-but (-2 -4 1 ))"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (inst - "0" )"2" expand "member" )"2" expand "BELOW" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" functions nil )"[numfield, numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )eq -decl nil number_fields nil )eq -decl nil real_types nil )eq -decl nil real_types nil )"bool" reals nil ) (> const-decl "bool" reals nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[bool, bool -> bool]" booleans nil )eq -decl nil real_types nil )"bool" reals nil )eq -decl nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"nat" exponentiation nil )"real" exponentiation nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nat" exponentiation nil )"int" integers nil )"posreal" nil )"[numfield, numfield -> numfield]" number_fields nil )nil exponentiation nil )"posreal" nil )"(total_order?[real])" nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )nil exponentiation nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )nil nn_root nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )eq -decl nil integers nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )eq -decl nil integers nil )eq -decl nil integers nil )"nnreal" exponentiation nil )nil real_props nil )"bool" functions nil )set type-eq -decl nil sets nil )"bool" sets nil )1 skolem-const-decl "(BELOW)" nn_root nil )nil bounded_real_defs nil )nil bounded_real_defs nil )"bool" bounded_real_defs nil )"bool" bounded_real_defs nil )1 skolem-const-decl "nnreal" nn_root nil )1 skolem-const-decl "[nnreal -> nnreal]" nn_root nil )"posreal" nil )"real" reals nil )eq -decl nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )1 skolem-const-decl "posreal" nn_root nil )"nzreal" nil )"real" reals nil )"[real -> boolean]" nn_root nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )1 skolem-const-decl "posreal" nn_root nil )1 skolem-const-decl "(BELOW)" nn_root nil )1 skolem-const-decl "real" nn_root nil )"(total_order?[real])" nil )"bool" bounded_real_defs nil )"bool" sets nil )"bool" sets nil )"bool" reals nil )"bool" functions nil ))0 1 nil 3427173466 "" (skosimp)"" (expand "nn_root" )"" (lemma "hat_bijective" ("pn" "pn!1" ))"" "bijective_inverse[nnreal, nnreal]" "f" "LAMBDA x: x ^ pn!1" "x" "0" "y" "0" ))"1" (replace -1 )"1" (assert )"1" (expand "^" )"1" (expand "expt" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"nnreal" nn_root nil )eq -decl nil real_types nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" functions nil )nil function_inverse nil )"nnreal" exponentiation nil )"nat" exponentiation nil )"real" exponentiation nil )"nnreal" nil )"nnreal" exponentiation nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nat" exponentiation nil )"int" integers nil )nil nn_root nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )eq -decl nil integers nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil ))0 1 nil 3427176918 "" (skosimp)"" (expand "nn_root" )"" (lemma "hat_bijective" ("pn" "pn!1" ))"" "bijective_inverse[nnreal, nnreal]" "f" "LAMBDA x: x ^ pn!1" "x" "1" "y" "1" ))"1" (assert ) (("1" (rewrite "expt_1i" ) nil nil )) nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"nnreal" nn_root nil )eq -decl nil real_types nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" functions nil )nil function_inverse nil )"nnreal" exponentiation nil )nil exponentiation nil )"posint" exponentiation nil )nil nn_root nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )eq -decl nil integers nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil ))0 1 nil 3427170363 "" (skosimp)"" (expand "nn_root" )"" (lemma "hat_bijective" ("pn" "1" ))"" "bijective_inverse[nnreal, nnreal]" "f" "LAMBDA x: x ^ 1" "y" "x!1" "x" "x!1" ))"1" (replace -1 )"1" (hide -1 )"1" (assert ) (("1" (rewrite "expt_x1" ) nil nil )) nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"nnreal" nn_root nil )eq -decl nil real_types nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"bool" functions nil )nil function_inverse nil )"nnreal" exponentiation nil )nil exponentiation nil )nil nn_root nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )eq -decl nil integers nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil ))0 1 nil 3427172270 "" (skosimp)"" (expand "nn_root" )"" (lemma "hat_bijective" ("pn" "pn!1" ))"" "LOW" "inverse[nnreal, nnreal](LAMBDA x: x ^ pn!1)(x!1)" )"" "HIGH" "inverse[nnreal, nnreal](LAMBDA x: x ^ pn!1)(y!1)" )"" (replace -1 )"" (replace -2 )"" "surjective_inverse[nnreal, nnreal]" "f" "LAMBDA x: x ^ pn!1" ))"1" (inst-cp - "HIGH" "y!1" )"1" (inst - "LOW" "x!1" )"1" (assert )"1" (replace -1 )"1" (replace -2 )"1" (hide-all-but (-6 1 ))"1" case -replace "LOW=0" )"1" (assert ) nil nil )"2" "both_sides_expt_pos_lt" "px" "LOW" "py" "HIGH" "pm" "pn!1" ))"1" (assert ) nil nil )"2" assert )"2" case -replace "HIGH=0" )"1" expand "^" -2 )"1" expand "expt" )"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "bijective?" ) (("2" (flatten) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"nnreal" nn_root nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )"D" function_inverse nil )eq -decl nil real_types nil )"[T, T -> boolean]" equalities nil )"nnreal" exponentiation nil )nil function_inverse nil )"bool" functions nil )nil exponentiation nil )eq -decl nil real_types nil )eq -decl nil real_types nil )"(strict_total_order?[real])" real_props nil )"real" exponentiation nil )"nnreal" nil )"nnreal" exponentiation nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nat" exponentiation nil )"(strict_total_order?[real])" real_props nil )"bool" functions nil )nil nn_root nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )eq -decl nil integers nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil ))0 1 nil 3427190654 "" (skosimp)"" (lemma "hat_bijective" ("pn" "pn!1" ))"" "bijective_inverse[nnreal, nnreal]" "f" "LAMBDA x: x ^ pn!1" ))"1" (expand "nn_root" )"1" (inst - "x!1" "x!1^pn!1" ) (("1" (assert ) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"nnreal" nn_root nil )"nnreal" exponentiation nil )nil function_inverse nil )"bool" functions nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )eq -decl nil real_types nil ))0 1 nil 3427190653 ("" (subtype-tcc) nil nil )"real" exponentiation nil )"D" function_inverse nil )"nnreal" nn_root nil ))nil ))0 1 nil 3427190771 "" (skosimp)"" (lemma "hat_bijective" ("pn" "pn!1" ))"" "bijective_inverse[nnreal, nnreal]" "f" "LAMBDA x: x ^ pn!1" ))"1" (expand "nn_root" )"1" (assert )"1" "inverse[nnreal, nnreal](LAMBDA x: x ^ pn!1)(x!1)" "x!1" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"nnreal" nn_root nil )"D" function_inverse nil )"nnreal" exponentiation nil )nil function_inverse nil )"bool" functions nil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )eq -decl nil real_types nil ))0 1 nil 3427191722 "" (skosimp)"" (lemma "expt_nn_root" ("x" "x!1" "pn" "pn!1" ))"" (split)"1" (flatten)"1" (replace -1 )"1" (expand "^" )"1" (expand "expt" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (flatten)"2" (replace -1 ) (("2" (rewrite "nn_root_0n" ) nil nil ))nil ))nil ))nil ))nil ))nil )eq -decl nil real_types nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )nil nn_root nil )"real" exponentiation nil )"int" integers nil )"nat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"real" exponentiation nil ))0 1 nil 3427191965 "" (skosimp)"" (lemma "nn_root_is_0" ("x" "px!1" "pn" "pn!1" ))"" (assert ) nil nil )) nil ))nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"(strict_total_order?[real])" real_props nil ))0 1 nil 3427192123 "" (skosimp)"" (split)"1" (flatten)"1" "both_sides_expt_pos_lt" "px" "1" "py" "nn_root(x!1, pn!1)" "pm" "pn!1" ))"1" (rewrite "expt_1i" )"1" (assert )"1" (rewrite "expt_nn_root" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (flatten)"2" "nn_root_strict_increasing" "x" "1" "y" "x!1" "pn" "pn!1" ))"2" (rewrite "nn_root_1n" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"nnreal" nn_root nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )"nnreal" exponentiation nil )"(strict_total_order?[real])" real_props nil )nil nn_root nil )nil exponentiation nil )nil nn_root nil )nil nn_root nil ))0 1 nil 3427192355 "" (skosimp)"" (lemma "nn_root_gt1" ("x" "x!1" "pn" "pn!1" ))"" (lemma "nn_root_1n" ("pn" "pn!1" ))"" (lemma "trich_lt" ("x" "x!1" "y" "1" ))"" (split -1 )"1" (assert )"1" (hide -2 1 )"1" (case -replace "x!1=0" )"1" (rewrite "nn_root_0n" ) nil nil )"2" (lemma "nn_root_pos" ("px" "x!1" "pn" "pn!1" ))"1" "both_sides_expt_pos_lt" "px" "nn_root(x!1, pn!1)" "py" "1" "pm" "pn!1" ))"1" (rewrite "expt_1i" )"1" (rewrite "expt_nn_root" )"1" (assert ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )eq -decl nil real_types nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"[T, T -> boolean]" equalities nil )nil nn_root nil )nil exponentiation nil )"nnreal" nn_root nil )nil nn_root nil )nil exponentiation nil )eq -decl nil real_types nil )eq -decl nil real_types nil )nil nn_root nil )nil nn_root nil ))0 1 nil 3427219585 "" (skosimp)"" "both_sides_expt2" "px" "nn_root(x!1 * y!1, pn!1)" "py" "nn_root(x!1, pn!1) * nn_root(y!1, pn!1)" "n0i" "pn!1" ))"1" (replace -1 1 rl)"1" (hide -1 )"1" (rewrite "expt_nn_root" )"1" (case -replace "x!1=0" )"1" (rewrite "nn_root_0n" )"1" (expand "^" +)"1" (expand "expt" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (lemma "nn_root_pos" ("px" "x!1" "pn" "pn!1" ))"1" (case -replace "y!1=0" )"1" (rewrite "nn_root_0n" )"1" (expand "^" 2 )"1" (expand "expt" ) (("1" (assert ) nil nil ))nil ))nil ))nil )"2" (lemma "nn_root_pos" ("px" "y!1" "pn" "pn!1" ))"1" (rewrite "mult_expt" )"1" (rewrite "expt_nn_root" )"1" (rewrite "expt_nn_root" ) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (case -replace "y!1=0" )"1" (rewrite "nn_root_0n" ) (("1" (assert ) nil nil )) nil )"2" (lemma "nn_root_pos" ("px" "y!1" "pn" "pn!1" ))"1" (case -replace "x!1=0" )"1" (rewrite "nn_root_0n" ) (("1" (assert ) nil nil )) nil )"2" (lemma "nn_root_pos" ("px" "x!1" "pn" "pn!1" ))"1" "posreal_times_posreal_is_posreal" "px" "nn_root(x!1, pn!1)" "py" "nn_root(y!1, pn!1)" ))"1" (propax) nil nil ) ("2" (propax) nil nil )"3" (propax) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"3" (case -replace "x!1=0" )"1" (rewrite "nn_root_0n" ) (("1" (assert ) nil nil )) nil )"2" (case -replace "y!1=0" )"1" (rewrite "nn_root_0n" ) (("1" (assert ) nil nil )) nil )"2" "posreal_times_posreal_is_posreal" "px" "x!1" "py" "y!1" ))"1" (lemma "nn_root_pos" ("px" "x!1*y!1" "pn" "pn!1" ))"1" (propax) nil nil ) ("2" (propax) nil nil )) nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )eq -decl nil number_fields nil )"nnreal" nn_root nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"boolean" notequal nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil exponentiation nil )"nnreal" nil )"(strict_total_order?[real])" real_props nil )"[T, T -> boolean]" equalities nil )"real" exponentiation nil )"real" exponentiation nil )nil nn_root nil )"int" integers nil )"nat" exponentiation nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )eq -decl nil reals nil )nil exponentiation nil )"nnreal" exponentiation nil )nil nn_root nil )nil nn_root nil )nil real_typesnil ))0 1 nil 3427220519 "" (skosimp)"" (lemma "nn_root_pos" ("px" "px!1" "pn" "pn!1" ))"" (assert ) nil nil )) nil ))nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"(strict_total_order?[real])" real_props nil ))nil ))0 1 nil 3427220740 "" (skosimp)"" (lemma "nn_root_pos" ("px" "px!1" "pn" "pn!1" ))"" (lemma "nn_root_pos" ("px" "1/px!1" "pn" "pn!1" ))"" (rewrite "div_cancel4" +)"" (rewrite "mult_nn_root" + :dir rl)"" (assert )"" (rewrite "div_cancel2" )"" (rewrite "nn_root_1n" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )nil real_props nil )eq -decl nil reals nil )eq -decl nil real_types nil )"nnreal" nn_root nil )"nnreal" nil )"(strict_total_order?[real])" real_props nil )nil nn_root nil )nil real_props nil )"posreal" nil )nil nn_root nil )"posreal" nil )eq -decl nil number_fields nil )"boolean" notequal nil )eq -decl nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil ))0 1 nil 3427220520 "" (skosimp)"" (lemma "inv_nn_root" ("px" "py!1" "pn" "pn!1" ))"" "mult_nn_root" ("x" "x!1" "y" "1 / py!1" "pn" "pn!1" ))"" (assert ) nil nil )) nil ))nil ))nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"real" reals nil )"nnreal" nil )"nzreal" nil )"nnreal" nil )"posreal" nil )nil nn_root nil )eq -decl nil real_types nil )eq -decl nil number_fields nil )"boolean" notequal nil )eq -decl nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil ))0 1 nil 3427263236 "" (skosimp)"" (case -replace "x!1=0" )"1" (rewrite "nn_root_0n" )"1" (rewrite "nn_root_0n" )"1" (rewrite "nn_root_0n" ) nil nil )) nil ))nil )"2" (lemma "nn_root_pos" ("px" "x!1" "pn" "pn!1*pm!1" ))"1" (lemma "nn_root_pos" ("px" "x!1" "pn" "pn!1" ))"1" "nn_root_pos" "px" "nn_root(x!1, pn!1)" "pn" "pm!1" ))"1" "both_sides_expt2" "px" "nn_root(x!1, pn!1 * pm!1)" "py" "nn_root(nn_root(x!1, pn!1), pm!1)" "n0i" "pn!1*pm!1" ))"1" (replace -1 2 rl)"1" (hide -1 )"1" (rewrite "expt_nn_root" )"1" "expt_times" "n0x" "nn_root(nn_root(x!1, pn!1), pm!1)" "i" "pm!1" "j" "pn!1" ))"1" (replace -1 )"1" (rewrite "expt_nn_root" )"1" (rewrite "expt_nn_root" ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )eq -decl nil number_fields nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nn_root nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"posint" nil )nil exponentiation nil )"boolean" notequal nil )eq -decl nil integers nil )nil exponentiation nil )eq -decl nil reals nil )nil nn_root nil )"nnreal" nn_root nil )"(strict_total_order?[real])" real_props nil )nil nn_root nil )eq -decl nil real_types nil )eq -decl nil real_types nil ))0 1 nil 3427219471 "" (skosimp)"" (lemma "nn_root_pos" ("px" "x!1" "pn" "pn!1" ))"1" (lemma "nn_root_pos" ("px" "x!1" "pn" "pm!1" ))"1" "both_sides_expt_pos_lt" "px" "nn_root(x!1, pn!1)" "py" "nn_root(x!1, pm!1)" "pm" "pn!1" ))"1" (rewrite "expt_nn_root" )"1" (replace -1 1 rl)"1" (hide -1 )"1" (lemma "nn_root_lt1" ("x" "x!1" "pn" "pm!1" ))"1" (assert )"1" (hide -3 )"1" "both_sides_expt_lt1_lt" "lt1x" "nn_root(x!1, pm!1)" "i" "pm!1" "j" "pn!1" ))"1" (rewrite "expt_nn_root" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"(strict_total_order?[real])" real_props nil )"nnreal" nn_root nil )nil exponentiation nil )nil nn_root nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil exponentiation nil )"(strict_total_order?[real])" real_props nil )"nnreal" exponentiation nil )nil nn_root nil ))0 1 nil 3427219122 "" (skosimp)"" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "x!1" ))"1" "both_sides_times_pos_lt1" "pz" "x!1" "x" "1/x!1" "y" "1" ))"1" (rewrite "div_cancel2" )"1" (assert )"1" "nn_root_increasing" "x" "1/x!1" "pn" "pn!1" "pm" "pm!1" ))"1" (assert )"1" (rewrite "inv_nn_root" )"1" (rewrite "inv_nn_root" )"1" "nn_root_pos" ("px" "x!1" "pn" "pn!1" ))"1" "nn_root_pos" ("px" "x!1" "pn" "pm!1" ))"1" (rewrite "both_sides_div_pos_lt2" -3 ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )eq -decl nil real_types nil )eq -decl nil real_types nil )"bool" reals nil )eq -decl nil real_types nil )"bool" reals nil )eq -decl nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_types nil )"(strict_total_order?[real])" real_props nil )eq -decl nil reals nil )nil real_props nil )nil nn_root nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )eq -decl nil integers nil )eq -decl nil integers nil )eq -decl nil integers nil )"(total_order?[real])" nil )nil nn_root nil )nil nn_root nil )"nnreal" nn_root nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"nzreal" nil )nil real_props nil )eq -decl nil number_fields nil )"boolean" notequal nil )eq -decl nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil ))0 1 nil 3429505681 "" (skosimp)"" "both_sides_expt_pos_le" "py" "1 + px!1 / pn!1" "px" "nn_root(1 + px!1, pn!1)" "pm" "pn!1" ))"1" (rewrite "expt_nn_root" )"1" (replace -1 1 rl)"1" (hide -1 )"1" "expt_lower_bound" ("px" "px!1/pn!1" "n" "pn!1" ))"1" (expand "^" ) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )"2" (hide 2 ) (("2" (rewrite "nn_root_pos" ) nil nil )) nil ))nil ))nil )"[numfield, nznum -> numfield]" number_fields nil )eq -decl nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )eq -decl nil number_fields nil )"nnreal" nn_root nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil exponentiation nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )nil exponentiation_aux nil )eq -decl nil naturalnumbers nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"posreal" nil )"(total_order?[real])" nil )"real" exponentiation nil )"posreal" nil )nil nn_root nil )nil nn_root nil ))0 1 nil 3427522760 "" (skosimp)"" "bij_inv_is_bij[nnreal, nnreal]" ("f" "lambda x: x^pn!1" ))"" (rewrite "hat_bijective" )"" (expand "nn_root" )"" (assert )"" case -replace "(LAMBDA x: LAMBDA (x_1: nnreal): x_1 ^ pn!1 )(x))=inverse[nnreal, nnreal](LAMBDA x: x ^ pn!1 )") "" (hide 2 )"" (apply -extensionality :hide? t) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )eq -decl nil real_types nil )"bool" reals nil )eq -decl nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil function_inverse nil )"nnreal" exponentiation nil )"nnreal" nn_root nil )"D" function_inverse nil )"[T, T -> boolean]" equalities nil )nil nn_root nil ))0 1 nil 3427522973 "" (skosimp)"" (case -replace "x1!1=0" )"1" (rewrite "nn_root_0n" )"1" (inst + "epsilon!1^pn!1" )"1" (skosimp)"1" (case -replace "x2!1=0" )"1" (rewrite "nn_root_0n" )"1" (expand "abs" ) (("1" (assert ) nil nil )) nil ))nil )"2" (case "x2!1>0" )"1" (hide 1 -2 )"1" (lemma "nn_root_pos" ("px" "x2!1" "pn" "pn!1" ))"1" (expand "abs" )"1" (assert )"1" "both_sides_expt_pos_lt" "px" "nn_root(x2!1, pn!1)" "py" "epsilon!1" "pm" "pn!1" ))"1" (rewrite "expt_nn_root" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (case "x1!1>0" )"1" (hide 1 )"1" (name "X_max" "(nn_root(x1!1, pn!1)+epsilon!1)^pn!1" )"1" case "forall (y:nnreal): x1!1<y & y <X_max => abs(nn_root(x1!1, pn!1) - nn_root(y, pn!1)) < epsilon!1" )"1" "X_min" "if nn_root(x1!1, pn!1) <= epsilon!1 then 0 else (nn_root(x1!1, pn!1) - epsilon!1) ^ pn!1 endif" )"1" case "FORALL (y: nnreal): 1 =>1 , pn!1 ) - nn_root(y, pn!1 )) < epsilon!1 ") "1" (case "X_max> x1!1" )"1" (case "x1!1>X_min & X_min>=0" )"1" (flatten)"1" (inst + "min(x1!1-X_min,X_max-x1!1)" )"1" (skosimp)"1" "trich_lt" "x" "x1!1" "y" "x2!1" ))"1" 1 )"1" 7 "x2!1" )"1" (assert ) nil nil ))nil )"2" replace -1 )"2" assert )"2" expand "abs" )"2" (assert ) nil nil ))nil ))nil ))nil )"3" 5 "x2!1" )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "min" )"2" assert )"2" case -replace "x1!1 - X_min > X_max - x1!1" )"1" (assert ) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2 2 -4 )"2" case -replace "nn_root(x1!1, pn!1) <= epsilon!1" )"1" (assert ) nil nil )"2" (assert )"2" (split 2 )"1" replace -2 1 rl)"1" 2 -3 2 )"1" "both_sides_expt_pos_lt" "px" "nn_root(x1!1, pn!1) - epsilon!1" "py" "nn_root(x1!1, pn!1)" "pm" "pn!1" ))"1" rewrite "expt_nn_root" )"1" expand ">" 1 )"1" replace -1 1 )"1" 1 )"1" "nn_root_strict_increasing" "x" "x1!1" "y" "X_max" "pn" "pn!1" ))"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "expt_pos" "px" "nn_root(x1!1, pn!1) - epsilon!1" "i" "pn!1" ))"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 -1 -3 )"2" (hide -1 )"2" "nn_root_pos" "px" "x1!1" "pn" "pn!1" ))"1" "expt_pos" "px" "nn_root(x1!1, pn!1) + epsilon!1" "i" "pn!1" ))"1" case "nn_root(x1!1, pn!1) + epsilon!1=nn_root(X_max,pn!1)" )"1" replace -4 )"1" "both_sides_expt_pos_lt" "px" "nn_root(x1!1, pn!1)" "py" "nn_root(X_max, pn!1)" "pm" "pn!1" ))"1" assert )"1" rewrite "expt_nn_root" )"1" rewrite "expt_nn_root" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" rewrite "nn_root_pos" )nil nil )"3" (propax) nil nil ))nil ))nil )"2" 2 )"2" replace -3 1 rl)"2" rewrite "nn_root_expt" )nil nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2 )"2" (case "X_min>=0" )"1" (hide -3 -4 )"1" (skosimp)"1" "nn_root_strict_increasing" "y" "x1!1" "x" "y!1" "pn" "pn!1" ))"1" (assert )"1" expand "abs" 1 )"1" case -replace "nn_root(x1!1, pn!1) <= epsilon!1" )"1" "nn_root_pos" "px" "y!1" "pn" "pn!1" ))"1" (assert ) nil nil ))nil )"2" replace 1 )"2" assert )"2" replace -5 * rl)"2" "nn_root_strict_increasing" "x" "(nn_root(x1!1, pn!1) - epsilon!1) ^ pn!1" "y" "y!1" "pn" "pn!1" ))"2" assert )"2" rewrite "nn_root_expt" 1 )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case -replace "nn_root(x1!1, pn!1) <= epsilon!1" )"1" (assert ) nil nil )"2" (assert )"2" case "nn_root(x1!1, pn!1) > epsilon!1" )"1" (hide 1 )"1" "expt_pos" "px" "nn_root(x1!1, pn!1) - epsilon!1" "i" "pn!1" ))"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2 )"2" (skosimp)"2" (replace -3 -2 rl)"2" (hide -3 )"2" "nn_root_strict_increasing" "x" "x1!1" "y" "y!1" "pn" "pn!1" ))"2" (assert )"2" (expand "abs" )"2" "nn_root_strict_increasing" "x" "y!1" "y" "(nn_root(x1!1, pn!1) + epsilon!1) ^ pn!1" "pn" "pn!1" ))"2" assert )"2" rewrite "nn_root_expt" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil real_types nil )"real" reals nil )"odd_int" integers nil )"(total_order?[real])" nil )"posreal" exponentiation nil )"nzreal" exponentiation nil )"real" exponentiation nil )"boolean" notequal nil )OR const-decl "[bool, bool -> bool]" booleans nil )eq -decl nil real_types nil )eq -decl nil real_types nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"(strict_total_order?[real])" real_props nil )nil exponentiation nil )"nnreal" nn_root nil )nil nn_root nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )nil nn_root nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nn_root nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nnreal" exponentiation nil )nil nn_root nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )1 skolem-const-decl "nnreal" nn_root nil )"real" nn_root nil )"posreal" nn_root nil )nil real_props nil )nil nn_root nil )nil exponentiation nil )NOT const-decl "[bool -> bool]" booleans nil )"(total_order?[real])" nil )"bool" reals nil )IF const-decl "[boolean, T, T -> T]" if_def nil )"posreal" nil )eq -decl nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil ))0 1 nil 3430536267 "" (skosimp)"" (split)"1" (flatten)"1" (case -replace "x!1=y!1" )"1" (assert ) nil nil )"2" "nn_root_strict_increasing" "x" "y!1" "y" "x!1" "pn" "pn!1" ))"2" (assert ) nil nil )) nil ))nil ))nil )"2" (flatten)"2" "nn_root_strict_increasing" "y" "y!1" "x" "x!1" "pn" "pn!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil real_types nil )"(strict_total_order?[real])" real_props nil )nil nn_root nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )eq -decl nil integers nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil ))0 1 nil 3430536347 "" (skosimp)"" (split)"1" (flatten)"1" (expand "<=" 1 )"1" (flatten)"1" "nn_root_strict_increasing" "x" "y!1" "y" "x!1" "pn" "pn!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "<=" )"2" (flatten)"2" (split)"1" "nn_root_strict_increasing" "y" "y!1" "x" "x!1" "pn" "pn!1" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )eq -decl nil real_types nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))0 1 nil 3430536079 "" (skosimp)"" "both_sides_nn_root_lt" ("x" "y!1" "y" "x!1" "pn" "pn!1" ))"" (assert )"" (split)"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )eq -decl nil real_types nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))0 1 nil 3430536144 "" (skosimp)"" "both_sides_nn_root_le" ("x" "y!1" "y" "x!1" "pn" "pn!1" ))"" (split)"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )eq -decl nil real_types nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))0 1 nil 3430536171 "" (skosimp)"" (lemma "trich_lt" ("x" "x!1" "y" "y!1" ))"" (split)"1" "both_sides_nn_root_lt" "x" "x!1" "y" "y!1" "pn" "pn!1" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil )"3" "both_sides_nn_root_lt" "y" "x!1" "x" "y!1" "pn" "pn!1" ))"3" (assert ) nil nil )) nil ))nil ))nil ))nil )eq -decl nil real_types nil )"bool" reals nil )eq -decl nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil nn_root nil )"(strict_total_order?[real])" real_props nil ))0 1 nil 3430536749 "" (skosimp)"" (split)"1" (flatten)"1" (case -replace "pn!1=pm!1" )"1" (assert ) nil nil )"2" "nn_root_increasing" "pn" "pm!1" "pm" "pn!1" "x" "lt1x!1" ))"2" (assert ) nil nil )) nil ))nil ))nil )"2" (flatten)"2" "nn_root_increasing" "pm" "pm!1" "pn" "pn!1" "x" "lt1x!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )eq -decl nil integers nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"(strict_total_order?[real])" real_props nil )nil nn_root nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil real_types nil )"bool" reals nil ))0 1 nil 3430536810 "" (skosimp)"" (split)"1" (flatten)"1" "nn_root_increasing" "pn" "pm!1" "pm" "pn!1" "x" "lt1x!1" ))"1" (assert ) nil nil )) nil ))nil )"2" (flatten)"2" (expand "<=" )"2" (flatten)"2" (split)"1" "nn_root_increasing" "pm" "pm!1" "pn" "pn!1" "x" "lt1x!1" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil booleans nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" reals nil ))0 1 nil 3430536863 "" (skosimp)"" "both_sides_nn_root_lt1_lt" "pn" "pm!1" "pm" "pn!1" "lt1x" "lt1x!1" ))"" (flatten)"" (split) (("1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil )eq -decl nil integers nil )eq -decl nil integers nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )eq -decl nil real_types nil )"bool" reals nil )eq -decl nil real_types nil )"bool" reals nil )eq -decl nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))0 1 nil 3430536903 "" (skosimp)"" "both_sides_nn_root_lt1_le" "pn" "pm!1" "pm" "pn!1" "lt1x" "lt1x!1" ))"" (flatten)"" (split) (("1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil )eq -decl nil integers nil )eq -decl nil integers nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )eq -decl nil real_types nil )"bool" reals nil )eq -decl nil real_types nil )"bool" reals nil )eq -decl nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))0 1 nil 3430537267 "" (skosimp)"" (split)"1" (flatten)"1" (case -replace "pm!1=pn!1" )"1" (assert ) nil nil )"2" "nn_root_decreasing" "pn" "pn!1" "pm" "pm!1" "x" "gt1x!1" ))"2" (assert ) nil nil )) nil ))nil ))nil )"2" (flatten)"2" "nn_root_decreasing" "pm" "pn!1" "pn" "pm!1" "x" "gt1x!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )eq -decl nil integers nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )"(strict_total_order?[real])" real_props nil )nil nn_root nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil real_types nil ))0 1 nil 3430537333 "" (skosimp)"" (expand "<=" )"" (split)"1" (flatten)"1" "nn_root_decreasing" "pn" "pn!1" "pm" "pm!1" "x" "gt1x!1" ))"1" (assert ) nil nil )) nil ))nil )"2" (flatten)"2" (split)"1" "nn_root_decreasing" "pm" "pn!1" "pn" "pm!1" "x" "gt1x!1" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )"(strict_total_order?[real])" real_props nil )nil nn_root nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )eq -decl nil integers nil )eq -decl nil booleans nil )"bool" reals nil )eq -decl nil integers nil )"bool" reals nil )eq -decl nil integers nil )eq -decl nil real_types nil )eq -decl nil real_types nil )eq -decl nil real_types nil ))0 1 nil 3430537395 "" (skosimp)"" "both_sides_nn_root_gt1_lt" "gt1x" "gt1x!1" "pm" "pn!1" "pn" "pm!1" ))"" (flatten)"" (split) (("1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil )eq -decl nil integers nil )eq -decl nil integers nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )eq -decl nil real_types nil )"bool" reals nil )eq -decl nil real_types nil )"bool" reals nil )eq -decl nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))0 1 nil 3430537435 "" (skosimp)"" "both_sides_nn_root_gt1_le" "gt1x" "gt1x!1" "pm" "pn!1" "pn" "pm!1" ))"" (flatten)"" (split) (("1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil ))nil ))nil )eq -decl nil integers nil )eq -decl nil integers nil )eq -decl nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )eq -decl nil real_types nil )"bool" reals nil )eq -decl nil real_types nil )"bool" reals nil )eq -decl nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))0 1 nil 3430537455 "" (skosimp)"" (split)"1" (flatten)"1" (case "x!1<1" )"1" "both_sides_nn_root_lt1_le" "pm" "pm!1" "pn" "pn!1" "lt1x" "x!1" ))"1" "both_sides_nn_root_lt1_ge" "pm" "pm!1" "pn" "pn!1" "lt1x" "x!1" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil )"2" "both_sides_nn_root_gt1_le" "pm" "pm!1" "pn" "pn!1" "gt1x" "x!1" ))"1" "both_sides_nn_root_gt1_ge" "pm" "pm!1" "pn" "pn!1" "gt1x" "x!1" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (flatten)"2" (split)"1" (replace -1 )"1" (rewrite "nn_root_0n" )"1" (rewrite "nn_root_0n" ) nil nil )) nil ))nil )"2" (replace -1 )"2" (rewrite "nn_root_1n" )"2" (rewrite "nn_root_1n" ) nil nil )) nil ))nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil )eq -decl nil real_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )eq -decl nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil nn_root nil )"(total_order?[real])" nil )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil nn_root nil )eq -decl nil real_types nil )"bool" reals nil )eq -decl nil real_types nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )eq -decl nil integers nil )eq -decl nil integers nil )eq -decl nil integers nil )nil nn_root nil )nil nn_root nil )nil nn_root nil )nil nn_root nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.147 Sekunden
(vorverarbeitet am 2026-06-04)
¤ *© Formatika GbR, Deutschland
