Impressum atan.prf
Sprache: Lisp
(atan (IMP_nth_derivatives_TCC1 0nil 3514558647"" (lemma "deriv_domain[real]" )"1" (propax) nil nil )"2" (lemma "connected_real" ) (("2" (propax) nil nil )) nil ))nil )nil deriv_domain "analysis/" )nil booleans nil )"bool" deriv_domain_def"analysis/" )"bool" deriv_domain_def "analysis/" )nil fundamental_theorem"analysis/" )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil ))nil 3514558647"" (expand "not_one_element?" )"" (skosimp*)"" (inst + "x!1+1" ) (("" (assert ) nil nil )) nil )) nil ))nil )"[numfield, numfield -> numfield]" number_fieldsnil )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 )"bool" deriv_domain_def"analysis/" ))nil ))nil 3514558647 ("" (assuming-tcc) nil nil )"bool" deriv_domain_def "analysis/" ))nil ))nil 3255851189"" (skosimp*)"" (lemma "sq_pos" ("a" "x!1" )) (("" (grind) nil nil )) nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil sq "reals/" )"nonneg_real" sq "reals/" )"(total_order?[real])" nil )"real" realsnil )"real" realsnil ))nil 3255875082"" (skosimp*)"" (lemma "sq_pos" ("a" "x!1" ))"" (expand "sq" )"" "posreal_div_posreal_is_posreal" "px" "1" "py" "1+x!1*x!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil sq "reals/" )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil real_typesnil )"real" realsnil )"(total_order?[real])" nil )"real" realsnil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nzreal" nil )"nonneg_real" sq "reals/" ))nil 3352177935"" (expand "atan_deriv_fn" )"" (expand "continuous?" )"" (skolem 1 ("x" ))"" (lemma "identity_continuous[real]" ("x0" "x" ))"" (expand "I" )"" "prod_continuous[real]" "f1" "LAMBDA (x: real): x" "f2" "LAMBDA (x: real): x" "x0" "x" ))"" (assert )"" "const_continuous[real]" "u" "1" "x0" "x" ))"" (expand "const_fun" )"" (expand "*" )"" "sum_continuous[real]" "f1" "LAMBDA (x: real): 1" "f2" "LAMBDA (x: real): x*x" "x0" "x" ))"" (assert )"" expand "+" )"" "inv_continuous[real]" "g" "LAMBDA (x: real): 1 + x * x" "x0" "x" ))"1" assert )"1" expand "/" )"1" (propax) nil nil ))nil ))nil )"2" "2" "2" "sq_pos" ("a" "x!1" ))"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" realsnil )"real" realsnil )"bool" continuous_functions"analysis/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil continuous_functions"analysis/" )nil continuous_functions"analysis/" )nil continuous_functions"analysis/" )"[T -> real]" real_fun_ops "reals/" )nil continuous_functions"analysis/" )"boolean" notequal nil )nil reals nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[T -> real]" real_fun_ops "reals/" )"(total_order?[real])" nil )"nonneg_real" sq "reals/" )nil sq "reals/" )"[T -> real]" real_fun_ops "reals/" )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )nil continuous_functions"analysis/" )"[T -> real]" real_fun_ops "reals/" )"(bijective?[T, T])" identity nil )"posreal" atan nil )"nzreal" nil ))nil )nil 3255875106"" (expand "atan_deriv_fn" )"" (expand "continuous?" )"" (skolem 1 ("x" ))"" (lemma "identity_continuous" ("x0" "x" ))"" (expand "I" )"" "prod_continuous" "f1" "LAMBDA (x: real): x" "f2" "LAMBDA (x: real): x" "x0" "x" ))"" (assert )"" (lemma "const_continuous" ("u" "1" "x0" "x" ))"" (expand "const_fun" )"" (expand "*" )"" "sum_continuous" "f1" "LAMBDA (x: real): 1" "f2" "LAMBDA (x: real): x*x" "x0" "x" ))"" (assert )"" expand "+" )"" "inv_continuous" "g" "LAMBDA (x: real): 1 + x * x" "x0" "x" ))"1" assert )"1" expand "/" )"1" (propax) nil nil ))nil ))nil )"2" "2" "2" "sq_pos" ("a" "x!1" ))"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil continuous_functions"analysis/" )nil continuous_functions"analysis/" )nil continuous_functions"analysis/" )nil continuous_functions"analysis/" )"nonneg_real" sq "reals/" )nil sq "reals/" )"[T -> real]" real_fun_ops "reals/" )nil continuous_functions"analysis/" )"[T -> real]" real_fun_ops "reals/" ))nil 3352178025"" (skolem 1 ("x" ))"" (lemma "one_over_one_plus_t_sq_cont" )"" "continuous_Integrable?[real]" "f" "atan_deriv_fn" "a" "0" "b" "x" ))"1" (expand "continuous?" -2)"1" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (skosimp*) (("2" (inst - "x!1" ) nil nil ))nil ))nil ))nil ))nil )"2" (expand "connected?" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil )nil atan nil )"bool" continuous_functions"analysis/" )nil intervals_real "reals/" )"bool" reals nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" deriv_domain_def"analysis/" )"bool" deriv_domain_def "analysis/" )nil integral "analysis/" )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil )nil 3255851329"" (skolem 1 ("x" ))"" (lemma "one_over_one_plus_t_sq_cont" )"" "continuous_Integrable?" "f" "atan_deriv_fn" "a" "0" "b" "x" ))"" (expand "continuous?" -2)"" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (skosimp*) (("2" (inst - "x!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integral"analysis/" ))nil 3352180534"" (expand "atan_value" )"" "Integral_a_to_a[real]" "a" "0" "f" "atan_deriv_fn" ))"1" (propax) nil nil )"2" (assert )"2" (expand "connected?" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil integral "analysis/" )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def"analysis/" )"real" atan nil ))nil )nil 3255979393"" (expand "atan_value" )"" (lemma "Integral_a_to_a" ("a" "0" "f" "atan_deriv_fn" ))"" (propax) nil nil )) nil ))nil )nil integral "analysis/" ))"fixit" 3394184058"" "derivs_eq[real]" "F" "LAMBDA (z:real): atan_value(-z)" "G" "LAMBDA (z:real): -atan_value(z)" ))"1" (skolem 1 ("x" ))"1" (lemma "identity_derivable_fun[real]" )"1" (lemma "deriv_id_fun[real]" )"1" "neg_derivable_fun[real]" "f" "LAMBDA (x:real): x" ))"1" "deriv_neg_fun[real]" "ff" "LAMBDA (x: real): x" ))"1" (expand "I" )"1" (lemma "one_over_one_plus_t_sq_cont" )"1" "fundamental[real]" "f" "atan_deriv_fn" "a" "0" "F" "atan_value" ))"1" (split -1)"1" (flatten -1)"1" "composition_derivable_fun[real,real]" "f" "-(LAMBDA (x: real): x)" "g" "atan_value" ))"1" "composition_derivable_fun[real,real]" "g" "-(LAMBDA (x: real): x)" "f" "atan_value" ))"1" assert )"1" assert )"1" "deriv_comp_fun[real,real]" "ff" "-(LAMBDA (x: real): x)" "gg" "atan_value" ))"1" "deriv_comp_fun[real,real]" "gg" "-(LAMBDA (x: real): x)" "ff" "atan_value" ))"1" expand "o" )"1" expand "-" )"1" expand "*" )"1" assert )"1" replace -6)"1" expand "const_fun" )"1" replace -10)"1" "1" replace -8)"1" "1" "1" replace "1" replace "1" "extensionality_postulate" "f" "LAMBDA (x: real): atan_deriv_fn(-x) * -1" "g" "LAMBDA (x: real): -1 * atan_deriv_fn(x)" ))"1" "1" "1" "extensionality_postulate" "f" "(LAMBDA (z: real): atan_value(-z))" "g" "(LAMBDA (z: real): -atan_value(z)) + (LAMBDA (x: real): c!1)" ))"1" replace "1" "0" )"1" expand "+" )"1" rewrite "atan_value_0" )"1" "x" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "atan_deriv_fn" )"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 )"2" (propax) nil nil )"3" (expand "atan_value" 1)"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "I" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (assert )"2" (lemma "not_one_element" )"2" (expand "not_one_element?" )"2" (expand "connected?" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil taylors "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"bool" derivatives "analysis/" )nil derivatives "analysis/" )nil atan nil )nil chain_rule"analysis/" )"[T -> real]" real_fun_ops "reals/" )"bool" deriv_domain_def "analysis/" )nil chain_rule "analysis/" )"T3" function_props nil )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil atan nil )"even_int" integersnil )"real" realsnil )"nzreal" nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil functions nil )"nzreal" nil )"odd_int" integersnil )"[T -> real]" real_fun_ops "reals/" )"real" realsnil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil fundamental_theorem "analysis/" )"(bijective?[T, T])" identity nil )"deriv_fun" derivatives"analysis/" )"continuous_fun" "analysis/" )"continuous_fun[T2]" "analysis/" )"continuous_fun[T]" "analysis/" )"continuous_fun[T]" "analysis/" )"continuous_fun[T]" "analysis/" )"continuous_fun[T]" integral"analysis/" )"continuous_fun[T]" "analysis/" )nil derivatives "analysis/" )nil derivatives"analysis/" )nil booleans nil )"bool" deriv_domain_def"analysis/" )"bool" deriv_domain_def "analysis/" )"real" reals nil )nil indefinite_integral "analysis/" )"real" atan nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil )nil 3352180601"" "derivs_eq[real]" "F" "LAMBDA (z:real): atan_value(-z)" "G" "LAMBDA (z:real): -atan_value(z)" ))"1" (skolem 1 ("x" ))"1" (lemma "identity_derivable_fun[real]" )"1" (lemma "deriv_id_fun[real]" )"1" "neg_derivable_fun[real]" "f" "LAMBDA (x:real): x" ))"1" "deriv_neg_fun[real]" "ff" "LAMBDA (x: real): x" ))"1" (expand "I" )"1" (lemma "one_over_one_plus_t_sq_cont" )"1" "fundamental[real]" "f" "atan_deriv_fn" "a" "0" "F" "atan_value" ))"1" (split -1)"1" (flatten -1)"1" "composition_derivable_fun[real,real]" "f" "-(LAMBDA (x: real): x)" "g" "atan_value" ))"1" "composition_derivable_fun[real,real]" "g" "-(LAMBDA (x: real): x)" "f" "atan_value" ))"1" assert )"1" assert )"1" "deriv_comp_fun[real,real]" "ff" "-(LAMBDA (x: real): x)" "gg" "atan_value" ))"1" "deriv_comp_fun[real,real]" "gg" "-(LAMBDA (x: real): x)" "ff" "atan_value" ))"1" expand "o" )"1" expand "-" )"1" expand "*" )"1" assert )"1" replace -6)"1" expand "const_fun" )"1" replace -10)"1" "1" replace -8)"1" "1" "1" replace "1" replace "1" assert )"1" "extensionality_postulate" "f" "LAMBDA (x: real): atan_deriv_fn(-x) * -1" "g" "LAMBDA (x: real): -1 * atan_deriv_fn(x)" ))"1" replace "1" "1" "1" "extensionality_postulate" "f" "(LAMBDA (z: real): atan_value(-z))" "g" "(LAMBDA (z: real): -atan_value(z)) + (LAMBDA (x: real): c!1)" ))"1" replace "1" "0" )"1" expand "+" )"1" rewrite "atan_value_0" )"1" "x" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "atan_deriv_fn" )"2" "sq_neg" "a" "x!1" ))"2" expand "sq" )"2" replace "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 )"2" (propax) nil nil )"3" (expand "atan_value" 1)"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "I" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (inst + "x!1+1" ) (("2" (assert ) nil nil )) nil )) nil ))nil )nil derivatives "analysis/" )nil derivatives "analysis/" )nil chain_rule"analysis/" )"(convergent_nz?)" "analysis/" )"continuous_fun[T]" integral "analysis/" )nil chain_rule "analysis/" )"[T -> real]" real_fun_ops "reals/" )"nonneg_real" sq "reals/" )nil sq "reals/" )"[T -> real]" real_fun_ops "reals/" )nil fundamental_theorem "analysis/" )"deriv_fun" derivatives"analysis/" )"continuous_fun" "analysis/" )"continuous_fun[T2]" "analysis/" )"continuous_fun[T]" "analysis/" )"continuous_fun[T]" "analysis/" )"continuous_fun[T]" "analysis/" )"continuous_fun[T]" integral"analysis/" )nil derivatives "analysis/" )nil derivatives"analysis/" ))nil )nil 3255979648"" "derivs_eq" "F" "LAMBDA (z:real): atan_value(-z)" "G" "LAMBDA (z:real): -atan_value(z)" ))"" (skolem 1 ("x" ))"" (lemma "identity_derivable_fun[real]" )"" (lemma "deriv_id_fun[real]" )"" "neg_derivable_fun[real]" "f" "LAMBDA (x:real): x" ))"" "deriv_neg_fun" ("ff" "LAMBDA (x: real): x" ))"1" (expand "I" )"1" (lemma "one_over_one_plus_t_sq_cont" )"1" "fundamental[real]" "f" "atan_deriv_fn" "a" "0" "F" "atan_value" ))"1" (split -1)"1" (flatten -1)"1" "composition_derivable_fun" "f" "-(LAMBDA (x: real): x)" "g" "atan_value" ))"1" "composition_derivable_fun" "g" "-(LAMBDA (x: real): x)" "f" "atan_value" ))"1" assert )"1" assert )"1" "deriv_comp_fun" "ff" "-(LAMBDA (x: real): x)" "gg" "atan_value" ))"1" "deriv_comp_fun" "gg" "-(LAMBDA (x: real): x)" "ff" "atan_value" ))"1" expand "o" )"1" expand "-" )"1" expand "*" )"1" assert )"1" replace -6)"1" expand "const_fun" )"1" replace -10)"1" "1" replace -8)"1" "1" "1" replace "1" replace "1" assert )"1" "extensionality_postulate" "f" "LAMBDA (x: real): atan_deriv_fn(-x) * -1" "g" "LAMBDA (x: real): -1 * atan_deriv_fn(x)" ))"1" replace "1" "1" "1" "extensionality_postulate" "f" "(LAMBDA (z: real): atan_value(-z))" "g" "(LAMBDA (z: real): -atan_value(z)) + (LAMBDA (x: real): c!1)" ))"1" replace "1" "0" )"1" expand "+" )"1" rewrite "atan_value_0" )"1" "x" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "atan_deriv_fn" )"2" "sq_neg" "a" "x!1" ))"2" expand "sq" )"2" replace "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 )"2" (propax) nil nil )"3" (expand "atan_value" 1)"3" (propax) nil nil )) nil ))nil )"2" (skosimp*)"2" (inst + "x!1+1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "I" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil derivatives "analysis/" )nil derivatives "analysis/" )nil chain_rule"analysis/" )nil chain_rule "analysis/" )"[T -> real]" real_fun_ops "reals/" )"nonneg_real" sq "reals/" )nil sq "reals/" )"[T -> real]" real_fun_ops "reals/" )nil fundamental_theorem "analysis/" )nil derivatives "analysis/" )nil derivatives"analysis/" ))nil 3352181608"" "derivs_eq[posreal]" "F" "LAMBDA (x:posreal): atan_value(x)" "G" "LAMBDA (x:posreal): atan_value(-1/x)" ))"1" (skolem 1 ("x" ))"1" "fundamental[real]" "f" "atan_deriv_fn" "F" "atan_value" "a" "0" ))"1" (split -1)"1" (flatten -1)"1" "restrict2_derivable[posreal,real]" "f" "atan_value" ))"1" "restrict2_deriv[posreal,real]" "f" "atan_value" ))"1" (expand "restrict2" )"1" (replace -2)"1" "composition_derivable_fun[posreal,real]" "f" "LAMBDA (x: posreal): -(1 / x)" "g" "atan_value" ))"1" "identity_derivable_fun[posreal]" )"1" (lemma "deriv_id_fun[posreal]" )"1" expand "I" )"1" expand "const_fun" )"1" "inv_derivable_fun[posreal]" "g" "(LAMBDA (x: posreal): x)" ))"1" assert )"1" expand "/" )"1" "deriv_inv_fun[posreal]" "gg" "(LAMBDA (x: posreal): x)" ))"1" replace -3)"1" expand "-" )"1" expand "/" )"1" expand "*" )"1" "neg_derivable_fun[posreal]" "f" "LAMBDA (x_1: posreal): 1 / x_1" ))"1" assert )"1" expand "-" )"1" "deriv_neg_fun[posreal]" "ff" "LAMBDA (x_1: posreal): 1 / x_1" ))"1" expand "-" )"1" replace "1" "1" "composition_derivable_fun[posreal,real]" "f" "LAMBDA (x: posreal): -(1 / x)" "g" "atan_value" ))"1" "deriv_comp_fun[posreal,real]" "ff" "LAMBDA (x: posreal): -(1 / x)" "gg" "atan_value" ))"1" expand "o" )"1" assert )"1" replace "1" replace "1" expand "*" )"1" expand "atan_deriv_fn" "1" "deriv_comp_fun[posreal,real]" "ff" "LAMBDA (x:posreal): x" "gg" "atan_value" ))"1" expand "o" )"1" replace "1" replace "1" expand "*" )"1" expand "atan_deriv_fn" "1" replace "1" replace "1" "extensionality_postulate" "f" "(LAMBDA (x_1: posreal): 1 / (1 + x_1 * x_1))" "g" "(LAMBDA (x_1: posreal): 1 / (1 + -(1 / x_1) * -(1 / x_1)) * -(-1 / (x_1 * x_1)))" ))"1" replace "1" "1" "1" "1" "c" ))"1" "extensionality_postulate" "f" "(LAMBDA (x: posreal): atan_value(x))" "g" "(LAMBDA (x: posreal): atan_value(-1 / x)) + (LAMBDA (x: posreal): c)" ))"1" replace "1" "1" expand "+" )"1" "1" )"1" "x" )"1" "atan_neg_value" )"1" "1" )"1" "1/x" )"1" replace "1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "z" ))"2" "div_times" "x" "1" "n0x" "1 + -(1 / z) * -(1 / z)" "y" "1" "n0y" "z*z" ))"2" replace "2" "2" rewrite "cross_mult" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1/x!1" )"2" "negreal_times_negreal_is_posreal" "nx" "-(1/x!1)" "ny" "-(1/x!1)" ))"1" assert )"1" "FF" "-(1 / x!1) * -(1 / x!1)" )"1" assert )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 )"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 )"2" (skosimp*) (("2" (inst + "x!1" ) nil nil ))nil ))nil ))nil )"2" (assert )"2" (lemma "one_over_one_plus_t_sq_cont" )"2" (propax) nil nil )) nil ))nil )"3" (expand "atan_value" ) (("3" (propax) nil nil ))nil ))nil )"2" (hide-all-but 1)"2" (assert )"2" (lemma "not_one_element" )"2" (expand "not_one_element?" )"2" (expand "connected?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (assert )"2" (expand "connected?" )"2" (skosimp*) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil )nil taylors "analysis/" )nil restrict2_deriv"analysis/" )"bool" derivatives "analysis/" )nil derivatives "analysis/" )"bool" deriv_domain_def "analysis/" )"[T, T -> boolean]" equalities nil )"[T1 -> real]" restrict2_deriv"analysis/" )"nzreal" nil )nil chain_rule"analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )"real" realsnil )"real" realsnil )"posreal" real_types nil )nil derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"posreal" real_types nil )nil derivatives "analysis/" )"T3" function_props nil )"posreal" real_types nil )"real" realsnil )nil functions nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"nzreal" nil )"[T -> real]" real_fun_ops "reals/" )nil atan nil )"real" reals nil )nil real_props nil )"(divides(n))" dividesnil )"odd_int" integersnil )"posint" nil )nil reals nil )nil real_props nil )nil real_typesnil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )NOT const-decl "[bool -> bool]" booleans nil )nil chain_rule "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )nil reals nil )nil derivatives "analysis/" )"(bijective?[T, T])" identity nil )nil derivatives"analysis/" )"odd_int" integersnil )nil restrict2_deriv "analysis/" )nil atan nil )"posreal" atan nil )nil fundamental_theorem "analysis/" )"bool" deriv_domain_def"analysis/" )"bool" deriv_domain_def "analysis/" )"nzreal" nil )nil indefinite_integral "analysis/" )"real" atan nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"[numfield -> numfield]" number_fields 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 )nil 3256911357"" "derivs_eq[posreal]" "F" "LAMBDA (x:posreal): atan_value(x)" "G" "LAMBDA (x:posreal): atan_value(-1/x)" ))"1" (skolem 1 ("x" ))"1" "fundamental" "f" "atan_deriv_fn" "F" "atan_value" "a" "0" ))"1" (split -1)"1" (flatten -1)"1" "restrict2_derivable[posreal,real]" "f" "atan_value" ))"1" "restrict2_deriv[posreal,real]" "f" "atan_value" ))"1" (expand "restrict2" )"1" (replace -2)"1" "composition_derivable_fun" "f" "LAMBDA (x: posreal): -(1 / x)" "g" "atan_value" ))"1" "identity_derivable_fun[posreal]" )"1" (lemma "deriv_id_fun[posreal]" )"1" expand "I" )"1" expand "const_fun" )"1" "inv_derivable_fun" "g" "(LAMBDA (x: posreal): x)" ))"1" assert )"1" expand "/" )"1" "deriv_inv_fun" "gg" "(LAMBDA (x: posreal): x)" ))"1" replace -3)"1" expand "-" )"1" expand "/" )"1" expand "*" )"1" "neg_derivable_fun" "f" "LAMBDA (x_1: posreal): 1 / x_1" ))"1" assert )"1" expand "-" )"1" "deriv_neg_fun" "ff" "LAMBDA (x_1: posreal): 1 / x_1" ))"1" expand "-" )"1" replace "1" "1" "composition_derivable_fun" "f" "LAMBDA (x: posreal): -(1 / x)" "g" "atan_value" ))"1" "deriv_comp_fun" "ff" "LAMBDA (x: posreal): -(1 / x)" "gg" "atan_value" ))"1" expand "o" )"1" assert )"1" replace "1" replace "1" expand "*" )"1" expand "atan_deriv_fn" "1" "deriv_comp_fun" "ff" "LAMBDA (x:posreal): x" "gg" "atan_value" ))"1" expand "o" )"1" replace "1" replace "1" expand "*" )"1" expand "atan_deriv_fn" "1" replace "1" replace "1" "extensionality_postulate" "f" "(LAMBDA (x_1: posreal): 1 / (1 + x_1 * x_1))" "g" "(LAMBDA (x_1: posreal): 1 / (1 + -(1 / x_1) * -(1 / x_1)) * -(-1 / (x_1 * x_1)))" ))"1" replace "1" "1" "1" "1" "c" ))"1" "extensionality_postulate" "f" "(LAMBDA (x: posreal): atan_value(x))" "g" "(LAMBDA (x: posreal): atan_value(-1 / x)) + (LAMBDA (x: posreal): c)" ))"1" replace "1" "1" expand "+" )"1" "1" )"1" "x" )"1" "atan_neg_value" )"1" "1" )"1" "1/x" )"1" replace "1" replace "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "z" ))"2" "div_times" "x" "1" "n0x" "1 + -(1 / z) * -(1 / z)" "y" "1" "n0y" "z*z" ))"2" replace "2" "2" rewrite "cross_mult" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "1/x!1" )"2" "negreal_times_negreal_is_posreal" "nx" "-(1/x!1)" "ny" "-(1/x!1)" ))"1" assert )"1" "FF" "-(1 / x!1) * -(1 / x!1)" )"1" assert )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 )"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 )"2" (skosimp*) (("2" (inst + "x!1" ) nil nil )) nil )"3" (skosimp*)"3" (inst + "x!1+1" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (lemma "one_over_one_plus_t_sq_cont" )"2" (propax) nil nil )) nil )"3" (expand "atan_value" ) (("3" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (inst + "x!1/2" ) (("2" (grind) nil nil )) nil )) nil ))nil )"3" (skosimp*) (("3" (assert ) nil nil )) nil ))nil )nil restrict2_deriv"analysis/" )nil derivatives "analysis/" )"[T1 -> real]" restrict2_deriv"analysis/" )nil chain_rule"analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil chain_rule "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives"analysis/" )nil restrict2_deriv "analysis/" )nil fundamental_theorem"analysis/" ))nil 3256987888"" (skosimp*)"" (lemma "atan_inv_value" ("px" "-nx!1" ))"" (rewrite "atan_neg_value" -1)"" (lemma "atan_neg_value" ("x" "1/nx!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans 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 )"nzreal" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nzreal" nil )"npreal" nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"real" realsnil )"real" reals nil )"even_int" integersnil )"nzint" integersnil )"real" realsnil )nil atan nil ))nil 3477838347"" (lemma "positive_derivative[real]" ("g" "atan_value" ))"1" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (skolem 1 ("x" ))"2" (lemma "one_over_one_plus_t_sq_cont" )"2" "fundamental[real]" "f" "atan_deriv_fn" "F" "atan_value" "a" "0" ))"2" (assert )"2" (split -1)"1" (flatten)"1" (expand "deriv" -2)"1" "extensionality_postulate" "g" "atan_deriv_fn" "f" "LAMBDA (x: real): deriv(atan_value, x)" ))"1" (replace -1 -3 rl)"1" "x" )"1" replace -3 1)"1" "atan_deriv_fn(x)" )"1" (propax) nil nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" assert )"2" expand "derivable?" -1)"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "atan_value" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "one_over_one_plus_t_sq_cont" )"2" "fundamental[real]" "f" "atan_deriv_fn" "F" "atan_value" "a" "0" ))"1" (assert )"1" (expand "atan_value" ) (("1" (propax) nil nil ))nil ))nil )"2" (assert )"2" (expand "connected?" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (assert )"3" (expand "connected?" ) (("3" (propax) nil nil )) nil ))nil ))nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil fundamental_theorem "analysis/" )"[T -> real]" derivatives "analysis/" )NOT const-decl "[bool -> bool]" booleans nil )"bool" deriv_domain_def "analysis/" )"real" derivatives_def "analysis/" )"bool" derivatives_def "analysis/" )nil functions nil )"(strict_total_order?[real])" real_props nil )nil atan nil )"bool" deriv_domain_def"analysis/" )"bool" deriv_domain_def "analysis/" )nil derivative_props"analysis/" )nil booleans nil )"bool" derivatives "analysis/" )nil derivatives "analysis/" )"real" atan nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil )nil 3256837487"" (lemma "positive_derivative[real]" ("g" "atan_value" ))"1" (postpone) nil nil ) ("2" (postpone) nil nil )"3" (postpone) nil nil ) ("4" (postpone) nil nil ))nil )nil derivatives "analysis/" )"bool" derivatives "analysis/" )nil derivative_props"analysis/" )"bool" derivatives_def "analysis/" )"real" derivatives_def "analysis/" )"bool" deriv_domain_def "analysis/" )nil deriv_domain "analysis/" )"[T -> real]" derivatives "analysis/" )"bool" deriv_domain_def"analysis/" )"bool" deriv_domain_def "analysis/" )nil fundamental_theorem"analysis/" ))nil 3256964578"" (skosimp*)"" "div_mult_pos_lt1" ("z" "-1" "py" "py!1" "x" "x!1" ))"" (assert ) nil nil )) nil ))nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil real_props nil )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"real" realsnil )"real" realsnil ))nil 3352182175"" (skolem 1 ("z" "x" ))"" (flatten)"" (typepred "z" )"" (hide -1)"" "div_mult_pos_lt1" ("z" "-1" "py" "z" "x" "x" ))"" (assert )"" "fundamental[real]" "f" "atan_deriv_fn" "F" "atan_value" "a" "0" ))"1" (lemma "one_over_one_plus_t_sq_cont" )"1" (expand "atan_value" -2 1)"1" (replace -1)"1" (flatten -2)"1" "identity_derivable_fun[{a:real| -1/z<a}]" )"1" "deriv_id_fun[{a:real| -1/z<a}]" )"1" expand "I" )"1" "deriv_const_fun[{a: real | -1 / z < a}]" "b" "1" ))"1" "const_derivable_fun[{a: real | -1 / z < a}]" "b" "1" ))"1" "const_derivable_fun[{a: real | -1 / z < a}]" "b" "z" ))"1" "deriv_const_fun[{a: real | -1 / z < a}]" "b" "z" ))"1" "prod_derivable_fun[{a: real | -1 / z < a}]" "f1" "LAMBDA (x: {a: real | -1 / z < a}): x" "f2" "LAMBDA (x: {a: real | -1 / z < a}): z" ))"1" assert )"1" "deriv_prod_fun[{a: real | -1 / z < a}]" "ff1" "LAMBDA (x: {a: real | -1 / z < a}): x" "ff2" "LAMBDA (x: {a: real | -1 / z < a}): z" ))"1" expand "*" )"1" expand "+" )"1" replace -3)"1" replace -7)"1" "1" "deriv_sum_fun[{a: real | -1 / z < a}]" "ff1" "LAMBDA (x: {a: real | -1 / z < a}): 1" "ff2" "LAMBDA (x_1: {a: real | -1 / z < a}): x_1 * z" ))"1" "sum_derivable_fun[{a: real | -1 / z < a}]" "f1" "LAMBDA (x: {a: real | -1 / z < a}): 1" "f2" "LAMBDA (x_1: {a: real | -1 / z < a}): x_1 * z" ))"1" assert )"1" replace "1" replace "1" expand "+" )"1" "diff_derivable_fun[{a: real | -1 / z < a}]" "f1" "LAMBDA (x: {a: real | -1 / z < a}): x" "f2" "LAMBDA (x_1: {a: real | -1 / z < a}): z" ))"1" assert )"1" "deriv_diff_fun[{a: real | -1 / z < a}]" "ff1" "LAMBDA (x: {a: real | -1 / z < a}): x" "ff2" "LAMBDA (x_1: {a: real | -1 / z < a}): z" ))"1" replace "1" replace "1" expand "-" )"1" "div_derivable_fun[{a: real | -1 / z < a}]" "f" "LAMBDA (x_1: {a: real | -1 / z < a}): x_1 - z" "g" "LAMBDA (x_1: {a: real | -1 / z < a}): 1 + x_1 * z" ))"1" assert )"1" "deriv_div_fun[{a: real | -1 / z < a}]" "ff" "LAMBDA (x_1: {a: real | -1 / z < a}): x_1 - z" "gg" "LAMBDA (x_1: {a: real | -1 / z < a}): 1 + x_1 * z" ))"1" replace "1" replace "1" expand "/" )"1" expand "-" )"1" expand "*" )"1" "composition_derivable_fun[{a: real | -1 / z < a},real]" "f" "LAMBDA (x: {a: real | -1 / z < a}): x" "g" "atan_value" ))"1" "composition_derivable_fun[{a: real | -1 / z < a},real]" "f" "LAMBDA (x: {a: real | -1 / z < a}): (x - z) / (1 + x * z)" "g" "atan_value" ))"1" "deriv_comp_fun[{a: real | -1 / z < a},real]" "ff" "LAMBDA (x: {a: real | -1 / z < a}): (x - z) / (1 + x * z)" "gg" "atan_value" ))"1" "deriv_comp_fun[{a: real | -1 / z < a},real]" "ff" "LAMBDA (x: {a: real | -1 / z < a}): x" "gg" "atan_value" ))"1" assert )"1" expand "o" )"1" replace "1" replace "1" replace "1" expand "*" )"1" "derivs_eq[{a: real | -1 / z < a}]" "F" "LAMBDA (x_1: {a: real | -1 / z < a}): atan_value((x_1 - z) / (1 + x_1 * z))" "G" "LAMBDA (x_1: {a: real | -1 / z < a}): atan_value(x_1)" ))"1" assert )"1" replace "1" replace "1" "1" "extensionality_postulate" "f" "LAMBDA (x_1: {a: real | -1 / z < a}): atan_deriv_fn((x_1 - z) / (1 + x_1 * z)) * ((1 + z * z) / (1 + 2 * (x_1 * z) + x_1 * x_1 * z * z))" "g" "LAMBDA (x_1: {a: real | -1 / z < a}): atan_deriv_fn(x_1)" ))"1" replace "1" "1" "1" "c" ))"1" expand "const_fun" )"1" expand "+" )"1" "extensionality_postulate" "f" "LAMBDA (x_1: {a: real | -1 / z < a}): atan_value((x_1 - z) / (1 + x_1 * z))" "g" "LAMBDA (x_1: {a: real | -1 / z < a}): atan_value(x_1) + c" ))"1" replace "1" "1" "1" "0" )"1" rewrite "atan_value_0" "1" "1" "atan_neg_value" "x" "z" ))"1" replace "1" replace "1" "x" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "div_mult_pos_lt1" "z" "-1" "py" "z" "x" "0" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!1" )"2" "div_mult_pos_lt1" "z" "-1" "x" "x!1" "py" "z" ))"2" assert )"2" "posreal_times_posreal_is_posreal" "px" "1+x!1*z" "py" "1+x!1*z" ))"2" "div_cancel3" "x" "atan_deriv_fn((x!1 - z) / (1 + x!1 * z)) * (1 + z * z)" "n0z" "(1 + x!1 * z) * (1 + x!1 * z)" "y" "atan_deriv_fn(x!1)" ))"1" replace "1" "1" "XMZ" "x!1-z" )"1" replace "1" "XZP1" "1+x!1*z" )"1" replace "1" "ZSQP1" "1+z*z" )"1" replace "1" expand "atan_deriv_fn" )"1" "sq_pos" "a" "x!1" ))"1" "sq_pos" "a" "XMZ/XZP1" ))"1" expand "sq" )"1" "cross_mult" "x" "ZSQP1" "n0x" "1 + XMZ / XZP1 * (XMZ / XZP1)" "y" "XZP1 * XZP1" "n0y" "1 + x!1 * x!1" ))"1" replace "1" "1" "div_times" "x" "XMZ" "n0x" "XZP1" "y" "XMZ" "n0y" "XZP1" ))"1" replace "1" "div_cancel1" "n0z" "XZP1 * XZP1" "x" "XMZ * XMZ" ))"1" "1" replace "1" replace "1" replace "1" replace "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 )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!1" )"2" "div_mult_pos_lt1" "z" "-1" "py" "z" "x" "x!1" ))"2" assert )"2" "posreal_times_posreal_is_posreal" "px" "x!1*z+1" "py" "x!1*z+1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "0" )"2" nil nil ))nil ))nil ))nil )"3" assert )"3" expand "connected?" )"3" "3" assert )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 )"2" "2" "2" "x!1" )"2" "2" assert )nil nil ))nil ))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 ))nil ))nil ))nil ))nil )"2" assert )"2" expand "not_one_element?" )"2" "2" "x!1+1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"3" "3" expand "deriv_domain?" )"3" "3" "e!1/2" )"3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide-all-but 1)"2" (assert )"2" (expand "connected?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" realsnil )"real" realsnil )"real" realsnil )"real" realsnil )"nzreal" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil atan nil )nil derivatives"analysis/" )"bool" reals nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"bool" deriv_domain_def "analysis/" )"(bijective?[T, T])" identity nil )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )"[T -> real]" real_fun_ops "reals/" )"posreal" real_types nil )"T3" function_props nil )"(total_order?[real])" nil )"nzreal" nil )nil functions nil )nil real_props nil )nil reals nil )"[T, T -> boolean]" equalities nil )nil sq "reals/" )"nonneg_real" sq "reals/" )nil real_props nil )nil real_props nil )nil real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )nil real_typesnil )nil atan nil )"nnreal" nil )nil atan nil )"real" reals nil )"nzreal" nil )"posreal" atan nil )"npreal" nil )"[T -> real]" real_fun_ops "reals/" )"bool" booleans nil )nil indefinite_integral "analysis/" )"posreal" real_types nil )nil chain_rule "analysis/" )nil chain_rule"analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"[numfield, numfield -> numfield]" number_fieldsnil )nil reals nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"[numfield, numfield -> numfield]" number_fieldsnil )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )"bool" derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"posreal" real_types nil )"{y: posreal | y >= x}" real_defs nil )"{n: nonneg_real | n >= m AND n >= -m}" nil )"bool" deriv_domain_def"analysis/" )"bool" deriv_domain_def "analysis/" )"posreal" atan nil )"real" atan nil )nil fundamental_theorem "analysis/" )"odd_int" integersnil )nil real_props nil )nil number_fields nil )"[numfield -> numfield]" number_fields 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 )nil real_types nil )"bool" reals nil )nil real_types nil ))nil )nil 3256965562"" (skolem 1 ("z" "x" ))"" (flatten)"" (typepred "z" )"" (hide -1)"" "div_mult_pos_lt1" ("z" "-1" "py" "z" "x" "x" ))"" (assert )"" "fundamental" "f" "atan_deriv_fn" "F" "atan_value" "a" "0" ))"" (lemma "one_over_one_plus_t_sq_cont" )"" (expand "atan_value" -2 1)"" (replace -1)"" (flatten -2)"" "identity_derivable_fun[{a:real| -1/z<a}]" )"1" "deriv_id_fun[{a:real| -1/z<a}]" )"1" expand "I" )"1" "deriv_const_fun[{a: real | -1 / z < a}]" "b" "1" ))"1" "const_derivable_fun[{a: real | -1 / z < a}]" "b" "1" ))"1" "const_derivable_fun[{a: real | -1 / z < a}]" "b" "z" ))"1" "deriv_const_fun[{a: real | -1 / z < a}]" "b" "z" ))"1" expand "const_fun" )"1" "prod_derivable_fun" "f1" "LAMBDA (x: {a: real | -1 / z < a}): x" "f2" "LAMBDA (x: {a: real | -1 / z < a}): z" ))"1" assert )"1" "deriv_prod_fun" "ff1" "LAMBDA (x: {a: real | -1 / z < a}): x" "ff2" "LAMBDA (x: {a: real | -1 / z < a}): z" ))"1" expand "*" )"1" expand "+" )"1" replace -3)"1" replace -7)"1" "1" "deriv_sum_fun" "ff1" "LAMBDA (x: {a: real | -1 / z < a}): 1" "ff2" "LAMBDA (x_1: {a: real | -1 / z < a}): x_1 * z" ))"1" "sum_derivable_fun" "f1" "LAMBDA (x: {a: real | -1 / z < a}): 1" "f2" "LAMBDA (x_1: {a: real | -1 / z < a}): x_1 * z" ))"1" assert )"1" replace "1" replace "1" expand "+" )"1" "diff_derivable_fun" "f1" "LAMBDA (x: {a: real | -1 / z < a}): x" "f2" "LAMBDA (x_1: {a: real | -1 / z < a}): z" ))"1" assert )"1" "deriv_diff_fun" "ff1" "LAMBDA (x: {a: real | -1 / z < a}): x" "ff2" "LAMBDA (x_1: {a: real | -1 / z < a}): z" ))"1" replace "1" replace "1" expand "-" )"1" "div_derivable_fun" "f" "LAMBDA (x_1: {a: real | -1 / z < a}): x_1 - z" "g" "LAMBDA (x_1: {a: real | -1 / z < a}): 1 + x_1 * z" ))"1" assert )"1" "deriv_div_fun" "ff" "LAMBDA (x_1: {a: real | -1 / z < a}): x_1 - z" "gg" "LAMBDA (x_1: {a: real | -1 / z < a}): 1 + x_1 * z" ))"1" replace "1" replace "1" expand "/" )"1" expand "-" )"1" expand "*" )"1" "composition_derivable_fun" "f" "LAMBDA (x: {a: real | -1 / z < a}): x" "g" "atan_value" ))"1" "composition_derivable_fun" "f" "LAMBDA (x: {a: real | -1 / z < a}): (x - z) / (1 + x * z)" "g" "atan_value" ))"1" "deriv_comp_fun" "ff" "LAMBDA (x: {a: real | -1 / z < a}): (x - z) / (1 + x * z)" "gg" "atan_value" ))"1" "deriv_comp_fun" "ff" "LAMBDA (x: {a: real | -1 / z < a}): x" "gg" "atan_value" ))"1" assert )"1" expand "o" )"1" replace "1" replace "1" replace "1" expand "*" )"1" "derivs_eq" "F" "LAMBDA (x_1: {a: real | -1 / z < a}): atan_value((x_1 - z) / (1 + x_1 * z))" "G" "LAMBDA (x_1: {a: real | -1 / z < a}): atan_value(x_1)" ))"1" assert )"1" replace "1" replace "1" "1" "extensionality_postulate" "f" "LAMBDA (x_1: {a: real | -1 / z < a}): atan_deriv_fn((x_1 - z) / (1 + x_1 * z)) * ((1 + z * z) / (1 + 2 * (x_1 * z) + x_1 * x_1 * z * z))" "g" "LAMBDA (x_1: {a: real | -1 / z < a}): atan_deriv_fn(x_1)" ))"1" replace "1" "1" "1" "c" ))"1" expand "const_fun" )"1" expand "+" )"1" "extensionality_postulate" "f" "LAMBDA (x_1: {a: real | -1 / z < a}): atan_value((x_1 - z) / (1 + x_1 * z))" "g" "LAMBDA (x_1: {a: real | -1 / z < a}): atan_value(x_1) + c" ))"1" replace "1" "1" "1" "0" )"1" rewrite "atan_value_0" "1" "1" "atan_neg_value" "x" "z" ))"1" replace "1" replace "1" "x" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "div_mult_pos_lt1" "z" "-1" "py" "z" "x" "0" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!1" )"2" "div_mult_pos_lt1" "z" "-1" "x" "x!1" "py" "z" ))"2" assert )"2" "posreal_times_posreal_is_posreal" "px" "1+x!1*z" "py" "1+x!1*z" ))"2" "div_cancel3" "x" "atan_deriv_fn((x!1 - z) / (1 + x!1 * z)) * (1 + z * z)" "n0z" "(1 + x!1 * z) * (1 + x!1 * z)" "y" "atan_deriv_fn(x!1)" ))"1" replace "1" "1" "XMZ" "x!1-z" )"1" replace "1" "XZP1" "1+x!1*z" )"1" replace "1" "ZSQP1" "1+z*z" )"1" replace "1" expand "atan_deriv_fn" )"1" "sq_pos" "a" "x!1" ))"1" "sq_pos" "a" "XMZ/XZP1" ))"1" expand "sq" )"1" "cross_mult" "x" "ZSQP1" "n0x" "1 + XMZ / XZP1 * (XMZ / XZP1)" "y" "XZP1 * XZP1" "n0y" "1 + x!1 * x!1" ))"1" replace "1" "1" "div_times" "x" "XMZ" "n0x" "XZP1" "y" "XMZ" "n0y" "XZP1" ))"1" replace "1" "div_cancel1" "n0z" "XZP1 * XZP1" "x" "XMZ * XMZ" ))"1" "1" replace "1" replace "1" replace "1" replace "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 )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!1" )"2" "div_mult_pos_lt1" "z" "-1" "py" "z" "x" "x!1" ))"2" assert )"2" "posreal_times_posreal_is_posreal" "px" "x!1*z+1" "py" "x!1*z+1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))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 )"2" "2" "x!1" )"2" "2" assert )nil nil ))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 ))nil ))nil ))nil ))nil ))nil )"2" "2" "x!1+1" )"2" (assert ) nil nil ))nil ))nil )"3" "3" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil derivatives"analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil chain_rule"analysis/" )nil chain_rule "analysis/" )"nonneg_real" sq "reals/" )nil sq "reals/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil fundamental_theorem"analysis/" ))nil 3256964644"" (skosimp*)"" "div_mult_pos_lt2" ("z" "-1" "py" "py!1" "x" "x!1" ))"" (assert ) nil nil )) nil ))nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil real_props nil )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"real" realsnil )"real" realsnil ))nil 3256974044"" (skolem 1 ("z" "x" ))"" (flatten)"" (typepred "z" )"" (hide -1)"" (lemma "atan_inv_value" ("px" "z" ))"" "posreal_div_posreal_is_posreal" "px" "1" "py" "z" ))"" (lemma "atan_inv_neg_value" ("nx" "x" ))"1" "atan_value_minus_x1" "py" "1/z" "x" "1/x" ))"1" (rewrite "div_div1" -1)"1" "div_mult_neg_lt2" "z" "1" "x" "-z" "ny" "x" ))"1" "div_mult_pos_lt2" "z" "-1" "x" "x" "py" "z" ))"1" (assert )"1" "minus_div1" "x" "1" "y" "1" "n0x" "x" "n0y" "z" ))"1" replace -1 -4)"1" "add_div" "x" "1" "y" "1" "n0x" "1" "n0y" "x*z" ))"1" replace -1 -5)"1" rewrite "div_div1" -5)"1" "div_cancel2" "x" "z-x" "n0z" "x*z" ))"1" replace -1 -6)"1" "atan_neg_value" "x" "(z - x) / (1 + x * z)" ))"1" replace -1 1)"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_typesnil )"posreal" real_types nil )"nzreal" nil )nil atan nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"nzreal" nil )nil real_props nil )"real" realsnil )"(strict_total_order?[real])" real_props nil )"posrat" nil )"posreal" real_types nil )nil real_props nil )nil atan nil )"real" reals nil )"posint" nil )"odd_int" integersnil )"(divides(n))" dividesnil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )nil real_props nil )nil real_props nil )nil real_props nil )"nzreal" nil )"real" realsnil )"even_int" integersnil )"nzint" integersnil )"real" realsnil )"real" realsnil )"odd_int" integersnil )nil real_props nil )nil reals nil )"[numfield -> numfield]" number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil atan nil )nil atan 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 )nil real_types nil )"bool" reals nil )nil real_types nil ))nil 3255979356 ("" (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 )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )"boolean" notequal nil )"real" realsnil ))nil 3257273262"" (skolem 1 ("x" "y" ))"" (flatten) (("" (hide -1) (("" (assert ) nil nil )) nil ))nil ))nil )"real" realsnil )"odd_int" integersnil )"real" realsnil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))nil 3257273262"" (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 3255980971"" (skolem 1 ("x" "y" ))"" (split 1)"1" (flatten)"1" (lemma "trichotomy" ("x" "y" ))"1" (split -1)"1" (lemma "atan_value_minus_x1" ("x" "x" "py" "y" ))"1" "div_mult_pos_lt1" "z" "-1" "py" "y" "x" "x" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil )"2" (replace -1)"2" (rewrite "atan_value_0" )"2" (assert ) nil nil )) nil ))nil )"3" "atan_value_minus_x1" ("x" "-x" "py" "-y" ))"1" "div_mult_pos_lt1" "z" "-1" "py" "-y" "x" "-x" ))"1" (assert )"1" (rewrite "atan_neg_value" -2)"1" (rewrite "atan_neg_value" -2)"1" "atan_neg_value" "x" "(x - y) / (1 + x * y)" ))"1" (replace -1 -3)"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (lemma "atan_value_minus_x2" ("x" "x" "py" "y" ))"1" "div_mult_pos_lt2" ("x" "x" "py" "y" "z" "-1" ))"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil )"3" (flatten)"3" (lemma "atan_value_minus_x2" ("x" "-x" "py" "-y" ))"1" "div_mult_pos_lt2" "x" "-x" "py" "-y" "z" "-1" ))"1" (rewrite "atan_neg_value" -2)"1" (rewrite "atan_neg_value" -2)"1" "atan_neg_value" "x" "(x - y) / (1 + x * y)" ))"1" (replace -1 -3) (("1" (assert ) nil nil ))nil )"2" (hide-all-but (-3 -4 1))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil real_axioms nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil atan nil )nil atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil atan nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nzreal" nil )"real" realsnil )"real" realsnil )"real" realsnil )"real" realsnil )"(strict_total_order?[real])" real_props nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil )"odd_int" integersnil )nil atan nil )nil real_props nil ))nil 3255875083"" (lemma "atan_value_strict_increasing" )"" (expand "strict_increasing?" )"" (expand "atan" )"" (inst - "0" "1" )"" (assert )"" (rewrite "atan_value_0" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_fun_preds "reals/" )"real" realsnil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil atan 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 ))nil 3323022914"" (typepred "pi" )"" (rewrite "abs_0" ) (("" (assert ) nil nil )) nil )) nil )"nzreal" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"nzreal" 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 )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil ))nil ))nil 3256838147"" (skolem 1 ("x" ))"" (lemma "atan_value_strict_increasing" )"" (expand "strict_increasing?" )"" case "FORALL (x:posreal): 0 < atan_value(x) AND atan_value(x) < 2*atan_value(1)" )"1" (lemma "trichotomy" ("x" "x" ))"1" (split -1)"1" (inst -2 "x" )"1" (flatten -2)"1" (assert )"1" (assert )"1" (expand "pi" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (replace -1)"2" (inst -2 "1" )"2" (rewrite "atan_value_0" )"2" (flatten -2)"2" (assert ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"3" (inst-cp -3 "x" "0" )"3" (inst -2 "-x" )"1" (rewrite "atan_value_0" )"1" (rewrite "atan_neg_value" )"1" (expand "pi" )"1" (assert ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*)"2" (typepred "x!1" )"2" (inst-cp - "0" "x!1" )"2" (rewrite "atan_value_0" )"2" (assert )"2" (assert )"2" "trich_lt" ("x" "x!1" "y" "1" ))"2" "1" "x!1" "1" )"1" (assert ) nil nil ))nil )"2" replace -1)"2" (assert ) nil nil ))nil )"3" "atan_value_minus" "x" "x!1" "y" "1" ))"3" assert )"3" "(x!1-1)/(x!1+1)" "1" )"3" "div_mult_pos_lt1" "z" "x!1-1" "py" "x!1+1" "x" "1" ))"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil atan nil )"[numfield, numfield -> numfield]" number_fieldsnil )nil number_fields nil )"real" atan nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans 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 )"posreal" atan nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"nzreal" nil )"real" atan nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil atan nil )"real" reals nil )"[numfield -> numfield]" number_fields nil )nil atan nil )nil real_axioms nil )nil real_props nil )nil atan nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )nil real_props nil )"odd_int" integersnil )"posreal" real_types nil )"real" realsnil )"posreal" real_types nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" real_fun_preds"reals/" ))nil 3408904315"" (expand "atan" )"" (assert ) (("" (expand "pi" ) (("" (propax) nil nil )) nil ))nil ))nil )"real" realsnil )"posreal" atan nil )"real_abs_lt_pi2" atan 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 atan nil )nil functions nil )"real" atan nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real_abs_lt_pi2" atan nil ))nil 3352182458"" (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_cont_fun[real]" "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[real]" "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" "0" "1" )"3" assert )"3" rewrite "atan_value_0" )"3" expand "pi" )"3" "0" "1" )"3" assert )"3" "intermediate1[real]" "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 "<=" "3" "1" "atan_inv_value" "px" "1/c" ))"1" "1/c" )"1" assert )nil nil ))nil )"2" assert )"2" "posreal_div_posreal_is_posreal" "px" "1" "py" "c" ))"2" assert )nil nil ))nil ))nil )"3" assert )nil nil ))nil )"2" assert )"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 ))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" assert )"3" "1" expand "pi" )"1" "intermediate1[real]" "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" )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )"2" replace -1)"2" rewrite "atan_value_0" )"2" assert )nil nil ))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[real]" "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 )"2" (lemma "one_over_one_plus_t_sq_cont" )"2" "fundamental[real]" "f" "atan_deriv_fn" "F" "atan_value" "a" "0" ))"1" (split -1)"1" (flatten) nil nil )"2" (propax) nil nil )"3" (expand "atan_value" )"3" (propax) nil nil )) nil ))nil )"2" (assert )"2" (expand "connected?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil atan nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" nil )nil booleans nil )nil numbers nil )nil real_props nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"bool" real_fun_preds "reals/" )"bool" functions nil )nil derivatives "analysis/" )"real" atan nil )nil atan nil )"bool" deriv_domain_def"analysis/" )"bool" deriv_domain_def "analysis/" )"posreal" atan nil )nil fundamental_theorem "analysis/" )"real_abs_lt_pi2" atan nil )nil atan nil )"(strict_total_order?[real])" real_props nil )"nzreal" nil )"posreal" real_types nil )"(total_order?[real])" nil )"bool" booleans nil )"bool" continuous_functions"analysis/" )nil continuous_functions_props"analysis/" )"real" realsnil )"real" reals nil )"real" realsnil )"bool" reals nil )nil atan nil )"(total_order?[real])" nil )nil real_typesnil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"real" realsnil )nil atan nil )"nzint" integersnil )"even_int" integersnil )nil real_types nil )nil real_types nil )nil atan nil )"odd_int" integersnil )nil real_axioms nil )nil atan nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil atan nil )"bool" functions nil )"bool" functions nil ))nil )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 fundamental_theorem "analysis/" )nil continuous_functions_props"analysis/" ))nil 3257226801"" (expand "atan" ) (("" (rewrite "atan_value_0" ) nil nil ))nil )nil atan nil )"real_abs_lt_pi2" atan nil ))nil 3264783397"" (skosimp*)"" (expand "pi" )"" (expand "atan" )"" (lemma "atan_inv_value" ("px" "px!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil )"real" realsnil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans 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 )"posreal" real_types nil )"real" realsnil )"real" realsnil )"real_abs_lt_pi2" atan nil ))nil 3264783474"" (skosimp*)"" (expand "pi" )"" (expand "atan" )"" (lemma "atan_inv_neg_value" ("nx" "nx!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil )"real" realsnil )"real" reals nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans 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 )"nzreal" nil )"npreal" nil )"real" realsnil )"nzint" integersnil )"even_int" integersnil )"real" realsnil )"real_abs_lt_pi2" atan nil ))nil 3257225947"" (skolem 1 ("x" ))"" (lemma "one_over_one_plus_t_sq_cont" )"" "continuous_Integrable?[real]" "f" "atan_deriv_fn" "a" "0" "b" "x" ))"1" (expand "continuous?" -2)"1" (expand "atan_deriv_fn" )"1" (split -1)"1" (propax) nil nil )"2" (skosimp*) (("2" (inst - "x!1" ) nil nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "connected?" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )nil atan nil )"nzreal" nil )"bool" continuous_functions"analysis/" )nil intervals_real "reals/" )"bool" reals nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" realsnil )"real" realsnil )"bool" deriv_domain_def"analysis/" )"bool" deriv_domain_def "analysis/" )nil integral "analysis/" )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil ))nil 3257226833"" (skolem 1 ("x" ))"" (expand "atan" )"" (expand "atan_value" )"" (expand "atan_deriv_fn" ) (("" (propax) nil nil ))nil ))nil ))nil ))nil )"real_abs_lt_pi2" atan nil )"posreal" atan nil )"real" atan nil ))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 )"real_abs_lt_pi2" atan nil )nil atan nil ))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" ))"" (flatten) (("" (hide -1) (("" (assert ) nil nil )) nil ))nil ))nil )"real" realsnil )"odd_int" integersnil )"real" realsnil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil ))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 3257227268"" (skolem 1 ("x" "y" ))"" (lemma "atan_value_minus" ("x" "x" "y" "y" ))"" (flatten -1)"" (expand "pi" )"" (expand "atan" )"" (replace -1)"" (replace -2) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))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" realsnil )"real" realsnil )"real" realsnil )"posreal" atan nil )"(strict_total_order?[real])" real_props nil )"odd_int" integersnil )"(strict_total_order?[real])" real_props nil )"real_abs_lt_pi2" atan nil ))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 3514307078 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3514307078 ("" (subtype-tcc) nil nil )"boolean" notequal nil )) nil ))nil 3514307078 ("" (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 3514307078"" (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 3352182759"" (lemma "one_over_one_plus_t_sq_cont" )"" "extensionality_postulate" "f" "atan_deriv_fn" "g" "LAMBDA (x: real): 1 / (1 + x * x)" ))"1" (flatten -1)"1" (hide -2)"1" (split -1)"1" "fundamental[real]" "f" "atan_deriv_fn" "F" "atan" "a" "0" ))"1" (split -1)"1" (replace -2 -1) (("1" (propax) nil nil ))nil )"2" (propax) nil nil )"3" (expand "atan" 1)"3" (expand "atan_value" 1)"3" (propax) nil nil )) nil ))nil ))nil )"2" (assert )"2" (expand "connected?" )"2" (propax) nil nil )) nil ))nil ))nil )"2" (expand "atan_deriv_fn" 1)"2" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "sq_pos" ("a" "x!1" ))"2" (expand "sq" )"2" (assert )"2" (hide -3 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))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 )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, nznum -> numfield]" number_fieldsnil )nil number_fields nil )"boolean" notequal nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil functions nil )"real" realsnil )"real" realsnil )"real_abs_lt_pi2" atan nil )nil atan nil )"posreal" atan nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil fundamental_theorem "analysis/" )"bool" deriv_domain_def "analysis/" )"bool" deriv_domain_def"analysis/" )"real" atan nil )"nzreal" nil )nil sq "reals/" )"(total_order?[real])" nil )"nonneg_real" sq "reals/" )nil atan nil ))nil )nil 3257228288"" (lemma "one_over_one_plus_t_sq_cont" )"" "extensionality_postulate" "f" "atan_deriv_fn" "g" "LAMBDA (x: real): 1 / (1 + x * x)" ))"1" (flatten -1)"1" (hide -2)"1" (split -1)"1" "fundamental" "f" "atan_deriv_fn" "F" "atan" "a" "0" ))"1" (split -1)"1" (replace -2 -1) (("1" (propax) nil nil ))nil )"2" (propax) nil nil )"3" (expand "atan" 1)"3" (expand "atan_value" 1)"3" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (expand "atan_deriv_fn" 1)"2" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "sq_pos" ("a" "x!1" ))"2" (expand "sq" )"2" (assert )"2" (hide -3 1) (("2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil fundamental_theorem "analysis/" )nil sq "reals/" )"nonneg_real" sq "reals/" ))nil 3352182779"" (lemma "deriv_atan_fun" )"" (flatten)"" (lemma "derivable_cont_fun[real]" ("f" "atan" ))"" (assert ) nil nil )) nil ))nil ))nil )"real" realsnil )"real" realsnil )"nzreal" nil )nil derivatives "analysis/" )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil atan nil )"real_abs_lt_pi2" atan nil )nil numbers nil )nil booleans nil )"[number -> boolean]" nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil atan nil ))nil )nil 3262324800"" (lemma "deriv_atan_fun" )"" (flatten)"" (lemma "derivable_continuous2[real]" ("f" "atan" ))"" (assert ) nil nil )) nil ))nil ))nil )nil shostak))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 3445345367"" (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" "1" "prod_derivable_fun[nnreal]" "f1" "LAMBDA (x: nnreal): x" "f2" "LAMBDA (x: nnreal): x" ))"1" assert )"1" "deriv_prod_fun[nnreal]" "ff1" "LAMBDA (x: nnreal): x" "ff2" "LAMBDA (x: nnreal): x" ))"1" replace -4 -1)"1" expand "*" )"1" expand "+" "1" "sum_derivable_fun[nnreal]" "f1" "LAMBDA (x: nnreal): 1" "f2" "LAMBDA (x: nnreal): x*x" ))"1" "const_derivable_fun[nnreal]" "b" "1" ))"1" assert )"1" "deriv_sum_fun[nnreal]" "ff1" "LAMBDA (x: nnreal): 1" "ff2" "LAMBDA (x: nnreal): x*x" ))"1" replace "1" replace "1" expand "+" )"1" "div_derivable_fun[nnreal]" "f" "LAMBDA (x: nnreal): x" "g" "LAMBDA (x: nnreal): 1 + x*x" ))"1" assert )"1" expand "/" "1" "deriv_div_fun[nnreal]" "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[nnreal]" "f1" "LAMBDA (u: nnreal): atan(u)" "f2" "LAMBDA (x: nnreal): x/(1+x*x)" ))"1" assert )"1" "deriv_diff_fun[nnreal]" "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 )"2" "diff_derivable_fun[nnreal]" "f1" "LAMBDA (x: nnreal): x" "f2" "LAMBDA (u: nnreal): atan(u)" ))"2" "deriv_diff_fun[nnreal]" "ff1" "LAMBDA (x: nnreal): x" "ff2" "LAMBDA (u: nnreal): atan(u)" ))"1" expand "-" "1" replace -4 -1)"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 )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (skosimp*) (("2" (inst + "x!1" ) 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 atan nil )nil atan nil )"real" realsnil )"nzreal" nil )"(total_order?[real])" nil )nil real_types nil )"bool" reals nil )nil real_types nil )nil restrict2_deriv "analysis/" )nil functions nil )"[numfield, numfield -> numfield]" number_fieldsnil )"[numfield, numfield -> numfield]" number_fieldsnil )"[T -> real]" derivatives "analysis/" )nil derivatives"analysis/" )nil derivatives "analysis/" )"nzreal" nil )"posreal" real_types nil )"posreal" real_types nil )"(strict_total_order?[real])" real_props nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil reals nil )"[T -> real]" real_fun_ops "reals/" )"real" realsnil )"nnreal" nil )"real" realsnil )"[numfield, numfield -> numfield]" number_fieldsnil )nil functions nil )"bool" derivatives_def "analysis/" )"real" derivatives_def "analysis/" )nil real_typesnil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil reals nil )nil real_props nil )"real" realsnil )"odd_int" integersnil )nil real_typesnil )"posreal" atan nil )nil real_props nil )nil derivatives "analysis/" )nil derivatives "analysis/" )"nnreal" nil )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil derivatives "analysis/" )"[T -> real]" real_fun_ops "reals/" )nil derivatives "analysis/" )nil derivatives "analysis/" )nil sq "reals/" )"nonneg_real" sq "reals/" )"(total_order?[real])" nil )"posrat" nil )"(divides(n))" dividesnil )"odd_int" integersnil )"posint" nil )"(bijective?[T, T])" identity nil )nil derivatives "analysis/" )"posreal" real_types nil )"nnreal" nil )"[T1 -> real]" restrict2_deriv"analysis/" )"[T, T -> boolean]" equalities nil )"bool" deriv_domain_def "analysis/" )nil restrict2_deriv"analysis/" )"bool" derivatives "analysis/" )nil derivatives "analysis/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fieldsnil )"[numfield -> numfield]" number_fields nil )"posreal" atan nil )nil atan nil )"real_abs_lt_pi2" atan nil )"bool" deriv_domain_def"analysis/" )"bool" deriv_domain_def "analysis/" )nil derivative_props "analysis/" )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 ))nil )nil 3352182936"" (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[nnreal]" "f1" "LAMBDA (x: nnreal): x" "f2" "LAMBDA (x: nnreal): x" ))"1" assert )"1" "deriv_prod_fun[nnreal]" "ff1" "LAMBDA (x: nnreal): x" "ff2" "LAMBDA (x: nnreal): x" ))"1" replace "1" expand "*" )"1" expand "+" "1" "sum_derivable_fun[nnreal]" "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[nnreal]" "ff1" "LAMBDA (x: nnreal): 1" "ff2" "LAMBDA (x: nnreal): x*x" ))"1" replace "1" replace "1" expand "+" )"1" "div_derivable_fun[nnreal]" "f" "LAMBDA (x: nnreal): x" "g" "LAMBDA (x: nnreal): 1 + x*x" ))"1" assert )"1" expand "/" "1" "deriv_div_fun[nnreal]" "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[nnreal]" "f1" "LAMBDA (u: nnreal): atan(u)" "f2" "LAMBDA (x: nnreal): x/(1+x*x)" ))"1" assert )"1" "deriv_diff_fun[nnreal]" "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" )
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.1.521Bemerkung:
(Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-05-01)
¤ *Bot Zugriff
2026-05-26
