Impressum trig_basic.prf
Sprache: Lisp
(trig_basicnil 3279386567"" (inst + "(pi_lb+pi_ub)/2" )"" (assert )"" (case "(pi_lb + pi_ub) / 2 > 0 " )"1" (assert )"1" (prop)"1" (cross-mult 1)"1" (assert ) (("1" (grind) nil nil )) nil )) nil )"2" (cross-mult 1) (("2" (grind) nil nil )) nil ))nil ))nil )"2" (hide 2)"2" (cross-mult 1) (("2" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"nonneg_int" nil )nil real_props nil )nil extra_real_props nil )"posreal" nil )"posrat" nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posreal" nil )"(strict_total_order?[real])" real_props nil )"posreal" nil )"(strict_total_order?[real])" real_props nil ))nil 3294394361 ("" (assert ) nil nil )"(strict_total_order?[real])" real_props nil )"posreal" nil ))nil 3264999679"" (skosimp*)"" (expand "sin" )"" (lemma "floor_def" ("x" "a!1 / (2 * pi)" ))"" (flatten)"" (rewrite "div_mult_pos_le2" -1)"" (rewrite "div_mult_pos_lt1" -2)"" "sin_phase(a!1 - 2 * (floor(a!1 / (2 * pi)) * pi))" )"1" (expand "abs" )"1" case "sin_phase(a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)) < 0" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3265001911"" (skosimp*)"" (expand "cos" )"" (lemma "floor_def" ("x" "a!1 / (2 * pi)" ))"" (rewrite "div_mult_pos_le2" -1)"" (rewrite "div_mult_pos_lt1" -1)"" (flatten)"" "cos_phase(a!1 - 2 * (floor(a!1 / (2 * pi)) * pi))" )"1" (expand "abs" )"1" case "cos_phase(a!1 - 2 * (floor(a!1 / (2 * pi)) * pi))<0" )"1" (assert ) nil nil ) ("2" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3264999490"" (skosimp*) (("" (rewrite "sin_range_ax" ) 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 3264999490"" (skosimp*) (("" (rewrite "cos_range_ax" ) 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 3264999490"" (skosimp*)"" (typepred "a!1" )"" (expand "Tan?" ) (("" (assert ) nil nil )) nil )) nil ))nil )"bool" trig_basic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"trig_range" trig_basic nil ))nil 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 )nil shostak))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" trig_basic nil )"trig_range" trig_basic 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" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil ))nil 3265002205"" (expand "cos" )"" (rewrite "floor_int" ) (("" (rewrite "cos_phase_0" ) nil nil ))nil ))nil )nil shostak))nil 3279387338"" (lemma "sin2_cos2" )"" (inst?)"" (rewrite "cos_0" )"" (expand "sq" )"" (rewrite "zero_times3" ) (("" (ground) nil nil )) nil ))nil ))nil ))nil ))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" trig_basic nil )"nonneg_real" sq "reals/" )nil real_props nil )"real" trig_basic nil )nil trig_basic nil )nil trig_basic nil ))nil )nil 3265002237"" (expand "sin" )"" (rewrite "floor_int" ) (("" (rewrite "sin_phase_0" ) nil nil ))nil ))nil )nil shostak))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 shostak))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 )nil sq "reals/" )"real" trig_basic nil )"posreal" nil )"trig_range" trig_basic 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 )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil ))nil 3264999490"" (expand "Tan?" )"" (rewrite "cos_0" ) (("" (assert ) nil nil )) nil )) nil )nil trig_basic nil )"bool" trig_basic nil ))nil 3265002274"" (expand "tan" )"" (rewrite "sin_0" )"" (rewrite "cos_0" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil trig_basic nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )nil trig_basic nil )"real" trig_basic 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 )nil shostak))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 )nil shostak))nil 3264999490"" (skosimp*)"" (typepred "a!1" )"" (expand "Tan?" )"" (lemma "cos_neg" ("a" "a!1" )) (("" (assert ) nil nil ))nil ))nil ))nil ))nil )"bool" trig_basic 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" trig_basic 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" trig_basic 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" trig_basic nil )nil trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"real" reals nil )"trig_range" trig_basic 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 )nil shostak))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 )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )"[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" trig_basic nil )"trig_range" trig_basic nil )"posreal" 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 )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil )"real" reals nil )"posreal" nil )"trig_range" trig_basic nil )nil trig_basic nil ))nil 3265010327"" (skosimp*)"" (lemma "sin_shift" ("a" "pi/2-a!1" )) (("" (assert ) nil nil ))nil ))nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )"posreal" nil )"trig_range" trig_basic 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" trig_basic nil )"posreal" nil )"real" reals nil )"trig_range" trig_basic nil )"posreal" nil )"real" reals nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, 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" trig_basic nil )"posreal" nil )"real" reals nil )"trig_range" trig_basic nil )"real" reals nil )"posreal" nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil trig_basic nil ))nil 3279387666"" (case "pi=pi/2 + pi/2" )"1" (replace -1 :hide? t)"1" (lemma "sin_minus" )"1" (inst -1 "pi/2" "-pi/2" )"1" (case "pi / 2 - -pi / 2 = pi / 2 + pi / 2" )"1" (replace -1 :hide? t)"1" (replace -1 :hide? t)"1" (case "(pi / 2 + pi / 2) / 2 = pi/2" )"1" (replace -1 :hide? t)"1" (case "-(pi / 2 + pi / 2)/2 = -(pi/2)" )"1" (replace -1 :hide? t)"1" (rewrite "sin_neg" )"1" (rewrite "cos_neg" )"1" (rewrite "sin_pi2" )"1" rewrite "cos_pi2" )"1" (ground) nil )))))))))))"2" (ground) nil )))))"2" (ground) nil )))))))"2" (ground) nil )))))))))"2" (ground) nil ))nil )nil 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 )nil shostak))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 )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 shostak))nil 3264999490"" (expand "Tan?" )"" (rewrite "cos_pi" ) (("" (assert ) nil nil )) nil )) nil )nil trig_basic nil )"odd_int" integers nil )"bool" trig_basic nil ))nil 3265006469"" (expand "tan" )"" (rewrite "sin_pi" )"" (rewrite "cos_pi" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil trig_basic nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"rat" rationals nil )"odd_int" integers nil )nil trig_basic nil )"real" trig_basic nil ))nil 3265010743"" (lemma "neg_sin" ("a" "pi/2" ))"" (rewrite "sin_pi2" ) (("" (assert ) nil nil )) nil )) nil )nil trig_basic nil )"trig_range" trig_basic 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 )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil ))nil 3265010800"" (lemma "neg_cos" ("a" "pi/2" ))"" (rewrite "cos_pi2" ) (("" (assert ) nil nil )) nil )) nil )nil trig_basic nil )"trig_range" trig_basic 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 )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil ))nil 3279154535"" (expand "sin" )"" (rewrite "div_simp" )"" (rewrite "floor_int" )"" (assert ) (("" (rewrite "sin_phase_0" ) nil nil )) nil ))nil ))nil ))nil )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 shostak))nil 3279154560"" (expand "cos" )"" (rewrite "div_simp" )"" (rewrite "floor_int" )"" (assert ) (("" (rewrite "cos_phase_0" ) nil nil )) nil ))nil ))nil ))nil )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 shostak))nil 3264999491"" (expand "Tan?" )"" (rewrite "cos_2pi" ) (("" (assert ) nil nil )) nil )) nil )nil trig_basic nil )"bool" trig_basic nil ))nil 3265006491"" (expand "tan" )"" (rewrite "sin_2pi" )"" (rewrite "cos_2pi" ) (("" (assert ) nil nil )) nil )) nil ))nil )nil trig_basic nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )nil trig_basic nil )"real" trig_basic 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 )nil shostak))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" trig_basic nil )"real" reals nil )"trig_range" trig_basic 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" trig_basic nil )"real" reals nil )"posreal" nil )"trig_range" trig_basic 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 )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil ))nil 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" trig_basic nil )"real" reals nil )"trig_range" trig_basic nil )nil trig_basic nil ))nil 3419263512"" (skosimp*)"" (rewrite "sin_minus" )"" (rewrite "sin_pi" )"" (rewrite "cos_pi" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )"odd_int" integers nil )nil trig_basic nil ))nil ))nil 3419263645"" (skosimp*)"" (rewrite "cos_minus" )"" (rewrite "cos_pi" )"" (rewrite "sin_pi" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil )nil trig_basic nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )nil trig_basic nil )"real" reals nil )"odd_int" integers nil )nil trig_basic nil ))nil 3264999490"" (skosimp*)"" (expand "tan" )"" (expand "Tan?" ) (("" (assert ) nil nil )) nil )) nil ))nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )"real" trig_basic nil )"real" reals nil )"real" reals nil )"bool" trig_basic 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" trig_basic 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" trig_basic nil )"real" trig_basic nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil trig_basic nil )"real" trig_basic nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil ))nil 3264999490"" (skosimp*) (("" (expand "tan" ) (("" (assert ) nil nil )) nil ))nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" trig_basic 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" trig_basic nil )nil trig_basic nil )"real" reals nil )"real" reals nil )"real" reals nil )nil trig_basic nil )nil booleans nil )"bool" trig_basic 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" nil nil ))nil )"3" expand "abs" )"3" 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" nil nil ))nil )"3" expand "abs" )"3" 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 sq "reals/" )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" )nil sq "reals/" )"{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/" )nil sqrt "reals/" )nil sq "reals/" )nil sq "reals/" )"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" trig_basic nil )"trig_range" trig_basic 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" trig_basic nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic 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" trig_basic nil )"real" reals nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic 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" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )"real" trig_basic nil )"nonneg_real" sq "reals/" )"real" reals nil )nil trig_basic nil )"odd_int" integers nil )nil sq "reals/" )"real" trig_basic 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" trig_basic nil )"trig_range" trig_basic nil )nil trig_basic nil ))nil 3264999490"" (skosimp*) (("" (expand "tan" ) (("" (assert ) nil nil )) nil ))nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" reals nil )"real" reals nil )"real" trig_basic 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 3279387961"" "FORALL (a: real, j: nat): sin(a) = sin(a + 2 * j * pi)" )"1" (skosimp*)"1" (case-replace "j!1 >= 0" )"1" (inst?) nil nil )"2" "sin(a!1 + 2 * j!1 * pi) = - sin(-a!1 + 2 * (-j!1) * pi)" )"1" (hide -1)"1" (inst -1 "-a!1" "-j!1" )"1" (assert )"1" (replace -1 * rl)"1" (hide -1)"1" (rewrite "sin_neg" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (hide -1 3)"2" (lemma "sin_neg" )"2" (inst - "-(a!1 + 2 * j!1 * pi)" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (induct "j" 1)"1" (assert ) nil nil )"2" (skosimp*)"2" "a!1 + (2 * (j!1 + 1)) * pi = a!1 + 2*pi + 2 * j!1 * pi" )"1" (hide -1)"1" (inst -1 "a!1+2*pi" )"1" (replace -1 * rl)"1" (hide -1)"1" (rewrite "sin_plus" )"1" (rewrite "sin_2pi" )"1" (rewrite "cos_2pi" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -1 2) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil trig_basic nil )"trig_range" trig_basic nil )nil trig_basic nil )nil trig_basic nil )"posint" nil )"posint" nil )"posreal" nil )nil naturalnumbers nil )nil defined_types nil )"[numfield -> numfield]" number_fields nil )"real" reals nil )"nnreal" nil )"nonneg_int" nil )"real" reals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )"int" integers nil )nil trig_basic nil )"integer" trig_basic nil )"(total_order?[real])" nil )nil integers nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"real" trig_basic nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals 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 )nil booleans nil )nil numbers nil )"real" reals nil )"trig_range" trig_basic nil ))nil )nil 3279387942"" "FORALL (a: real, j: nat): sin(a) = sin(a + 2 * j * PI)" )"1" (skosimp*)"1" (case-replace "j!1 >= 0" )"1" (inst?) nil )"2" "sin(a!1 + 2 * j!1 * PI) = - sin(-a!1 + 2 * (-j!1) * PI)" )"1" (hide -1)"1" (inst -1 "-a!1" "-j!1" )"1" (assert )"1" (replace -1 * rl)"1" (hide -1)"1" (rewrite "sin_neg" )"1" (assert ) nil )))))))))"2" (assert ) nil )))))"2" (hide -1 3)"2" (lemma "sin_neg" )"2" (inst - "-(a!1 + 2 * j!1 * PI)" )"2" (assert ) nil )))))))))))))"2" (hide 2)"2" (induct "j" 1)"1" (assert ) nil )"2" (skosimp*)"2" "a!1 + (2 * (j!1 + 1)) * PI = a!1 + 2*PI + 2 * j!1 * PI" )"1" (hide -1)"1" (inst -1 "a!1+2*PI" )"1" (replace -1 * rl)"1" (hide -1)"1" (rewrite "sin_plus" )"1" (rewrite "sin_2PI" )"1" (rewrite "cos_2PI" )"1" (assert ) nil )))))))))))))))"2" (hide -1 2) (("2" (assert ) nil ))))))))))))nil )nil 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 )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 )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 )"posreal" nil )"real" reals nil )"trig_range" trig_basic nil )nil trig_basic nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil 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 3279471831"" (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 )"bool" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[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" trig_basic 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 3279471795"" (skosimp*)"" (expand "Tan?" )"" (lemma "cos_period" )"" (inst?)"" (case "even?(j!1)" )"1" (inst - "j!1/2" )"1" (assert ) nil )"2" (expand "even?" )"2" (skosimp*) (("2" (assert ) nil )))))))"2" (case "even?(j!1-1)" )"1" (inst - "(j!1-1)/2" )"1" (assert )"1" "2 * ((j!1-1) / 2 * pi) + a!1 = a!1 + (j!1-1)*pi" )"1" (hide -1)"1" (assert )"1" (lemma "cos_minus" )"1" (inst -1 "pi*j!1+a!1" "pi" )"1" (rewrite "cos_pi" )"1" rewrite "sin_pi" )"1" (assert ) nil )))))))))))))"2" (assert ) nil )))))"2" (expand "even?" )"2" (skosimp*) (("2" (assert ) nil )))))))"2" (rewrite "even_plus" ) nil ))))))))))))nil )nil nil )nil 3279471776"" (skosimp*)"" (expand "Tan?" )"" (lemma "cos_period" )"" (inst?)"" (case "even?(j!1)" )"1" (inst - "j!1/2" )"1" (assert ) nil )"2" (expand "even?" )"2" (skosimp*) (("2" (assert ) nil )))))))"2" (case "even?(j!1-1)" )"1" (inst - "(j!1-1)/2" )"1" (assert )"1" "2 * ((j!1-1) / 2 * PI) + a!1 = a!1 + (j!1-1)*PI" )"1" (hide -1)"1" (assert )"1" (lemma "cos_minus" )"1" (inst -1 "PI*j!1+a!1" "PI" )"1" (rewrite "cos_PI" )"1" rewrite "sin_PI" )"1" (assert ) nil )))))))))))))"2" (assert ) nil )))))"2" (expand "even?" )"2" (skosimp*) (("2" (assert ) nil )))))))"2" (rewrite "even_plus" ) nil ))))))))))))nil )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 )nil shostak))nil 3308047949"" (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 )"real" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil trig_basic nil )"real" reals 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" trig_basic nil )"trig_range" trig_basic 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 )nil shostak))nil 3308047988"" (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 )nil trig_basic nil )"real" reals nil )"odd_int" integers nil )"trig_range" trig_basic 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 )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil ))nil )nil 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 )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" trig_basic nil )"real" reals nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"even_int" integersnil )nil trig_basic nil ))nil 3265073319"" (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 | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil trig_basic nil )"nzreal" nil )"nzreal" exponentiation nil )"rat" exponentiation nil )"real" reals nil )"trig_range" trig_basic nil )"odd_int" integers nil )"real" reals nil )nil trig_basic nil )"odd_int" integersnil ))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" trig_basic nil )"real" reals nil )"posreal" nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil trig_basic nil )"real" reals nil ))nil 3264999491"" (skosimp*)"" (expand "Tan?" )"" (lemma "cos_k_pi" ("k" "k!1" )) (("" (assert ) nil nil )) nil ))nil ))nil )"bool" trig_basic nil )"odd_int" integers nil )"nzreal" exponentiation nil )"rat" exponentiation nil )"real" reals nil )"trig_range" trig_basic 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" trig_basic nil )"real" reals nil )"real" reals nil )"trig_range" trig_basic nil )"trig_range" trig_basic 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 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 )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 shostak))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 )"posreal" nil )"real" reals nil )"trig_range" trig_basic 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 )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil ))nil 3279388306"" (skosimp*)"" (lemma "sin_eq_0" )"" (inst?)"" (ground)"1" (skosimp*)"1" (case "i!1 >= 0" )"1" (hide -2)"1" (replace -3 -)"1" (lemma "both_sides_times_pos_le1" )"1" (inst?)"1" (assert )"1" (hide -3 -5 -6)"1" "i!1 = 0 OR i!1 = 1 OR i!1 = 2" )"1" (ground) nil )"2" (flatten)"2" (assert ) nil )))))))))))))))))"2" (hide -1 -2 -5 3 4)"2" (lemma "pos_times_ge" )"2" (inst?) (("2" (assert ) nil )))))))))))"2" (lemma "sin_0" ) (("2" (assert ) nil )))"3" (lemma "sin_pi" ) (("3" (assert ) nil )))"4" (lemma "sin_2pi" ) (("4" (assert ) nil ))))))))))nil )nil trig_basic nil )"posreal" nil )"trig_range" trig_basic nil )"(total_order?[real])" nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"(total_order?[real])" nil )"real" reals nil )nil real_props nil )nil real_props nil )nil trig_basic nil )nil trig_basic nil )nil trig_basic nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil )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 )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 shostak))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 )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[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" trig_basic nil )"real" reals 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 3474885556"" (skeep)"" (lemma "sin_eq_0" )"" (inst?)"" (expand "tan" )"" (prop)"1" (skosimp*) (("1" (assert ) nil nil )) nil )"2" (cross-mult -1) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil trig_basic nil )"trig_range" trig_basic nil )"trig_range" trig_basic nil )"real" trig_basic nil )nil real_props nil )"boolean" notequal nil )nil reals nil )"real" trig_basic nil )"real" trig_basic nil )"real" reals nil )"real" reals nil )"bool" trig_basic nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3279388043"" (skosimp*)"" (prop)"1" (case-replace "cos(a!1) = 0" )"1" (lemma "cos_eq_0" )"1" (inst?)"1" (assert )"1" (skosimp*)"1" (case "even?(i!1)" )"1" (expand "even?" )"1" (skosimp*)"1" (replace -1)"1" (inst + "j!1" ) (("1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (lemma "sin_3pi2" )"2" (lemma "sin_period" )"2" (inst?)"2" (inst -1 "(i!1-1)/2" )"1" (assert ) nil nil )"2" (hide -1 -2 -3 -4)"2" "even?(i!1-1)" )"1" expand "even?" )"1" "1" (assert ) nil nil ))nil ))nil )"2" "2" "odd_iff_even_succ" )"2" "i!1-1" )"2" assert )"2" "2" "odd_or_even_int" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case-replace "sq(sin(a!1)) = 1" )"1" (hide -2)"1" (rewrite "sin2" )"1" (expand "sq" )"1" (assert )"1" (lemma "zero_times3" )"1" (inst -1 "cos(a!1)" "cos(a!1)" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "sq" ) (("2" (assert ) nil nil )) nil ))nil ))nil )"2" (skosimp*)"2" (replace -1)"2" (hide -1)"2" (rewrite "sin_plus" )"2" (rewrite "sin_pi2" )"2" (rewrite "cos_pi2" )"2" (assert )"2" (lemma "cos_2k_pi" )"2" (inst -1 "i!1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" trig_basic nil )"nonneg_real" sq "reals/" )nil trig_basic nil )"real" reals nil )nil real_props nil )nil trig_basic nil )"trig_range" trig_basic nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" integers nil )"real" reals nil )nil trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )nil naturalnumbers nil )"int" integers nil )nil naturalnumbers nil )"odd_int" integers nil )"rat" rationals nil )"posreal" nil )nil integers nil )"int" trig_basic nil )"[numfield, numfield -> numfield]" number_fields nil )"rat" rationals nil )"int" integers nil )nil trig_basic nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"real" reals nil )"posreal" nil )"real" trig_basic 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 )"trig_range" trig_basic nil )nil trig_basic nil )nil trig_basic nil )nil trig_basic nil )nil trig_basic nil ))nil )nil 3279388017"" (skosimp*)"" (prop)"1" (case-replace "cos(a!1) = 0" )"1" (lemma "cos_eq_0" )"1" (inst?)"1" (assert )"1" (skosimp*)"1" (case "even?(i!1)" )"1" (expand "even?" )"1" (skosimp*)"1" (replace -1)"1" (inst + "j!1" )"1" (assert ) nil )))))))))"2" (hide 2)"2" (lemma "sin_3PI2" )"2" (lemma "sin_period" )"2" (inst?)"2" (inst -1 "(i!1-1)/2" )"1" (assert ) nil )"2" (hide -1 -2 -3 -4)"2" "even?(i!1-1)" )"1" expand "even?" )"1" "1" (assert ) nil )))))"2" "2" rewrite "even_plus" )nil )))))))))))))))))))))))))))"2" (case-replace "sq(sin(a!1)) = 1" )"1" (hide -2)"1" (rewrite "sin2" )"1" (expand "sq" )"1" (assert )"1" (lemma "zero_times3" )"1" (inst -1 "cos(a!1)" "cos(a!1)" )"1" (assert ) nil )))))))))))))"2" (expand "sq" ) (("2" (assert ) nil )))))))"2" (skosimp*)"2" (replace -1)"2" (hide -1)"2" (rewrite "sin_plus" )"2" (rewrite "sin_PI2" )"2" (rewrite "cos_PI2" )"2" (assert )"2" (lemma "cos_2k_PI" )"2" (inst -1 "i!1" )"2" (assert ) nil ))))))))))))))))))))))nil )nil 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 )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 )nil shostak))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 )"posreal" nil )"real" reals nil )"trig_range" trig_basic 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 )AND const-decl "[bool, bool -> bool]" booleans nil )"posreal" trig_basic nil )"bool" reals nil )"posreal" trig_basic nil )"{r: posreal | r > pi_lb AND r < pi_ub}" trig_basicnil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.0.323Bemerkung:
(vorverarbeitet am 2026-04-26)
¤ *Bot Zugriff
2026-05-26
