(trig_aux
(sin_cos_eq_0 0
(sin_cos_eq_0-1 nil 3385302546
("" (skosimp)
(("" (rewrite "sin_eq_0")
(("" (skosimp)
(("" (replace -1)
(("" (rewrite "cos_k_pi") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((sin_eq_0 formula-decl nil trig_basic "trig/")
(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_times_real_is_real application-judgement "real" reals 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)
(int nonempty-type-eq-decl nil 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)
(cos_k_pi formula-decl nil trig_basic "trig/"))
shostak))
(eq_iff_periodic 0
(eq_iff_periodic-1 nil 3385302828
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (lemma "cos_minus" ("a" "a!1" "b" "b!1"))
(("1" (replace -2)
(("1" (replace -3)
(("1" (rewrite "sq_rew")
(("1" (rewrite "sq_rew")
(("1" (lemma "sin2_cos2" ("a" "b!1"))
(("1" (assert)
(("1" (replace -1)
(("1" (rewrite "cos_eq_1" -2)
(("1" (skosimp)
(("1" (inst + "i!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (replace -1)
(("2" (rewrite "sin_period" 1 :dir rl)
(("2" (rewrite "cos_period" 1 :dir rl) 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)
(cos_minus formula-decl nil trig_basic "trig/")
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(sin const-decl "real" trig_basic "trig/")
(real_minus_real_is_real application-judgement "real" reals nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(cos_eq_1 formula-decl nil trig_basic "trig/")
(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)
(real_plus_real_is_real application-judgement "real" reals nil)
(sin2_cos2 formula-decl nil trig_basic "trig/")
(sq_rew formula-decl nil sq "reals/")
(cos const-decl "real" trig_basic "trig/")
(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)
(real_times_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" trig_basic "trig/")
(cos_range application-judgement "trig_range" trig_basic "trig/")
(cos_period formula-decl nil trig_basic "trig/")
(integer nonempty-type-from-decl nil integers nil)
(sin_period formula-decl nil trig_basic "trig/"))
shostak)))
¤ Dauer der Verarbeitung: 0.12 Sekunden
(vorverarbeitet)
¤
*© Formatika GbR, Deutschland
