|
(trig_rew
(tr_rew1 0
(tr_rew1-1 nil 3507030636 ("" (rewrite "cos_0") nil nil)
((cos_0 formula-decl nil trig_basic nil)) nil))
(tr_rew2 0
(tr_rew2-1 nil 3507030636 ("" (rewrite "sin_0") nil nil)
((sin_0 formula-decl nil trig_basic nil)) nil))
(tr_rew3 0
(tr_rew3-1 nil 3507030636 ("" (rewrite "sin_pi2") nil nil)
((sin_pi2 formula-decl nil trig_basic nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil))
nil))
(tr_rew4 0
(tr_rew4-1 nil 3507030636 ("" (rewrite "cos_pi2") nil nil)
((cos_pi2 formula-decl nil trig_basic nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil))
nil))
(tr_rew5_TCC1 0
(tr_rew5_TCC1-1 nil 3507030636
("" (expand "Tan?")
(("" (rewrite "cos_0") (("" (assert) nil nil)) nil)) nil)
((cos_0 formula-decl nil trig_basic nil)
(Tan? const-decl "bool" sincos_def nil))
nil))
(tr_rew5 0
(tr_rew5-1 nil 3507030636 ("" (rewrite "tan_0") nil nil)
((tan_0 formula-decl nil trig_basic nil)) nil))
(tr_rew6 0
(tr_rew6-1 nil 3507030636 ("" (rewrite "sin_pi") nil nil)
((sin_pi formula-decl nil trig_basic nil)) nil))
(tr_rew7 0
(tr_rew7-1 nil 3507030636 ("" (rewrite "cos_pi") nil nil)
((cos_pi formula-decl nil trig_basic nil)) nil))
(tr_rew8_TCC1 0
(tr_rew8_TCC1-1 nil 3507030636
("" (expand "Tan?")
(("" (rewrite "cos_pi") (("" (assert) nil nil)) nil)) nil)
((cos_pi formula-decl nil trig_basic nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(Tan? const-decl "bool" sincos_def nil))
nil))
(tr_rew8 0
(tr_rew8-1 nil 3507030636 ("" (rewrite "tan_pi") nil nil)
((tan_pi formula-decl nil trig_basic nil)) nil))
(tr_rew9 0
(tr_rew9-1 nil 3507030636 ("" (rewrite "sin_3pi2") 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)
(sin_3pi2 formula-decl nil trig_basic nil))
nil))
(tr_rew10 0
(tr_rew10-1 nil 3507030636 ("" (rewrite "cos_3pi2") 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)
(cos_3pi2 formula-decl nil trig_basic nil))
nil))
(tr_rew11 0
(tr_rew11-1 nil 3507030636 ("" (rewrite "sin_2pi") nil nil)
((sin_2pi formula-decl nil trig_basic nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil))
nil))
(tr_rew12 0
(tr_rew12-1 nil 3507030636 ("" (rewrite "cos_2pi") nil nil)
((cos_2pi formula-decl nil trig_basic nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil))
nil))
(tr_rew13_TCC1 0
(tr_rew13_TCC1-1 nil 3507030636
("" (expand "Tan?")
(("" (rewrite "cos_2pi") (("" (assert) nil nil)) nil)) nil)
((cos_2pi formula-decl nil trig_basic nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(Tan? const-decl "bool" sincos_def nil))
nil))
(tr_rew13 0
(tr_rew13-1 nil 3507030636 ("" (rewrite "tan_2pi") nil nil)
((tan_2pi formula-decl nil trig_basic nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil))
nil))
(tr_rew14 0
(tr_rew14-1 nil 3507030636
("" (skosimp*) (("" (rewrite "sin_shift") nil nil)) 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))
nil))
(tr_rew15 0
(tr_rew15-1 nil 3507030636
("" (skosimp*) (("" (rewrite "cos_shift") nil nil)) nil)
((cos_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))
nil))
(tr_rew16 0
(tr_rew16-1 nil 3507030636
("" (skosimp*) (("" (rewrite "sin_k_pi") nil nil)) nil)
((sin_k_pi 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)
(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))
nil))
(tr_rew17 0
(tr_rew17-1 nil 3507030636
("" (skosimp*) (("" (rewrite "cos_2k_pi") nil nil)) nil)
((cos_2k_pi 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)
(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))
nil))
(tr_rew20_TCC1 0
(tr_rew20_TCC1-1 nil 3507030636
("" (skosimp*)
(("" (expand "Tan?")
(("" (rewrite "cos_k_pi") (("" (rewrite "expt_nonzero") nil nil))
nil))
nil))
nil)
((Tan? const-decl "bool" sincos_def nil)
(expt_nonzero formula-decl nil exponentiation nil)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(rat_exp application-judgement "rat" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(integer nonempty-type-from-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)
(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_k_pi formula-decl nil trig_basic nil))
nil))
(tr_rew20 0
(tr_rew20-1 nil 3507030636
("" (skosimp*) (("" (rewrite "tan_k_pi") nil nil)) nil)
((tan_k_pi 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)
(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))
nil))
(tr_rew22 0
(tr_rew22-1 nil 3507030636
("" (skosimp*) (("" (rewrite "sin_neg") nil nil)) nil)
((sin_neg 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))
nil))
(tr_rew23 0
(tr_rew23-1 nil 3507030636
("" (skosimp*) (("" (rewrite "cos_neg") nil nil)) nil)
((cos_neg 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))
nil))
(tr_rew24_TCC1 0
(tr_rew24_TCC1-1 nil 3507030636
("" (skosimp*)
(("" (typepred "a!1")
(("" (expand "Tan?") (("" (rewrite "cos_neg") nil nil)) nil))
nil))
nil)
((Tan? const-decl "bool" 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)
(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)
(cos_range application-judgement "trig_range" sincos_def nil)
(cos_neg formula-decl nil trig_basic nil))
nil))
(tr_rew24 0
(tr_rew24-1 nil 3507030636
("" (skosimp*) (("" (rewrite "tan_neg") nil nil)) nil)
((tan_neg 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)
(Tan? const-decl "bool" sincos_def nil))
nil)))
¤ Dauer der Verarbeitung: 0.2 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.
|
