(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" quality 100%
¤ Dauer der Verarbeitung: 0.33 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
