SSL trig_extra.prf
Interaktion und
(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 )"posreal" atan nil )"nzint" integers nil )"even_int" integers nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def nil )"trig_range" sincos_def 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 )"posreal" atan nil )"nzint" integers nil )"even_int" integers nil )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"bool" sincos_def nil )"trig_range" sincos_def 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 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 )"real" integral_def "analysis/" )"real" atan nil )"posreal" atan nil )"real" sincos_def nil )"bool" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"real" reals nil )"real" reals nil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (rewrite "sin_minus_2pi" )"" (rewrite "cos_minus_2pi" ) nil nil )) nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"real" sincos_def nil )nil trig_extra nil )"trig_range" sincos_def nil )"even_int" integers nil )"nzint" integers nil )"trig_range" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" 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 )"posreal" atan nil )"trig_range" sincos_def nil )"trig_range" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" 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 )"posreal" atan nil )"trig_range" sincos_def nil )"trig_range" sincos_def 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" sincos_def nil )"real" reals nil )"trig_range" sincos_def 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 )"posreal" atan nil )"bool" sincos_def nil )"posreal" nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" 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" sincos_def nil )"trig_range" sincos_def 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" sincos_def nil )"real" sincos_def nil )"trig_range" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"posreal" nil )"real" sincos_def nil )nil trig_extra nil )"real" reals nil )"nzreal" nil )"trig_range" sincos_def nil )"real" reals nil )"trig_range" sincos_def 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 )"posreal" atan nil )"odd_int" integers nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def nil )"trig_range" sincos_def 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 )"posreal" atan nil )"odd_int" integers nil )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"bool" sincos_def nil )"real" reals nil )"trig_range" sincos_def 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 )"posreal" atan nil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (rewrite "sin_minus_pi" )"" (rewrite "cos_minus_pi" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"real" sincos_def nil )nil trig_extra nil )"real" reals nil )"real" reals nil )"trig_range" sincos_def nil )"odd_int" integers nil )"trig_range" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" 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 )"posreal" atan nil )"trig_range" sincos_def nil )"trig_range" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" 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 )"posreal" atan nil )"trig_range" sincos_def nil )"trig_range" sincos_def 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 )"posreal" atan 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" sincos_def nil )"trig_range" sincos_def nil )nil trig_basic nil )"bool" sincos_def nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (rewrite "sin_minus_pi2" )"" (rewrite "cos_minus_pi2" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"real" sincos_def nil )nil trig_extra nil )"nzreal" nil )"real" reals nil )"trig_range" sincos_def nil )"real" reals nil )"trig_range" sincos_def 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 )"posreal" atan nil )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def 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 )"posreal" atan nil )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"bool" sincos_def nil )"trig_range" sincos_def nil )"trig_range" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"real" sincos_def nil )nil trig_extra nil )"real" reals nil )"trig_range" sincos_def nil )"real" reals nil )"trig_range" sincos_def 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 )"posreal" atan nil )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"trig_range" sincos_def 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 )"posreal" atan nil )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"trig_range" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"bool" sincos_def 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" sincos_def nil )"real" reals nil )"trig_range" sincos_def 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 )"posreal" atan nil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (rewrite "sin_3pi2_minus" )"" (rewrite "cos_3pi2_minus" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"real" sincos_def nil )nil trig_extra nil )"nzreal" nil )"real" reals nil )"trig_range" sincos_def nil )"real" reals nil )"trig_range" sincos_def 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 )"posreal" atan nil )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def 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 )"posreal" atan nil )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def 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" sincos_def nil )nil trig_basic nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def 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" sincos_def nil )nil trig_extra nil )"real" reals nil )"trig_range" sincos_def nil )"real" reals nil )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" 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 )"posreal" atan nil )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def 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 )"posreal" atan nil )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"bool" sincos_def nil )nil trig_basic nil )"posreal" nil )"trig_range" sincos_def nil )"trig_range" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"real" sincos_def nil )nil trig_extra nil )"nzreal" nil )"trig_range" sincos_def nil )"real" reals nil )"trig_range" sincos_def 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" sincos_def nil )"trig_range" sincos_def 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" sincos_def nil )"trig_range" sincos_def 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" sincos_def nil )"trig_range" sincos_def 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" sincos_def nil )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" sincos_def 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" sincos_def nil )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" sincos_def 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" sincos_def nil )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" sincos_def nil )nil sincos_def nil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )"real" sincos_def 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" sincos_def nil )"trig_range" sincos_def nil )"real" reals nil )"nzint" integers nil )"even_int" integers nil )"[T, T -> boolean]" equalities nil )"real" sincos_def nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield -> numfield]" number_fields nil )nil sincos_def nil )nil trig_basic nil ))nil ))nil 3269431996"" (skosimp*)"" (expand "Tan?" )"" (rewrite "zero_times3" ) (("" (ground) nil nil )) nil )) nil ))nil )"bool" sincos_def nil )"trig_range" sincos_def nil )"real" sincos_def 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 ))nil ))nil ))nil )"2" (assert ) (("2" (assert ) nil nil )) nil )"3" (assert )"3" (assert )"3" (hide 2)"3" (expand "Tan?" )"3" (lemma "zero_times3" )"3" (inst?) (("3" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"4" (assert )"4" (assert )"4" (expand "Tan?" ) (("4" (propax) nil nil )) nil )) nil ))nil )"5" (assert )"5" (assert )"5" (expand "Tan?" ) (("5" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )"real" reals nil )"real" sincos_def 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" sincos_def nil )"real" sincos_def 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" sincos_def nil )"real" reals nil )"odd_int" integers nil )nil trig_basic nil )"nnreal" nil )"trig_range" sincos_def 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" sincos_def nil )"real" reals nil )nil trig_basic nil )"nnreal" nil )"trig_range" sincos_def 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 ) 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" sincos_def nil )"real" reals nil )"trig_range" sincos_def nil )nil trig_extra nil )"nonneg_rat" nil )"real" sincos_def 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" sincos_def nil )nil trig_extra nil )nil sq "reals/" )"nonneg_rat" nil )"real" sincos_def 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" sincos_def nil )"trig_range" sincos_def 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" sincos_def 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" sincos_def nil ))nil ))nil 3269431996"" (skosimp)"" (expand "tan" )"" (rewrite "sq_div" )"1" (rewrite "sq_sin" )"1" (rewrite "sq_cos" )"1" (assert )"1" (rewrite "div_div2" )"1" (rewrite "div_cancel1" ) nil nil )) 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" sincos_def nil )"real" sincos_def nil )"nonneg_real" sq "reals/" )nil trig_extra nil )nil real_props nil )nil real_props nil )"boolean" notequal nil )nil reals nil )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil trig_extra nil )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" sincos_def nil )"real" reals nil )"real" sincos_def nil )"real" sincos_def 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" sincos_def 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" sincos_def nil )"(total_order?[real])" nil )"odd_int" integers nil )"real" reals nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"(total_order?[real])" nil )"real" reals nil ))nil ))nil 3269431996"" (skosimp*)"" (typepred "cos(a!1)" ) (("" (assert ) nil nil )) nil )) nil )"real" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"(total_order?[real])" nil )"real" reals nil )"trig_range" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def nil )"nonneg_real" sq "reals/" )nil real_types nil )"bool" reals nil )nil booleans nil )"real" sincos_def 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" sincos_def nil ))nil ))nil 3269431996"" (skosimp*)"" (typepred "cos(a!1)" ) (("" (assert ) nil nil )) nil )) nil )"real" sincos_def 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" sincos_def nil )"(total_order?[real])" nil )"odd_int" integers nil )"real" reals nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"(total_order?[real])" nil )"real" reals nil ))nil ))nil 3269431996"" (skosimp*)"" (typepred "cos(a!1)" ) (("" (assert ) nil nil )) nil )) nil )"real" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"(total_order?[real])" nil )"real" reals nil )"trig_range" sincos_def nil ))nil ))nil 3269431996"" (skosimp*)"" (typepred "cos(a!1)" ) (("" (assert ) nil nil )) nil )) nil )"real" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"(total_order?[real])" nil )"real" reals nil )"trig_range" sincos_def 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def 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" sincos_def 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" sincos_def 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" sincos_def 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" sincos_def 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" sincos_def nil )"trig_range" sincos_def 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 )"real" reals nil )"real" integral_def "analysis/" )"real" atan nil )"posreal" atan nil )"real" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"real" reals nil )"real" reals 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" sincos_def 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" sincos_def nil )"real" reals nil )nil real_props nil )nil reals nil )nil trig_extra nil )"real" reals nil )"trig_range" sincos_def nil )"trig_range" sincos_def 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" sincos_def 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" sincos_def nil )"real" reals nil )"trig_range" sincos_def 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" sincos_def nil )nil trig_basic nil )"trig_range" sincos_def nil )"real" reals nil )"trig_range" sincos_def 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" sincos_def nil )"trig_range" sincos_def 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" sincos_def nil )"trig_range" sincos_def 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" sincos_def 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 )"posreal" atan 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" sincos_def nil )"real" reals nil )"real" reals nil )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" 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" sincos_def 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" sincos_def 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" sincos_def nil )"real" reals nil )"real" reals nil )nil trig_extra nil )"trig_range" sincos_def nil )"odd_int" integers nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"real" reals nil )"real" reals nil )"real" sincos_def 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 )"posreal" atan 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" sincos_def nil )"real" sincos_def 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" sincos_def nil )"trig_range" sincos_def nil )nil trig_extra nil )"odd_int" integers nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"real" reals nil )"real" sincos_def nil )"bool" sincos_def 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 )"posreal" atan nil )nil integers nil )nil trig_basic nil )nil trig_basic nil ))nil ))nil 3409057622"" (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" sincos_def nil )"trig_range" sincos_def 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 )"posreal" atan 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil )nil 3409057569";;; Proof sin_eq_sin-1 for formula trig_extra.sin_eq_sin" ";;; Proof sin_eq_sin-1 for formula trig_extra.sin_eq_sin" (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 )))))))))))"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 )))))))))))))))))))))))))))"2" (assert ) 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 )))))))))))))))))))))))"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 ))))))))))))))))))))))))))))))))))))))))))))))))))))))";;; developed with shostak decision procedures") nil nil ))nil 3422960416"" (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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def nil )"trig_range" sincos_def 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 )"posreal" atan 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 ))nil 3422960557"" (skosimp*)"" (expand "tan" ) (("" (rewrite "sin_eq_cos" ) nil nil )) nil ))nil )"real" sincos_def 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" sincos_def nil )"trig_range" sincos_def nil )"real" reals nil ))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" sincos_def nil )"rat" exponentiation nil )"nzreal" exponentiation nil )"odd_int" integers nil )"{r: posreal | pi_lb < r AND r < pi_ub}" 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 )"posreal" atan 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" sincos_def nil )"rat" exponentiation nil )"nzreal" exponentiation nil )"odd_int" integers nil )"{r: posreal | pi_lb < r AND r < pi_ub}" 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 )"posreal" atan 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 3409057644"" (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" sincos_def nil )"trig_range" sincos_def nil )"real" reals nil ))nil ))nil 3409057669"" (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" sincos_def nil )"real" sincos_def 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" sincos_def nil )"real" reals nil )nil real_props nil )"trig_range" sincos_def 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" sincos_def nil ))nil ))nil 3422960309 ("" (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 3422960329"" (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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )nil application-judgement "nnreal_lt_2pi" atan2 nil )"trig_range" sincos_def nil )"trig_range" sincos_def 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.176 Sekunden
(vorverarbeitet am 2026-05-01)
¤ *© Formatika GbR, Deutschland
2026-05-26
