Quelle trig_basic.prf
Sprache: Lisp
(trig_basicnil 3265002048"" (skosimp*)"" (expand "sin" )"" (expand "cos" )"" (lemma "floor_def" ("x" "a!1 / (2 * pi)" ))"" (rewrite "div_mult_pos_le2" -1)"" (rewrite "div_mult_pos_lt1" -1)"" (flatten -1)"" "sin2_cos2_phase" "x" "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)" ))"1" (assert ) nil nil ) ("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"real" reals nil )"real" sincos_def 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, 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 floor_ceil nil )"real" reals nil )nil real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil sincos_phase nil )nil real_types nil )nil sincos_phase nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"nnreal" nil )"real" reals nil )"(total_order?[real])" nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_props nil )"real" sincos_def nil ))nil 3265002167"" (skosimp*)"" (lemma "sin2_cos2" ("a" "a!1" )) (("" (assert ) nil nil )) nil ))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 )"nnreal" nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )"real" reals nil ))nil 3265002192"" (skosimp*)"" (lemma "sin2_cos2" ("a" "a!1" )) (("" (assert ) nil nil )) nil ))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 )"nnreal" nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )"real" reals nil ))nil 3265002205"" (expand "cos" )"" (rewrite "floor_int" ) (("" (rewrite "cos_phase_0" ) nil nil ))nil ))nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nnreal" nil )nil floor_ceil 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 )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 )"real" reals nil )"nnreal" nil )nil sincos_phase nil )"real" sincos_def nil )"nat" floor_ceil nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil 3265002237"" (expand "sin" )"" (rewrite "floor_int" ) (("" (rewrite "sin_phase_0" ) nil nil ))nil ))nil )AND const-decl "[bool, bool -> bool]" booleans nil )"nnreal" nil )nil floor_ceil 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 )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 )"real" reals nil )"nnreal" nil )nil sincos_phase nil )"real" sincos_def nil )"nat" floor_ceil nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil 3265002302"" (expand "sin" )"" (rewrite "div_div2" )"" (lemma "div_cancel1" ("x" "1/4" "n0z" "pi" ))"" (replace -1)"" (lemma "floor_val" ("i" "1" "j" "4" "k" "0" ))"" (split -1)"1" (replace -1)"1" (rewrite "sin_phase_pi2" ) nil nil )) nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_props 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 )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 sincos_phase nil )"(total_order?[real])" nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"(strict_total_order?[real])" real_props nil )"posint" nil )"even_int" integersnil )"posint" nil )"odd_int" integers nil )nil integers nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil floor_ceil nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil real_props nil )"posrat" nil )"real" sincos_def nil )"nnreal" nil )"nat" floor_ceil nil )"posreal" nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil 3265002447"" (lemma "sin2_cos2" ("a" "pi/2" ))"" (rewrite "sin_pi2" )"" (rewrite "sq_1" )"" (lemma "sq_eq_0" ("a" "cos(pi/2)" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil )nil trig_basic nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )nil sq "reals/" )"real" sincos_def nil )"posreal" nil )"trig_range" sincos_def nil )"posreal" sq "reals/" )nil sq "reals/" )"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 ))nil 3264999490"" (expand "Tan?" )"" (expand "cos" )"" (rewrite "floor_int" )"" (rewrite "cos_phase_0" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"nat" floor_ceil nil )"real" sincos_def nil )nil sincos_phase nil )"nnreal" 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 )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil floor_ceil nil )"nnreal" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" sincos_def nil ))nil 3265002274"" (expand "tan" )"" (rewrite "sin_0" )"" (rewrite "cos_0" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil trig_basic nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )nil trig_basic nil )"real" sincos_def nil ))nil 3265008367"" (skosimp*)"" (expand "sin" )"" (lemma "floor_neg" ("x" "a!1/(2*pi)" ))"" (case "integer?(a!1 / (2 * pi))" )"1" (assert )"1" (replace -2)"1" (lemma "floor_def" ("x" "-a!1 / (2 * pi)" ))"1" (flatten -1)"1" "div_mult_pos_le2" "x" "floor(-a!1 / (2 * pi))" "z" "-a!1" "py" "2 * pi" ))"1" (replace -1 -2)"1" "div_mult_pos_lt1" "x" "floor(-a!1 / (2 * pi))+1" "z" "-a!1" "py" "2 * pi" ))"1" (replace -1 -4)"1" (hide -1 -2)"1" (rewrite "floor_int" -4)"1" case "floor(-(a!1 / (2 * pi))) = -a!1/(2*pi)" )"1" replace -1)"1" "div_cancel1" "x" "a!1" "n0z" "2*pi" ))"1" replace -1)"1" "div_cancel1" "x" "-a!1" "n0z" "2*pi" ))"1" replace -1)"1" "1" rewrite "sin_phase_0" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (replace -1 2)"2" (case "a!1 = - 2 * (floor(-a!1 / (2 * pi)) * pi)" )"1" (assert ) nil nil )"2" "sin_phase_neg" "px" "-a!1 - 2 * (floor(-a!1 / (2 * pi)) * pi)" ))"1" (assert ) nil nil )"2" (assert )"2" (lemma "floor_def" ("x" "-a!1 / (2 * pi)" ))"2" (flatten -1)"2" (rewrite "div_mult_pos_le2" -1)"2" (rewrite "div_mult_pos_lt1" -2)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"real" reals nil )"posreal" nil )"real" reals nil )"real" sincos_def nil )"bool" integers nil )nil floor_ceil nil )"real" reals nil )nil sincos_phase nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"even_int" integers nil )nil reals nil )nil real_props nil )"[T, T -> boolean]" equalities nil )nil real_props nil )"int" integers nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_props nil )"[numfield -> numfield]" number_fields nil )nil floor_ceil nil )"real" reals nil )"int" integers nil )nil sincos_phase nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"nzint" integers nil )"int" integers nil )"real" reals nil )nil floor_ceil 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 ))nil 3265009425"" (skosimp*)"" (expand "cos" )"" (lemma "floor_neg" ("x" "a!1 / (2 * pi)" ))"" (case "integer?(a!1 / (2 * pi))" )"1" (assert ) nil nil )"2" (assert )"2" (replace -1)"2" case "-a!1 - 2 * (floor(-a!1 / (2 * pi)) * pi) = 0" )"1" (assert ) nil nil )"2" "cos_phase_neg" "px" "-a!1 - 2 * (floor(-a!1 / (2 * pi)) * pi)" ))"1" (assert ) nil nil )"2" (lemma "floor_def" ("x" "-a!1 / (2 * pi)" ))"2" (flatten)"2" (rewrite "div_mult_pos_le2" -1)"2" (rewrite "div_mult_pos_lt1" -2)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"real" reals nil )"posreal" nil )"real" reals nil )"real" sincos_def nil )"bool" integers nil )"real" reals nil )"int" integers nil )nil sincos_phase nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )nil real_props nil )nil floor_ceil nil )"[T, T -> boolean]" equalities nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"int" integers nil )"real" reals nil )nil floor_ceil 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 ))nil 3264999490"" (skosimp*)"" (typepred "a!1" )"" (expand "Tan?" )"" (lemma "cos_neg" ("a" "a!1" )) (("" (assert ) nil nil ))nil ))nil ))nil ))nil )"bool" sincos_def 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 )nil trig_basic nil )"trig_range" sincos_def nil )"real" reals nil ))nil 3265006358"" (skosimp*)"" (typepred "a!1" )"" (expand "Tan?" )"" (expand "tan" )"" (rewrite "cos_neg" )"" (rewrite "sin_neg" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" sincos_def 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" sincos_def nil )nil trig_basic nil )"real" reals nil )"trig_range" sincos_def nil )"real" reals nil )"trig_range" sincos_def nil )nil trig_basic nil ))nil 3265009874"" (skosimp*)"" (expand "cos" )"" (expand "sin" )"" (lemma "floor_def" ("x" "a!1 / (2 * pi)" ))"" (rewrite "div_mult_pos_le2" -1)"" (rewrite "div_mult_pos_lt1" -1)"" (lemma "floor_def" ("x" "(pi/2+a!1 )/ (2 * pi)" ))"" (rewrite "div_mult_pos_le2" -1)"" (rewrite "div_mult_pos_lt1" -1)"" (flatten)"" "cos_eqv_sin_phase" "x" "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)" ))"1" (replace -1)"1" (hide -1)"1" "floor_plus" "x" "a!1 / (2 * pi)" "y" "1/4" ))"1" "floor_val" "i" "1" "j" "4" "k" "0" ))"1" "1" replace -1)"1" "div_cancel1" "x" "1/4" "n0z" "pi" ))"1" "div_distributes" "x" "pi/2" "y" "a!1" "n0z" "2*pi" ))"1" replace -2 -1)"1" replace -1 * rl)"1" replace -4)"1" assert )"1" replace -1)"1" "FL" "floor(a!1 / (2 * pi))" )"1" replace -1)"1" case "fractional(1/4) = 1/4" )"1" replace -1)"1" case "fractional(a!1 / (2 * pi)) = a!1/(2*pi) - FL" )"1" replace "1" case "a!1 - 2 * (FL * pi) < 3 * pi / 2" )"1" assert )"1" case "floor(1 / 4 + a!1 / (2 * pi) - FL) = 0" )"1" assert )nil nil )"2" "2" "floor_def" "x" "1 / 4 + a!1 / (2 * pi) - FL" ))"2" "2" "K1" "floor(1 / 4 + a!1 / (2 * pi) - FL)" )"2" "trichotomy" "x" "K1" ))"2" "1" case "K1=1" )"1" replace "1" assert )nil nil ))nil )"2" case "K1>1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "floor(1 / 4 + (a!1 / (2 * pi) - FL)) = 1" )"1" replace "1" "1" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" expand "fractional" "2" replace "2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "fractional" "2" "floor_val" "i" "1" "j" "4" "k" "0" ))"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"real" reals nil )"real" sincos_def 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, 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 floor_ceil nil )"real" reals nil )nil real_props nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"posrat" nil )nil floor_ceil nil )nil real_props nil )nil reals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )nil real_axioms nil )"even_int" integersnil )"posint" nil )"(strict_total_order?[real])" real_props nil )"odd_int" integers nil )"{x | 0 <= x & x < 1}" floor_ceil nil )"[T, T -> boolean]" equalities nil )nil real_props nil )"nat" floor_ceil nil )"nonneg_int" nil )"even_int" integersnil )"posint" nil )"even_int" integersnil )"posint" nil )"odd_int" integers nil )nil integers nil )nil integers nil )nil floor_ceil nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil sincos_phase nil )nil real_types nil )nil sincos_phase nil )"real" reals nil )"(total_order?[real])" nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil real_props nil )"real" sincos_def nil )"real" reals nil )"posreal" nil ))nil 3265010005"" (skosimp*)"" (lemma "cos_sin" ("a" "-(a!1+pi/2)" ))"" (lemma "cos_neg" ("a" "a!1+pi/2" ))"" (lemma "sin_neg" ("a" "a!1" )) (("" (assert ) 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 )"[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 )nil trig_basic nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )nil trig_basic nil )"real" reals nil ))nil 3265074854"" (skosimp*)"" (lemma "sin_neg" ("a" "pi/2-a!1" ))"" (lemma "sin_cos" ("a" "a!1-pi/2" )) (("" (assert ) 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 )"real" reals nil )"trig_range" sincos_def nil )"real" reals nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"trig_range" sincos_def nil )nil trig_basic nil ))nil 3265010327"" (skosimp*)"" (lemma "sin_shift" ("a" "pi/2-a!1" )) (("" (assert ) 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 )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def nil ))nil 3265010987"" (skosimp*)"" (rewrite "cos_sin" )"" (rewrite "sin_cos" ) (("" (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 )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"real" reals nil )"trig_range" sincos_def nil )"posreal" 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, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil trig_basic nil ))nil 3265071739"" (skosimp*)"" (rewrite "sin_cos" )"" (rewrite "cos_sin" ) (("" (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 )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"real" reals nil )"trig_range" sincos_def nil )"real" reals nil )"posreal" 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 trig_basic nil ))nil 3265006547"" (expand "sin" )"" (lemma "div_cancel1" ("x" "1/2" "n0z" "pi" ))"" (replace -1 1)"" (lemma "floor_val" ("i" "1" "j" "2" "k" "0" ))"" (split -1)"1" (replace -1)"1" (assert )"1" (expand "sin_phase" )"1" (lemma "div_cancel1" ("x" "2" "n0z" "pi" ))"1" (replace -1)"1" (rewrite "sin_value_0" )"1" (rewrite "floor_int" 1)"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans 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 )nil real_props nil )"posrat" nil )nil floor_ceil nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )nil integers nil )"odd_int" integers nil )"posint" nil )"even_int" integersnil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"(total_order?[real])" nil )"real_abs_le1" sincos_phase nil )nil floor_ceil nil )"even_int" integers nil )nil sincos_quad nil )"real" reals nil )"posreal" nil )"real" sincos_def nil )"nnreal" nil )"nat" floor_ceil nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil 3279154503"" (expand "cos" )"" (lemma "div_cancel1" ("x" "1/2" "n0z" "pi" ))"" (replace -1)"" (lemma "floor_val" ("i" "1" "j" "2" "k" "0" ))"" (split -1)"1" (replace -1)"1" (simplify 1)"1" (expand "cos_phase" )"1" (rewrite "cos_value_pi" ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans 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 )nil real_props nil )"posrat" nil )nil floor_ceil nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil integers nil )nil integers nil )"odd_int" integers nil )"posint" nil )"even_int" integersnil )"posint" nil )"(strict_total_order?[real])" real_props nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )"(total_order?[real])" nil )"real_abs_le1" sincos_phase nil )nil sincos_quad nil )"odd_int" integers nil )"real" reals nil )"posreal" nil )"real" sincos_def nil )"nnreal" nil )"nat" floor_ceil nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil )nil 3265008251"" (expand "pi" )"" (expand "cos" )"" (lemma "div_cancel1" ("x" "1/2" "n0z" "pi" ))"" (replace -1)"" (lemma "floor_val" ("i" "1" "j" "2" "k" "0" ))"" (split -1)"1" (replace -1)"1" (simplify 1)"1" (expand "cos_phase" )"1" (rewrite "cos_value_pi" ) nil nil )) nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sincos_quad nil )"real_abs_le1" sincos_phase nil )"posreal" atan nil ))nil 3264999490"" (expand "Tan?" )"" (rewrite "cos_pi" ) (("" (assert ) nil nil )) nil )) nil )nil trig_basic nil )"odd_int" integers nil )"bool" sincos_def nil ))nil 3265006469"" (expand "tan" )"" (rewrite "sin_pi" )"" (rewrite "cos_pi" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil trig_basic nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )"rat" rationals nil )"odd_int" integers nil )nil trig_basic nil )"real" sincos_def nil ))nil 3265010743"" (lemma "neg_sin" ("a" "pi/2" ))"" (rewrite "sin_pi2" ) (("" (assert ) nil nil )) nil )) nil )nil trig_basic nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def nil )"posreal" nil )"odd_int" integers 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 )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil ))nil 3265010800"" (lemma "neg_cos" ("a" "pi/2" ))"" (rewrite "cos_pi2" ) (("" (assert ) nil nil )) nil )) nil )nil trig_basic nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def nil )"posreal" nil )"even_int" integers 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 )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil ))nil 3279154535"" (expand "sin" )"" (rewrite "div_simp" )"" (rewrite "floor_int" )"" (assert ) (("" (rewrite "sin_phase_0" ) nil nil )) nil ))nil ))nil ))nil )nil real_props 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 )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 )"real" reals nil )nil sincos_phase nil )nil floor_ceil nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"real" sincos_def nil )"nnreal" nil )"nat" floor_ceil nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil )nil 3265010441"" (expand "pi" )"" (expand "sin" )"" (rewrite "div_simp" )"" (rewrite "floor_int" )"" (assert ) (("" (rewrite "sin_phase_0" ) nil nil )) nil ))nil ))nil ))nil ))nil )nil sincos_phase nil )"posreal" atan nil ))nil 3279154560"" (expand "cos" )"" (rewrite "div_simp" )"" (rewrite "floor_int" )"" (assert ) (("" (rewrite "cos_phase_0" ) nil nil )) nil ))nil ))nil ))nil )nil real_props 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 )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 )"real" reals nil )nil sincos_phase nil )nil floor_ceil nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"real" sincos_def nil )"nnreal" nil )"nat" floor_ceil nil )"posreal" nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil ))nil )nil 3265010493"" (expand "cos" )"" (expand "pi" )"" (rewrite "div_simp" )"" (rewrite "floor_int" )"" (assert ) (("" (rewrite "cos_phase_0" ) nil nil )) nil ))nil ))nil ))nil ))nil )nil sincos_phase nil )"posreal" atan nil ))nil 3264999491"" (expand "Tan?" )"" (rewrite "cos_2pi" ) (("" (assert ) nil nil )) nil )) nil )nil trig_basic nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"bool" sincos_def nil ))nil 3265006491"" (expand "tan" )"" (rewrite "sin_2pi" )"" (rewrite "cos_2pi" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil trig_basic nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )nil trig_basic nil )"real" sincos_def nil ))nil 3265083493"" (skosimp*)"" (expand "sin" )"" (expand "cos" )"" (name "FLA" "floor(a!1 / (2 * pi))" )"" (name "FLB" "floor(b!1 / (2 * pi))" )"" (replace -1)"" (replace -2)"" "floor_plus" "x" "a!1/(2*pi)" "y" "b!1/(2*pi)" ))"" (replace -2)"" (replace -3)"" "sin_phase_sum" "x" "a!1 - 2 * (FLA * pi)" "y" "b!1 - 2 * (FLB * pi)" ))"1" (replace -1 1)"1" (hide -1)"1" case "a!1 - 2 * (FLA * pi) + (b!1 - 2 * (FLB * pi)) < 2 * pi" )"1" assert )"1" case "floor(fractional(a!1 / (2 * pi)) + fractional(b!1 / (2 * pi))) = 0" )"1" (assert ) nil nil )"2" "2" "floor_def" "x" "fractional(a!1 / (2 * pi)) + fractional(b!1 / (2 * pi))" ))"2" "2" expand "fractional" )"2" replace -4)"2" replace -5)"2" "both_sides_times_pos_le1" "x" "floor(a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB)" "y" "a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB" "pz" "2*pi" ))"2" "both_sides_times_pos_lt1" "y" "1+floor(a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB)" "x" "a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB" "pz" "2*pi" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" case "floor((a!1 + b!1) / (2 * pi)) = FLA+FLB+1" )"1" (assert ) nil nil )"2" "2" case "floor(fractional(a!1 / (2 * pi)) + fractional(b!1 / (2 * pi))) = 1" )"1" (assert ) nil nil )"2" "2" expand "fractional" 1)"2" replace -2)"2" replace -3)"2" "2" "floor_def" "x" "a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB" ))"2" "both_sides_times_pos_lt1" "y" "1+floor(a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB)" "x" "a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB" "pz" "2*pi" ))"2" "both_sides_times_pos_lt1" "x" "floor(a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB)" "y" "a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB" "pz" "2*pi" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "floor_def" ("x" "b!1/(2*pi)" ))"2" (rewrite "div_mult_pos_lt1" -1)"2" rewrite "div_mult_pos_le2" -1)"2" "2" replace -4)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (hide-all-but 1)"3" (expand "FLA" )"3" "floor_def" ("x" "a!1/(2*pi)" ))"3" rewrite "div_mult_pos_lt1" -1)"3" rewrite "div_mult_pos_le2" -1)"3" "3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"real" reals nil )"posreal" nil )"real" reals nil )"trig_range" sincos_def nil )"real" sincos_def nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" reals nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"real" reals nil )"real" reals nil )nil floor_ceil nil )"{i | i <= a!1 / (2 * pi) & a!1 / (2 * pi) < 1 + i}" trig_basicnil )nil real_props nil )nil real_props nil )"{x | 0 <= x & x < 1}" floor_ceil nil )nil floor_ceil nil )nil real_props nil )"(total_order?[real])" nil )nil real_props nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil sincos_phase nil )nil real_types nil )nil sincos_phase nil )"int" integers nil )"real" sincos_def nil ))nil 3265007645"" (skosimp*)"" (lemma "sin_plus" ("a" "a!1" "b" "-b!1" ))"" (rewrite "sin_neg" )"" (rewrite "cos_neg" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"[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 )nil trig_basic nil )"real" reals nil )"real" reals nil )"trig_range" sincos_def nil )"real" reals nil )"trig_range" sincos_def nil )nil trig_basic nil ))nil 3265071786"" (skosimp*)"" (rewrite "cos_sin" )"" (rewrite "cos_sin" )"" (lemma "sin_cos" ("a" "a!1" ))"" (lemma "sin_plus" ("a" "pi/2+a!1" "b" "b!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))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 )"trig_range" sincos_def nil )"real" reals nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"trig_range" sincos_def nil )nil trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic 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 ))nil 3265007693"" (skosimp*)"" (lemma "cos_plus" ("a" "a!1" "b" "-b!1" ))"" (rewrite "cos_neg" )"" (rewrite "sin_neg" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )"[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 )nil trig_basic nil )"real" reals nil )"real" reals nil )"trig_range" sincos_def nil )"real" reals nil )"trig_range" sincos_def nil )nil trig_basic nil ))nil 3264999490"" (skosimp*)"" (expand "tan" )"" (expand "Tan?" ) (("" (assert ) nil nil )) nil )) nil ))nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )"real" reals nil )"real" reals nil )"real" sincos_def nil )"real" reals nil )"real" reals nil )"bool" sincos_def nil ))nil 3265074705"" (skosimp*)"" (expand "Tan?" )"" (expand "tan" )"" (rewrite "sin_plus" 2)"" (rewrite "cos_plus" 2)"" (rewrite "cross_mult" 2) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" sincos_def 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 )"real" reals nil )nil real_props nil )"boolean" notequal nil )nil reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" sincos_def nil )"real" sincos_def nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil trig_basic nil )"real" sincos_def nil )"real" reals nil )"real" reals nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil ))nil 3264999490"" (skosimp*) (("" (expand "tan" ) (("" (assert ) nil nil )) nil ))nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )"real" reals nil )"real" sincos_def nil )"real" reals nil )"odd_int" integers nil )"real" reals nil )"real" reals nil ))nil 3265071900"" (skosimp*)"" (lemma "tan_plus" ("a" "a!1" "b" "-b!1" ))"" (rewrite "tan_neg" -1)"" (assert )"" (expand "Tan?" ) (("" (rewrite "cos_neg" 1) nil nil ))nil ))nil ))nil ))nil ))nil )"[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 )"real" reals nil )"odd_int" integers nil )"trig_range" sincos_def nil )nil trig_basic nil )"real" reals nil )"real" reals nil )"real" reals nil )nil trig_basic nil )nil booleans nil )"bool" sincos_def nil ))nil 3265002655"" (skosimp*)"" (case "c!1=0" )"1" (replace -1)"1" (inst + "0" )"1" (rewrite "zero_times1" 1)"1" (lemma "sq_eq_0" ("a" "a!1" ))"1" (lemma "sq_eq_0" ("a" "b!1" ))"1" (rewrite "sq_0" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (typepred "sq(b!1)" )"2" (typepred "sq(a!1)" )"2" (lemma "sq_nz_pos" ("nz" "c!1" ))"1" (case "sq(a!1)<=sq(c!1)" )"1" "div_mult_pos_le1" "z" "sq(a!1)" "py" "sq(c!1)" "x" "1" ))"1" (lemma "sq_div" ("a" "a!1" "d" "c!1" ))"1" (assert )"1" (replace -1 -2 rl)"1" (hide -1)"1" "sq_le_abs" ("a" "a!1/c!1" "b" "1" ))"1" (rewrite "sq_1" )"1" (replace -2 -1)"1" "1" expand "abs" -1 2)"1" case "sq(b!1) <= sq(c!1)" )"1" "div_mult_pos_le1" "z" "sq(b!1)" "py" "sq(c!1)" "x" "1" ))"1" replace -2 -1)"1" "1" "sq_le_abs" "a" "b!1/c!1" "b" "1" ))"1" rewrite "sq_div" -1)"1" rewrite "sq_1" -1)"1" replace -2 -1)"1" "1" expand "abs" "1" case "sq(a!1/c!1)+sq(b!1/c!1) =1" )"1" case "FORALL (x,y: {x: nnreal | x <= 1}): sq(x) + sq(y) = 1 => (EXISTS (z: {z: nnreal | z <= pi / 2}): x = cos(z) & y = sin(z))" )"1" expand "abs" "1" case "b!1 / c!1 < 0" )"1" case "a!1 / c!1 < 0" )"1" "-(a!1/c!1)" "-(b!1/c!1)" )"1" rewrite "sq_neg" )"1" rewrite "sq_neg" )"1" assert )"1" "1" "z!1+pi" )"1" "neg_cos" "a" "z!1" ))"1" "neg_sin" "a" "z!1" ))"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil )"2" "-(b!1/c!1)" "a!1/c!1" )"1" rewrite "sq_neg" )"1" assert )"1" "1" "cos_sin" "a" "z!1-pi/2" ))"1" "sin_cos" "a" "z!1-pi/2" ))"1" assert )"1" "z!1-pi/2" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil )"2" case "a!1 / c!1 < 0" )"1" "b!1/c!1" "-(a!1/c!1)" )"1" rewrite "sq_neg" )"1" assert )"1" "1" rewrite "cos_sin" "1" rewrite "sin_cos" "1" "pi/2+z!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil )"2" "a!1/c!1" "b!1/c!1" )"1" assert )"1" "1" "z!1" )"1" assert )nil nil ))nil ))nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil )"2" "2" "2" "x!1" )"2" "y!1" )"2" "acos(x!1)" )"1" case "x!1 = cos(acos(x!1))" )"1" assert )"1" "acos(x!1)" )"1" expand ">=" "1" expand "<=" "1" "1" "acos_strict_decreasing" )"1" expand "strict_decreasing?" )"1" "0" "x!1" )"1" assert )"1" rewrite "acos_0" )"1" expand "cos" )"1" expand "sin" )"1" case "floor(acos(x!1) / (2 * pi)) = 0" )"1" replace "1" assert )"1" "sin_q1" "x" "acos(x!1)" ))"1" rewrite "phase_sin_q1" "1" replace "1" "sin_eqv_sqrt_cos_value" "q1" "acos(x!1)" ))"1" replace "1" rewrite "cos_value_acos" "1" "sq_eq" "nna" "y!1" "nnb" "sqrt(1 - sq(x!1))" ))"1" replace "1" rewrite "sq_sqrt" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "floor_def" "x" "acos(x!1)/(2*pi)" ))"2" rewrite "div_mult_pos_le2" "2" "2" "div_mult_pos_lt1" "x" "floor(acos(x!1) / (2 * pi)) + 1" "py" "2*pi" "z" "acos(x!1)" ))"2" replace "2" "2" "K1" "floor(acos(x!1) / (2 * pi))" )"2" "trichotomy" "x" "K1" ))"2" "1" case "K1=1" )"1" assert )nil nil )"2" case "K1>1" )"1" "both_sides_times_pos_lt1" "x" "1" "y" "K1" "pz" "2*pi" ))"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil )"2" nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" replace "2" rewrite "acos_0" )"2" "sin_pi2" )"2" expand "pi" )"2" replace "2" rewrite "sq_0" )"2" "sq_eq" "nna" "y!1" "nnb" "1" ))"2" rewrite "sq_1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" expand "cos" )"2" case "floor(acos(x!1) / (2 * pi))=0" )"1" replace "1" assert )"1" rewrite "cos_phase_acos" )nil nil ))nil ))nil )"2" "2" "acos(x!1)" )"2" "floor_def" "x" "acos(x!1) / (2 * pi)" ))"2" rewrite "div_mult_pos_lt1" "2" rewrite "div_mult_pos_le2" "2" "2" "K1" "floor(acos(x!1) / (2 * pi))" )"2" "trichotomy" "x" "K1" ))"2" "1" case "K1=1" )"1" assert )nil nil )"2" case "K1>1" )"1" "both_sides_times_pos_lt1" "x" "1" "y" "K1" "pz" "2*pi" ))"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil )"2" nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "abs" )"3" nil nil ))nil ))nil )"2" "acos_strict_decreasing" )"2" expand "strict_decreasing?" )"2" expand ">=" "2" expand "<=" "2" "1" "0" "x!1" )"1" rewrite "acos_0" )"1" assert )nil nil ))nil )"2" expand "abs" )"2" assert )nil nil ))nil ))nil )"2" replace "2" rewrite "acos_0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" expand "abs" )"3" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" rewrite "sq_div" )"2" rewrite "sq_div" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )nil sq "reals/" )nil sq "reals/" )"nnreal" nil )nil real_props nil )"real" sincos_def nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )"bool" reals nil )nil sq "reals/" )nil sq "reals/" )nil number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )nil real_types nil )"[bool, bool -> bool]" booleans nil )"posreal" atan nil )AND const-decl "[bool, bool -> bool]" booleans nil )"real" sincos_def nil )"bool" reals nil )"real" reals nil )nil trig_basic nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil trig_basic nil )"real" reals nil )"[numfield -> numfield]" number_fields nil )"real" trig_basic nil )"real" trig_basic nil )"real" trig_basic nil )nil trig_basic nil )"real" reals nil )nil trig_basic nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )nil sq "reals/" )"posreal" nil )nil trig_basic nil )nil acos nil )nil acos nil )nil real_props nil )"posint" nil )nil real_props nil )nil real_axioms nil )nil real_props nil )nil floor_ceil nil )nil sincos_phase nil )nil sincos_phase nil )nil sq "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil sqrt "reals/" )nil sincos_quad nil )nil sincos_quad nil )nil sincos_quad nil )nil sincos_phase nil )"[numfield, numfield -> numfield]" number_fields nil )"{i | i <= x & x < i + 1}" floor_ceil nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"nnreal" nil )"nat" floor_ceil nil )"posreal" nil )"bool" real_fun_preds "reals/" )nil sincos_phase nil )"{x: nnreal | x <= 1}" trig_basic nil )"nnreal_le_pi" acos nil )nil acos nil )nil asin nil )"[numfield, numfield -> numfield]" number_fields nil )nil sq "reals/" )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals nil )"nnreal" nil )"(strict_total_order?[real])" real_props nil )nil real_types nil )"bool" reals nil )nil real_props nil )nil reals nil )"boolean" notequal nil )nil sq "reals/" )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil real_types nil )"nonneg_real" sq "reals/" ))nil 3265083183"" (skosimp*)"" (lemma "arc_sin_cos" ("a" "a!1" "b" "b!1" "c" "nnc!1" ))"" (assert )"" (skosimp*)"" (inst + "d!1" )"" (lemma "sin2_cos2" ("a" "d!1" ))"" (expand "sq" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))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 trig_basic nil )nil trig_basic nil )"nnreal" nil )"real" reals nil )"nonneg_real" sq "reals/" )"nnreal" nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )"real" reals nil ))nil 3265007761"" (skosimp*)"" (lemma "sin_plus" ("a" "a!1" "b" "a!1" ))"" (assert ) nil nil )) nil ))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 )"real" reals nil )"real" reals nil )"trig_range" sincos_def nil ))nil 3265007796"" (skosimp*)"" (lemma "cos_plus" ("a" "a!1" "b" "a!1" ))"" (assert ) nil nil )) nil ))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 )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" sincos_def nil ))nil 3265007818"" (skosimp*)"" (rewrite "cos_2a" )"" (rewrite "sq_rew" )"" (rewrite "sq_rew" )"" (lemma "sin2_cos2" ("a" "a!1" ))"" (expand "sq" ) (("" (assert ) 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 )"trig_range" sincos_def nil )"trig_range" sincos_def nil )"real" reals nil )"real" reals nil )"real" sincos_def nil )"nonneg_real" sq "reals/" )"real" reals nil )nil trig_basic nil )"odd_int" integers nil )nil sq "reals/" )"real" sincos_def nil ))nil 3265007915"" (skosimp*)"" (lemma "sin2_cos2" ("a" "a!1" ))"" (rewrite "cos_2a" )"" (expand "sq" ) (("" (assert ) nil nil )) nil )) nil ))nil ))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 )"nonneg_real" sq "reals/" )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )nil trig_basic nil ))nil 3264999490"" (skosimp*) (("" (expand "tan" ) (("" (assert ) nil nil )) nil ))nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )"real" reals nil )"real" reals nil )"real" sincos_def nil )"real" reals nil ))nil 3265072074"" (skosimp*)"" (lemma "tan_plus" ("a" "a!1" "b" "a!1" ))"" (assert ) nil nil )) nil ))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 )"real" reals nil ))nil 3279154594"" (skosimp*)"" (expand "sin" )"" (lemma "floor_plus_int" ("x" "a!1/(2*pi)" "i" "j!1" ))"" (lemma "div_cancel1" ("x" "j!1" "n0z" "2*pi" ))"" "div_distributes" "x" "2*j!1*pi" "y" "a!1" "n0z" "2*pi" ))"" (replace -2)"" (replace -1)"" (replace -3) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"real" reals nil )"real" reals nil )"real" sincos_def nil )nil real_props nil )nil reals nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" reals nil )"int" integers nil )nil real_props nil )"real" reals nil )nil floor_ceil 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 )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 ))nil )nil 3265073926"" (skosimp*)"" (expand "pi" )"" (expand "sin" )"" (lemma "floor_plus_int" ("x" "a!1/(2*pi)" "i" "j!1" ))"" (lemma "div_cancel1" ("x" "j!1" "n0z" "2*pi" ))"" "div_distributes" "x" "2*j!1*pi" "y" "a!1" "n0z" "2*pi" ))"" (replace -2)"" (replace -1)"" (replace -3) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" atan nil )) shostak))nil 3265073058"" (skosimp*)"" (rewrite "cos_sin" )"" (rewrite "cos_sin" )"" (lemma "sin_period" ("a" "pi/2+a!1" "j" "j!1" ))"" (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 )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" reals nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"real" reals nil )"trig_range" sincos_def nil )nil trig_basic nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil ))nil 3308056533"" (skosimp*)"" (expand "Tan?" )"" (lemma "odd_or_even_int" ("x" "j!1" ))"" (split -1)"1" (expand "odd?" )"1" (skosimp*)"1" (replace -1)"1" (lemma "cos_period" ("a" "pi+a!1" "j" "j!2" ))"1" (replace -1 -3 rl)"1" (lemma "neg_cos" ("a" "a!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "even?" )"2" (skosimp*)"2" (replace -1)"2" (lemma "cos_period" ("a" "a!1" "j" "j!2" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"bool" sincos_def 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_basic nil )"real" reals nil )nil trig_basic nil )"real" reals nil )"trig_range" sincos_def nil )"nzreal" nil )"odd_int" integers nil )"real" reals nil )"bool" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"bool" integers nil )nil naturalnumbers 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 )nil integers nil ))nil )nil 3264999491"" (skosimp*)"" (expand "Tan?" )"" (lemma "odd_or_even_int" ("i" "j!1" ))"" (split -1)"1" (expand "odd?" )"1" (skosimp*)"1" (replace -1)"1" (lemma "cos_period" ("a" "pi+a!1" "j" "j!2" ))"1" (replace -1 -3 rl)"1" (lemma "neg_cos" ("a" "a!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "even?" )"2" (skosimp*)"2" (replace -1)"2" (lemma "cos_period" ("a" "a!1" "j" "j!2" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sincos_def nil )"posreal" atan nil ))nil 3308056563"" (skosimp*)"" (expand "tan" )"" (lemma "odd_or_even_int" ("x" "j!1" ))"" (split -1)"1" (expand "odd?" )"1" (skosimp*)"1" (replace -1)"1" (lemma "sin_period" ("a" "a!1+pi" "j" "j!2" ))"1" (lemma "cos_period" ("a" "a!1+pi" "j" "j!2" ))"1" (replace -1 1 rl)"1" (replace -2 1 rl)"1" (lemma "neg_cos" ("a" "a!1" ))"1" (lemma "neg_sin" ("a" "a!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "even?" )"2" (skosimp*)"2" (replace -1)"2" (lemma "sin_period" ("a" "a!1" "j" "j!2" ))"2" (lemma "cos_period" ("a" "a!1" "j" "j!2" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"real" sincos_def nil )"real" reals nil )nil trig_basic 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 )"odd_int" integers nil )"nzreal" nil )nil trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )nil trig_basic nil )"real" reals nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )"bool" integers nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"bool" integers nil )nil naturalnumbers 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 )nil integers nil ))nil )nil 3265072739"" (skosimp*)"" (expand "tan" )"" (lemma "odd_or_even_int" ("i" "j!1" ))"" (split -1)"1" (expand "odd?" )"1" (skosimp*)"1" (replace -1)"1" (lemma "sin_period" ("a" "a!1+pi" "j" "j!2" ))"1" (lemma "cos_period" ("a" "a!1+pi" "j" "j!2" ))"1" (replace -1 1 rl)"1" (replace -2 1 rl)"1" (lemma "neg_cos" ("a" "a!1" ))"1" (lemma "neg_sin" ("a" "a!1" ))"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "even?" )"2" (skosimp*)"2" (replace -1)"2" (lemma "sin_period" ("a" "a!1" "j" "j!2" ))"2" (lemma "cos_period" ("a" "a!1" "j" "j!2" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" sincos_def nil )"posreal" atan nil ))nil 3308056581"" (skosimp*)"" (lemma "odd_or_even_int" ("x" "k!1" ))"" (split -1)"1" (expand "odd?" )"1" (skosimp*)"1" (replace -1)"1" (lemma "sin_period" ("a" "pi" "j" "j!1" ))"1" (rewrite "sin_pi" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "even?" )"2" (skosimp*)"2" (replace -1)"2" (lemma "sin_period" ("a" "0" "j" "j!1" ))"2" (rewrite "sin_0" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil naturalnumbers nil )"bool" integers nil )nil trig_basic nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"bool" integers nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )nil trig_basic nil )"real" reals nil )"odd_int" integers nil )"trig_range" sincos_def nil )"real" reals nil )"nzreal" nil )nil trig_basic nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil ))nil )nil 3265072136"" (skosimp*)"" (lemma "odd_or_even_int" ("i" "k!1" ))"" (split -1)"1" (expand "odd?" )"1" (skosimp*)"1" (replace -1)"1" (lemma "sin_period" ("a" "pi" "j" "j!1" ))"1" (rewrite "sin_pi" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "even?" )"2" (skosimp*)"2" (replace -1)"2" (lemma "sin_period" ("a" "0" "j" "j!1" ))"2" (rewrite "sin_0" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" atan nil )) shostak))nil 3265073272"" (skosimp*)"" (lemma "cos_period" ("a" "0" "j" "k!1" ))"" (rewrite "cos_0" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals 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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )nil trig_basic nil ))nil 3308056609"" (skosimp*)"" (lemma "odd_or_even_int" ("x" "k!1" ))"" (split -1)"1" (lemma "not_even_m1_pow" ("i" "k!1" ))"1" (split -1)"1" (expand "odd?" )"1" (skosimp*)"1" (replace -2)"1" (replace -1)"1" (lemma "cos_period" ("a" "pi" "j" "j!1" ))"1" (rewrite "cos_pi" -1)"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "even_iff_not_odd" ) nil nil ))nil ))nil )"2" (lemma "even_m1_pow" ("i" "k!1" ))"2" (assert )"2" (replace -1)"2" (expand "even?" )"2" (skosimp*)"2" (replace -2)"2" (lemma "cos_period" ("a" "0" "j" "j!1" ))"2" (rewrite "cos_0" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil integers nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil naturalnumbers nil )nil exponentiation nil )nil trig_basic nil )"bool" integers nil )nil exponentiation nil )nil naturalnumbers nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"bool" integers nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )nil trig_basic nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )"nzreal" nil )"nzreal" exponentiation nil )"rat" exponentiation nil )"real" reals nil )"trig_range" sincos_def nil )"odd_int" integers nil )"real" reals nil )nil trig_basic nil )"odd_int" integersnil ))nil )nil 3265073319"" (skosimp*)"" (lemma "odd_or_even_int" ("i" "k!1" ))"" (split -1)"1" (lemma "not_even_m1_pow" ("i" "k!1" ))"1" (split -1)"1" (expand "odd?" )"1" (skosimp*)"1" (replace -2)"1" (replace -1)"1" (lemma "cos_period" ("a" "pi" "j" "j!1" ))"1" (rewrite "cos_pi" -1)"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "even_iff_not_odd" ) nil nil ))nil ))nil )"2" (lemma "even_m1_pow" ("i" "k!1" ))"2" (assert )"2" (replace -1)"2" (expand "even?" )"2" (skosimp*)"2" (replace -2)"2" (lemma "cos_period" ("a" "0" "j" "j!1" ))"2" (rewrite "cos_0" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" atan nil )) shostak))nil 3265073635"" (skosimp*)"" (lemma "cos_k_pi" ("k" "k!1" ))"" (rewrite "cos_sin" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals 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 )"odd_int" integers nil )"nzreal" exponentiation nil )"rat" exponentiation nil )"trig_range" sincos_def nil )"real" reals nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" 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_basic nil )"real" reals nil ))nil 3264999491"" (skosimp*)"" (expand "Tan?" )"" (lemma "cos_k_pi" ("k" "k!1" )) (("" (assert ) nil nil )) nil ))nil ))nil )"bool" sincos_def nil )"odd_int" integers nil )"nzreal" exponentiation nil )"rat" exponentiation nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"real" reals nil )"trig_range" sincos_def 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 -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil ))nil 3265072687"" (skosimp*)"" (expand "tan" )"" (rewrite "sin_k_pi" ) (("" (assert ) nil nil )) nil )) nil ))nil )"real" sincos_def nil )"real" reals nil )"real" reals nil )"trig_range" sincos_def nil )"trig_range" sincos_def nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals 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 ))nil 3279154671"" (skosimp*)"" (split 1)"1" (flatten)"1" (expand "<=" -3)"1" (split -3)"1" (expand "sin" )"1" (case "floor(a!1 / (2 * pi))=0" )"1" (replace -1)"1" (assert )"1" (hide -1)"1" (lemma "sin_value_bij" )"1" (expand "bijective?" )"1" (expand "injective?" )"1" (flatten)"1" "1" "0" "_" )"1" rewrite "sin_value_0" )"1" "cos_value_strict_decreasing" )"1" expand "strict_decreasing?" )"1" "_" "pi/2" )"1" rewrite "cos_value_pi2" )"1" "phases_sin" "x" "a!1" ))"1" "1" rewrite "sin_q1" -5)"1" "a!1" )"1" assert )nil nil )"2" expand "abs" 1)"2" rewrite "phase_sin_q1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "sin_q2" -5)"2" rewrite "phase_sin_q2" )"2" "a!1-pi/2" )"1" assert )"1" "1" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" rewrite "sin_q3" -5)"3" rewrite "phase_sin_q3" )"3" "3" "a!1-pi" )"1" assert )nil nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" rewrite "sin_q4" -5)"4" rewrite "phase_sin_q4" )"4" "a!1-3*pi/2" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2 2 3 4)"2" (lemma "floor_def" ("x" "a!1/(2*pi)" ))"2" (rewrite "div_mult_pos_lt1" -1)"2" (rewrite "div_mult_pos_le2" -1)"2" (flatten)"2" "K1" "floor(a!1 / (2 * pi))" )"2" (lemma "trichotomy" ("x" "K1" ))"2" "1" case "K1=1" )"1" (assert ) nil nil )"2" case "K1>1" )"1" "both_sides_times_pos_lt1" "x" "1" "y" "K1" "pz" "2*pi" ))"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (propax) nil nil )"3" assert )"3" case "K1=-1" )"1" (assert ) nil nil )"2" case "K1<-1" )"1" assert )"1" "both_sides_times_pos_lt1" "x" "K1" "y" "-1" "pz" "2*pi" ))"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil )"2" (flatten)"2" (split -1)"1" (replace -1) (("1" (rewrite "sin_0" ) nil nil )) nil )"2" (replace -1) (("2" (rewrite "sin_pi" ) nil nil )) nil )"3" (replace -1) (("3" (rewrite "sin_2pi" ) nil nil )) nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"bool" reals nil )"posreal" nil )"real" reals nil )"real" sincos_def nil )nil real_props nil )"int" integers nil )nil real_axioms nil )"nzreal" nil )"odd_int" integers nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )nil real_props nil )nil real_props nil )nil floor_ceil nil )"bool" functions nil )"posreal" nil )"nzreal" nil )nil asin nil )"[numfield -> numfield]" number_fields nil )nil sincos_quad nil )nil acos nil )nil real_types nil )nil sincos_phase nil )nil sincos_phase nil )"(total_order?[real])" nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )"real" reals nil )nil sincos_phase nil )nil sincos_phase nil )"[numfield, numfield -> numfield]" number_fields nil )"real" trig_basic nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_quad nil )"bool" real_fun_preds "reals/" )nil sincos_quad nil )"bool" functions nil )"nzreal" real_typesnil )nil sincos_quad nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"nnreal" nil )"(total_order?[real])" nil )"real" reals nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities 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 )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"posreal" atan nil )nil trig_basic nil )nil trig_basic nil )nil trig_basic nil ))nil )nil 3279154637"" (skosimp*)"" (split 1)"1" (flatten)"1" (expand "<=" -3)"1" (split -3)"1" (expand "sin" )"1" (case "floor(a!1 / (2 * pi))=0" )"1" (replace -1)"1" (assert )"1" (hide -1)"1" (lemma "sin_value_bij" )"1" (expand "bijective?" )"1" (expand "injective?" )"1" (flatten)"1" "1" "0" "_" )"1" rewrite "sin_value_0" )"1" "cos_value_strict_decreasing" )"1" expand "strict_decreasing?" )"1" "_" "pi/2" )"1" rewrite "cos_value_pi2" )"1" "phases_sin" "x" "a!1" ))"1" "1" rewrite "sin_q1" -5)"1" "a!1" )"1" assert )nil nil )"2" expand "abs" 1)"2" rewrite "phase_sin_q1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "sin_q2" -5)"2" rewrite "phase_sin_q2" )"2" "a!1-pi/2" )"1" assert )"1" "1" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" rewrite "sin_q3" -5)"3" rewrite "phase_sin_q3" )"3" "3" "a!1-pi" )"1" assert )nil nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" rewrite "sin_q4" -5)"4" rewrite "phase_sin_q4" )"4" "a!1-3*pi/2" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2 2 3 4)"2" (expand "pi" )"2" (lemma "floor_def" ("x" "a!1/(2*pi)" ))"2" (rewrite "div_mult_pos_lt1" -1)"2" (rewrite "div_mult_pos_le2" -1)"2" (flatten)"2" "K1" "floor(a!1 / (2 * pi))" )"2" "trichotomy" ("x" "K1" ))"2" "1" case "K1=1" )"1" assert )"1" (postpone) nil nil ))nil )"2" case "K1>1" )"1" "both_sides_times_pos_lt1" "x" "1" "y" "K1" "pz" "2*pi" ))"1" assert )"1" (postpone) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (postpone) nil nil )"3" assert )"3" case "K1=-1" )"1" (assert ) nil nil )"2" case "K1<-1" )"1" assert )"1" "both_sides_times_pos_lt1" "x" "K1" "y" "-1" "pz" "2*pi" ))"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil )"2" (flatten)"2" (split -1)"1" (replace -1) (("1" (rewrite "sin_0" ) nil nil )) nil )"2" (replace -1) (("2" (rewrite "sin_pi" ) nil nil )) nil )"3" (replace -1) (("3" (rewrite "sin_2pi" ) nil nil )) nil ))nil ))nil ))nil ))nil )nil nil )nil 3265085066"" (skosimp*)"" (split 1)"1" (flatten)"1" (expand "<=" -3)"1" (split -3)"1" (expand "sin" )"1" (case "floor(a!1 / (2 * pi))=0" )"1" (replace -1)"1" (expand "pi" )"1" (assert )"1" (hide -1)"1" (lemma "sin_value_bij" )"1" (expand "bijective?" )"1" (expand "injective?" )"1" "1" "1" "0" "_" )"1" rewrite "sin_value_0" )"1" "cos_value_strict_decreasing" )"1" expand "strict_decreasing?" )"1" "_" "pi/2" )"1" rewrite "cos_value_pi2" )"1" "phases_sin" "x" "a!1" ))"1" "1" rewrite "sin_q1" "1" "a!1" )"1" assert )nil nil )"2" expand "abs" "2" rewrite "phase_sin_q1" )"2" assert )nil nil ))nil ))nil ))nil ))nil )"2" rewrite "sin_q2" "2" rewrite "phase_sin_q2" )"2" "a!1-pi/2" )"1" assert )"1" "1" assert )nil nil ))nil ))nil )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"3" rewrite "sin_q3" "3" rewrite "phase_sin_q3" )"3" "3" "a!1-pi" )"1" assert )nil nil )"2" expand "abs" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" rewrite "sin_q4" "4" rewrite "phase_sin_q4" )"4" "a!1-3*pi/2" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "abs" 1)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -2 2 3 4)"2" (expand "pi" )"2" (lemma "floor_def" ("x" "a!1/(2*pi)" ))"2" (rewrite "div_mult_pos_lt1" -1)"2" (rewrite "div_mult_pos_le2" -1)"2" (flatten)"2" "K1" "floor(a!1 / (2 * pi))" )"2" "trichotomy" ("x" "K1" ))"2" "1" case "K1=1" )"1" (assert ) nil nil )"2" case "K1>1" )"1" "both_sides_times_pos_lt1" "x" "1" "y" "K1" "pz" "2*pi" ))"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (propax) nil nil )"3" assert )"3" case "K1=-1" )"1" (assert ) nil nil )"2" case "K1<-1" )"1" assert )"1" "both_sides_times_pos_lt1" "x" "K1" "y" "-1" "pz" "2*pi" ))"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil )"2" (flatten)"2" (split -1)"1" (replace -1) (("1" (rewrite "sin_0" ) nil nil )) nil )"2" (replace -1) (("2" (rewrite "sin_pi" ) nil nil )) nil )"3" (replace -1) (("3" (rewrite "sin_2pi" ) nil nil )) nil ))nil ))nil ))nil ))nil )nil sincos_quad nil )nil sincos_quad nil )"bool" real_fun_preds "reals/" )nil sincos_quad nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_phase nil )nil acos nil )nil sincos_quad nil )"posreal" atan nil ))nil 3265087288"" (skosimp*)"" (split)"1" (flatten)"1" (case "a!1<=3*pi/2" )"1" (rewrite "cos_sin" )"1" (lemma "sin_eq_0_2pi" ("a" "a!1+pi/2" ))"1" (assert ) nil nil )) nil ))nil )"2" (lemma "cos_period" ("a" "a!1" "j" "-1" ))"2" (replace -2)"2" (hide -2)"2" (rewrite "cos_sin" )"2" "sin_eq_0_2pi" "a" "pi / 2 - 2 * pi + a!1" ))"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (split -1)"1" (replace -1) (("1" (rewrite "cos_pi2" ) nil nil )) nil )"2" (replace -1) (("2" (rewrite "cos_3pi2" ) nil nil )) nil ))nil ))nil ))nil ))nil )"posreal" atan nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields 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 )"posreal" nil )nil trig_basic nil )"[numfield, numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"trig_range" sincos_def nil )"real" reals nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )nil trig_basic nil )"nzint" integersnil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nzreal" nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield -> numfield]" number_fields nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil trig_basic nil )"odd_int" integers nil )nil trig_basic nil )nil trig_basic nil ))nil 3308057228"" (skosimp*)"" (expand "sin" )"" (split)"1" (flatten)"1" (lemma "floor_def" ("x" "a!1 / (2 * pi)" ))"1" (rewrite "div_mult_pos_lt1" -1)"1" (rewrite "div_mult_pos_le2" -1)"1" (flatten -1)"1" "sin_eq_0_2pi" "a" "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)" ))"1" (split -1)"1" (flatten -1)"1" (hide -2)"1" (split -1)"1" (inst + "2 * floor(a!1 / (2 * pi))" )"1" (assert ) nil nil )) nil )"2" "2 * (floor(a!1 / (2 * pi))) +1" )"2" (assert ) nil nil )) nil )"3" "2 * (floor(a!1 / (2 * pi))) +2" )"3" (assert ) nil nil )) nil )"4" (hide 2)"4" expand "sin" )"4" case "(floor((a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)) / ") "1" replace -1)"1" (assert ) nil nil ))nil )"2" "2" "div_cancel1" "x" "floor(a!1 / (2 * pi))" "n0z" "2*pi" ))"2" replace -1)"2" "minus_div2" "x" "a!1" "y" "2 * (floor(a!1 / (2 * pi)) * pi)" "n0x" "2 * pi" ))"2" replace -1 1 rl)"2" replace -2)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (skosimp*)"2" (replace -1)"2" (lemma "div_cancel1" ("x" "i!1/2" "n0z" "pi" ))"2" (replace -1)"2" (lemma "odd_or_even_int" ("x" "i!1" ))"2" (split -1)"1" (expand "odd?" )"1" (skosimp*)"1" (replace -1)"1" (hide -1 -2 -3)"1" "floor_val" "i" "1+2*j!1" "j" "2" "k" "j!1" ))"1" "1" replace -1)"1" assert )"1" "sin_pi" )"1" expand "sin" )"1" "div_cancel1" "x" "1/2" "n0z" "pi" ))"1" replace -1)"1" "floor_val" "i" "1" "j" "2" "k" "0" ))"1" "1" replace -1)"1" assert )nil nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "even?" )"2" (skosimp*)"2" (replace -1)"2" "div_cancel1" "x" "j!1" "n0z" "2" ))"2" replace -1)"2" rewrite "floor_int" )"2" assert )"2" rewrite "sin_phase_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"real" reals nil )"real" sincos_def nil )"nzrat" rationalsnil )"nat" floor_ceil nil )"posreal" nil )"(total_order?[real])" nil )"nonneg_int" nil )"posint" nil )"even_int" integersnil )"posint" nil )"posrat" nil )nil trig_basic nil )nil integers nil )nil floor_ceil nil )"odd_int" integers nil )"bool" integers nil )nil floor_ceil nil )nil sincos_phase nil )"rat" rationals nil )"bool" integers nil )nil naturalnumbers nil )"rat" rationals nil )"int" integers nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"(strict_total_order?[real])" real_props nil )"[T, T -> boolean]" equalities nil )"nnreal" nil )"even_int" integers nil )"nzint" integers nil )nil real_props nil )nil reals nil )nil real_props nil )"even_int" integersnil )"odd_int" integers nil )"nzreal" nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )nil integers nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil trig_basic nil )"real" reals nil )"(total_order?[real])" nil )nil real_props nil )"real" reals nil )nil floor_ceil 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 ))nil )nil 3279154729"" (skosimp*)"" (expand "sin" )"" (split)"1" (flatten)"1" (lemma "floor_def" ("x" "a!1 / (2 * pi)" ))"1" (rewrite "div_mult_pos_lt1" -1)"1" (rewrite "div_mult_pos_le2" -1)"1" (flatten -1)"1" "sin_eq_0_2pi" "a" "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)" ))"1" (split -1)"1" (flatten -1)"1" (hide -2)"1" (split -1)"1" (inst + "2 * floor(a!1 / (2 * pi))" )"1" (assert ) nil nil )) nil )"2" "2 * (floor(a!1 / (2 * pi))) +1" )"2" (assert ) nil nil )) nil )"3" "2 * (floor(a!1 / (2 * pi))) +2" )"3" (assert ) nil nil )) nil )"4" (hide 2)"4" expand "sin" )"4" case "(floor((a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)) / ") "1" replace -1)"1" (assert ) nil nil ))nil )"2" "2" "div_cancel1" "x" "floor(a!1 / (2 * pi))" "n0z" "2*pi" ))"2" replace -1)"2" "minus_div2" "x" "a!1" "y" "2 * (floor(a!1 / (2 * pi)) * pi)" "n0x" "2 * pi" ))"2" replace -1 1 rl)"2" replace -2)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ) ("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (skosimp*)"2" (replace -1)"2" (lemma "div_cancel1" ("x" "i!1/2" "n0z" "pi" ))"2" (replace -1)"2" (lemma "odd_or_even_int" ("i" "i!1" ))"2" (split -1)"1" (expand "odd?" )"1" (skosimp*)"1" (replace -1)"1" (hide -1 -2 -3)"1" "floor_val" "i" "1+2*j!1" "j" "2" "k" "j!1" ))"1" "1" replace -1)"1" assert )"1" "sin_pi" )"1" expand "sin" )"1" "div_cancel1" "x" "1/2" "n0z" "pi" ))"1" replace -1)"1" "floor_val" "i" "1" "j" "2" "k" "0" ))"1" "1" replace -1)"1" assert )nil nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "even?" )"2" (skosimp*)"2" (replace -1)"2" "div_cancel1" "x" "j!1" "n0z" "2" ))"2" replace -1)"2" rewrite "floor_int" )"2" assert )"2" rewrite "sin_phase_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" sincos_def nil )nil sincos_phase nil )"posreal" atan nil ))nil )nil 3265087685"" (skosimp*)"" (expand "sin" )"" (split)"1" (flatten)"1" (lemma "floor_def" ("x" "a!1 / (2 * pi)" ))"1" (rewrite "div_mult_pos_lt1" -1)"1" (rewrite "div_mult_pos_le2" -1)"1" (flatten -1)"1" "sin_eq_0_2pi" "a" "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)" ))"1" (split -1)"1" (flatten -1)"1" (hide -2)"1" (split -1)"1" (expand "pi" )"1" "2 * floor(a!1 / (2 * pi))" )"1" (assert ) nil nil ))nil ))nil )"2" (expand "pi" )"2" "2 * (floor(a!1 / (2 * pi))) +1" )"2" (assert ) nil nil ))nil ))nil )"3" (expand "pi" )"3" "2 * (floor(a!1 / (2 * pi))) +2" )"3" (assert ) nil nil ))nil ))nil )"4" (hide 2)"4" expand "sin" )"4" case "(floor((a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)) / ") "1" replace -1)"1" (assert ) nil nil ))nil )"2" "2" "div_cancel1" "x" "floor(a!1 / (2 * pi))" "n0z" "2*pi" ))"2" replace -1)"2" "minus_div2" "x" "a!1" "y" "2 * (floor(a!1 / (2 * pi)) * pi)" "n0x" "2 * pi" ))"2" replace -1 1 rl)"2" replace -2)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert )"3" (expand "pi" ) (("3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (skosimp*)"2" (replace -1)"2" (expand "pi" )"2" (lemma "div_cancel1" ("x" "i!1/2" "n0z" "pi" ))"2" (replace -1)"2" (lemma "odd_or_even_int" ("i" "i!1" ))"2" (split -1)"1" (expand "odd?" )"1" (skosimp*)"1" (replace -1)"1" "1" "floor_val" "i" "1+2*j!1" "j" "2" "k" "j!1" ))"1" "1" replace -1)"1" assert )"1" "sin_pi" )"1" expand "pi" )"1" expand "sin" )"1" "div_cancel1" "x" "1/2" "n0z" "pi" ))"1" replace -1)"1" "floor_val" "i" "1" "j" "2" "k" "0" ))"1" "1" replace -1)"1" assert )nil nil ))nil )"2" assert )nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "even?" )"2" (skosimp*)"2" (replace -1)"2" "div_cancel1" "x" "j!1" "n0z" "2" ))"2" replace -1)"2" rewrite "floor_int" )"2" assert )"2" rewrite "sin_phase_0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil sincos_phase nil )"posreal" atan nil ))nil 3265087979"" (skosimp*)"" (lemma "cos_sin" ("a" "a!1" ))"" (lemma "sin_eq_0" ("a" "a!1+pi/2" ))"" (replace -2 -1 rl)"" (hide -2)"" (split)"1" (flatten)"1" (assert )"1" (skosimp*)"1" (inst + "i!1-1" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (skosimp*)"2" (replace -1)"2" (split -3)"1" (propax) nil nil )"2" (inst + "i!1+1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))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 )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"real" reals nil )"trig_range" sincos_def nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"real" reals nil )"int" integers nil )"real" reals nil )nil trig_basic nil )nil number_fields nil )"[numfield, numfield -> numfield]" 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 ))nil 3279154781"" (skosimp*)"" (split)"1" (flatten)"1" (expand "sin" )"1" (lemma "floor_def" ("x" "a!1/(2*pi)" ))"1" (rewrite "div_mult_pos_lt1" )"1" (rewrite "div_mult_pos_le2" )"1" (flatten)"1" (inst + "floor(a!1/(2*pi))" )"1" (lemma "phases_sin" )"1" "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)" )"1" (lemma "cos_value_bij" )"1" (expand "bijective?" )"1" (expand "injective?" )"1" "1" "1" "sin_value_strict_increasing" )"1" expand "strict_increasing?" )"1" "1" rewrite "sin_q1" -6)"1" rewrite "phase_sin_q1" -1)"1" "1" "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)" "pi/2" )"1" assert )"1" rewrite "sin_value_pi2" )"1" assert )nil nil ))nil ))nil )"2" expand "abs" 1)"2" assert )nil nil ))nil )"3" expand "abs" 1)"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "sin_q2" -6)"2" rewrite "phase_sin_q2" -1)"2" "2" "-1 * (pi / 2) - 2 * (floor(a!1 / (2 * pi)) * pi) + a!1" "0" )"1" rewrite "cos_value_0" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" rewrite "sin_q3" -6)"3" rewrite "phase_sin_q3" -1)"3" "3" "-pi/2" "-1 * pi - 2 * (floor(a!1 / (2 * pi)) * pi) + a!1" )"1" assert )"1" rewrite "sin_value_minus_pi2" )"1" assert )nil nil ))nil ))nil )"2" expand "abs" 1)"2" assert )nil nil ))nil )"3" expand "abs" 1)"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" rewrite "sin_q4" -6)"4" rewrite "phase_sin_q4" -1)"4" "4" "pi" "-1 * (3 * pi / 2) - 2 * (floor(a!1 / (2 * pi)) * pi) + ") "1" rewrite "cos_value_pi" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (skosimp*)"2" (replace -1)"2" (hide -1)"2" (lemma "sin_period" ("a" "pi/2" "j" "i!1" ))"2" (rewrite "sin_pi2" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"real" reals nil )"real" sincos_def nil )"int" integers nil )nil real_props nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (< const-decl "bool" reals nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"(strict_total_order?[real])" real_props nil )nil sincos_phase nil )nil sincos_quad nil )"bool" functions nil )"nzreal" real_typesnil )"bool" real_fun_preds "reals/" )nil sincos_phase nil )nil sincos_quad nil )nil sincos_phase nil )nil sincos_phase nil )"real" reals nil )nil sincos_quad nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_quad nil )"odd_int" integers nil )nil acos nil )"nzreal" nil )nil sincos_phase nil )nil sincos_phase nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"posreal" nil )nil sincos_quad nil )"[numfield -> numfield]" number_fields nil )nil asin nil )"nzreal" nil )"real" reals nil )nil sincos_phase nil )nil sincos_quad nil )"bool" functions nil )nil real_types nil )nil sincos_phase nil )"real" trig_basic nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )"(total_order?[real])" nil )nil integers nil )"(total_order?[real])" nil )nil real_props nil )"real" reals nil )nil floor_ceil 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 )nil trig_basic nil )"trig_range" sincos_def nil )nil trig_basic nil ))nil )nil 3265137440"" (skosimp*)"" (split)"1" (flatten)"1" (expand "sin" )"1" (lemma "floor_def" ("x" "a!1/(2*pi)" ))"1" (rewrite "div_mult_pos_lt1" )"1" (rewrite "div_mult_pos_le2" )"1" (flatten)"1" (expand "pi" )"1" (inst + "floor(a!1/(2*pi))" )"1" (lemma "phases_sin" )"1" "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)" )"1" (lemma "cos_value_bij" )"1" (expand "bijective?" )"1" expand "injective?" )"1" "1" "1" "sin_value_strict_increasing" )"1" expand "strict_increasing?" )"1" "1" rewrite "sin_q1" -6)"1" rewrite "phase_sin_q1" "1" "1" "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)" "pi/2" )"1" assert )"1" rewrite "sin_value_pi2" )"1" assert )nil nil ))nil ))nil )"2" expand "abs" 1)"2" assert )nil nil ))nil )"3" expand "abs" 1)"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "sin_q2" -6)"2" rewrite "phase_sin_q2" "2" "2" "-1 * (pi / 2) - 2 * (floor(a!1 / (2 * pi)) * pi) + a!1" "0" )"1" rewrite "cos_value_0" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil )"3" rewrite "sin_q3" -6)"3" rewrite "phase_sin_q3" "3" "3" "-pi/2" "-1 * pi - 2 * (floor(a!1 / (2 * pi)) * pi) + a!1" )"1" assert )"1" rewrite "sin_value_minus_pi2" )"1" assert )nil nil ))nil ))nil )"2" expand "abs" 1)"2" assert )nil nil ))nil )"3" expand "abs" 1)"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"4" rewrite "sin_q4" -6)"4" rewrite "phase_sin_q4" "4" "4" "pi" "-1 * (3 * pi / 2) - 2 * (floor(a!1 / (2 * pi)) * pi) + ") "1" rewrite "cos_value_pi" )"1" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (skosimp*)"2" (replace -1)"2" (hide -1)"2" (lemma "sin_period" ("a" "pi/2" "j" "i!1" ))"2" (rewrite "sin_pi2" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" atan nil )nil sincos_phase nil )nil sincos_quad nil )"bool" real_fun_preds "reals/" )nil sincos_phase nil )nil sincos_quad nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_quad nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_quad nil )nil acos nil )nil sincos_phase nil )nil sincos_phase nil )nil sincos_quad nil )nil sincos_phase nil )nil sincos_quad nil )nil sincos_phase nil ))nil 3265137585"" (skosimp*)"" (rewrite "cos_sin" )"" (lemma "sin_eq_1" ("a" "a!1+pi/2" ))"" (split 1)"1" (flatten) (("1" (assert ) nil nil )) nil )"2" (flatten)"2" (hide -2)"2" (skosimp*)"2" (split -2)"1" (assert ) nil nil )"2" (inst + "i!1" ) (("2" (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 )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"{r: posreal | pi_lb < r AND r < pi_ub}" nil )"posreal" nil )"real" reals nil )"trig_range" sincos_def nil )"real" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil trig_basic nil )nil number_fields nil )"[numfield, numfield -> numfield]" 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 ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.375 Sekunden
(vorverarbeitet am 2026-04-26)
¤ *© Formatika GbR, Deutschland
2026-05-26
