|
(trig_extra
(sin_minus_2pi 0
(sin_minus_2pi-1 nil 3269431996
("" (skosimp)
(("" (rewrite "sin_minus")
(("" (rewrite "sin_2pi")
(("" (rewrite "cos_2pi") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_minus formula-decl nil trig_basic 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 "[numfield, numfield -> numfield]" number_fields 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)
(pi const-decl "posreal" atan nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(cos_2pi formula-decl nil trig_basic nil)
(sin_2pi formula-decl nil trig_basic nil))
nil))
(cos_minus_2pi 0
(cos_minus_2pi-1 nil 3269431996
("" (skosimp)
(("" (rewrite "cos_minus")
(("" (rewrite "cos_2pi")
(("" (rewrite "sin_2pi") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_minus formula-decl nil trig_basic 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 "[numfield, numfield -> numfield]" number_fields 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)
(pi const-decl "posreal" atan nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_2pi formula-decl nil trig_basic nil)
(cos_2pi formula-decl nil trig_basic nil))
nil))
(tan_minus_2pi_TCC1 0
(tan_minus_2pi_TCC1-1 nil 3269431996
("" (skosimp)
(("" (expand "Tan?")
(("" (rewrite "cos_minus_2pi") (("" (assert) nil nil)) nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(Tan? const-decl "bool" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types 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)
(cos_minus_2pi formula-decl nil trig_extra nil))
nil))
(tan_minus_2pi_TCC2 0
(tan_minus_2pi_TCC2-1 nil 3269431996 ("" (subtype-tcc) 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)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(Integral const-decl "real" integral_def "analysis/")
(atan_value const-decl "real" atan nil)
(pi const-decl "posreal" atan nil)
(cos const-decl "real" sincos_def nil)
(Tan? const-decl "bool" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(tan_minus_2pi 0
(tan_minus_2pi-1 nil 3269431996
("" (skosimp)
(("" (expand "tan")
(("" (rewrite "sin_minus_2pi")
(("" (rewrite "cos_minus_2pi") nil nil)) nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(tan const-decl "real" sincos_def nil)
(cos_minus_2pi formula-decl nil trig_extra nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types 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)
(sin_minus_2pi formula-decl nil trig_extra nil))
nil))
(sin_minus_3pi2 0
(sin_minus_3pi2-1 nil 3269431996
("" (skosimp)
(("" (rewrite "sin_minus")
(("" (rewrite "sin_3pi2")
(("" (rewrite "cos_3pi2") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_minus formula-decl nil trig_basic 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields 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)
(pi const-decl "posreal" atan nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(cos_3pi2 formula-decl nil trig_basic nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sin_3pi2 formula-decl nil trig_basic nil))
nil))
(cos_minus_3pi2 0
(cos_minus_3pi2-1 nil 3269431996
("" (skosimp)
(("" (rewrite "cos_minus")
(("" (rewrite "cos_3pi2")
(("" (rewrite "sin_3pi2") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_minus formula-decl nil trig_basic 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields 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)
(pi const-decl "posreal" atan nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_3pi2 formula-decl nil trig_basic nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(cos_3pi2 formula-decl nil trig_basic nil))
nil))
(tan_minus_3pi2_TCC1 0
(tan_minus_3pi2_TCC1-1 nil 3269431996
("" (expand "Tan?")
(("" (skosimp*)
(("" (lemma "sin_shift" ("a" "a!1-3*pi/2"))
(("" (lemma "sin_period" ("a" "-a!1" "j" "1"))
(("" (rewrite "sin_neg" -1) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((minus_real_is_real application-judgement "real" reals nil)
(sin_period formula-decl nil trig_basic nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(integer nonempty-type-from-decl nil integers nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(sin_neg formula-decl nil trig_basic nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sin_shift formula-decl nil trig_basic 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 "[numfield, numfield -> numfield]" 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 -> numfield]" number_fields 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)
(pi const-decl "posreal" atan nil)
(Tan? const-decl "bool" sincos_def nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil))
nil))
(tan_minus_3pi2_TCC2 0
(tan_minus_3pi2_TCC2-1 nil 3269431996
("" (skosimp)
(("" (expand "tan")
(("" (lemma "div_eq_zero")
(("" (inst -1 "cos(a!1)" "sin(a!1)")
(("1" (replace -1 * lr) (("1" (propax) nil nil)) nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
((tan const-decl "real" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def 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)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(cos const-decl "real" sincos_def nil)
(sin const-decl "real" sincos_def nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(div_eq_zero formula-decl nil real_props nil))
nil))
(tan_minus_3pi2 0
(tan_minus_3pi2-1 nil 3269431996
("" (skosimp)
(("" (expand "tan")
(("" (rewrite "sin_minus_3pi2")
(("" (rewrite "cos_minus_3pi2") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(tan const-decl "real" sincos_def nil)
(cos_minus_3pi2 formula-decl nil trig_extra nil)
(minus_real_is_real application-judgement "real" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(sin_minus_3pi2 formula-decl nil trig_extra nil))
nil))
(sin_minus_pi 0
(sin_minus_pi-1 nil 3269431996
("" (skosimp)
(("" (rewrite "sin_minus")
(("" (rewrite "sin_pi")
(("" (rewrite "cos_pi") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((sin_minus formula-decl nil trig_basic 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)
(pi const-decl "posreal" atan nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(cos_pi formula-decl nil trig_basic nil)
(minus_real_is_real application-judgement "real" reals nil)
(sin_pi formula-decl nil trig_basic nil))
nil))
(cos_minus_pi 0
(cos_minus_pi-1 nil 3269431996
("" (skosimp)
(("" (rewrite "cos_minus")
(("" (rewrite "cos_pi")
(("" (rewrite "sin_pi") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((cos_minus formula-decl nil trig_basic 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)
(pi const-decl "posreal" atan nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_pi formula-decl nil trig_basic nil)
(minus_real_is_real application-judgement "real" reals nil)
(cos_pi formula-decl nil trig_basic nil))
nil))
(tan_minus_pi_TCC1 0
(tan_minus_pi_TCC1-1 nil 3269431996
("" (skosimp*)
(("" (expand "Tan?")
(("" (lemma "neg_cos" ("a" "a!1-pi")) (("" (assert) nil nil))
nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(Tan? const-decl "bool" sincos_def nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(neg_cos formula-decl nil trig_basic 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 "[numfield, numfield -> numfield]" number_fields 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)
(pi const-decl "posreal" atan nil))
nil))
(tan_minus_pi 0
(tan_minus_pi-1 nil 3269431996
("" (skosimp)
(("" (expand "tan")
(("" (rewrite "sin_minus_pi")
(("" (rewrite "cos_minus_pi") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(tan const-decl "real" sincos_def nil)
(cos_minus_pi formula-decl nil trig_extra nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(cos_range application-judgement "trig_range" sincos_def 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)
(sin_minus_pi formula-decl nil trig_extra nil))
nil))
(sin_minus_pi2 0
(sin_minus_pi2-1 nil 3269431996
("" (skosimp)
(("" (rewrite "sin_minus")
(("" (rewrite "cos_pi2")
(("" (rewrite "sin_pi2") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_minus formula-decl nil trig_basic 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)
(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)
(pi const-decl "posreal" atan nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sin_pi2 formula-decl nil trig_basic nil)
(minus_real_is_real application-judgement "real" reals nil)
(cos_pi2 formula-decl nil trig_basic nil))
nil))
(cos_minus_pi2 0
(cos_minus_pi2-1 nil 3269431996
("" (skosimp)
(("" (rewrite "cos_minus")
(("" (rewrite "cos_pi2")
(("" (rewrite "sin_pi2") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_minus formula-decl nil trig_basic 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)
(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)
(pi const-decl "posreal" atan nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_pi2 formula-decl nil trig_basic nil)
(cos_pi2 formula-decl nil trig_basic nil))
nil))
(tan_minus_pi2_TCC1 0
(tan_minus_pi2_TCC1-1 nil 3269431996
("" (skolem 1 ("a"))
(("" (flatten)
(("" (expand "Tan?")
(("" (lemma "cos_neg" ("a" "a-pi/2"))
(("" (lemma "cos_shift" ("a" "a"))
(("" (replace -1) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
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)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal 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)
(cos_neg formula-decl nil trig_basic nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_shift formula-decl nil trig_basic nil)
(Tan? const-decl "bool" sincos_def nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil))
nil))
(tan_minus_pi2 0
(tan_minus_pi2-1 nil 3269431996
("" (skosimp)
(("" (expand "tan")
(("" (rewrite "sin_minus_pi2")
(("" (rewrite "cos_minus_pi2") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(tan const-decl "real" sincos_def nil)
(cos_minus_pi2 formula-decl nil trig_extra nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(minus_odd_is_odd application-judgement "odd_int" integers 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)
(sin_minus_pi2 formula-decl nil trig_extra nil))
nil))
(sin_2pi_minus 0
(sin_2pi_minus-1 nil 3269431996
("" (skosimp)
(("" (rewrite "sin_minus")
(("" (rewrite "sin_2pi")
(("" (rewrite "cos_2pi") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_minus formula-decl nil trig_basic 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 "[numfield, numfield -> numfield]" number_fields 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)
(pi const-decl "posreal" atan nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(cos_2pi formula-decl nil trig_basic nil)
(minus_real_is_real application-judgement "real" reals nil)
(sin_2pi formula-decl nil trig_basic nil))
nil))
(cos_2pi_minus 0
(cos_2pi_minus-1 nil 3269431996
("" (skosimp)
(("" (rewrite "cos_minus")
(("" (rewrite "cos_2pi")
(("" (rewrite "sin_2pi") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_minus formula-decl nil trig_basic 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 "[numfield, numfield -> numfield]" number_fields 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)
(pi const-decl "posreal" atan nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_2pi formula-decl nil trig_basic nil)
(cos_2pi formula-decl nil trig_basic nil))
nil))
(tan_2pi_minus_TCC1 0
(tan_2pi_minus_TCC1-1 nil 3269431996
("" (skosimp)
(("" (expand "Tan?")
(("" (rewrite "cos_2pi_minus") (("" (assert) nil nil)) nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(Tan? const-decl "bool" sincos_def nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types 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)
(cos_2pi_minus formula-decl nil trig_extra nil))
nil))
(tan_2pi_minus 0
(tan_2pi_minus-1 nil 3269431996
("" (skosimp)
(("" (expand "tan")
(("" (rewrite "sin_2pi_minus")
(("" (rewrite "cos_2pi_minus") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(tan const-decl "real" sincos_def nil)
(cos_2pi_minus formula-decl nil trig_extra nil)
(minus_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types 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)
(sin_2pi_minus formula-decl nil trig_extra nil))
nil))
(sin_3pi2_minus 0
(sin_3pi2_minus-1 nil 3269431996
("" (skosimp)
(("" (rewrite "sin_minus")
(("" (rewrite "sin_3pi2")
(("" (rewrite "cos_3pi2") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_minus formula-decl nil trig_basic 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields 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)
(pi const-decl "posreal" atan nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(cos_3pi2 formula-decl nil trig_basic nil)
(minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sin_3pi2 formula-decl nil trig_basic nil))
nil))
(cos_3pi2_minus 0
(cos_3pi2_minus-1 nil 3269431996
("" (skosimp)
(("" (rewrite "cos_minus")
(("" (rewrite "cos_3pi2")
(("" (rewrite "sin_3pi2") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_minus formula-decl nil trig_basic 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)
(* const-decl "[numfield, numfield -> numfield]" number_fields 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)
(pi const-decl "posreal" atan nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_3pi2 formula-decl nil trig_basic nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_real_is_real application-judgement "real" reals nil)
(cos_3pi2 formula-decl nil trig_basic nil))
nil))
(tan_3pi2_minus_TCC1 0
(tan_3pi2_minus_TCC1-1 nil 3269431996
("" (skosimp*)
(("" (expand "Tan?")
(("" (lemma "cos_sin" ("a" "3*pi/2-a!1"))
(("" (lemma "sin_period" ("a" "-a!1" "j" "1"))
(("" (replace -1 -2 rl)
(("" (rewrite "sin_neg" -2) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(Tan? const-decl "bool" sincos_def nil)
(minus_real_is_real application-judgement "real" reals nil)
(sin_period formula-decl nil trig_basic nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(integer nonempty-type-from-decl nil integers nil)
(sin_neg formula-decl nil trig_basic nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(cos_sin formula-decl nil trig_basic 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 "[numfield, numfield -> numfield]" 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 -> numfield]" number_fields 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)
(pi const-decl "posreal" atan nil))
nil))
(tan_3pi2_minus 0
(tan_3pi2_minus-1 nil 3269431996
("" (skosimp)
(("" (expand "tan")
(("" (rewrite "sin_3pi2_minus")
(("" (rewrite "cos_3pi2_minus") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(tan const-decl "real" sincos_def nil)
(cos_3pi2_minus formula-decl nil trig_extra nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types 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)
(sin_3pi2_minus formula-decl nil trig_extra nil))
nil))
(sin_pi_minus 0
(sin_pi_minus-1 nil 3269431996
("" (skosimp)
(("" (rewrite "sin_minus")
(("" (rewrite "sin_pi")
(("" (rewrite "cos_pi") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((sin_minus formula-decl nil trig_basic 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)
(pi const-decl "posreal" atan nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(cos_pi formula-decl nil trig_basic nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sin_pi formula-decl nil trig_basic nil))
nil))
(cos_pi_minus 0
(cos_pi_minus-1 nil 3269431996
("" (skosimp)
(("" (rewrite "cos_minus")
(("" (rewrite "cos_pi")
(("" (rewrite "sin_pi") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((cos_minus formula-decl nil trig_basic 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)
(pi const-decl "posreal" atan nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_pi formula-decl nil trig_basic nil)
(minus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(cos_pi formula-decl nil trig_basic nil))
nil))
(tan_pi_minus_TCC1 0
(tan_pi_minus_TCC1-1 nil 3269431996
("" (skosimp*)
(("" (expand "Tan?")
(("" (lemma "neg_cos" ("a" "-a!1"))
(("" (rewrite "cos_neg" -1) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((Tan? const-decl "bool" sincos_def nil)
(cos_neg formula-decl nil trig_basic nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(neg_cos formula-decl nil trig_basic 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 "[numfield -> numfield]" number_fields nil))
nil))
(tan_pi_minus 0
(tan_pi_minus-1 nil 3269431996
("" (skosimp)
(("" (expand "tan")
(("" (rewrite "sin_pi_minus")
(("" (rewrite "cos_pi_minus") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((tan const-decl "real" sincos_def nil)
(cos_pi_minus formula-decl nil trig_extra nil)
(minus_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx 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)
(sin_pi_minus formula-decl nil trig_extra nil))
nil))
(sin_pi2_minus 0
(sin_pi2_minus-1 nil 3269431996
("" (skosimp)
(("" (rewrite "sin_minus")
(("" (rewrite "sin_pi2")
(("" (rewrite "cos_pi2") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin_minus formula-decl nil trig_basic 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)
(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)
(pi const-decl "posreal" atan nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(cos_pi2 formula-decl nil trig_basic nil)
(sin_pi2 formula-decl nil trig_basic nil))
nil))
(cos_pi2_minus 0
(cos_pi2_minus-1 nil 3269431996
("" (skosimp)
(("" (rewrite "cos_minus")
(("" (rewrite "cos_pi2")
(("" (rewrite "sin_pi2") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_minus formula-decl nil trig_basic 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)
(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)
(pi const-decl "posreal" atan nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_pi2 formula-decl nil trig_basic nil)
(cos_pi2 formula-decl nil trig_basic nil))
nil))
(tan_pi2_minus_TCC1 0
(tan_pi2_minus_TCC1-1 nil 3269431996
("" (skosimp*)
(("" (expand "Tan?")
(("" (lemma "sin_cos" ("a" "-a!1"))
(("" (rewrite "sin_neg" -1) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(Tan? const-decl "bool" sincos_def nil)
(sin_neg formula-decl nil trig_basic nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_real_is_real application-judgement "real" reals nil)
(sin_cos formula-decl nil trig_basic 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 "[numfield -> numfield]" number_fields nil))
nil))
(tan_pi2_minus 0
(tan_pi2_minus-1 nil 3269431996
("" (skosimp)
(("" (expand "tan")
(("" (rewrite "sin_pi2_minus")
(("" (rewrite "cos_pi2_minus") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(tan const-decl "real" sincos_def nil)
(cos_pi2_minus formula-decl nil trig_extra nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types 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)
(sin_pi2_minus formula-decl nil trig_extra nil))
nil))
(sin_times_cos 0
(sin_times_cos-1 nil 3269431996
("" (skosimp)
(("" (rewrite "sin_plus")
(("" (rewrite "sin_minus") (("" (assert) nil nil)) nil)) nil))
nil)
((sin_plus formula-decl nil trig_basic 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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(sin_range application-judgement "trig_range" sincos_def 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)
(sin_minus formula-decl nil trig_basic nil))
nil))
(cos_times_cos 0
(cos_times_cos-1 nil 3269431996
("" (skosimp)
(("" (rewrite "cos_plus")
(("" (rewrite "cos_minus") (("" (assert) nil nil)) nil)) nil))
nil)
((cos_plus formula-decl nil trig_basic 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)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(cos_minus formula-decl nil trig_basic nil))
nil))
(sin_times_sin 0
(sin_times_sin-1 nil 3269431996
("" (skosimp)
(("" (rewrite "cos_plus")
(("" (rewrite "cos_minus") (("" (assert) nil nil)) nil)) nil))
nil)
((cos_plus formula-decl nil trig_basic 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)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(cos_minus formula-decl nil trig_basic nil))
nil))
(sin_sum 0
(sin_sum-1 nil 3269431996
("" (skosimp*)
(("" (lemma "sin_plus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2"))
(("" (lemma "sin_minus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2"))
(("" (assert) nil nil)) nil))
nil))
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)
(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)
(sin_plus formula-decl nil trig_basic nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(sin_minus formula-decl nil trig_basic nil))
nil))
(sin_diff 0
(sin_diff-1 nil 3269431996
("" (skosimp*)
(("" (lemma "sin_plus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2"))
(("" (lemma "sin_minus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2"))
(("" (assert) nil nil)) nil))
nil))
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)
(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)
(sin_plus formula-decl nil trig_basic nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(sin_minus formula-decl nil trig_basic nil))
nil))
(cos_sum 0
(cos_sum-1 nil 3269431996
("" (skosimp*)
(("" (lemma "cos_plus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2"))
(("" (lemma "cos_minus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2"))
(("" (assert)
(("" (replace -1)
(("" (replace -2)
(("" (assert)
(("" (name-replace "K1" "cos((a!1 + b!1) / 2)")
(("" (name-replace "K2" "cos((a!1 - b!1) / 2)")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(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)
(cos_plus formula-decl nil trig_basic nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(trig_range type-eq-decl nil sincos_def nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(cos const-decl "real" sincos_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(cos_minus formula-decl nil trig_basic nil))
nil))
(cos_diff 0
(cos_diff-1 nil 3269431996
("" (skosimp*)
(("" (lemma "cos_plus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2"))
(("" (lemma "cos_minus" ("a" "(a!1+b!1)/2" "b" "(a!1-b!1)/2"))
(("" (replace -1)
(("" (replace -2)
(("" (assert)
(("" (name-replace "K1" "sin((a!1 + b!1) / 2)")
(("" (name-replace "K2" "sin((a!1 - b!1) / 2)")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(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)
(cos_plus formula-decl nil trig_basic nil)
(real_div_nzreal_is_real application-judgement "real" reals 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)
(cos_range application-judgement "trig_range" sincos_def nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(real_times_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)
(= const-decl "[T, T -> boolean]" equalities nil)
(sin const-decl "real" sincos_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(trig_range type-eq-decl nil sincos_def nil)
(cos_minus formula-decl nil trig_basic nil))
nil))
(tan_diff_TCC1 0
(tan_diff_TCC1-1 nil 3269431996
("" (skosimp*)
(("" (expand "Tan?")
(("" (rewrite "zero_times3") (("" (ground) nil nil)) nil)) nil))
nil)
((Tan? const-decl "bool" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(cos const-decl "real" sincos_def 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)
(zero_times3 formula-decl nil real_props nil))
nil))
(tan_diff 0
(tan_diff-1 nil 3269431996
("" (skosimp*)
(("" (expand "tan")
((""
(case "(sin(a!1) / cos(a!1) - sin(b!1) / cos(b!1) = sin(a!1 - b!1)
/
(cos(a!1)
*
cos(b!1))) = (sin(a!1 - b!1)
/
(cos(a!1)
*
cos
(b!1)) = sin(a!1)
/
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.55 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
