Quelle trig_extra.prf
Sprache: Lisp
(trig_extranil 3269431996"" (skosimp)"" (rewrite "sin_minus" )"" (rewrite "sin_2pi" )"" (rewrite "cos_2pi" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"nzint" integers nil )"even_int" integers nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "cos_minus" )"" (rewrite "cos_2pi" )"" (rewrite "sin_2pi" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"nzint" integers nil )"even_int" integers nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (expand "Tan?" )"" (rewrite "cos_minus_2pi" ) (("" (assert ) nil nil )) nil ))nil ))nil )"bool" trig_basic nil )"trig_range" trig_basic nil )"even_int" integers nil )"nzint" integers nil )"posreal" nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_extra nil ))nil ))nil 3269431996 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )"bool" trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (rewrite "sin_minus_2pi" )"" (rewrite "cos_minus_2pi" ) nil nil )) nil ))nil ))nil )"real" trig_basic nil )nil trig_extra nil )"trig_range" trig_basic nil )"even_int" integers nil )"nzint" integers nil )"trig_range" trig_basic nil )"posreal" nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_extra nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "sin_minus" )"" (rewrite "sin_3pi2" )"" (rewrite "cos_3pi2" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" nil )"posreal" nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )"odd_int" integers nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "cos_minus" )"" (rewrite "cos_3pi2" )"" (rewrite "sin_3pi2" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" nil )"posreal" nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )"odd_int" integers nil )"real" reals nil )nil trig_basic nil ))nil ))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 )"real" reals nil )nil trig_basic nil )"[numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"posreal" nil )"trig_range" trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )nil trig_basic nil )"real" reals nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"bool" trig_basic nil )"posreal" nil )"posreal" nil ))nil ))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 )"real" trig_basic nil )"trig_range" trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil )nil reals nil )"real" trig_basic nil )"real" trig_basic nil )"trig_range" trig_basic nil )nil real_props nil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (rewrite "sin_minus_3pi2" )"" (rewrite "cos_minus_3pi2" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"posreal" nil )"posreal" nil )"real" trig_basic nil )nil trig_extra nil )"real" reals nil )"nzreal" nil )"trig_range" trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"odd_int" integers nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_extra nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "sin_minus" )"" (rewrite "sin_pi" )"" (rewrite "cos_pi" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"odd_int" integers nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )"real" reals nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "cos_minus" )"" (rewrite "cos_pi" )"" (rewrite "sin_pi" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"odd_int" integers nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )"real" reals nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp*)"" (expand "Tan?" )"" (lemma "neg_cos" ("a" "a!1-pi" )) (("" (assert ) nil nil ))nil ))nil ))nil )"bool" trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (rewrite "sin_minus_pi" )"" (rewrite "cos_minus_pi" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"real" trig_basic nil )nil trig_extra nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil )"odd_int" integers nil )"trig_range" trig_basic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_extra nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "sin_minus" )"" (rewrite "cos_pi2" )"" (rewrite "sin_pi2" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )"real" reals nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "cos_minus" )"" (rewrite "cos_pi2" )"" (rewrite "sin_pi2" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )nil trig_basic nil ))nil ))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 )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )nil trig_basic nil )"bool" trig_basic nil )"posreal" nil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (rewrite "sin_minus_pi2" )"" (rewrite "cos_minus_pi2" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"posreal" nil )"real" trig_basic nil )nil trig_extra nil )"nzreal" nil )"real" reals nil )"trig_range" trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"odd_int" integers nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_extra nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "sin_minus" )"" (rewrite "sin_2pi" )"" (rewrite "cos_2pi" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )"real" reals nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "cos_minus" )"" (rewrite "cos_2pi" )"" (rewrite "sin_2pi" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (expand "Tan?" )"" (rewrite "cos_2pi_minus" ) (("" (assert ) nil nil )) nil ))nil ))nil )"bool" trig_basic nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"posreal" nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_extra nil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (rewrite "sin_2pi_minus" )"" (rewrite "cos_2pi_minus" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"real" trig_basic nil )nil trig_extra nil )"real" reals nil )"trig_range" trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"posreal" nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_extra nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "sin_minus" )"" (rewrite "sin_3pi2" )"" (rewrite "cos_3pi2" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"trig_range" trig_basic nil )"posreal" nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )"real" reals nil )"odd_int" integers nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "cos_minus" )"" (rewrite "cos_3pi2" )"" (rewrite "sin_3pi2" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"trig_range" trig_basic nil )"posreal" nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )"odd_int" integers nil )"real" reals nil )nil trig_basic nil ))nil ))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 )"posreal" nil )"bool" trig_basic nil )"real" reals nil )nil trig_basic nil )"[numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"posreal" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"posint" nil )"real" reals nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (rewrite "sin_3pi2_minus" )"" (rewrite "cos_3pi2_minus" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"posreal" nil )"real" trig_basic nil )nil trig_extra nil )"nzreal" nil )"real" reals nil )"trig_range" trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"posreal" nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_extra nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "sin_minus" )"" (rewrite "sin_pi" )"" (rewrite "cos_pi" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )"odd_int" integers nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "cos_minus" )"" (rewrite "cos_pi" )"" (rewrite "sin_pi" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )"real" reals nil )"odd_int" integers nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp*)"" (expand "Tan?" )"" (lemma "neg_cos" ("a" "-a!1" ))"" (rewrite "cos_neg" -1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"bool" trig_basic nil )nil trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )"real" reals nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (rewrite "sin_pi_minus" )"" (rewrite "cos_pi_minus" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"real" trig_basic nil )nil trig_extra nil )"real" reals nil )"trig_range" trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_extra nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "sin_minus" )"" (rewrite "sin_pi2" )"" (rewrite "cos_pi2" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "cos_minus" )"" (rewrite "cos_pi2" )"" (rewrite "sin_pi2" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"posreal" nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp*)"" (expand "Tan?" )"" (lemma "sin_cos" ("a" "-a!1" ))"" (rewrite "sin_neg" -1) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"bool" trig_basic nil )nil trig_basic nil )"posreal" nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )"real" reals nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (rewrite "sin_pi2_minus" )"" (rewrite "cos_pi2_minus" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"real" trig_basic nil )nil trig_extra nil )"nzreal" nil )"trig_range" trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"posreal" nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_extra nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "sin_plus" )"" (rewrite "sin_minus" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"odd_int" integers nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "cos_plus" )"" (rewrite "cos_minus" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"odd_int" integers nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )"real" reals nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (rewrite "cos_plus" )"" (rewrite "cos_minus" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"odd_int" integers nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )"real" reals nil )"real" reals nil )nil trig_basic nil ))nil ))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 )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil )nil trig_basic nil ))nil ))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 )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil )nil trig_basic nil ))nil ))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 )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil )nil trig_basic nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"real" trig_basic nil )"[T, T -> boolean]" equalities nil )"odd_int" integers nil )nil trig_basic nil ))nil ))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 )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic nil )"real" reals nil )"real" reals nil )"real" reals nil )"odd_int" integers nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"nzint" integers nil )"even_int" integers nil )"[T, T -> boolean]" equalities nil )"real" trig_basic nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil trig_basic nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp*)"" (expand "Tan?" )"" (rewrite "zero_times3" ) (("" (ground) nil nil )) nil )) nil ))nil )"bool" trig_basic nil )"trig_range" trig_basic nil )"real" trig_basic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil real_props nil ))nil ))nil 3269431996"" (skosimp*)"" (expand "tan" )"" case "(sin(a!1) / cos(a!1) - sin(b!1) / cos(b!1) = sin(a!1 - b!1) ") "1" (replace -1 1 :hide? t)"1" (rewrite "div_cancel3" 1)"1" (rewrite "times_div1" 1)"1" "(cos(a!1) * cos(b!1) * sin(a!1)) / cos(a!1) = cos(b!1) * sin(a!1)" )"1" "cos(a!1) * cos(b!1) * (sin(b!1) / cos(b!1)) = cos(a!1) * sin(b!1)" )"1" (hide -1 -2)"1" (rewrite "sin_minus" )"1" (assert ) nil nil )) nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" (expand "Tan?" ) (("2" (propax) nil nil )) nil ))nil )"2" (expand "Tan?" ) (("2" (propax) nil nil )) nil )"3" (expand "Tan?" ) (("3" (propax) nil nil )) nil )"4" (flatten)"4" (expand "Tan?" )"4" (flatten) (("4" (mult-cases -1) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" trig_basic nil )nil real_props nil )"odd_int" integers nil )nil trig_basic nil )nil real_props nil )nil reals nil )"real" reals nil )"real" reals nil )nil booleans nil )"[T, T -> boolean]" equalities nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" trig_basic nil )"real" trig_basic nil )"[numfield, numfield -> numfield]" number_fieldsnil ))nil ))nil 3269431996"" (skosimp)"" (lemma "sin2_cos2" )"" (inst -1 "a!1" )"" (replace -1 * rl)"" (hide -1)"" (lemma "cos_plus" )"" (inst -1 "a!1" "a!1" )"" (replace -1 * lr)"" (hide -1)"" (expand "sq" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"odd_int" integers nil )nil trig_basic nil )"nnreal" nil )"trig_range" trig_basic nil )"real" reals nil )"nonneg_real" sq "reals/" )"real" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3269431996"" (skosimp)"" (lemma "sin2_cos2" )"" (inst -1 "a!1" )"" (replace -1 * rl)"" (hide -1)"" (lemma "cos_plus" )"" (inst -1 "a!1" "a!1" )"" (replace -1 * lr)"" (hide -1)"" (expand "sq" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )nil trig_basic nil )"nnreal" nil )"trig_range" trig_basic nil )"real" reals nil )"nonneg_real" sq "reals/" )"real" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3269431996"" (skosimp)"" (prop)"1" (lemma "sq_sin" )"1" (inst -1 "a!1/2" )"1" (replace -2 * lr)"1" (expand "sq" ) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (lemma "sq_sin" )"2" (inst -1 "a!1/2" )"2" (replace -2 * lr)"2" (assert )"2" (lemma "sq_eq_0" )"2" (inst -1 "sin(a!1/2)" )"2" (assert )"2" (replace -1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"nonneg_real" sq "reals/" )"real" reals nil )"trig_range" trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )nil trig_extra nil )"nonneg_rat" nil )"real" trig_basic nil )nil sq "reals/" ))nil ))nil 3269431996"" (skosimp)"" (prop)"1" (lemma "sq_cos" )"1" (inst -1 "a!1/2" )"1" (replace -2 * lr)"1" (expand "sq" ) (("1" (assert ) nil nil )) nil )) nil ))nil ))nil )"2" (lemma "sq_cos" )"2" (inst -1 "a!1/2" )"2" (replace -2 * lr)"2" (lemma "sq_eq_0" )"2" (inst -1 "cos(a!1/2)" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"nonneg_real" sq "reals/" )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil )nil trig_extra nil )nil sq "reals/" )"nonneg_rat" nil )"real" trig_basic nil )"real" reals nil ))nil ))nil 3269431996"" (skosimp)"" (lemma "sin_plus" )"" (inst -1 "a!1/2" "a!1/2" )"" (replace -2 * lr) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil trig_basic nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil ))nil 3269431996"" (skosimp)"" (expand "Tan?" )"" (prop)"" (rewrite "cos_half_zeroes" :dir rl)"" (assert ) nil nil )) nil ))nil ))nil ))nil )"bool" trig_basic nil )"real" reals nil )nil trig_extra nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (rewrite "sq_div" )"1" (rewrite "sq_sin" )"1" (rewrite "sq_cos" ) (("1" (grind-reals) nil nil )) nil ))nil )"2" (hide 3)"2" (lemma "sq_cos" )"2" (inst -1 "a!1" )"2" (prop)"2" (replace -2 * lr)"2" (expand "sq" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic nil )"real" trig_basic nil )"nonneg_real" sq "reals/" )nil trig_extra nil )nil real_props nil )nil real_props nil )nil trig_extra nil )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil )"real" reals nil )"real" trig_basic nil )"real" trig_basic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sq "reals/" ))nil ))nil 3269431996"" (skosimp*)"" (typepred "cos(a!1)" ) (("" (assert ) nil nil )) nil )) nil )"real" trig_basic nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"trig_range" trig_basic nil )"(total_order?[real])" nil )"odd_int" integers nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil ))nil ))nil 3269431996"" (skosimp*)"" (typepred "cos(a!1)" ) (("" (assert ) nil nil )) nil )) nil )"real" trig_basic nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"odd_int" integers nil )"real" reals nil )"posreal" nil )"(total_order?[real])" nil )"real" reals nil )"trig_range" trig_basic nil ))nil ))nil 3269431996"" (skosimp*)"" (lemma "cos_2a_sin" )"" (inst -1 "a!1/2" )"" (case-replace "2 * (a!1 / 2) = a!1" )"1" (hide -1)"1" (replace -1)"1" (hide -1)"1" "(2 * (sin(a!1 / 2) * sin(a!1 / 2)) / 2) = sq(sin(a!1/2))" )"1" (hide -1)"1" (prop)"1" (rewrite "sqrt_sq" )"1" (hide 2)"1" (rewrite "sin_ge_0" ) nil nil )) nil ))nil )"2" (rewrite "sqrt_sq_abs" )"2" (expand "abs" )"2" (lift-if)"2" (ground)"2" "sin_le_0" )"2" "a!1/2" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "sq" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )nil trig_basic nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"trig_range" trig_basic nil )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )nil booleans nil )"real" trig_basic nil )nil trig_ineq nil )nil sqrt "reals/" )"(total_order?[real])" nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil sqrt "reals/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"posreal" nil )nil trig_ineq nil )nil sqrt "reals/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil ))nil ))nil 3269431996"" (skosimp*)"" (typepred "cos(a!1)" ) (("" (assert ) nil nil )) nil )) nil )"real" trig_basic nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"trig_range" trig_basic nil )"(total_order?[real])" nil )"odd_int" integers nil )"real" reals nil )"posreal" nil )"(total_order?[real])" nil )"real" reals nil ))nil ))nil 3269431996"" (skosimp*)"" (typepred "cos(a!1)" ) (("" (assert ) nil nil )) nil )) nil )"real" trig_basic nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"odd_int" integers nil )"real" reals nil )"posreal" nil )"posreal" nil )"(total_order?[real])" nil )"real" reals nil )"trig_range" trig_basic nil ))nil ))nil 3269431996"" (skosimp*)"" (typepred "cos(a!1)" ) (("" (assert ) nil nil )) nil )) nil )"real" trig_basic nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(total_order?[real])" nil )"odd_int" integers nil )"real" reals nil )"posreal" nil )"posreal" nil )"(total_order?[real])" nil )"real" reals nil )"trig_range" trig_basic nil ))nil ))nil 3269431996"" (skosimp*)"" (lemma "cos_2a_sin" )"" (inst -1 "a!1/2" )"" (case-replace "2 * (a!1 / 2) = a!1" )"1" (hide -1)"1" (replace -1)"1" (hide -1)"1" (assert )"1" "sin(a!1 / 2) * sin(a!1 / 2) = sq(sin(a!1/2))" )"1" "(2 - 2 * sq(sin(a!1 / 2))) / 2 = (1 - sq(sin(a!1 / 2)))" )"1" (hide -1)"1" (rewrite "cos2" :dir rl)"1" (ground)"1" (case-replace "cos(a!1/2) >= 0" )"1" (rewrite "sqrt_sq" ) nil nil )"2" "2" (rewrite "cos_ge_0" ) nil nil ))nil ))nil )"2" (case "cos(a!1/2) <= 0" )"1" rewrite "sqrt_sq_abs" )"1" expand "abs" )"1" "1" (assert ) nil nil ))nil ))nil ))nil )"2" "2" (rewrite "cos_le_0" ) nil nil ))nil ))nil )"3" (case "cos(a!1/2) >= 0" )"1" (rewrite "sqrt_sq" ) nil nil )"2" "2" rewrite "cos_ge_0_3pi2" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (assert ) nil nil )) nil ))nil )"2" (hide 2)"2" (expand "sq" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )nil trig_basic nil )"[numfield, numfield -> numfield]" number_fields nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"posreal" nil )"trig_range" trig_basic nil )"real" reals nil )"posreal" nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil trig_basic nil )nil trig_ineq nil )"bool" reals nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil sqrt "reals/" )nil trig_ineq nil )"real" trig_basic nil )nil sqrt "reals/" )"nzreal" real_typesnil )"nzreal" nil )nil trig_ineq nil )"real" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nnreal" nil )"real" trig_basic nil )nil booleans nil )"bool" reals nil )nil real_types nil )"nonneg_real" sq "reals/" )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (expand "Tan?" )"" (lemma "cos_2a" )"" (inst -1 "a!1/2" )"" (replace -1 * lr)"" (hide -1)"" (prop)"" (replace -1 * lr)"" (assert )"" (lemma "sin2" )"" (inst -1 "a!1/2" )"" (expand "sq" )"" (replace -1 * lr)"" (hide -1) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" trig_basic nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )nil trig_basic nil )"nonneg_real" sq "reals/" )"real" reals nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"odd_int" integers nil )nil trig_basic nil ))nil ))nil 3269431996 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" reals nil )"odd_int" integers nil )"boolean" notequal nil )"trig_range" trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (lemma "sin_plus" )"" (inst -1 "a!1/2" "a!1/2" )"" (replace -1 * lr)"" (hide -1)"" (lemma "sq_cos" )"" (inst -1 "a!1/2" )"" (rewrite "div_cancel1" )"" (lemma "div_cancel1" )"" (inst -1 "2" "1+cos(a!1)" )"" (replace -2 * rl)"" (replace -1 * rl)"" (hide -2 -1)"" expand "sq" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" trig_basic nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"real" reals nil )"nonneg_real" sq "reals/" )"odd_int" integers nil )"even_int" integersnil )"[numfield, numfield -> numfield]" number_fields nil )"real" trig_basic nil )"real" reals nil )nil real_props nil )nil reals nil )nil trig_extra nil )"real" reals nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (expand "Tan?" )"" (lemma "sin_2a" )"" (inst -1 "a!1/2" )"" (replace -1 * lr)"" (hide -1)"" (prop)"" (replace -1 * lr) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" trig_basic nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"trig_range" trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp*)"" (name "BB" "a!1/2" )"" (replace -1)"" (case-replace "a!1 = 2*BB" )"1" (hide -1 -2)"1" (rewrite "sin_2a" )"1" (rewrite "cos_2a_sin" )"1" (assert )"1" (expand "tan" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil trig_basic nil )"real" trig_basic nil )nil trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"trig_range" trig_basic nil ))nil ))nil 3269431996"" (skosimp)"" (lemma "sin_plus" )"" (inst -1 "a!1" "2*a!1" )"" (rewrite "sin_2a" )"" (rewrite "cos_2a" )"" (assert )"" (replace -1)"" (assert )"" (hide -1)"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (assert )"" "sin_plus" )"" "a!1" "2*a!1" )"" rewrite "sin_2a" )"" rewrite "cos_2a" )"" assert )"" "cos2" )"" "" expand "sq" )"" replace -1)"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trig_basic nil )nil trig_basic nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" exponentiation nil )nil trig_basic nil )"nonneg_real" sq "reals/" )"real" reals nil )nil trig_basic nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil ))nil 3269431996"" (skosimp)"" (lemma "cos_plus" )"" (inst -1 "a!1" "2*a!1" )"" (rewrite "sin_2a" )"" (assert )"" (replace -1)"" (hide -1)"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (expand "expt" )"" (lemma "cos2" )"" (inst?)"" (expand "sq" )"" replace -1)"" rewrite "cos_2a" )"" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trig_basic nil )nil trig_basic nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" exponentiation nil )nil trig_basic nil )"nonneg_real" sq "reals/" )nil trig_basic nil )"real" reals nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"real" reals nil ))nil ))nil 3269431996"" (skosimp*)"" (prop)"1" (case "sin(a!1) - sin(b!1) = 0" )"1" (hide -2)"1" (rewrite "sin_diff" )"1" (rewrite "zero_times3" )"1" (rewrite "zero_times3" )"1" (prop)"1" (rewrite "cos_eq_0" )"1" (skosimp*)"1" (inst + "i!1" )"1" (assert )"1" (flatten) (("1" (ground) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "sin_eq_0" )"2" (skosimp*)"2" (lemma "both_sides_times1" )"2" "2" "(a!1 - b!1) / 2" "i!1 * pi" )"2" (replace -1 -2 rl t)"2" (rewrite "div_cancel2" -1)"2" "i!1" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (skosimp*)"2" (prop)"1" (replace -1)"1" (hide -1)"1" (rewrite "sin_plus" )"1" (assert )"1" (lemma "sin_k_pi" )"1" (inst -1 "2*k!1" )"1" (replace -1)"1" (hide -1)"1" (lemma "cos_2k_pi" )"1" (inst -1 "k!1" )"1" replace -1)"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (hide -1)"2" (lemma "sin_minus" )"2" (inst -1 "pi + 2*k!1*pi" "b!1" )"2" (replace -1)"2" (hide -1)"2" (lemma "sin_k_pi" )"2" (inst -1 "2*k!1+1" )"2" (assert )"2" (replace -1)"2" "2" assert )"2" rewrite "cos_plus" )"2" assert )"2" "cos_2k_pi" )"2" "k!1" )"2" replace -1)"2" "2" "sin_k_pi" )"2" "2*k!1" )"2" replace -1)"2" assert )"2" rewrite "cos_pi" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"real" trig_basic nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"posreal" nil )nil trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )nil real_props nil )nil real_props nil )nil trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )nil trig_extra nil )"real" reals nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"real" trig_basic nil )nil integers nil )nil trig_basic nil )nil trig_basic nil )nil trig_basic nil )"odd_int" integers nil )"odd_int" integers nil )nil trig_basic nil )nil trig_basic nil )"nzreal" nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp*)"" (prop)"1" (case-replace "cos(a!1)-cos(b!1) = 0" )"1" (hide -2)"1" (rewrite "cos_diff" )"1" (rewrite "zero_times3" )"1" (rewrite "zero_times3" )"1" (prop)"1" (rewrite "sin_eq_0" )"1" (skosimp*)"1" (inst + "i!1" ) (("1" (ground) nil nil ))nil ))nil ))nil )"2" (rewrite "sin_eq_0" )"2" (skosimp*)"2" (inst + "i!1" )"2" (flatten) (("2" (ground) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (skosimp*)"2" (prop)"1" (replace -1)"1" (hide -1)"1" (rewrite "cos_plus" )"1" (lemma "cos_2k_pi" )"1" (inst -1 "k!1" )"1" (replace -1)"1" (hide -1)"1" (lemma "sin_k_pi" )"1" (inst -1 "2*k!1" )"1" (replace -1)"1" "1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -1)"2" (hide -1)"2" (rewrite "cos_plus" )"2" (lemma "sin_k_pi" )"2" (inst -1 "2*k!1" )"2" (replace -1)"2" (assert )"2" (hide -1)"2" (lemma "cos_2k_pi" )"2" (inst -1 "k!1" )"2" replace -1)"2" assert )"2" "2" (rewrite "cos_neg" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"real" trig_basic nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil trig_basic nil )"nzint" integers nil )"even_int" integers nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_extra nil )"trig_range" trig_basic nil )"odd_int" integers nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" reals nil )"real" reals nil )"real" trig_basic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"real" reals nil )nil trig_basic nil )nil trig_basic nil )nil integers nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil trig_basic nil )nil trig_basic nil )"[numfield -> numfield]" number_fields nil ))nil ))nil 3269431996"" (skosimp*)"" (prop)"1" (case-replace "tan(a!1) - tan(b!1) = 0" )"1" (hide -2)"1" (rewrite "tan_diff" )"1" (rewrite "div_eq_zero" )"1" (rewrite "sin_eq_0" )"1" (skosimp*)"1" (inst + "i!1" ) (("1" (assert ) nil nil )) nil ))nil ))nil )"2" (hide -1 2)"2" (expand "Tan?" )"2" (lemma "zero_times3" )"2" (inst?) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (skosimp*)"2" (replace -1)"2" (hide -1)"2" (expand "tan" )"2" (expand "Tan?" )"2" (rewrite "sin_plus" )"2" (rewrite "cos_plus" )"2" (rewrite "sin_k_pi" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" trig_basic nil )"real" trig_basic nil )"[numfield, numfield -> numfield]" number_fields nil )nil reals nil )"boolean" notequal nil )nil real_props nil )"real" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )nil trig_extra nil )"odd_int" integers nil )"real" reals nil )"real" trig_basic nil )"bool" trig_basic nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"real" reals nil )nil trig_basic nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )nil integers nil )nil trig_basic nil )nil trig_basic nil ))nil ))nil 3409054007"" (skosimp*)"" (lemma "sin_eq_sin" )"" (inst?)"" (assert )"" (lemma "cos_eq_cos" )"" (inst?)"" (assert )"" (skosimp*)"" (case-replace "k!1 = 0" )"1" (assert ) nil nil )"2" (case-replace "k!2 = 0" )"1" (assert )"1" (case-replace "k!1 <= -1" )"1" (mult-by -1 "2*pi" )"1" (case-replace "k!1 >= 1" )"1" "2*pi" )"1" (ground) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (assert )"2" (case-replace "k!1 >= 1" )"1" "2*pi" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (case-replace "k!1 >= 1" )"1" (mult-by -1 "2*pi" )"1" (assert )"1" (case-replace "k!1 <= -1" )"1" "2*pi" )"1" (assert ) nil nil ))nil )"2" assert )"2" "1" "k!2 >= 1" )"1" "pi" )"1" "2*pi" )"1" (assert ) nil nil ))nil ))nil )"2" assert )"2" "k!2 <= -1" )"1" "2*pi" )"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" "2" replace -1)"2" "2" "(2*k!2+1) * pi = 2 * (k!1 * pi)" )"1" "1" "pi" )"1" assert )"1" "2 * (k!1 * pi) / pi = 2*k!1" )"1" assert )nil nil )"2" assert )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case-replace "k!1 <= -1" )"1" (mult-by -1 "2*pi" )"1" (assert ) nil nil )) nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trig_extra nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )"odd_int" integers nil )"(total_order?[real])" nil )nil extra_real_propsnil )"(total_order?[real])" nil )"nzreal" nil )nil extra_real_propsnil )"posreal" nil )"real" reals nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"odd_int" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )nil real_props nil )"boolean" notequal nil )nil reals nil )nil extra_real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil )"odd_int" integers nil )"real" reals nil )"nnreal" nil )"nnreal" nil )"[T, T -> boolean]" equalities nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"real" reals nil )nil trig_extra nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3414489003"" (skeep)"" (lemma "cos_plus" )"" (inst - "a" "pi/4" )"" (rewrite "cos_pi4" )"" (rewrite "sin_pi4" )"" (replace -2)"" (assert )"" (lemma "cos_eq_0" )"" (inst?)"" (assert )"" (skosimp*)"" (inst + "i!1" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trig_basic nil )nil trig_values nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"posreal" sqrt "reals/" )nil trig_basic nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"real" reals nil )nil trig_values nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil ))nil 3414489630"" (skosimp*)"" (expand "tan" ) (("" (rewrite "sin_eq_cos" ) nil nil )) nil ))nil )"real" trig_basic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_extra nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil ))nil 3269431996"" (skosimp*)"" (ground)"1" (lemma "sin_k_pi2" )"1" (inst -1 "i!1" )"1" (replace -1 * rl)"1" (hide -1)"1" (rewrite "sin_eq_sin" )"1" (skosimp*)"1" (prop)"1" (inst + "k!1" ) (("1" (assert ) nil nil )) nil )"2" (inst + "k!1-i!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "sin_k_pi2" )"2" (inst -1 "2*j!1+i!1" )"2" (replace -2 * rl)"2" (hide -2)"2" (replace -1)"2" (hide -1)"2" (lemma "expt_plus" )"2" (inst -1 "2*j!1" "i!1" "-1" )"2" (replace -1)"2" (hide -1)"2" (case "(-1) ^ (2 * j!1) = 1" )"1" (assert ) nil nil )"2" "2" (rewrite "even_m1_pow" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic nil )"rat" exponentiation nil )"nzreal" exponentiation nil )"odd_int" integers nil )"real" reals nil )"posreal" nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"nzreal" nil )nil integers nil )"real" reals nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil trig_extra nil )nil trig_basic nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil exponentiation nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"nzrat" rationalsnil )nil exponentiation nil )nil reals nil )"[numfield -> numfield]" number_fields nil )"int" integers nil ))nil ))nil 3269431996"" (skosimp*)"" (ground)"1" (lemma "cos_k_pi" )"1" (inst -1 "i!1" )"1" (replace -1 * rl)"1" (hide -1)"1" (rewrite "cos_eq_cos" )"1" (skosimp*)"1" (prop)"1" (inst + "k!1" ) (("1" (assert ) nil nil )) nil )"2" (inst + "k!1-i!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (lemma "cos_k_pi" )"2" (inst -1 "2*j!1+i!1" )"2" (replace -2 * rl)"2" (hide -2)"2" (replace -1)"2" (hide -1)"2" (lemma "expt_plus" )"2" (inst -1 "2*j!1" "i!1" "-1" )"2" (replace -1)"2" (hide -1)"2" (case "(-1) ^ (2 * j!1) = 1" )"1" (assert ) nil nil )"2" "2" (rewrite "even_m1_pow" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"trig_range" trig_basic nil )"rat" exponentiation nil )"nzreal" exponentiation nil )"odd_int" integers nil )"real" reals nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil integers nil )"real" reals nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil trig_extra nil )nil trig_basic nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil exponentiation nil )"[T, T -> boolean]" equalities nil )OR const-decl "[bool, bool -> bool]" booleans nil )"real" exponentiation nil )"nzrat" rationalsnil )nil exponentiation nil )"boolean" notequal nil )nil reals nil )"[numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil ))nil ))nil 3355652616"" (assert )"" (skosimp*)"" (rewrite "sin_plus" ) (("" (assert ) nil nil )) nil )) nil ))nil )"real" reals nil )"nnreal" nil )"posreal" sq "reals/" )"real" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil ))nil 3355738156"" (skosimp*)"" (hide -1)"" (expand "tan" )"" (cross-mult -1)"" (invoke (case "sq(%1) = sq(%2)" ) (? -1 "%1 = %2" ))"1" (rewrite "sq_times" )"1" (rewrite "sq_times" )"1" (lemma "sin2_cos2" )"1" (inst?)"1" (hide -3)"1" (prop)"1" (move-terms -1 l 1)"1" (replace -1)"1" (hide -1)"1" assert )"1" "1" "1" replace -2 - rl)"1" "sq(C!1)" )"1" rewrite "sq_div" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (move-terms -1 l 2)"2" (replace -1)"2" (hide -1)"2" assert )"2" "2" "2" replace -2 - rl)"2" "2" "sq(C!1)" )"2" rewrite "sq_div" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"real" reals nil )nil real_props nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"real" trig_basic nil )"real" trig_basic nil )nil reals nil )"boolean" notequal nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"trig_range" trig_basic nil )"real" reals nil )nil real_props nil )"trig_range" trig_basic nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil sq "reals/" )"nnreal" nil )nil trig_basic nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )"nnreal" nil )"nnreal" nil )nil sq "reals/" )nil extra_real_props nil )nil reals nil )nil real_props nil )"posreal" sq "reals/" )"[T, T -> boolean]" equalities nil )nil booleans nil )"bool" reals nil )nil real_types nil )"nonneg_real" sq "reals/" )"real" trig_basic nil ))nil 3420197393 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"boolean" notequal nil ))nil ))nil 3420197428"" (skosimp*)"" (rewrite "sin_plus" )"" (rewrite "sin_atan2" )"" (rewrite "cos_atan2" )"" (lift-if)"" (assert )"" (split +)"1" (flatten)"1" (replace -1)"1" (assert ) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (flatten)"2" "sqrt(1 + sq(y!1 / x!1)) = sqrt(sq(x!1)+sq(y!1))/sqrt(sq(x!1))" )"1" (assert ) nil nil )"2" (hide 3)"2" (lemma "sqrt_div" )"2" (inst - "sq(x!1) + sq(y!1)" "sq(x!1)" )"2" (split)"1" (replace -1 :dir RL)"1" case "%1=%2" )"1" (assert ) nil nil )"2" "2" "2" expand "sq" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (use "sq_gt_0" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"3" (hide 3)"3" (rewrite "sqrt_sq_abs" )"3" (expand "abs" )"3" (lift-if) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil )"4" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )"real" atan2 nil )nil application-judgement "nnreal_lt_2pi" atan2 nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil atan2 nil )"posreal" sqrt "reals/" )"real" reals nil )"nzreal" nil )"posreal" nil )"odd_int" integers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil sqrt "reals/" )nil sq "reals/" )"nnreal" nil )nil reals nil )nil real_props nil )nil sqrt "reals/" )"real" reals nil )"posreal" nil )"nnreal" nil )"bool" reals nil )nil real_types nil )nil real_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )"[numfield, numfield -> numfield]" number_fields nil )"nonneg_real" sq "reals/" )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil sq "reals/" )nil sqrt "reals/" )nil sqrt "reals/" )"real" reals nil )nil atan2 nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.89 Sekunden
(vorverarbeitet am 2026-05-04)
¤ *© Formatika GbR, Deutschland
2026-05-26
