| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig_fnd/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 MB |
|
Impressum atan.prfInteraktion undPortierbarkeitLisp |
|||||||||||||||
|
(atan (IMP_nth_derivatives_TCC1 0 (IMP_nth_derivatives_TCC1-1 nil 3514558647 ("" (lemma "deriv_domain[real]") (("1" (propax) nil nil) ("2" (lemma "connected_real") (("2" (propax) nil nil)) nil)) nil) ((connected_real formula-decl nil deriv_domain "analysis/") (bool nonempty-type-eq-decl nil booleans nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (deriv_domain formula-decl nil fundamental_theorem "analysis/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil)) nil)) (IMP_nth_derivatives_TCC2 0 (IMP_nth_derivatives_TCC2-1 nil 3514558647 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_plus_real_is_real application-judgement "real" reals nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) nil)) (IMP_taylors_TCC1 0 (IMP_taylors_TCC1-1 nil 3514558647 ("" (assuming-tcc) nil nil) ((connected? const-decl "bool" deriv_domain_def "analysis/")) nil)) (atan_deriv_fn_TCC1 0 (atan_deriv_fn_TCC1-1 nil 3255851189 ("" (skosimp*) (("" (lemma "sq_pos" ("a" "x!1")) (("" (grind) nil nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sq_pos formula-decl nil sq "reals/") (sq const-decl "nonneg_real" sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (atan_deriv_fn_TCC2 0 (atan_deriv_fn_TCC2-1 nil 3255875082 ("" (skosimp*) (("" (lemma "sq_pos" ("a" "x!1")) (("" (expand "sq") (("" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "1+x!1*x!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sq_pos formula-decl nil sq "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sq const-decl "nonneg_real" sq "reals/")) shostak)) (one_over_one_plus_t_sq_cont 0 (one_over_one_plus_t_sq_cont-2 nil 3352177935 ("" (expand "atan_deriv_fn") (("" (expand "continuous?") (("" (skolem 1 ("x")) (("" (lemma "identity_continuous[real]" ("x0" "x")) (("" (expand "I") (("" (lemma "prod_continuous[real]" ("f1" "LAMBDA (x: real): x" "f2" "LAMBDA (x: real): x" "x0" "x")) (("" (assert) (("" (lemma "const_continuous[real]" ("u" "1" "x0" "x")) (("" (expand "const_fun") (("" (expand "*") (("" (lemma "sum_continuous[real]" ("f1" "LAMBDA (x: real): 1" "f2" "LAMBDA (x: real): x*x" "x0" "x")) (("" (assert) (("" (expand "+") (("" (lemma "inv_continuous[real]" ("g" "LAMBDA (x: real): 1 + x * x" "x0" "x")) (("1" (assert) (("1" (expand "/") (("1" (propax) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "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_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (continuous? const-decl "bool" continuous_functions "analysis/") (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (identity_continuous formula-decl nil continuous_functions "analysis/") (prod_continuous formula-decl nil continuous_functions "analysis/") (const_continuous formula-decl nil continuous_functions "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (inv_continuous formula-decl nil continuous_functions "analysis/") (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq const-decl "nonneg_real" sq "reals/") (sq_pos formula-decl nil sq "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sum_continuous formula-decl nil continuous_functions "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (I const-decl "(bijective?[T, T])" identity nil) (atan_deriv_fn const-decl "posreal" atan nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) nil) (one_over_one_plus_t_sq_cont-1 nil 3255875106 ("" (expand "atan_deriv_fn") (("" (expand "continuous?") (("" (skolem 1 ("x")) (("" (lemma "identity_continuous" ("x0" "x")) (("" (expand "I") (("" (lemma "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 "*") (("" (lemma "sum_continuous" ("f1" "LAMBDA (x: real): 1" "f2" "LAMBDA (x: real): x*x" "x0" "x")) (("" (assert) (("" (expand "+") (("" (lemma "inv_continuous" ("g" "LAMBDA (x: real): 1 + x * x" "x0" "x")) (("1" (assert) (("1" (expand "/") (("1" (propax) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "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) ((identity_continuous formula-decl nil continuous_functions "analysis/") (prod_continuous formula-decl nil continuous_functions "analysis/") (const_continuous formula-decl nil continuous_functions "analysis/") (inv_continuous formula-decl nil continuous_functions "analysis/") (sq const-decl "nonneg_real" sq "reals/") (sq_pos formula-decl nil sq "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (sum_continuous formula-decl nil continuous_functions "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/")) shostak)) (atan_value_TCC1 0 (atan_value_TCC1-2 nil 3352178025 ("" (skolem 1 ("x")) (("" (lemma "one_over_one_plus_t_sq_cont") (("" (lemma "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) ((one_over_one_plus_t_sq_cont formula-decl nil atan nil) (continuous? const-decl "bool" continuous_functions "analysis/") (Closed_interval type-eq-decl nil intervals_real "reals/") (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (continuous_Integrable? formula-decl nil integral "analysis/") (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (atan_deriv_fn const-decl "posreal" atan nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil)) nil) (atan_value_TCC1-1 nil 3255851329 ("" (skolem 1 ("x")) (("" (lemma "one_over_one_plus_t_sq_cont") (("" (lemma "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) ((continuous_Integrable? formula-decl nil integral "analysis/")) shostak)) (atan_value_0 0 (atan_value_0-2 nil 3352180534 ("" (expand "atan_value") (("" (lemma "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) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (atan_deriv_fn const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (Integral_a_to_a formula-decl nil integral "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (atan_value const-decl "real" atan nil)) nil) (atan_value_0-1 nil 3255979393 ("" (expand "atan_value") (("" (lemma "Integral_a_to_a" ("a" "0" "f" "atan_deriv_fn")) (("" (propax) nil nil)) nil)) nil) ((Integral_a_to_a formula-decl nil integral "analysis/")) shostak)) (atan_neg_value 0 (atan_neg_value-3 "fixit" 3394184058 ("" (lemma "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" (lemma "neg_derivable_fun[real]" ("f" "LAMBDA (x:real): x")) (("1" (lemma "deriv_neg_fun[real]" ("ff" "LAMBDA (x: real): x")) (("1" (expand "I") (("1" (lemma "one_over_one_plus_t_sq_cont") (("1" (lemma "fundamental[real]" ("f" "atan_deriv_fn" "a" "0" "F" "atan_value")) (("1" (split -1) (("1" (flatten -1) (("1" (lemma "composition_derivable_fun[real,real]" ("f" "-(LAMBDA (x: real): x)" "g" "atan_value")) (("1" (lemma "composition_derivable_fun[real,real]" ("g" "-(LAMBDA (x: real): x)" "f" "atan_value")) (("1" (assert) (("1" (assert) (("1" (lemma "deriv_comp_fun[real,real]" ("ff" "-(LAMBDA (x: real): x)" "gg" "atan_value")) (("1" (lemma "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" (simplify -8) (("1" (replace -8) (("1" (simplify -2) (("1" (simplify -1) (("1" (replace -1) (("1" (replace -2) (("1" (lemma "extensionality_postulate" ("f" "LAMBDA (x: real): atan_deriv_fn(-x) * -1" "g" "LAMBDA (x: real): -1 * atan_deriv_fn(x)")) (("1" (split -13) (("1" (skosimp*) (("1" (lemma "extensionality_postulate" ("f" "(LAMBDA (z: real): atan_value(-z))" "g" "(LAMBDA (z: real): -atan_value(z)) + (LAMBDA (x: real): c!1)")) (("1" (replace -1 -2 rl) (("1" (inst-cp -2 "0") (("1" (expand "+") (("1" (rewrite "atan_value_0") (("1" (inst -2 "x") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("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) ((not_one_element formula-decl nil taylors "analysis/") (deriv_id_fun formula-decl nil derivatives "analysis/") (deriv_neg_fun formula-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (one_over_one_plus_t_sq_cont formula-decl nil atan nil) (composition_derivable_fun formula-decl nil chain_rule "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (deriv_comp_fun formula-decl nil chain_rule "analysis/") (O const-decl "T3" function_props nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (atan_value_0 formula-decl nil atan nil) (minus_even_is_even application-judgement "even_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (extensionality_postulate formula-decl nil functions nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (atan_deriv_fn const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (fundamental formula-decl nil fundamental_theorem "analysis/") (I const-decl "(bijective?[T, T])" identity nil) (derivable_id name-judgement "deriv_fun" derivatives "analysis/") (id_fun_continuous name-judgement "continuous_fun" continuous_functions "analysis/") (id_fun_continuous name-judgement "continuous_fun[T2]" lim_of_composition "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" unif_cont_fun "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral_step "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral_split_scaf "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" indefinite_integral "analysis/") (neg_derivable_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (bool nonempty-type-eq-decl nil booleans nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (minus_real_is_real application-judgement "real" reals nil) (derivs_eq formula-decl nil indefinite_integral "analysis/") (atan_value const-decl "real" atan nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil)) nil) (atan_neg_value-2 nil 3352180601 ("" (lemma "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" (lemma "neg_derivable_fun[real]" ("f" "LAMBDA (x:real): x")) (("1" (lemma "deriv_neg_fun[real]" ("ff" "LAMBDA (x: real): x")) (("1" (expand "I") (("1" (lemma "one_over_one_plus_t_sq_cont") (("1" (lemma "fundamental[real]" ("f" "atan_deriv_fn" "a" "0" "F" "atan_value")) (("1" (split -1) (("1" (flatten -1) (("1" (lemma "composition_derivable_fun[real,real]" ("f" "-(LAMBDA (x: real): x)" "g" "atan_value")) (("1" (lemma "composition_derivable_fun[real,real]" ("g" "-(LAMBDA (x: real): x)" "f" "atan_value")) (("1" (assert) (("1" (assert) (("1" (lemma "deriv_comp_fun[real,real]" ("ff" "-(LAMBDA (x: real): x)" "gg" "atan_value")) (("1" (lemma "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" (simplify -8) (("1" (replace -8) (("1" (simplify -2) (("1" (simplify -1) (("1" (replace -1) (("1" (replace -2) (("1" (assert) (("1" (lemma "extensionality_postulate" ("f" "LAMBDA (x: real): atan_deriv_fn(-x) * -1" "g" "LAMBDA (x: real): -1 * atan_deriv_fn(x)")) (("1" (replace -1 -13 rl) (("1" (split -13) (("1" (skosimp*) (("1" (lemma "extensionality_postulate" ("f" "(LAMBDA (z: real): atan_value(-z))" "g" "(LAMBDA (z: real): -atan_value(z)) + (LAMBDA (x: real): c!1)")) (("1" (replace -1 -2 rl) (("1" (inst-cp -2 "0") (("1" (expand "+") (("1" (rewrite "atan_value_0") (("1" (inst -2 "x") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "atan_deriv_fn") (("2" (lemma "sq_neg" ("a" "x!1")) (("2" (expand "sq") (("2" (replace -1) (("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) ((deriv_id_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (constant_seq2 application-judgement "(convergent_nz?)" convergence_ops "analysis/") (const_fun_continuous application-judgement "continuous_fun[T]" integral "analysis/") (deriv_comp_fun formula-decl nil chain_rule "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (sq const-decl "nonneg_real" sq "reals/") (sq_neg formula-decl nil sq "reals/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (fundamental formula-decl nil fundamental_theorem "analysis/") (derivable_id name-judgement "deriv_fun" derivatives "analysis/") (id_fun_continuous name-judgement "continuous_fun" continuous_functions "analysis/") (id_fun_continuous name-judgement "continuous_fun[T2]" lim_of_composition "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" unif_cont_fun "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral_step "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral_split_scaf "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral "analysis/") (neg_derivable_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/")) nil) (atan_neg_value-1 nil 3255979648 ("" (lemma "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]") (("" (lemma "neg_derivable_fun[real]" ("f" "LAMBDA (x:real): x")) (("" (lemma "deriv_neg_fun" ("ff" "LAMBDA (x: real): x")) (("1" (expand "I") (("1" (lemma "one_over_one_plus_t_sq_cont") (("1" (lemma "fundamental[real]" ("f" "atan_deriv_fn" "a" "0" "F" "atan_value")) (("1" (split -1) (("1" (flatten -1) (("1" (lemma "composition_derivable_fun" ("f" "-(LAMBDA (x: real): x)" "g" "atan_value")) (("1" (lemma "composition_derivable_fun" ("g" "-(LAMBDA (x: real): x)" "f" "atan_value")) (("1" (assert) (("1" (assert) (("1" (lemma "deriv_comp_fun" ("ff" "-(LAMBDA (x: real): x)" "gg" "atan_value")) (("1" (lemma "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" (simplify -8) (("1" (replace -8) (("1" (simplify -2) (("1" (simplify -1) (("1" (replace -1) (("1" (replace -2) (("1" (assert) (("1" (lemma "extensionality_postulate" ("f" "LAMBDA (x: real): atan_deriv_fn(-x) * -1" "g" "LAMBDA (x: real): -1 * atan_deriv_fn(x)")) (("1" (replace -1 -13 rl) (("1" (split -13) (("1" (skosimp*) (("1" (lemma "extensionality_postulate" ("f" "(LAMBDA (z: real): atan_value(-z))" "g" "(LAMBDA (z: real): -atan_value(z)) + (LAMBDA (x: real): c!1)")) (("1" (replace -1 -2 rl) (("1" (inst-cp -2 "0") (("1" (expand "+") (("1" (rewrite "atan_value_0") (("1" (inst -2 "x") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "atan_deriv_fn") (("2" (lemma "sq_neg" ("a" "x!1")) (("2" (expand "sq") (("2" (replace -1) (("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) ((deriv_id_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (deriv_comp_fun formula-decl nil chain_rule "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (sq const-decl "nonneg_real" sq "reals/") (sq_neg formula-decl nil sq "reals/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (fundamental formula-decl nil fundamental_theorem "analysis/") (neg_derivable_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/")) shostak)) (atan_inv_value 0 (atan_inv_value-2 nil 3352181608 ("" (lemma "derivs_eq[posreal]" ("F" "LAMBDA (x:posreal): atan_value(x)" "G" "LAMBDA (x:posreal): atan_value(-1/x)")) (("1" (skolem 1 ("x")) (("1" (lemma "fundamental[real]" ("f" "atan_deriv_fn" "F" "atan_value" "a" "0")) (("1" (split -1) (("1" (flatten -1) (("1" (lemma "restrict2_derivable[posreal,real]" ("f" "atan_value")) (("1" (lemma "restrict2_deriv[posreal,real]" ("f" "atan_value")) (("1" (expand "restrict2") (("1" (replace -2) (("1" (lemma "composition_derivable_fun[posreal,real]" ("f" "LAMBDA (x: posreal): -(1 / x)" "g" "atan_value")) (("1" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "deriv_id_fun[posreal]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "inv_derivable_fun[posreal]" ("g" "(LAMBDA (x: posreal): x)")) (("1" (assert) (("1" (expand "/") (("1" (lemma "deriv_inv_fun[posreal]" ("gg" "(LAMBDA (x: posreal): x)")) (("1" (replace -3) (("1" (expand "-") (("1" (expand "/") (("1" (expand "*") (("1" (lemma "neg_derivable_fun[posreal]" ("f" "LAMBDA (x_1: posreal): 1 / x_1")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_neg_fun[posreal]" ("ff" "LAMBDA (x_1: posreal): 1 / x_1")) (("1" (expand "-") (("1" (replace -3 -1) (("1" (simplify -1) (("1" (lemma "composition_derivable_fun[posreal,real]" ("f" "LAMBDA (x: posreal): -(1 / x)" "g" "atan_value")) (("1" (lemma "deriv_comp_fun[posreal,real]" ("ff" "LAMBDA (x: posreal): -(1 / x)" "gg" "atan_value")) (("1" (expand "o") (("1" (assert) (("1" (replace -13) (("1" (replace -3) (("1" (expand "*") (("1" (expand "atan_deriv_fn" -1) (("1" (lemma "deriv_comp_fun[posreal,real]" ("ff" "LAMBDA (x:posreal): x" "gg" "atan_value")) (("1" (expand "o") (("1" (replace -13) (("1" (replace -8) (("1" (expand "*") (("1" (expand "atan_deriv_fn" -1) (("1" (replace -1 -14) (("1" (replace -2 -14) (("1" (lemma "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 -15 rl) (("1" (hide -1) (("1" (simplify -14) (("1" (split -14) (("1" (skolem -1 ("c")) (("1" (lemma "extensionality_postulate" ("f" "(LAMBDA (x: posreal): atan_value(x))" "g" "(LAMBDA (x: posreal): atan_value(-1 / x)) + (LAMBDA (x: posreal): c)")) (("1" (replace -1 -2 rl) (("1" (hide-all-but (-2 1)) (("1" (expand "+") (("1" (inst-cp - "1") (("1" (inst - "x") (("1" (lemma "atan_neg_value") (("1" (inst-cp - "1") (("1" (inst - "1/x") (("1" (replace -1) (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skolem 1 ("z")) (("2" (lemma "div_times" ("x" "1" "n0x" "1 + -(1 / z) * -(1 / z)" "y" "1" "n0y" "z*z")) (("2" (replace -1 1) (("2" (hide -1) (("2" (rewrite "cross_mult") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "1/x!1") (("2" (lemma "negreal_times_negreal_is_posreal" ("nx" "-(1/x!1)" "ny" "-(1/x!1)")) (("1" (assert) (("1" (name-replace "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" (propax) 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) ((not_one_element formula-decl nil taylors "analysis/") (restrict2_derivable formula-decl nil restrict2_deriv "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (= const-decl "[T, T -> boolean]" equalities nil) (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (composition_derivable_fun formula-decl nil chain_rule "analysis/") (deriv_id_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (deriv_inv_fun formula-decl nil derivatives "analysis/") (nz_deriv_fun type-eq-decl nil derivatives "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[T -> real]" real_fun_ops "reals/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (deriv_neg_fun formula-decl nil derivatives "analysis/") (O const-decl "T3" function_props nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (extensionality_postulate formula-decl nil functions nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (atan_neg_value formula-decl nil atan nil) (minus_real_is_real application-judgement "real" reals nil) (cross_mult formula-decl nil real_props nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_times formula-decl nil real_props nil) (negreal_times_negreal_is_posreal judgement-tcc nil real_types nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (negreal nonempty-type-eq-decl nil real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (deriv_comp_fun formula-decl nil chain_rule "analysis/") (neg_derivable_fun formula-decl nil derivatives "analysis/") (/ const-decl "[T -> real]" real_fun_ops "reals/") (/ const-decl "[T -> real]" real_fun_ops "reals/") (nzreal nonempty-type-eq-decl nil reals nil) (inv_derivable_fun formula-decl nil derivatives "analysis/") (I const-decl "(bijective?[T, T])" identity nil) (identity_derivable_fun formula-decl nil derivatives "analysis/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (restrict2_deriv formula-decl nil restrict2_deriv "analysis/") (one_over_one_plus_t_sq_cont formula-decl nil atan nil) (atan_deriv_fn const-decl "posreal" atan nil) (fundamental formula-decl nil fundamental_theorem "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (derivs_eq formula-decl nil indefinite_integral "analysis/") (atan_value const-decl "real" atan nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil)) nil) (atan_inv_value-1 nil 3256911357 ("" (lemma "derivs_eq[posreal]" ("F" "LAMBDA (x:posreal): atan_value(x)" "G" "LAMBDA (x:posreal): atan_value(-1/x)")) (("1" (skolem 1 ("x")) (("1" (lemma "fundamental" ("f" "atan_deriv_fn" "F" "atan_value" "a" "0")) (("1" (split -1) (("1" (flatten -1) (("1" (lemma "restrict2_derivable[posreal,real]" ("f" "atan_value")) (("1" (lemma "restrict2_deriv[posreal,real]" ("f" "atan_value")) (("1" (expand "restrict2") (("1" (replace -2) (("1" (lemma "composition_derivable_fun" ("f" "LAMBDA (x: posreal): -(1 / x)" "g" "atan_value")) (("1" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "deriv_id_fun[posreal]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "inv_derivable_fun" ("g" "(LAMBDA (x: posreal): x)")) (("1" (assert) (("1" (expand "/") (("1" (lemma "deriv_inv_fun" ("gg" "(LAMBDA (x: posreal): x)")) (("1" (replace -3) (("1" (expand "-") (("1" (expand "/") (("1" (expand "*") (("1" (lemma "neg_derivable_fun" ("f" "LAMBDA (x_1: posreal): 1 / x_1")) (("1" (assert) (("1" (expand "-") (("1" (lemma "deriv_neg_fun" ("ff" "LAMBDA (x_1: posreal): 1 / x_1")) (("1" (expand "-") (("1" (replace -3 -1) (("1" (simplify -1) (("1" (lemma "composition_derivable_fun" ("f" "LAMBDA (x: posreal): -(1 / x)" "g" "atan_value")) (("1" (lemma "deriv_comp_fun" ("ff" "LAMBDA (x: posreal): -(1 / x)" "gg" "atan_value")) (("1" (expand "o") (("1" (assert) (("1" (replace -13) (("1" (replace -3) (("1" (expand "*") (("1" (expand "atan_deriv_fn" -1) (("1" (lemma "deriv_comp_fun" ("ff" "LAMBDA (x:posreal): x" "gg" "atan_value")) (("1" (expand "o") (("1" (replace -13) (("1" (replace -8) (("1" (expand "*") (("1" (expand "atan_deriv_fn" -1) (("1" (replace -1 -14) (("1" (replace -2 -14) (("1" (lemma "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 -15 rl) (("1" (hide -1) (("1" (simplify -14) (("1" (split -14) (("1" (skolem -1 ("c")) (("1" (lemma "extensionality_postulate" ("f" "(LAMBDA (x: posreal): atan_value(x))" "g" "(LAMBDA (x: posreal): atan_value(-1 / x)) + (LAMBDA (x: posreal): c)")) (("1" (replace -1 -2 rl) (("1" (hide-all-but (-2 1)) (("1" (expand "+") (("1" (inst-cp - "1") (("1" (inst - "x") (("1" (lemma "atan_neg_value") (("1" (inst-cp - "1") (("1" (inst - "1/x") (("1" (replace -1) (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skolem 1 ("z")) (("2" (lemma "div_times" ("x" "1" "n0x" "1 + -(1 / z) * -(1 / z)" "y" "1" "n0y" "z*z")) (("2" (replace -1 1) (("2" (hide -1) (("2" (rewrite "cross_mult") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "1/x!1") (("2" (lemma "negreal_times_negreal_is_posreal" ("nx" "-(1/x!1)" "ny" "-(1/x!1)")) (("1" (assert) (("1" (name-replace "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" (propax) 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) ((restrict2_derivable formula-decl nil restrict2_deriv "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (deriv_id_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (deriv_inv_fun formula-decl nil derivatives "analysis/") (nz_deriv_fun type-eq-decl nil derivatives "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (deriv_comp_fun formula-decl nil chain_rule "analysis/") (neg_derivable_fun formula-decl nil derivatives "analysis/") (inv_derivable_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (restrict2_deriv formula-decl nil restrict2_deriv "analysis/") (fundamental formula-decl nil fundamental_theorem "analysis/")) shostak)) (atan_inv_neg_value 0 (atan_inv_neg_value-1 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) ((negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (atan_inv_value formula-decl nil atan nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnreal_div_negreal_is_npreal application-judgement "npreal" real_types nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (minus_even_is_even application-judgement "even_int" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (atan_neg_value formula-decl nil atan nil)) shostak)) (atan_value_strict_increasing 0 (atan_value_strict_increasing-2 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" (lemma "fundamental[real]" ("f" "atan_deriv_fn" "F" "atan_value" "a" "0")) (("2" (assert) (("2" (split -1) (("1" (flatten) (("1" (expand "deriv" -2) (("1" (lemma "extensionality_postulate" ("g" "atan_deriv_fn" "f" "LAMBDA (x: real): deriv(atan_value, x)")) (("1" (replace -1 -3 rl) (("1" (inst -3 "x") (("1" (replace -3 1) (("1" (typepred "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" (lemma "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) ((atan_deriv_fn const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (fundamental formula-decl nil fundamental_theorem "analysis/") (deriv const-decl "[T -> real]" derivatives "analysis/") (NOT const-decl "[bool -> bool]" booleans nil) (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (deriv const-decl "real" derivatives_def "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (extensionality_postulate formula-decl nil functions nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (one_over_one_plus_t_sq_cont formula-decl nil atan nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (positive_derivative formula-decl nil derivative_props "analysis/") (bool nonempty-type-eq-decl nil booleans nil) (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (atan_value const-decl "real" atan nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil)) nil) (atan_value_strict_increasing-1 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) ((deriv_fun type-eq-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (positive_derivative formula-decl nil derivative_props "analysis/") (derivable? const-decl "bool" derivatives_def "analysis/") (deriv const-decl "real" derivatives_def "analysis/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (deriv_domain_real formula-decl nil deriv_domain "analysis/") (deriv const-decl "[T -> real]" derivatives "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (fundamental formula-decl nil fundamental_theorem "analysis/")) shostak)) (atan_value_minus_x1_TCC1 0 (atan_value_minus_x1_TCC1-1 nil 3256964578 ("" (skosimp*) (("" (lemma "div_mult_pos_lt1" ("z" "-1" "py" "py!1" "x" "x!1")) (("" (assert) nil nil)) nil)) nil) ((- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (atan_value_minus_x1 0 (atan_value_minus_x1-2 nil 3352182175 ("" (skolem 1 ("z" "x")) (("" (flatten) (("" (typepred "z") (("" (hide -1) (("" (lemma "div_mult_pos_lt1" ("z" "-1" "py" "z" "x" "x")) (("" (assert) (("" (lemma "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" (lemma "identity_derivable_fun[{a:real| -1/z<a}]") (("1" (lemma "deriv_id_fun[{a:real| -1/z<a}]") (("1" (expand "I") (("1" (lemma "deriv_const_fun[{a: real | -1 / z < a}]" ("b" "1")) (("1" (lemma "const_derivable_fun[{a: real | -1 / z < a}]" ("b" "1")) (("1" (lemma "const_derivable_fun[{a: real | -1 / z < a}]" ("b" "z")) (("1" (lemma "deriv_const_fun[{a: real | -1 / z < a}]" ("b" "z")) (("1" (lemma "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" (lemma "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" (simplify -1) (("1" (lemma "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" (lemma "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 -3) (("1" (replace -8) (("1" (expand "+") (("1" (lemma "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" (lemma "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 -7) (("1" (replace -11) (("1" (expand "-") (("1" (lemma "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" (lemma "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 -3) (("1" (replace -6) (("1" (expand "/") (("1" (expand "-") (("1" (expand "*") (("1" (lemma "composition_derivable_fun[{a: real | -1 / z < a},real]" ("f" "LAMBDA (x: {a: real | -1 / z < a}): x" "g" "atan_value")) (("1" (lemma "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" (lemma "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" (lemma "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 -17) (("1" (replace -21) (("1" (replace -5) (("1" (expand "*") (("1" (lemma "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 -2) (("1" (replace -3) (("1" (hide -2 -3 -6 -8 -11) (("1" (lemma "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 * "g" "LAMBDA (x_1: {a: real | -1 / z < a}): atan_deriv_fn(x_1)")) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (split -1) (("1" (skolem -1 ("c")) (("1" (expand "const_fun") (("1" (expand "+") (("1" (lemma "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 -2 rl) (("1" (hide -1) (("1" (simplify -1) (("1" (inst-cp -1 "0") (("1" (rewrite "atan_value_0" -2) (("1" (simplify -2) (("1" (lemma "atan_neg_value" ("x" "z")) (("1" (replace -1) (("1" (replace -3 -2 rl) (("1" (inst -2 "x") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "div_mult_pos_lt1" ("z" "-1" "py" "z" "x" "0")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -18)) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (lemma "div_mult_pos_lt1" ("z" "-1" "x" "x!1" "py" "z")) (("2" (assert) (("2" (lemma "posreal_times_posreal_is_posreal" ("px" "1+x!1*z" "py" "1+x!1*z")) (("2" (lemma "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 lr) (("1" (hide -1) (("1" (name "XMZ" "x!1-z") (("1" (replace -1) (("1" (name "XZP1" "1+x!1*z") (("1" (replace -1) (("1" (name "ZSQP1" "1+z*z") (("1" (replace -1) (("1" (expand "atan_deriv_fn") (("1" (lemma "sq_pos" ("a" "x!1")) (("1" (lemma "sq_pos" ("a" "XMZ/XZP1")) (("1" (expand "sq") (("1" (lemma "cross_mult" ("x" "ZSQP1" "n0x" "1 + XMZ / XZP1 * (XMZ / XZP1)" "y" "XZP1 * XZP1" "n0y" "1 + x!1 * x!1")) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "div_times" ("x" "XMZ" "n0x" "XZP1" "y" "XMZ" "n0y" "XZP1")) (("1" (replace -1 1) (("1" (lemma "div_cancel1" ("n0z" "XZP1 * XZP1" "x" "XMZ * XMZ")) (("1" (simplify 1) (("1" (replace -1 1) (("1" (replace -7 * rl) (("1" (replace -6 * rl) (("1" (replace -5 * rl) (("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" (hide -1 2) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (lemma "div_mult_pos_lt1" ("z" "-1" "py" "z" "x" "x!1")) (("2" (assert) (("2" (lemma "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" (hide-all-but 1) (("2" (inst + "0") (("2" (cross-mult 1) nil nil)) nil)) nil)) nil) ("3" (assert) (("3" (expand "connected?") (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (cross-mult -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "not_one_element?") (("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide 2 -1 -2 -3) (("3" (expand "deriv_domain?") (("3" (skosimp*) (("3" (inst + "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_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (one_over_one_plus_t_sq_cont formula-decl nil atan nil) (identity_derivable_fun formula-decl nil derivatives "analysis/") (< const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (I const-decl "(bijective?[T, T])" identity nil) (const_derivable_fun formula-decl nil derivatives "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (sum_derivable_fun formula-decl nil derivatives "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (/ const-decl "[T -> real]" real_fun_ops "reals/") (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (O const-decl "T3" function_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (extensionality_postulate formula-decl nil functions nil) (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (sq_pos formula-decl nil sq "reals/") (sq const-decl "nonneg_real" sq "reals/") (div_times formula-decl nil real_props nil) (div_cancel1 formula-decl nil real_props nil) (cross_mult formula-decl nil real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (atan_value_0 formula-decl nil atan nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (atan_neg_value formula-decl nil atan nil) (minus_real_is_real application-judgement "real" reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (z skolem-const-decl "posreal" atan nil) (npreal_div_posreal_is_npreal application-judgement "npreal" real_types nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (TRUE const-decl "bool" booleans nil) (derivs_eq formula-decl nil indefinite_integral "analysis/") (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (deriv_comp_fun formula-decl nil chain_rule "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (nz_deriv_fun type-eq-decl nil derivatives "analysis/") (deriv_div_fun formula-decl nil derivatives "analysis/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (div_derivable_fun formula-decl nil derivatives "analysis/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (deriv_sum_fun formula-decl nil derivatives "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (deriv_fun type-eq-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_prod_fun formula-decl nil derivatives "analysis/") (prod_derivable_fun formula-decl nil derivatives "analysis/") (deriv_const_fun formula-decl nil derivatives "analysis/") (deriv_id_fun formula-decl nil derivatives "analysis/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}" real_defs nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (atan_deriv_fn const-decl "posreal" atan nil) (atan_value const-decl "real" atan nil) (fundamental formula-decl nil fundamental_theorem "analysis/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil)) nil) (atan_value_minus_x1-1 nil 3256965562 ("" (skolem 1 ("z" "x")) (("" (flatten) (("" (typepred "z") (("" (hide -1) (("" (lemma "div_mult_pos_lt1" ("z" "-1" "py" "z" "x" "x")) (("" (assert) (("" (lemma "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) (("" (lemma "identity_derivable_fun[{a:real| -1/z<a}]") (("1" (lemma "deriv_id_fun[{a:real| -1/z<a}]") (("1" (expand "I") (("1" (lemma "deriv_const_fun[{a: real | -1 / z < a}]" ("b" "1")) (("1" (lemma "const_derivable_fun[{a: real | -1 / z < a}]" ("b" "1")) (("1" (lemma "const_derivable_fun[{a: real | -1 / z < a}]" ("b" "z")) (("1" (lemma "deriv_const_fun[{a: real | -1 / z < a}]" ("b" "z")) (("1" (expand "const_fun") (("1" (lemma "prod_derivable_fun" ("f1" "LAMBDA (x: {a: real | -1 / z < a}): x" "f2" "LAMBDA (x: {a: real | -1 / z < a}): z")) (("1" (assert) (("1" (lemma "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" (simplify -1) (("1" (lemma "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" (lemma "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 -3) (("1" (replace -8) (("1" (expand "+") (("1" (lemma "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" (lemma "deriv_diff_fun" ("ff1" "LAMBDA (x: {a: real | -1 / z < a}): x" "ff2" "LAMBDA (x_1: {a: real | -1 / z < a}): z")) (("1" (replace -7) (("1" (replace -11) (("1" (expand "-") (("1" (lemma "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" (lemma "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 -3) (("1" (replace -6) (("1" (expand "/") (("1" (expand "-") (("1" (expand "*") (("1" (lemma "composition_derivable_fun" ("f" "LAMBDA (x: {a: real | -1 / z < a}): x" "g" "atan_value")) (("1" (lemma "composition_derivable_fun" ("f" "LAMBDA (x: {a: real | -1 / z < a}): (x - z) / (1 + x * z)" "g" "atan_value")) (("1" (lemma "deriv_comp_fun" ("ff" "LAMBDA (x: {a: real | -1 / z < a}): (x - z) / (1 + x * z)" "gg" "atan_value")) (("1" (lemma "deriv_comp_fun" ("ff" "LAMBDA (x: {a: real | -1 / z < a}): x" "gg" "atan_value")) (("1" (assert) (("1" (expand "o") (("1" (replace -17) (("1" (replace -21) (("1" (replace -5) (("1" (expand "*") (("1" (lemma "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 -2) (("1" (replace -3) (("1" (hide -2 -3 -6 -8 -11) (("1" (lemma "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 * "g" "LAMBDA (x_1: {a: real | -1 / z < a}): atan_deriv_fn(x_1)")) (("1" (replace -1 -2 rl) (("1" (hide -1) (("1" (split -1) (("1" (skolem -1 ("c")) (("1" (expand "const_fun") (("1" (expand "+") (("1" (lemma "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 -2 rl) (("1" (hide -1) (("1" (simplify -1) (("1" (inst-cp -1 "0") (("1" (rewrite "atan_value_0" -2) (("1" (simplify -2) (("1" (lemma "atan_neg_value" ("x" "z")) (("1" (replace -1) (("1" (replace -3 -2 rl) (("1" (inst -2 "x") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "div_mult_pos_lt1" ("z" "-1" "py" "z" "x" "0")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -18)) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (lemma "div_mult_pos_lt1" ("z" "-1" "x" "x!1" "py" "z")) (("2" (assert) (("2" (lemma "posreal_times_posreal_is_posreal" ("px" "1+x!1*z" "py" "1+x!1*z")) (("2" (lemma "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 lr) (("1" (hide -1) (("1" (name "XMZ" "x!1-z") (("1" (replace -1) (("1" (name "XZP1" "1+x!1*z") (("1" (replace -1) (("1" (name "ZSQP1" "1+z*z") (("1" (replace -1) (("1" (expand "atan_deriv_fn") (("1" (lemma "sq_pos" ("a" "x!1")) (("1" (lemma "sq_pos" ("a" "XMZ/XZP1")) (("1" (expand "sq") (("1" (lemma "cross_mult" ("x" "ZSQP1" "n0x" "1 + XMZ / XZP1 * (XMZ / XZP1)" "y" "XZP1 * XZP1" "n0y" "1 + x!1 * x!1")) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "div_times" ("x" "XMZ" "n0x" "XZP1" "y" "XMZ" "n0y" "XZP1")) (("1" (replace -1 1) (("1" (lemma "div_cancel1" ("n0z" "XZP1 * XZP1" "x" "XMZ * XMZ")) (("1" (simplify 1) (("1" (replace -1 1) (("1" (replace -7 * rl) (("1" (replace -6 * rl) (("1" (replace -5 * rl) (("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" (hide -1 2) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (lemma "div_mult_pos_lt1" ("z" "-1" "py" "z" "x" "x!1")) (("2" (assert) (("2" (lemma "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" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "x!1") (("2" (cross-mult -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil) ("3" (hide 2 -1 -2 -3) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((identity_derivable_fun formula-decl nil derivatives "analysis/") (const_derivable_fun formula-decl nil derivatives "analysis/") (prod_derivable_fun formula-decl nil derivatives "analysis/") (deriv_prod_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (deriv_sum_fun formula-decl nil derivatives "analysis/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (deriv_diff_fun formula-decl nil derivatives "analysis/") (div_derivable_fun formula-decl nil derivatives "analysis/") (deriv_div_fun formula-decl nil derivatives "analysis/") (nz_deriv_fun type-eq-decl nil derivatives "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (deriv_comp_fun formula-decl nil chain_rule "analysis/") (sq const-decl "nonneg_real" sq "reals/") (sq_pos formula-decl nil sq "reals/") (sum_derivable_fun formula-decl nil derivatives "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (deriv_const_fun formula-decl nil derivatives "analysis/") (deriv_id_fun formula-decl nil derivatives "analysis/") (fundamental formula-decl nil fundamental_theorem "analysis/")) shostak)) (atan_value_minus_x2_TCC1 0 (atan_value_minus_x2_TCC1-1 nil 3256964644 ("" (skosimp*) (("" (lemma "div_mult_pos_lt2" ("z" "-1" "py" "py!1" "x" "x!1")) (("" (assert) nil nil)) nil)) nil) ((- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (atan_value_minus_x2 0 (atan_value_minus_x2-1 nil 3256974044 ("" (skolem 1 ("z" "x")) (("" (flatten) (("" (typepred "z") (("" (hide -1) (("" (lemma "atan_inv_value" ("px" "z")) (("" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "z")) (("" (lemma "atan_inv_neg_value" ("nx" "x")) (("1" (lemma "atan_value_minus_x1" ("py" "1/z" "x" "1/x")) (("1" (rewrite "div_div1" -1) (("1" (lemma "div_mult_neg_lt2" ("z" "1" "x" "-z" "ny" "x")) (("1" (lemma "div_mult_pos_lt2" ("z" "-1" "x" "x" "py" "z")) (("1" (assert) (("1" (lemma "minus_div1" ("x" "1" "y" "1" "n0x" "x" "n0y" "z")) (("1" (replace -1 -4) (("1" (lemma "add_div" ("x" "1" "y" "1" "n0x" "1" "n0y" "x*z")) (("1" (replace -1 -5) (("1" (rewrite "div_div1" -5) (("1" (lemma "div_cancel2" ("x" "z-x" "n0z" "x*z")) (("1" (replace -1 -6) (("1" (lemma "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) ((posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (atan_value_minus_x1 formula-decl nil atan nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (div_mult_neg_lt2 formula-decl nil real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (div_cancel2 formula-decl nil real_props nil) (atan_neg_value formula-decl nil atan nil) (minus_real_is_real application-judgement "real" reals nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (add_div formula-decl nil real_props nil) (minus_div1 formula-decl nil real_props nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_even_is_even application-judgement "even_int" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (div_div1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (atan_inv_neg_value formula-decl nil atan nil) (atan_inv_value formula-decl nil atan nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil)) shostak)) (atan_value_minus_TCC1 0 (atan_value_minus_TCC1-1 nil 3255979356 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (atan_value_minus_TCC2 0 (atan_value_minus_TCC2-1 nil 3257273262 ("" (skolem 1 ("x" "y")) (("" (flatten) (("" (hide -1) (("" (assert) nil nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (atan_value_minus_TCC3 0 (atan_value_minus_TCC3-1 nil 3257273262 ("" (skolem 1 ("x" "y")) (("" (flatten) (("" (hide -1 -2) (("" (assert) nil nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (atan_value_minus 0 (atan_value_minus-1 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" (lemma "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" (lemma "atan_value_minus_x1" ("x" "-x" "py" "-y")) (("1" (lemma "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" (lemma "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" (lemma "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" (lemma "div_mult_pos_lt2" ("x" "-x" "py" "-y" "z" "-1")) (("1" (rewrite "atan_neg_value" -2) (("1" (rewrite "atan_neg_value" -2) (("1" (lemma "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) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (trichotomy formula-decl nil real_axioms nil) (minus_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (atan_neg_value formula-decl nil atan nil) (atan_value_0 formula-decl nil atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (atan_value_minus_x1 formula-decl nil atan nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (atan_value_minus_x2 formula-decl nil atan nil) (div_mult_pos_lt2 formula-decl nil real_props nil)) shostak)) (pi_TCC1 0 (pi_TCC1-1 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) ((strict_increasing? const-decl "bool" real_fun_preds "reals/") (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (atan_value_0 formula-decl nil atan nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (atan_value_strict_increasing formula-decl nil atan nil)) shostak)) (real_abs_lt_pi2_TCC1 0 (real_abs_lt_pi2_TCC1-1 nil 3323022914 ("" (typepred "pi") (("" (rewrite "abs_0") (("" (assert) nil nil)) nil)) nil) ((nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil)) nil)) (atan_TCC1 0 (atan_TCC1-1 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" (lemma "trich_lt" ("x" "x!1" "y" "1")) (("2" (split -1) (("1" (inst - "x!1" "1") (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) nil nil)) nil) ("3" (lemma "atan_value_minus" ("x" "x!1" "y" "1")) (("3" (assert) (("3" (inst -5 "(x!1-1)/(x!1+1)" "1") (("3" (lemma "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) ((atan_value_strict_increasing formula-decl nil atan nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (atan_value const-decl "real" atan nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (pi const-decl "posreal" atan nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (x skolem-const-decl "real" atan nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (atan_value_0 formula-decl nil atan nil) (minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (atan_neg_value formula-decl nil atan nil) (trichotomy formula-decl nil real_axioms nil) (trich_lt formula-decl nil real_props nil) (atan_value_minus formula-decl nil atan nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/")) shostak)) (pi_value 0 (pi_value-1 nil 3408904315 ("" (expand "atan") (("" (assert) (("" (expand "pi") (("" (propax) nil nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (pi const-decl "posreal" atan nil) (atan const-decl "real_abs_lt_pi2" atan nil)) shostak)) (atan_strict_increasing 0 (atan_strict_increasing-1 nil 3257226677 ("" (expand "atan") (("" (lemma "atan_value_strict_increasing") (("" (lemma "extensionality_postulate" ("f" "atan_value" "g" "LAMBDA (x: real): atan_value(x)")) (("" (assert) nil nil)) nil)) nil)) nil) ((atan_value_strict_increasing formula-decl nil atan nil) (extensionality_postulate formula-decl nil functions nil) (atan_value const-decl "real" atan nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (atan const-decl "real_abs_lt_pi2" atan nil)) shostak)) (atan_bij 0 (atan_bij-2 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" (lemma "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" (lemma "trich_lt" ("x" "y!1" "y" "atan_value(1)")) (("1" (split -1) (("1" (lemma "intermediate1[real]" ("g" "atan_value" "a" "0" "b" "1" "x" "y!1")) (("1" (rewrite "atan_value_0") (("1" (assert) (("1" (skosimp*) (("1" (inst + "c!1") nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (inst + "1") (("2" (assert) nil nil)) nil) ("3" (inst-cp - "0" "1") (("3" (assert) (("3" (rewrite "atan_value_0") (("3" (expand "pi") (("3" (inst-cp - "0" "1") (("3" (assert) (("3" (lemma "intermediate1[real]" ("a" "0" "b" "1" "x" "2*atan_value(1)-y!1" "g" "atan_value")) (("3" (rewrite "atan_value_0") (("3" (assert) (("3" (skolem -1 ("c")) (("3" (flatten) (("3" (expand "<=" -1) (("3" (split -1) (("1" (lemma "atan_inv_value" ("px" "1/c")) (("1" (inst + "1/c") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "c")) (("2" (assert) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil) ("2" (assert) (("2" (replace -1 * rl) (("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" (inst + "0") (("2" (rewrite "atan_value_0") (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "trich_lt" ("x" "y!1" "y" "-atan_value(1)")) (("3" (assert) (("3" (split -1) (("1" (expand "pi") (("1" (lemma "intermediate1[real]" ("a" "-1" "b" "0" "x" "-2*atan_value(1)-y!1" "g" "atan_value")) (("1" (rewrite "atan_neg_value" -1) (("1" (rewrite "atan_value_0" -1) (("1" (assert) (("1" (skolem -1 ("c")) (("1" (flatten) (("1" (expand "<=" -2) (("1" (split -2) (("1" (lemma "atan_inv_neg_value" ("nx" "c")) (("1" (replace -4 -1) (("1" (simplify -1) (("1" (inst + "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" (inst + "-1") (("2" (rewrite "atan_neg_value") (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "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" (skolem -1 ("c")) (("3" (flatten -1) (("3" (inst + "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" (lemma "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) ((atan_strict_increasing formula-decl nil atan nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (trich_lt formula-decl nil real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (injective? const-decl "bool" functions nil) (derivable_cont_fun formula-decl nil derivatives "analysis/") (atan_value const-decl "real" atan nil) (one_over_one_plus_t_sq_cont formula-decl nil atan nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (atan_deriv_fn const-decl "posreal" atan nil) (fundamental formula-decl nil fundamental_theorem "analysis/") (atan const-decl "real_abs_lt_pi2" atan nil) (atan_value_0 formula-decl nil atan nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (TRUE const-decl "bool" booleans nil) (continuous? const-decl "bool" continuous_functions "analysis/") (intermediate1 formula-decl nil continuous_functions_props "analysis/") (real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (<= const-decl "bool" reals nil) (atan_inv_value formula-decl nil atan nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (atan_neg_value formula-decl nil atan nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (atan_inv_neg_value formula-decl nil atan nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (trichotomy formula-decl nil real_axioms nil) (atan_value_strict_increasing formula-decl nil atan nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil)) nil) (atan_bij-1 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" (lemma "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" (lemma "trich_lt" ("x" "y!1" "y" "atan_value(1)")) (("1" (split -1) (("1" (lemma "intermediate1" ("g" "atan_value" "a" "0" "b" "1" "x" "y!1")) (("1" (rewrite "atan_value_0") (("1" (assert) (("1" (skosimp*) (("1" (inst + "c!1") nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (inst + "1") (("2" (assert) nil nil)) nil) ("3" (expand "abs") (("3" (inst-cp - "0" "1") (("3" (assert) (("3" (rewrite "atan_value_0") (("3" (lemma "intermediate1" ("a" "0" "b" "1" "x" "2*atan_value(1)-y!1" "g" "atan_value")) (("3" (rewrite "atan_value_0") (("3" (assert) (("3" (skolem -1 ("c")) (("3" (flatten) (("3" (expand "<=" -1) (("3" (split -1) (("1" (lemma "atan_inv_value" ("px" "1/c")) (("1" (inst + "1/c") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (lemma "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 -1 * rl) (("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" (inst + "0") (("2" (rewrite "atan_value_0") (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "trich_lt" ("x" "y!1" "y" "-atan_value(1)")) (("3" (expand "abs") (("3" (assert) (("3" (split -1) (("1" (lemma "intermediate1" ("a" "-1" "b" "0" "x" "-2*atan_value(1)-y!1" "g" "atan_value")) (("1" (rewrite "atan_neg_value" -1) (("1" (rewrite "atan_value_0" -1) (("1" (assert) (("1" (skolem -1 ("c")) (("1" (flatten) (("1" (expand "<=" -2) (("1" (split -2) (("1" (lemma "atan_inv_neg_value" ("nx" "c")) (("1" (replace -4 -1) (("1" (simplify -1) (("1" (inst + "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" (inst + "-1") (("2" (rewrite "atan_neg_value") (("2" (assert) nil nil)) nil)) nil) ("3" (lemma "intermediate1" ("a" "-1" "b" "0" "x" "y!1" "g" "atan_value")) (("3" (rewrite "atan_value_0") (("3" (rewrite "atan_neg_value") (("3" (assert) (("3" (skolem -1 ("c")) (("3" (flatten -1) (("3" (inst + "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" (lemma "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) ((strict_increasing? const-decl "bool" real_fun_preds "reals/") (fundamental formula-decl nil fundamental_theorem "analysis/") (intermediate1 formula-decl nil continuous_functions_props "analysis/")) shostak)) (atan_0 0 (atan_0-1 nil 3257226801 ("" (expand "atan") (("" (rewrite "atan_value_0") nil nil)) nil) ((atan_value_0 formula-decl nil atan nil) (atan const-decl "real_abs_lt_pi2" atan nil)) shostak)) (atan_inv 0 (atan_inv-1 nil 3264783397 ("" (skosimp*) (("" (expand "pi") (("" (expand "atan") (("" (lemma "atan_inv_value" ("px" "px!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (pi const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (atan_inv_value formula-decl nil atan nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (atan const-decl "real_abs_lt_pi2" atan nil)) shostak)) (atan_inv_neg 0 (atan_inv_neg-1 nil 3264783474 ("" (skosimp*) (("" (expand "pi") (("" (expand "atan") (("" (lemma "atan_inv_neg_value" ("nx" "nx!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (pi const-decl "posreal" atan nil) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (atan_inv_neg_value formula-decl nil atan nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnreal_div_negreal_is_npreal application-judgement "npreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (atan const-decl "real_abs_lt_pi2" atan nil)) shostak)) (atan_def_TCC1 0 (atan_def_TCC1-1 nil 3257225947 ("" (skolem 1 ("x")) (("" (lemma "one_over_one_plus_t_sq_cont") (("" (lemma "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) ((one_over_one_plus_t_sq_cont formula-decl nil atan nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (continuous? const-decl "bool" continuous_functions "analysis/") (Closed_interval type-eq-decl nil intervals_real "reals/") (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (continuous_Integrable? formula-decl nil integral "analysis/") (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (atan_deriv_fn const-decl "posreal" atan nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil)) shostak)) (atan_def 0 (atan_def-1 nil 3257226833 ("" (skolem 1 ("x")) (("" (expand "atan") (("" (expand "atan_value") (("" (expand "atan_deriv_fn") (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((atan const-decl "real_abs_lt_pi2" atan nil) (atan_deriv_fn const-decl "posreal" atan nil) (atan_value const-decl "real" atan nil)) shostak)) (acot_TCC1 0 (acot_TCC1-1 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) ((atan_0 formula-decl nil atan nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (quotient_pos_lt formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (quotient_neg_lt formula-decl nil real_props nil) (trichotomy formula-decl nil real_axioms nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (atan_strict_increasing formula-decl nil atan nil)) shostak)) (atan_neg 0 (atan_neg-1 nil 3257226889 ("" (lemma "atan_neg_value") (("" (expand "atan") (("" (propax) nil nil)) nil)) nil) ((atan const-decl "real_abs_lt_pi2" atan nil) (atan_neg_value formula-decl nil atan nil)) shostak)) (acot_neg 0 (acot_neg-1 nil 3257226968 ("" (expand "acot") (("" (skolem 1 ("nzx")) (("" (lemma "atan_neg" ("x" "1/nzx")) (("" (assert) nil nil)) nil)) nil)) nil) ((minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (atan_neg formula-decl nil atan nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nzreal nonempty-type-eq-decl nil reals nil) (acot const-decl "nzreal" atan nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (atan_minus_TCC1 0 (atan_minus_TCC1-1 nil 3257273266 ("" (skolem 1 ("x" "y")) (("" (flatten) (("" (hide -1) (("" (assert) nil nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (atan_minus_TCC2 0 (atan_minus_TCC2-1 nil 3257273266 ("" (skolem 1 ("x" "y")) (("" (flatten) (("" (hide -1 -2) (("" (assert) nil nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (atan_minus 0 (atan_minus-1 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) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (atan_value_minus formula-decl nil atan nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (pi const-decl "posreal" atan nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (atan const-decl "real_abs_lt_pi2" atan nil)) shostak)) (atan_plus_TCC1 0 (atan_plus_TCC1-1 nil 3257228828 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (atan_plus_TCC2 0 (atan_plus_TCC2-1 nil 3257273266 ("" (skolem 1 ("x" "y")) (("" (flatten) (("" (hide -1) (("" (assert) nil nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (atan_plus_TCC3 0 (atan_plus_TCC3-1 nil 3257275668 ("" (skolem 1 ("x" "y")) (("" (flatten) (("" (hide -1 -2) (("" (assert) nil nil)) nil)) nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (atan_plus 0 (atan_plus-1 nil 3257227479 ("" (skolem 1 ("x" "y")) (("" (lemma "atan_minus" ("x" "x" "y" "-y")) (("" (rewrite "atan_neg" -1) (("" (flatten) (("" (lemma "both_sides_times_neg_lt1" ("y" "x*y" "x" "1" "nz" "-1")) (("" (lemma "both_sides_times_neg_lt1" ("x" "x*y" "y" "1" "nz" "-1")) (("" (replace -1) (("" (replace -2) (("" (lemma "both_sides_times_neg_lt1" ("x" "y" "y" "0" "nz" "-1")) (("" (lemma "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) ((- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (atan_minus formula-decl nil atan nil) (minus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (trichotomy formula-decl nil real_axioms nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (negreal nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (<= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (both_sides_times_neg_lt1 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (atan_neg formula-decl nil atan nil)) shostak)) (atan_sub_swap_TCC1 0 (atan_sub_swap_TCC1-1 nil 3514307078 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (atan_sub_swap_TCC2 0 (atan_sub_swap_TCC2-1 nil 3514307078 ("" (subtype-tcc) nil nil) ((/= const-decl "boolean" notequal nil)) nil)) (atan_sub_swap_TCC3 0 (atan_sub_swap_TCC3-1 nil 3514307078 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (/= const-decl "boolean" notequal nil) (real_times_real_is_real application-judgement "real" reals nil)) nil)) (atan_sub_swap 0 (atan_sub_swap-1 nil 3514307078 ("" (skeep) (("" (lemma "atan_minus") (("" (inst?) (("" (assert) (("" (case-replace "(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) ((atan_minus formula-decl nil atan nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (expt def-decl "real" exponentiation nil) (^ const-decl "real" exponentiation nil) (>= const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil)) shostak)) (deriv_atan_fun 0 (deriv_atan_fun-2 nil 3352182759 ("" (lemma "one_over_one_plus_t_sq_cont") (("" (lemma "extensionality_postulate" ("f" "atan_deriv_fn" "g" "LAMBDA (x: real): 1 / (1 + x * x)")) (("1" (flatten -1) (("1" (hide -2) (("1" (split -1) (("1" (lemma "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) ((numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (atan_deriv_fn const-decl "posreal" atan nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (extensionality_postulate formula-decl nil functions nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (atan const-decl "real_abs_lt_pi2" atan nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (pi const-decl "posreal" atan nil) (- const-decl "[numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (fundamental formula-decl nil fundamental_theorem "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (atan_value const-decl "real" atan nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sq_pos formula-decl nil sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq const-decl "nonneg_real" sq "reals/") (one_over_one_plus_t_sq_cont formula-decl nil atan nil)) nil) (deriv_atan_fun-1 nil 3257228288 ("" (lemma "one_over_one_plus_t_sq_cont") (("" (lemma "extensionality_postulate" ("f" "atan_deriv_fn" "g" "LAMBDA (x: real): 1 / (1 + x * x)")) (("1" (flatten -1) (("1" (hide -2) (("1" (split -1) (("1" (lemma "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) ((fundamental formula-decl nil fundamental_theorem "analysis/") (sq_pos formula-decl nil sq "reals/") (sq const-decl "nonneg_real" sq "reals/")) shostak)) (continuous_atan 0 (continuous_atan-2 nil 3352182779 ("" (lemma "deriv_atan_fun") (("" (flatten) (("" (lemma "derivable_cont_fun[real]" ("f" "atan")) (("" (assert) nil nil)) nil)) nil)) nil) ((real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (derivable_cont_fun formula-decl nil derivatives "analysis/") (bool nonempty-type-eq-decl nil booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (atan const-decl "real_abs_lt_pi2" atan nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (deriv_atan_fun formula-decl nil atan nil)) nil) (continuous_atan-1 nil 3262324800 ("" (lemma "deriv_atan_fun") (("" (flatten) (("" (lemma "derivable_continuous2[real]" ("f" "atan")) (("" (assert) nil nil)) nil)) nil)) nil) nil shostak)) (atan_1 0 (atan_1-1 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" (lemma "atan_minus" ("x" "120/119" "y" "1/239")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "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_minus_rat_is_rat application-judgement "rat" rationals nil) (posrat_plus_nnrat_is_posrat application-judgement "posrat" rationals nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (real_plus_real_is_real application-judgement "real" reals nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (atan_minus formula-decl nil atan nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (cross_mult formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (atan_plus formula-decl nil atan nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)) shostak)) (atan_bnds 0 (atan_bnds-3 nil 3445345367 ("" (skolem 1 ("x")) (("" (lemma "deriv_atan_fun") (("" (flatten) (("" (lemma "atan_0") (("" (lemma "mean_value[nnreal]" ("a" "0")) (("1" (inst - "x" "_") (("1" (lemma "restrict2_derivable[nnreal,real]" ("f" "atan")) (("1" (lemma "restrict2_deriv[nnreal,real]" ("f" "atan")) (("1" (expand "restrict2") (("1" (replace -6 -1) (("1" (simplify -1) (("1" (lemma "extensionality" ("f" "LAMBDA (a: nnreal): 1 / (1 + a * a)" "g" "deriv[nnreal](LAMBDA (u: nnreal): atan(u))")) (("1" (simplify -1) (("1" (replace -2 -1) (("1" (hide -2 -6 -7) (("1" (lemma "identity_derivable_fun[nnreal]") (("1" (lemma "deriv_id_fun[nnreal]") (("1" (lemma "deriv_const_fun[nnreal]" ("b" "1")) (("1" (expand "I") (("1" (split 1) (("1" (lemma "prod_derivable_fun[nnreal]" ("f1" "LAMBDA (x: nnreal): x" "f2" "LAMBDA (x: nnreal): x")) (("1" (assert) (("1" (lemma "deriv_prod_fun[nnreal]" ("ff1" "LAMBDA (x: nnreal): x" "ff2" "LAMBDA (x: nnreal): x")) (("1" (replace -4 -1) (("1" (expand "*") (("1" (expand "+" -1) (("1" (lemma "sum_derivable_fun[nnreal]" ("f1" "LAMBDA (x: nnreal): 1" "f2" "LAMBDA (x: nnreal): x*x")) (("1" (lemma "const_derivable_fun[nnreal]" ("b" "1")) (("1" (assert) (("1" (lemma "deriv_sum_fun[nnreal]" ("ff1" "LAMBDA (x: nnreal): 1" "ff2" "LAMBDA (x: nnreal): x*x")) (("1" (replace -4 -1) (("1" (replace -6 -1) (("1" (expand "+") (("1" (lemma "div_derivable_fun[nnreal]" ("f" "LAMBDA (x: nnreal): x" "g" "LAMBDA (x: nnreal): 1 + x*x")) (("1" (assert) (("1" (expand "/" -1) (("1" (lemma "deriv_div_fun[nnreal]" ("ff" "LAMBDA (x: nnreal): x" "gg" "LAMBDA (x: nnreal): 1 + x*x")) (("1" (replace -3 -1) (("1" (replace -9 -1) (("1" (expand "/") (("1" (expand "-" -1) (("1" (expand "*" -1) (("1" (lemma "diff_derivable_fun[nnreal]" ("f1" "LAMBDA (u: nnreal): atan(u)" "f2" "LAMBDA (x: nnreal): x/(1+x*x)")) (("1" (assert) (("1" (lemma "deriv_diff_fun[nnreal]" ("ff1" "LAMBDA (u: nnreal): atan(u)" "ff2" "LAMBDA (x: nnreal): x/(1+x*x)")) (("1" (expand "-") (("1" (replace -3 -1) (("1" (replace -13 -1 rl) (("1" (simplify -1) (("1" (inst -15 "LAMBDA (x_1: nnreal): atan(x_1) - x_1 / (1 + x_1 * x_1)") (("1" (assert) (("1" (skolem - "c") (("1" (expand "deriv" -1) (("1" (lemma "congruence" ("f" "(LAMBDA (x: nnreal): deriv(LAMBDA (x_1: nnreal): atan(x_1) - x_1 / (1 + x_1 * x_1), x))" "g" "(LAMBDA (x_1: nnreal): 1 / (1 + x_1 * x_1) - (1 - x_1 * x_1) / (1 + 2 * (x_1 * x_1) + x_1 * x_1 * x_1 * x_1))" "x1" "c" "x2" "c")) (("1" (assert) (("1" (replace -1 -16) (("1" (replace -17 -16) (("1" (hide-all-but (-16 1)) (("1" (flatten) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "c" "py" "c")) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "1+c*c" "py" "1+c*c")) (("1" (lemma "minus_div1" ("x" "1" "n0x" "1+c*c" "y" "1-c*c" "n0y" "(1 + c * c) * (1 + c * c)")) (("1" (replace -1 -6) (("1" (lemma "div_cancel1" ("x" "2*(c*c)/((1 + c * c) * (1 + c * c))" "n0z" "1+c*c")) (("1" (name "CC" "c*c") (("1" (replace -1) (("1" (name "CCP1" "1+CC") (("1" (replace -1) (("1" (rewrite "div_div2" -3) (("1" (case "1 * (CCP1 * CCP1) - (1 - CC) * CCP1 = CCP1 * 2*CC") (("1" (replace -1 -10) (("1" (replace -4 -10) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "2*CC" "py" "CCP1*CCP1")) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "2*CC/(CCP1*CCP1)")) (("1" (inst - "x") (("1" (replace -12 -1) (("1" (assert) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "CCP1" 1) (("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) (("2" (propax) 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" (lemma "diff_derivable_fun[nnreal]" ("f1" "LAMBDA (x: nnreal): x" "f2" "LAMBDA (u: nnreal): atan(u)")) (("2" (lemma "deriv_diff_fun[nnreal]" ("ff1" "LAMBDA (x: nnreal): x" "ff2" "LAMBDA (u: nnreal): atan(u)")) (("1" (expand "-" (-1 -2)) (("1" (replace -4 -1) (("1" (replace -6 -1 rl) (("1" (simplify -1) (("1" (assert) (("1" (inst - "LAMBDA (x_1: nnreal): x_1 - atan(x_1)") (("1" (assert) (("1" (skolem -8 ("c")) (("1" (expand "deriv" -1) (("1" (replace -9 -8) (("1" (lemma "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 -9) (("1" (hide -1 -2 -3 -4 -5 -6 -7 -8 -10) (("1" (flatten) (("1" (lemma "minus_div1" ("x" "1" "n0x" "1" "y" "1" "n0y" "1+c*c")) (("1" (case "1+c*c > 0") (("1" (replace -2 -5) (("1" (simplify -5) (("1" (lemma "posreal_div_posreal_is_posreal" ("px" "c*c" "py" "1+c*c")) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "c*c/(1+c*c)")) (("1" (inst -1 "x") (("1" (assert) (("1" (replace -7 -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (lemma "posreal_times_posreal_is_posreal" ("px" "c" "py" "c")) (("1" (propax) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "sq_pos" ("a" "c")) (("2" (hide-all-but (-1 1)) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "derivable?" -2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("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) ((deriv_atan_fun formula-decl nil atan nil) (atan_0 formula-decl nil atan nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (restrict2_deriv formula-decl nil restrict2_deriv "analysis/") (extensionality formula-decl nil functions nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (deriv const-decl "[T -> real]" derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (deriv_const_fun formula-decl nil derivatives "analysis/") (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (const_derivable_fun formula-decl nil derivatives "analysis/") (deriv_sum_fun formula-decl nil derivatives "analysis/") (div_derivable_fun formula-decl nil derivatives "analysis/") (nzreal nonempty-type-eq-decl nil reals nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (congruence formula-decl nil functions nil) (derivable? const-decl "bool" derivatives_def "analysis/") (deriv const-decl "real" derivatives_def "analysis/") (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_div1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel1 formula-decl nil real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (CCP1 skolem-const-decl "posreal" atan nil) (div_div2 formula-decl nil real_props nil) (deriv_diff_fun formula-decl nil derivatives "analysis/") (diff_derivable_fun formula-decl nil derivatives "analysis/") (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (nz_deriv_fun type-eq-decl nil derivatives "analysis/") (deriv_div_fun formula-decl nil derivatives "analysis/") (sum_derivable_fun formula-decl nil derivatives "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (deriv_prod_fun formula-decl nil derivatives "analysis/") (prod_derivable_fun formula-decl nil derivatives "analysis/") (sq_pos formula-decl nil sq "reals/") (sq const-decl "nonneg_real" sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (I const-decl "(bijective?[T, T])" identity nil) (deriv_id_fun formula-decl nil derivatives "analysis/") (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (restrict2 const-decl "[T1 -> real]" restrict2_deriv "analysis/") (= const-decl "[T, T -> boolean]" equalities nil) (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (restrict2_derivable formula-decl nil restrict2_deriv "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (AND const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (pi const-decl "posreal" atan nil) (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil) (atan const-decl "real_abs_lt_pi2" atan nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (mean_value formula-decl nil derivative_props "analysis/") (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil)) nil) (atan_bnds-2 nil 3352182936 ("" (skolem 1 ("x")) (("" (lemma "deriv_atan_fun") (("" (flatten) (("" (lemma "atan_0") (("" (lemma "mean_value[nnreal]" ("a" "0")) (("1" (inst - "x" "_") (("1" (lemma "restrict2_derivable[nnreal,real]" ("f" "atan")) (("1" (lemma "restrict2_deriv[nnreal,real]" ("f" "atan")) (("1" (expand "restrict2") (("1" (replace -6 -1) (("1" (simplify -1) (("1" (lemma "extensionality" ("f" "LAMBDA (a: nnreal): 1 / (1 + a * a)" "g" "deriv[nnreal](LAMBDA (u: nnreal): atan(u))")) (("1" (simplify -1) (("1" (replace -2 -1) (("1" (hide -2 -6 -7) (("1" (lemma "identity_derivable_fun[nnreal]") (("1" (lemma "deriv_id_fun[nnreal]") (("1" (lemma "deriv_const_fun[nnreal]" ("b" "1")) (("1" (expand "I") (("1" (expand "const_fun") (("1" (split 1) (("1" (lemma "prod_derivable_fun[nnreal]" ("f1" "LAMBDA (x: nnreal): x" "f2" "LAMBDA (x: nnreal): x")) (("1" (assert) (("1" (lemma "deriv_prod_fun[nnreal]" ("ff1" "LAMBDA (x: nnreal): x" "ff2" "LAMBDA (x: nnreal): x")) (("1" (replace -4 -1) (("1" (expand "*") (("1" (expand "+" -1) (("1" (lemma "sum_derivable_fun[nnreal]" ("f1" "LAMBDA (x: nnreal): 1" "f2" "LAMBDA (x: nnreal): x*x")) (("1" (lemma "const_derivable_fun[nnreal]" ("b" "1")) (("1" (expand "const_fun") (("1" (assert) (("1" (lemma "deriv_sum_fun[nnreal]" ("ff1" "LAMBDA (x: nnreal): 1" "ff2" "LAMBDA (x: nnreal): x*x")) (("1" (replace -4 -1) (("1" (replace -6 -1) (("1" (expand "+") (("1" (lemma "div_derivable_fun[nnreal]" ("f" "LAMBDA (x: nnreal): x" "g" "LAMBDA (x: nnreal): 1 + x*x")) (("1" (assert) (("1" (expand "/" -1) (("1" (lemma "deriv_div_fun[nnreal]" ("ff" "LAMBDA (x: nnreal): x" "gg" "LAMBDA (x: nnreal): 1 + x*x")) (("1" (replace -3 -1) (("1" (replace -9 -1) (("1" (expand "/") (("1" (expand "-" -1) (("1" (expand "*" -1) (("1" (lemma "diff_derivable_fun[nnreal]" ("f1" "LAMBDA (u: nnreal): atan(u)" "f2" "LAMBDA (x: nnreal): x/(1+x*x)")) (("1" (assert) (("1" (lemma "deriv_diff_fun[nnreal]" ("ff1" "LAMBDA (u: nnreal): atan(u)" "ff2" "LAMBDA (x: nnreal): x/(1+x*x)")) (("1" (expand "-") (("1" (replace -3 -1) (("1" (replace -13 -1 rl) (("1" (simplify -1) (("1" (inst -15 "LAMBDA (x_1: nnreal): atan(x_1) - x_1 / (1 + x_1 * x_1)") (("1" (assert) (("1" (skolem - "c") (("1" (expand "deriv" -1) (("1" (lemma "congruence" ("f" "(LAMBDA (x: nnreal): deriv(LAMBDA (x_1: nnreal): atan(x_1) - x_1 / (1 + x_1 * x_1), x))" "g" "(LAMBDA (x_1: nnreal): 1 / (1 + x_1 * x_1) - (1 - x_1 * x_1) / (1 + 2 * (x_1 * x_1) + x_1 * x_1 * x_1 * x_1))" "x1" "c" "x2" "c")) (("1" (assert) (("1" (replace -1 -16) (("1" (replace -17 -16) (("1" (hide-all-but (-16 1)) (("1" (flatten) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "c" "py" "c")) (("1" (lemma "posreal_times_posreal_is_posreal" ("px" "1+c*c" "py" "1+c*c")) (("1" (lemma "minus_div1" ("x" "1" "n0x" "1+c*c" "y" "1-c*c" "n0y" "(1 + c * c) * (1 + c * c)")) (("1" (replace -1 -6) (("1" (lemma "div_cancel1" ("x" "2*(c*c)/((1 + c * c) * (1 + c * c))" "n0z" "1+c*c")) (("1" (name "CC" "c*c") (("1" (replace -1) (("1" (name "CCP1" "1+CC") (("1" (replace -1) (("1" (rewrite "div_div2" -3) (("1" (case "1 * (CCP1 * CCP1) - (1 - CC) * CCP1 = CCP1 * 2*CC") --> -------------------- --> maximum size reached --> --------------------
¤ Dauer der Verarbeitung: 0.862 Sekunden (vorverarbeitet am 2026-05-01) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26