(atan (real_abs_lt_pi2_TCC1 0nil 3323017154"" (subtype-tcc) nil nil )"nzreal" nil )"nzreal" nil )"posreal" real_types nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3257226677"" (expand "atan" )"" (lemma "atan_value_strict_increasing" )"" "extensionality_postulate" "f" "atan_value" "g" "LAMBDA (x: real): atan_value(x)" ))"" (assert ) nil nil )) nil ))nil ))nil )nil shostak))nil 3257310468"" (expand "bijective?" )"" (split 1)"1" (expand "injective?" )"1" (skolem 1 ("x" "y" ))"1" (flatten)"1" (lemma "atan_strict_increasing" )"1" (expand "strict_increasing?" )"1" (lemma "trich_lt" ("x" "x" "y" "y" ))"1" (split -1)"1" (inst - "x" "y" )"1" (assert ) nil nil )) nil )"2" (propax) nil nil )"3" (inst - "y" "x" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "surjective?" )"2" (skosimp*)"2" (typepred "y!1" )"2" "derivable_continuous2" ("f" "atan_value" ))"2" (split -1)"1" (expand "atan" )"1" (lemma "atan_value_strict_increasing" )"1" (expand "strict_increasing?" )"1" (lemma "trichotomy" ("x" "y!1" ))"1" (split -1)"1" "trich_lt" "x" "y!1" "y" "atan_value(1)" ))"1" "1" "intermediate1" "g" "atan_value" "a" "0" "b" "1" "x" "y!1" ))"1" rewrite "atan_value_0" )"1" assert )"1" "1" "c!1" )nil nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" "1" )"2" (assert ) nil nil ))nil )"3" expand "abs" )"3" "0" "1" )"3" assert )"3" rewrite "atan_value_0" )"3" "intermediate1" "a" "0" "b" "1" "x" "2*atan_value(1)-y!1" "g" "atan_value" ))"3" rewrite "atan_value_0" )"3" assert )"3" "c" ))"3" "3" expand "<=" -1)"3" "1" "atan_inv_value" "px" "1/c" ))"1" "1/c" )"1" assert )nil nil )"2" assert )nil nil ))nil )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "c" ))"1" assert )nil nil )"2" assert )nil nil ))nil )"3" assert )nil nil ))nil )"2" replace "2" rewrite "atan_value_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "0" )"2" rewrite "atan_value_0" )"2" (assert ) nil nil ))nil ))nil )"3" "trich_lt" "x" "y!1" "y" "-atan_value(1)" ))"3" expand "abs" )"3" assert )"3" "1" "intermediate1" "a" "-1" "b" "0" "x" "-2*atan_value(1)-y!1" "g" "atan_value" ))"1" rewrite "atan_neg_value" "1" rewrite "atan_value_0" "1" assert )"1" "c" ))"1" "1" expand "<=" -2)"1" "1" "atan_inv_neg_value" "nx" "c" ))"1" replace "1" "1" "1/c" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" replace -1)"2" rewrite "atan_value_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "-1" )"2" rewrite "atan_neg_value" )"2" (assert ) nil nil ))nil ))nil )"3" "intermediate1" "a" "-1" "b" "0" "x" "y!1" "g" "atan_value" ))"3" rewrite "atan_value_0" )"3" rewrite "atan_neg_value" )"3" assert )"3" "c" ))"3" "3" "c" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (lemma "one_over_one_plus_t_sq_cont" )"2" "fundamental" "f" "atan_deriv_fn" "F" "atan_value" "a" "0" ))"2" (split -1)"1" (flatten) nil nil )"2" (propax) nil nil )"3" (expand "atan_value" )"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_fun_preds"reals/" ))nil 3257226801"" (expand "atan" ) (("" (rewrite "atan_value_0" ) nil nil ))nil )nil shostak))nil 3264783397"" (skosimp*)"" (rewrite "pi_value" )"" (expand "atan" )"" (lemma "atan_inv_value" ("px" "px!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil )nil shostak))nil 3264783474"" (skosimp*)"" (rewrite "pi_value" )"" (expand "atan" )"" (lemma "atan_inv_neg_value" ("nx" "nx!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil )nil shostak))nil 3257226194"" (skolem 1 ("nzx" ))"" (lemma "atan_0" )"" (lemma "atan_strict_increasing" )"" (expand "strict_increasing?" )"" (lemma "trichotomy" ("x" "nzx" ))"" (split -1)"1" (inst - "0" "1/nzx" )"1" (lemma "quotient_pos_lt" ("n0x" "nzx" ))"1" (assert ) nil nil )) nil ))nil )"2" (assert ) nil nil )"3" (lemma "quotient_neg_lt" ("n0x" "nzx" ))"3" (inst - "1/nzx" "0" )"3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil atan nil )"bool" real_fun_preds "reals/" )nil real_props nil )nil reals nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"(strict_total_order?[real])" real_props nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"nzreal" nil )nil real_props nil )nil real_axioms nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )nil reals nil )nil atan nil ))nil 3257226889"" (lemma "atan_neg_value" )"" (expand "atan" ) (("" (propax) nil nil )) nil )) nil )nil shostak))nil 3257226968"" (expand "acot" )"" (skolem 1 ("nzx" ))"" (lemma "atan_neg" ("x" "1/nzx" ))"" (assert ) nil nil )) nil ))nil ))nil )"real" reals nil )"nzreal" nil )nil atan nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil reals nil )"nzreal" atan nil )"nzreal" nil ))nil 3257273266"" (skolem 1 ("x" "y" ))"" (assert ) (("" (flatten) (("" (assert ) nil nil )) nil ))nil ))nil )"real" realsnil )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )"real" realsnil ))nil 3257273266"" (skolem 1 ("x" "y" ))"" (flatten) (("" (hide -1 -2) (("" (assert ) nil nil )) nil ))nil ))nil )"real" realsnil )"odd_int" integersnil )"real" realsnil )"(strict_total_order?[real])" real_props nil ))nil 3408966186 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" realsnil )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"real" realsnil )"real" realsnil )"real" realsnil ))nil ))nil 3257227268"" (skolem 1 ("x" "y" ))"" (lemma "atan_value_minus" ("x" "x" "y" "y" ))"" (flatten -1)"" (rewrite "pi_value" )"" (expand "atan" )"" (replace -1)"" (replace -2) (("" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3257228828 ("" (grind) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" realsnil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"real" realsnil ))nil 3257273266"" (skolem 1 ("x" "y" ))"" (flatten) (("" (hide -1) (("" (assert ) nil nil )) nil ))nil ))nil )"real" realsnil )"real" realsnil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil 3257275668"" (skolem 1 ("x" "y" ))"" (flatten) (("" (hide -1 -2) (("" (assert ) nil nil )) nil ))nil ))nil )"real" realsnil )"real" realsnil )"(strict_total_order?[real])" real_props nil ))nil 3257227479"" (skolem 1 ("x" "y" ))"" (lemma "atan_minus" ("x" "x" "y" "-y" ))"" (rewrite "atan_neg" -1)"" (flatten)"" "both_sides_times_neg_lt1" "y" "x*y" "x" "1" "nz" "-1" ))"" "both_sides_times_neg_lt1" "x" "x*y" "y" "1" "nz" "-1" ))"" (replace -1)"" (replace -2)"" "both_sides_times_neg_lt1" "x" "y" "y" "0" "nz" "-1" ))"" "both_sides_times_neg_lt1" "y" "y" "x" "0" "nz" "-1" ))"" (lemma "trichotomy" ("x" "y" ))"" (split -1)"1" assert )"1" replace -6 1)"1" replace -8 1)"1" (propax) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" assert )"3" replace -6 1)"3" replace -7 1)"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil atan nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"even_int" nil )"(divides(n))" dividesnil )"(divides(m))" dividesnil )"odd_int" integersnil )"real" realsnil )nil real_axioms nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil real_props nil )"odd_int" integersnil )"nzreal" nil )"real" realsnil )"real" realsnil )"real" realsnil )nil atan nil ))nil 3514303177 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3514303177 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3514303177 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )"real" realsnil ))nil ))nil 3514303178"" (skeep)"" (lemma "atan_minus" )"" (inst?)"" (assert )"" "(x / y - y / x) / (1 + x / y * (y / x)) = (x ^ 2 - y ^ 2) / (2 * (x * y))" )"" (hide -1 4)"" (expand "^" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil atan nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"real" exponentiation nil )"real" exponentiation nil )"bool" reals nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"[T, T -> boolean]" equalities nil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"real" realsnil )"real" realsnil )"real" realsnil )"real" realsnil )"odd_int" integersnil ))nil 3259650470"" (lemma "atan_plus" ("x" "1/5" "y" "1/5" ))"" (assert )"" (case "(2 * (1 / 5) / (1 - 1 / 5 * (1 / 5))) = 5/12" )"1" (replace -1)"1" (lemma "atan_plus" ("x" "5/12" "y" "5/12" ))"1" (assert )"1" case "(2 * (5 / 12) / (1 - 5 / 12 * (5 / 12))) = 120/119" )"1" (replace -1)"1" (hide -1 -3)"1" (replace -2 -1 rl)"1" (simplify -1)"1" (replace -1 1)"1" "atan_minus" "x" "120/119" "y" "1/239" ))"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" "cross_mult" "x" "2*(5/12)" "n0x" "(1 - 5 / 12 * (5 / 12))" "y" "120" "n0y" "119" ))"2" (replace -1)"2" (hide -1) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"rat" rationalsnil )"posrat" nil )"nzrat" nil )"real" realsnil )"posrat" nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"real" realsnil )"real" realsnil )nil atan nil )"odd_int" integersnil )"rat" rationalsnil )nil real_props nil )nil reals nil )"rat" rationalsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"[T, T -> boolean]" equalities nil )"posrat" nil )nil atan nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil ))nil 3259651388"" (skolem 1 ("x" ))"" (lemma "deriv_atan_fun" )"" (flatten)"" (lemma "atan_0" )"" (lemma "mean_value[nnreal]" ("a" "0" ))"1" (inst - "x" "_" )"1" "restrict2_derivable[nnreal,real]" "f" "atan" ))"1" "restrict2_deriv[nnreal,real]" "f" "atan" ))"1" (expand "restrict2" )"1" (replace -6 -1)"1" (simplify -1)"1" "extensionality" "f" "LAMBDA (a: nnreal): 1 / (1 + a * a)" "g" "deriv[nnreal](LAMBDA (u: nnreal): atan(u))" ))"1" "1" replace -2 -1)"1" "1" "identity_derivable_fun[nnreal]" )"1" "deriv_id_fun[nnreal]" )"1" "deriv_const_fun[nnreal]" "b" "1" ))"1" expand "I" )"1" expand "const_fun" )"1" "1" "prod_derivable_fun" "f1" "LAMBDA (x: nnreal): x" "f2" "LAMBDA (x: nnreal): x" ))"1" assert )"1" "deriv_prod_fun" "ff1" "LAMBDA (x: nnreal): x" "ff2" "LAMBDA (x: nnreal): x" ))"1" replace "1" expand "*" )"1" expand "+" "1" "sum_derivable_fun" "f1" "LAMBDA (x: nnreal): 1" "f2" "LAMBDA (x: nnreal): x*x" ))"1" "const_derivable_fun[nnreal]" "b" "1" ))"1" expand "const_fun" )"1" assert )"1" "deriv_sum_fun" "ff1" "LAMBDA (x: nnreal): 1" "ff2" "LAMBDA (x: nnreal): x*x" ))"1" replace "1" replace "1" expand "+" )"1" "div_derivable_fun" "f" "LAMBDA (x: nnreal): x" "g" "LAMBDA (x: nnreal): 1 + x*x" ))"1" assert )"1" expand "/" "1" "deriv_div_fun" "ff" "LAMBDA (x: nnreal): x" "gg" "LAMBDA (x: nnreal): 1 + x*x" ))"1" replace "1" replace "1" expand "/" )"1" expand "-" "1" expand "*" "1" "diff_derivable_fun" "f1" "LAMBDA (u: nnreal): atan(u)" "f2" "LAMBDA (x: nnreal): x/(1+x*x)" ))"1" assert )"1" "deriv_diff_fun" "ff1" "LAMBDA (u: nnreal): atan(u)" "ff2" "LAMBDA (x: nnreal): x/(1+x*x)" ))"1" expand "-" )"1" replace "1" replace "1" "1" "LAMBDA (x_1: nnreal): atan(x_1) - x_1 / (1 + x_1 * x_1)" )"1" assert )"1" "c" )"1" expand "deriv" "1" "congruence" "f" "(LAMBDA (x: nnreal): LAMBDA (x_1: nnreal): atan(x_1) - x_1 / (1 + x_1 * x_1), x))" "g" "(LAMBDA (x_1: nnreal): " "x1" "c" "x2" "c" ))"1" assert )"1" replace "1" replace "1" "1" "1" "posreal_times_posreal_is_posreal" "px" "c" "py" "c" ))"1" "posreal_times_posreal_is_posreal" "px" "1+c*c" "py" "1+c*c" ))"1" "minus_div1" "x" "1" "n0x" "1+c*c" "y" "1-c*c" "n0y" "(1 + c * c) * (1 + c * c)" ))"1" replace "1" "div_cancel1" "x" "2*(c*c)/((1 + c * c) * (1 + c * c))" "n0z" "1+c*c" ))"1" "CC" "c*c" )"1" replace "1" "CCP1" "1+CC" )"1" replace "1" rewrite "div_div2" "1" case "1 * (CCP1 * CCP1) - (1 - CC) * CCP1 = CCP1 * 2*CC" )"1" replace "1" replace "1" "posreal_div_posreal_is_posreal" "px" "2*CC" "py" "CCP1*CCP1" ))"1" "posreal_times_posreal_is_posreal" "px" "2*CC/(CCP1*CCP1)" ))"1" "x" )"1" replace "1" assert )nil nil ))nil ))nil )"2" nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil )"2" expand "CCP1" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "derivable" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "diff_derivable_fun" "f1" "LAMBDA (x: nnreal): x" "f2" "LAMBDA (u: nnreal): atan(u)" ))"2" "deriv_diff_fun" "ff1" "LAMBDA (x: nnreal): x" "ff2" "LAMBDA (u: nnreal): atan(u)" ))"1" expand "-" "1" replace "1" replace "1" "1" assert )"1" "LAMBDA (x_1: nnreal): x_1 - atan(x_1)" )"1" assert )"1" "c" ))"1" expand "deriv" "1" replace "1" "congruence" "f" "(LAMBDA (x: nnreal): deriv(LAMBDA (x_1: nnreal): x_1 - atan(x_1), x))" "g" "(LAMBDA (x_1: nnreal): 1 - 1 / (1 + x_1 * x_1))" "x1" "c" "x2" "c" ))"1" assert )"1" replace "1" "1" "1" "minus_div1" "x" "1" "n0x" "1" "y" "1" "n0y" "1+c*c" ))"1" case "1+c*c > 0" )"1" replace "1" "1" "posreal_div_posreal_is_posreal" "px" "c*c" "py" "1+c*c" ))"1" "posreal_times_posreal_is_posreal" "px" "c*c/(1+c*c)" ))"1" "x" )"1" assert )"1" replace "1" assert )nil nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "posreal_times_posreal_is_posreal" "px" "c" "py" "c" ))"1" nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "sq_pos" "a" "c" ))"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "derivable" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*) (("2" (inst + "x!1" ) nil nil ))nil ))nil )"3" (skosimp*)"3" (inst + "x!1+1" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst + "x!1+1" ) (("2" (assert ) nil nil ))nil ))nil )"3" (hide-all-but 1) (("3" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"nonneg_real" sq "reals/" )nil sq "reals/" ))nil 3259662678"" (rewrite "pi_value" )"" (rewrite "atan_1" )"" (lemma "atan_bnds" ("px" "1/5" ))"" (lemma "atan_bnds" ("px" "1/239" ))"" (flatten)"" "both_sides_times_pos_lt1" "pz" "16" "x" "5/26" "y" "atan(1/5)" ))"" "both_sides_times_pos_lt1" "pz" "16" "y" "1/5" "x" "atan(1/5)" ))"" "both_sides_times_neg_lt1" "nz" "-4" "x" "1/239" "y" "atan(1/239)" ))"" "both_sides_times_neg_lt1" "nz" "-4" "y" "239/57122" "x" "atan(1/239)" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil atan nil )"posrat" nil )"real" realsnil )"real_abs_lt_pi2" atan nil )nil atan nil )"{r: posreal | r > pi_lb AND r < pi_ub}" nil )"posreal" trig_basic nil )"posreal" trig_basic nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_props nil )"nzint" integersnil )"even_int" integersnil )nil real_props nil )"bool" reals nil )nil real_types nil )nil real_types nil )"nzrat" nil )"posrat" nil )"posrat" nil )"(strict_total_order?[real])" real_props nil )nil atan nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"real" realsnil )"nzreal" nil )nil atan nil ))nil 3258433066 ("" (grind) nil nil )"nonneg_int" nil )"even_int" nil )"(divides(n))" dividesnil )"(divides(m))" dividesnil )"boolean" notequal nil ))nil 3322495613 ("" (assuming-tcc) nil nil )"(total_order?[real])" nil ))nil ))nil 3408966186 ("" (subtype-tcc) nil nil )nil nil ))nil 3514650812 ("" (assuming-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )nil integers nil )"(total_order?[real])" nil )"(total_order?[real])" nil ))nil ))nil 3260165696 ("" (grind) nil nil )"nonneg_int" nil )"even_int" nil )"(divides(n))" dividesnil )"(divides(m))" dividesnil )"boolean" notequal nil ))nil 3260166047"" (skolem 1 ("n" "x" ))"" (lemma "atan_taylors" ("x" "x" "n" "n" ))"" (skolem -1 ("c" ))"" (replace -1)"" (lemma "atan_series_prep8" ("n" "n+1" "x" "c" ))"" (simplify 1)"" (rewrite "abs_div" 1)"1" (rewrite "abs_mult" 1)"1" (expand "abs" 1 3)"1" "ATANC" "nderiv(2 * (n + 1) + 1, atan)(c)" )"1" (hide -2)"1" (lemma "trichotomy" ("x" "ATANC" ))"1" expand "abs" -2)"1" expand "abs" 1 1)"1" "div_cancel1" "n0z" "factorial(2*n+2)" "x" "abs(x ^ (3 + 2 * n)) / (3 + 2 * n)" ))"1" rewrite "div_div2" -1)"1" replace -1 1 rl)"1" "1" expand "factorial" 1 1)"1" "1" assert )"1" case "x=0" )"1" replace -1)"1" expand "^" )"1" expand "expt" )"1" assert )"1" rewrite "zero_times1" "1" expand "abs" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (n:nat): abs(x^n) > 0" )"1" "3+2*n" )"1" "posreal_div_posreal_is_posreal" "px" "abs(x ^ (3 + 2 * n))" "py" "(3 * factorial(2 + 2 * n) + 2 * (factorial(2 + 2 * n) * n))" ))"1" "both_sides_times_pos_le1" "x" "ATANC" "y" "factorial(2+2*n)" "pz" "abs(x ^ (3 + 2 * n)) / ")) "1" assert )"1" "K1" "(3 * factorial(2 + 2 * n) + 2 * (factorial(2 + 2 * n) * n))" )"1" "K2" "abs(x ^ (3 + 2 * n))" )"1" assert )nil nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" nil nil ))nil ))nil )"2" "2" "n" )"1" nil nil )"2" "2" "expt_plus" "n0x" "x" "i" "1" "j" "j!1" ))"1" rewrite "expt_x1" )"1" replace "1" rewrite "abs_mult" )"1" "posreal_times_posreal_is_posreal" "px" "abs(x)" "py" "abs(x^j!1)" ))"1" nil nil )"2" nil nil )"3" "3" nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace -1)"2" assert )nil nil ))nil )"3" assert )"3" case "x=0" )"1" replace -1)"1" expand "^" )"1" expand "expt" )"1" rewrite "zero_times1" )"1" expand "abs" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (n:nat): abs(x^n) > 0" )"1" "3+2*n" )"1" "posreal_div_posreal_is_posreal" "px" "abs(x^(3+2*n))" "py" "(3 * factorial(2 + 2 * n) + 2 * (factorial(2 + 2 * n) * n))" ))"1" "both_sides_times_pos_le1" "x" "-ATANC" "y" "factorial(2+2*n)" "pz" "abs(x ^ (3 + 2 * n)) / ")) "1" assert )nil nil ))nil ))nil ))nil )"2" "2" "n" )"1" nil nil )"2" "2" "expt_plus" "n0x" "x" "i" "1" "j" "j!1" ))"1" rewrite "expt_x1" )"1" replace "1" rewrite "abs_mult" )"1" "posreal_times_posreal_is_posreal" "px" "abs(x)" "py" "abs(x^j!1)" ))"1" nil nil )"2" nil nil )"3" "3" 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 )"2" "atan_n_times_derivable" "n" "3+2*n" ))"2" (propax) nil nil )) nil ))nil ))nil )"2" "atan_n_times_derivable" ("n" "3+2*n" ))"2" (propax) nil nil )) nil ))nil )"2" "atan_n_times_derivable" ("n" "3+2*n" ))"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak)))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.80Bemerkung:
(vorverarbeitet am 2026-04-26)
¤ *Bot Zugriff
