|
(atan (real_abs_lt_pi2_TCC1 0
(real_abs_lt_pi2_TCC1-1 nil 3323017154
("" (subtype-tcc) nil nil)
((minus_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
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))
nil))
(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)
nil shostak))
(atan_bij 0
(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/"))
shostak))
(atan_0 0
(atan_0-1 nil 3257226801
("" (expand "atan") (("" (rewrite "atan_value_0") nil nil))
nil)
nil shostak))
(atan_inv 0
(atan_inv-1 nil 3264783397
("" (skosimp*)
(("" (rewrite "pi_value")
(("" (expand "atan")
(("" (lemma "atan_inv_value" ("px" "px!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
nil shostak))
(atan_inv_neg 0
(atan_inv_neg-1 nil 3264783474
("" (skosimp*)
(("" (rewrite "pi_value")
(("" (expand "atan")
(("" (lemma "atan_inv_neg_value" ("nx" "nx!1"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
nil shostak))
(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)
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"))
(("" (assert) (("" (flatten) (("" (assert) nil nil)) nil))
nil))
nil)
((real_times_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)
(real_plus_real_is_real application-judgement "real" reals
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_TCC3 0
(atan_minus_TCC3-1 nil 3408966186 ("" (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)
(real_div_nzreal_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)
(real_minus_real_is_real application-judgement "real" reals
nil)
(real_plus_real_is_real application-judgement "real" reals
nil))
nil))
(atan_minus 0
(atan_minus-1 nil 3257227268
("" (skolem 1 ("x" "y"))
(("" (lemma "atan_value_minus" ("x" "x" "y" "y"))
(("" (flatten -1)
(("" (rewrite "pi_value")
(("" (expand "atan")
(("" (replace -1)
(("" (replace -2) (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil shostak))
(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 3514303177 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(atan_sub_swap_TCC2 0
(atan_sub_swap_TCC2-1 nil 3514303177 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(atan_sub_swap_TCC3 0
(atan_sub_swap_TCC3-1 nil 3514303177 ("" (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 3514303178
("" (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))
(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-1 nil 3259651388
("" (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"
("f1"
"LAMBDA (x: nnreal): x"
"f2"
"LAMBDA (x: nnreal): x"))
(("1"
(assert)
(("1"
(lemma
"deriv_prod_fun"
("ff1"
"LAMBDA (x: nnreal): x"
"ff2"
"LAMBDA (x: nnreal): x"))
(("1"
(replace
-4
-1)
(("1"
(expand "*")
(("1"
(expand
"+"
-1)
(("1"
(lemma
"sum_derivable_fun"
("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"
("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"
("f"
"LAMBDA (x: nnreal): x"
"g"
"LAMBDA (x: nnreal): 1 + x*x"))
(("1"
(assert)
(("1"
(expand
"/"
-1)
(("1"
(lemma
"deriv_div_fun"
("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"
("f1"
"LAMBDA (u: nnreal): atan(u)"
"f2"
"LAMBDA (x: nnreal): x/(1+x*x)"))
(("1"
(assert)
(("1"
(lemma
"deriv_diff_fun"
("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
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.67 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
