| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 279 kB |
|
Quelle trig_basic.prfSprache: Lisp |
|||||||||||||||
|
(trig_basic (pi_TCC1 0 (pi_TCC1-1 nil 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) ((mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (trig_phase_TCC1 0 (trig_phase_TCC1-1 nil 3294394361 ("" (assert) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (sin_range_ax 0 (sin_range_ax-1 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) (("" (typepred "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)) (cos_range_ax 0 (cos_range_ax-1 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) (("" (typepred "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)) (sin_range 0 (sin_range-1 nil 3264999490 ("" (skosimp*) (("" (rewrite "sin_range_ax") nil nil)) nil) ((sin_range_ax formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil)) shostak)) (cos_range 0 (cos_range-1 nil 3264999490 ("" (skosimp*) (("" (rewrite "cos_range_ax") nil nil)) nil) ((cos_range_ax formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil)) shostak)) (tan_TCC1 0 (tan_TCC1-1 nil 3264999490 ("" (skosimp*) (("" (typepred "a!1") (("" (expand "Tan?") (("" (assert) nil nil)) nil)) nil)) nil) ((Tan? const-decl "bool" trig_basic nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (cos_range application-judgement "trig_range" trig_basic nil)) shostak)) (sin2_cos2 0 (sin2_cos2-1 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) (("" (lemma "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)) (cos2 0 (cos2-1 nil 3265002167 ("" (skosimp*) (("" (lemma "sin2_cos2" ("a" "a!1")) (("" (assert) nil nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin2_cos2 formula-decl nil trig_basic nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (sin2 0 (sin2-1 nil 3265002192 ("" (skosimp*) (("" (lemma "sin2_cos2" ("a" "a!1")) (("" (assert) nil nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin2_cos2 formula-decl nil trig_basic nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (cos_0 0 (cos_0-1 nil 3265002205 ("" (expand "cos") (("" (rewrite "floor_int") (("" (rewrite "cos_phase_0") nil nil)) nil)) nil) nil shostak)) (sin_0 0 (sin_0-2 nil 3279387338 ("" (lemma "sin2_cos2") (("" (inst?) (("" (rewrite "cos_0") (("" (expand "sq") (("" (rewrite "zero_times3") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (sq const-decl "nonneg_real" sq "reals/") (zero_times3 formula-decl nil real_props nil) (sin const-decl "real" trig_basic nil) (cos_0 formula-decl nil trig_basic nil) (sin2_cos2 formula-decl nil trig_basic nil)) nil) (sin_0-1 nil 3265002237 ("" (expand "sin") (("" (rewrite "floor_int") (("" (rewrite "sin_phase_0") nil nil)) nil)) nil) nil shostak)) (sin_pi2 0 (sin_pi2-1 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)) (cos_pi2 0 (cos_pi2-1 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) ((sin_pi2 formula-decl nil trig_basic nil) (sq_eq_0 formula-decl nil sq "reals/") (cos const-decl "real" trig_basic nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (cos_range application-judgement "trig_range" trig_basic nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_1 formula-decl nil sq "reals/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin2_cos2 formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil)) shostak)) (tan_0_TCC1 0 (tan_0_TCC1-1 nil 3264999490 ("" (expand "Tan?") (("" (rewrite "cos_0") (("" (assert) nil nil)) nil)) nil) ((cos_0 formula-decl nil trig_basic nil) (Tan? const-decl "bool" trig_basic nil)) shostak)) (tan_0 0 (tan_0-1 nil 3265002274 ("" (expand "tan") (("" (rewrite "sin_0") (("" (rewrite "cos_0") (("" (assert) nil nil)) nil)) nil)) nil) ((sin_0 formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (cos_0 formula-decl nil trig_basic nil) (tan const-decl "real" trig_basic nil)) shostak)) (sin_neg 0 (sin_neg-1 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" (lemma "div_mult_pos_le2" ("x" "floor(-a!1 / (2 * pi))" "z" "-a!1" "py" "2 * pi")) (("1" (replace -1 -2) (("1" (lemma "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" (lemma "div_cancel1" ("x" "a!1" "n0z" "2*pi")) (("1" (replace -1) (("1" (lemma "div_cancel1" ("x" "-a!1" "n0z" "2*pi")) (("1" (replace -1) (("1" (simplify 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" (lemma "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)) (cos_neg 0 (cos_neg-1 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" (lemma "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)) (tan_neg_TCC1 0 (tan_neg_TCC1-1 nil 3264999490 ("" (skosimp*) (("" (typepred "a!1") (("" (expand "Tan?") (("" (lemma "cos_neg" ("a" "a!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((Tan? const-decl "bool" trig_basic nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (cos_neg formula-decl nil trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (tan_neg 0 (tan_neg-1 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) ((Tan? const-decl "bool" trig_basic nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (tan const-decl "real" trig_basic nil) (sin_neg formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_neg formula-decl nil trig_basic nil)) shostak)) (cos_sin 0 (cos_sin-1 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) (("" (lemma "cos_eqv_sin_phase" ("x" "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)")) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "floor_plus" ("x" "a!1 / (2 * pi)" "y" "1/4")) (("1" (lemma "floor_val" ("i" "1" "j" "4" "k" "0")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "div_cancel1" ("x" "1/4" "n0z" "pi")) (("1" (lemma "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" (name "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) (("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" (hide 2) (("2" (lemma "floor_def" ("x" "1 / 4 + a!1 / (2 * pi) - FL")) (("2" (flatten -1) (("2" (name-replace "K1" "floor(1 / 4 + a!1 / (2 * pi) - FL)") (("2" (lemma "trichotomy" ("x" "K1")) (("2" (split -1) (("1" (case "K1=1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (case "K1>1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (propax) 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" (hide-all-but (1 2)) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "fractional" 1) (("2" (replace -2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "fractional" 1) (("2" (lemma "floor_val" ("i" "1" "j" "4" "k" "0")) (("2" (hide-all-but (-1 1)) (("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)) (sin_cos 0 (sin_cos-1 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) ((pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (cos_sin formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (sin_neg formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_neg formula-decl nil trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (sin_shift 0 (sin_shift-1 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) ((pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin_neg formula-decl nil trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_range application-judgement "trig_range" trig_basic nil) (sin_cos formula-decl nil trig_basic nil)) shostak)) (cos_shift 0 (cos_shift-1 nil 3265010327 ("" (skosimp*) (("" (lemma "sin_shift" ("a" "pi/2-a!1")) (("" (assert) nil nil)) nil)) nil) ((pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin_shift formula-decl nil trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_range application-judgement "trig_range" trig_basic nil)) shostak)) (neg_cos 0 (neg_cos-1 nil 3265010987 ("" (skosimp*) (("" (rewrite "cos_sin") (("" (rewrite "sin_cos") (("" (assert) nil nil)) nil)) nil)) nil) ((cos_sin formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sin_cos formula-decl nil trig_basic nil)) shostak)) (neg_sin 0 (neg_sin-1 nil 3265071739 ("" (skosimp*) (("" (rewrite "sin_cos") (("" (rewrite "cos_sin") (("" (assert) nil nil)) nil)) nil)) nil) ((sin_cos formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (cos_sin formula-decl nil trig_basic nil)) shostak)) (sin_pi 0 (sin_pi-2 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) (sin_pi-1 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)) (cos_pi 0 (cos_pi-2 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) (cos_pi-1 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)) (tan_pi_TCC1 0 (tan_pi_TCC1-1 nil 3264999490 ("" (expand "Tan?") (("" (rewrite "cos_pi") (("" (assert) nil nil)) nil)) nil) ((cos_pi formula-decl nil trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (Tan? const-decl "bool" trig_basic nil)) shostak)) (tan_pi 0 (tan_pi-1 nil 3265006469 ("" (expand "tan") (("" (rewrite "sin_pi") (("" (rewrite "cos_pi") (("" (assert) nil nil)) nil)) nil)) nil) ((sin_pi formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cos_pi formula-decl nil trig_basic nil) (tan const-decl "real" trig_basic nil)) shostak)) (sin_3pi2 0 (sin_3pi2-1 nil 3265010743 ("" (lemma "neg_sin" ("a" "pi/2")) (("" (rewrite "sin_pi2") (("" (assert) nil nil)) nil)) nil) ((sin_pi2 formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (neg_sin formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil)) shostak)) (cos_3pi2 0 (cos_3pi2-1 nil 3265010800 ("" (lemma "neg_cos" ("a" "pi/2")) (("" (rewrite "cos_pi2") (("" (assert) nil nil)) nil)) nil) ((cos_pi2 formula-decl nil trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_even_is_even application-judgement "even_int" integers nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (neg_cos formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil)) shostak)) (sin_2pi 0 (sin_2pi-2 nil 3279154535 ("" (expand "sin") (("" (rewrite "div_simp") (("" (rewrite "floor_int") (("" (assert) (("" (rewrite "sin_phase_0") nil nil)) nil)) nil)) nil)) nil) nil nil) (sin_2pi-1 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)) (cos_2pi 0 (cos_2pi-2 nil 3279154560 ("" (expand "cos") (("" (rewrite "div_simp") (("" (rewrite "floor_int") (("" (assert) (("" (rewrite "cos_phase_0") nil nil)) nil)) nil)) nil)) nil) nil nil) (cos_2pi-1 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)) (tan_2pi_TCC1 0 (tan_2pi_TCC1-1 nil 3264999491 ("" (expand "Tan?") (("" (rewrite "cos_2pi") (("" (assert) nil nil)) nil)) nil) ((cos_2pi formula-decl nil trig_basic nil) (Tan? const-decl "bool" trig_basic nil)) shostak)) (tan_2pi 0 (tan_2pi-1 nil 3265006491 ("" (expand "tan") (("" (rewrite "sin_2pi") (("" (rewrite "cos_2pi") (("" (assert) nil nil)) nil)) nil)) nil) ((sin_2pi formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (cos_2pi formula-decl nil trig_basic nil) (tan const-decl "real" trig_basic nil)) shostak)) (sin_plus 0 (sin_plus-1 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) (("" (lemma "floor_plus" ("x" "a!1/(2*pi)" "y" "b!1/(2*pi)")) (("" (replace -2) (("" (replace -3) (("" (lemma "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" (hide -2 2) (("2" (lemma "floor_def" ("x" "fractional(a!1 / (2 * pi)) + fractional(b!1 / (2 * pi))")) (("2" (flatten) (("2" (expand "fractional") (("2" (replace -4) (("2" (replace -5) (("2" (lemma "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" (lemma "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" (hide 3) (("2" (case "floor(fractional(a!1 / (2 * pi)) + fractional(b!1 / (2 * pi))) = 1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "fractional" 1) (("2" (replace -2) (("2" (replace -3) (("2" (hide -1) (("2" (lemma "floor_def" ("x" "a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB")) (("2" (lemma "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" (lemma "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" (flatten) (("2" (replace -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand "FLA") (("3" (lemma "floor_def" ("x" "a!1/(2*pi)")) (("3" (rewrite "div_mult_pos_lt1" -1) (("3" (rewrite "div_mult_pos_le2" -1) (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (sin_minus 0 (sin_minus-1 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) ((- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin_plus formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (cos_neg formula-decl nil trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_neg formula-decl nil trig_basic nil)) shostak)) (cos_plus 0 (cos_plus-1 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_plus_real_is_real application-judgement "real" reals nil) (cos_sin formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_range application-judgement "trig_range" trig_basic nil) (sin_cos formula-decl nil trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (sin_plus formula-decl nil trig_basic nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil)) shostak)) (cos_minus 0 (cos_minus-1 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) ((- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (cos_plus formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (sin_neg formula-decl nil trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_neg formula-decl nil trig_basic nil)) shostak)) (sin_pi_minus 0 (sin_pi_minus-1 nil 3419263512 ("" (skosimp*) (("" (rewrite "sin_minus") (("" (rewrite "sin_pi") (("" (rewrite "cos_pi") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((sin_minus formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_pi formula-decl nil trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sin_pi formula-decl nil trig_basic nil)) nil)) (cos_pi_minus 0 (cos_pi_minus-1 nil 3419263645 ("" (skosimp*) (("" (rewrite "cos_minus") (("" (rewrite "cos_pi") (("" (rewrite "sin_pi") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((cos_minus formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_pi formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cos_pi formula-decl nil trig_basic nil)) shostak)) (tan_plus_TCC1 0 (tan_plus_TCC1-1 nil 3264999490 ("" (skosimp*) (("" (expand "tan") (("" (expand "Tan?") (("" (assert) nil nil)) nil)) nil)) nil) ((sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (tan const-decl "real" trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (Tan? const-decl "bool" trig_basic nil)) shostak)) (tan_plus 0 (tan_plus-1 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) ((Tan? const-decl "bool" trig_basic nil) (sin_plus formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (cross_mult formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (cos const-decl "real" trig_basic nil) (sin const-decl "real" trig_basic nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (cos_plus formula-decl nil trig_basic nil) (tan const-decl "real" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil)) shostak)) (tan_minus_TCC1 0 (tan_minus_TCC1-1 nil 3264999490 ("" (skosimp*) (("" (expand "tan") (("" (assert) nil nil)) nil)) nil) ((sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (tan const-decl "real" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (tan_minus 0 (tan_minus-1 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) ((- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (tan_plus formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cos_range application-judgement "trig_range" trig_basic nil) (cos_neg formula-decl nil trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (tan_neg formula-decl nil trig_basic nil) (bool nonempty-type-eq-decl nil booleans nil) (Tan? const-decl "bool" trig_basic nil)) shostak)) (arc_sin_cos 0 (arc_sin_cos-1 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" (lemma "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" (lemma "sq_le_abs" ("a" "a!1/c!1" "b" "1")) (("1" (rewrite "sq_1") (("1" (replace -2 -1) (("1" (flatten -1) (("1" (expand "abs" -1 2) (("1" (case "sq(b!1) <= sq(c!1)") (("1" (lemma "div_mult_pos_le1" ("z" "sq(b!1)" "py" "sq(c!1)" "x" "1")) (("1" (replace -2 -1) (("1" (flatten -1) (("1" (lemma "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" (flatten) (("1" (expand "abs" -1 2) (("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) &&n (("1" (expand "abs" (-3 -6)) (("1" (case "b!1 / c!1 < 0") (("1" (case "a!1 / c!1 < 0") (("1" (inst - "-(a!1/c!1)" "-(b!1/c!1)") (("1" (rewrite "sq_neg") (("1" (rewrite "sq_neg") (("1" (assert) (("1" (skosimp*) (("1" (inst + "z!1+pi") (("1" (lemma "neg_cos" ("a" "z!1")) (("1" (lemma "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" (inst - "-(b!1/c!1)" "a!1/c!1") (("1" (rewrite "sq_neg") (("1" (assert) (("1" (skosimp*) (("1" (lemma "cos_sin" ("a" "z!1-pi/2")) (("1" (lemma "sin_cos" ("a" "z!1-pi/2")) (("1" (assert) (("1" (inst + "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" (inst - "b!1/c!1" "-(a!1/c!1)") (("1" (rewrite "sq_neg") (("1" (assert) (("1" (skosimp*) (("1" (rewrite "cos_sin" -2) (("1" (rewrite "sin_cos" -3) (("1" (inst + "pi/2+z!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil) ("2" (inst - "a!1/c!1" "b!1/c!1") (("1" (assert) (("1" (skosimp*) (("1" (inst + "z!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (typepred "y!1") (("2" (inst + "acos(x!1)") (("1" (case "x!1 = cos(acos(x!1))") (("1" (assert) (("1" (typepred "acos(x!1)") (("1" (expand ">=" -6) (("1" (expand "<=" -6) (("1" (split -6) (("1" (lemma "acos_strict_decreasing") (("1" (expand "strict_decreasing?") (("1" (inst - "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) (("1" (assert) (("1" (lemma "sin_q1" ("x" "acos(x!1)")) (("1" (rewrite "phase_sin_q1" -1) (("1" (replace -1) (("1" (lemma "sin_eqv_sqrt_cos_value" ("q1" "acos(x!1)")) (("1" (replace -1 * rl) (("1" (rewrite "cos_value_acos" 1) (("1" (lemma "sq_eq" ("nna" "y!1" "nnb" "sqrt(1 - sq(x!1))")) (("1" (replace -1 1 rl) (("1" (rewrite "sq_sqrt") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -5 2) (("2" (lemma "floor_def" ("x" "acos(x!1)/(2*pi)")) (("2" (rewrite "div_mult_pos_le2" -1) (("2" (flatten) (("2" (lemma "div_mult_pos_lt1" ("x" "floor(acos(x!1) / (2 * pi)) + 1" "py" "2*pi" "z" "acos(x!1)")) (("2" (replace -1 -3) (("2" (hide -1) (("2" (name-replace "K1" "floor(acos(x!1) / (2 * pi))") (("2" (lemma "trichotomy" ("x" "K1")) (("2" (split -1) (("1" (case "K1=1") (("1" (assert) nil nil) ("2" (case "K1>1") (("1" (lemma "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) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (propax) nil nil)) nil) ("3" (expand "abs") (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (rewrite "acos_0") (("2" (lemma "sin_pi2") (("2" (expand "pi") (("2" (replace -1) (("2" (rewrite "sq_0") (("2" (lemma "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" (hide 2) (("2" (hide -1 -2 -5) (("2" (expand "cos") (("2" (case "floor(acos(x!1) / (2 * pi))=0") (("1" (replace -1) (("1" (assert) (("1" (rewrite "cos_phase_acos") nil nil)) nil)) nil) ("2" (hide 2) (("2" (typepred "acos(x!1)") (("2" (lemma "floor_def" ("x" "acos(x!1) / (2 * pi)")) (("2" (rewrite "div_mult_pos_lt1" -1) (("2" (rewrite "div_mult_pos_le2" -1) (("2" (flatten) (("2" (name-replace "K1" "floor(acos(x!1) / (2 * pi))") (("2" (lemma "trichotomy" ("x" "K1")) (("2" (split -1) (("1" (case "K1=1") (("1" (assert) nil nil) ("2" (case "K1>1") (("1" (lemma "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) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "abs") (("3" (propax) nil nil)) nil)) nil) ("2" (lemma "acos_strict_decreasing") (("2" (expand "strict_decreasing?") (("2" (expand ">=" -4) (("2" (expand "<=" -4) (("2" (split -4) (("1" (inst - "0" "x!1") (("1" (rewrite "acos_0") (("1" (assert) nil nil)) nil) ("2" (expand "abs") (("2" (propax) nil nil)) nil) ("3" (expand "abs") (("3" (assert) nil nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (rewrite "acos_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "abs") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("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) ((sq_eq_0 formula-decl nil sq "reals/") (sq_0 formula-decl nil sq "reals/") (sq_div formula-decl nil sq "reals/") (sq_le_abs formula-decl nil sq "reals/") (sq_neg formula-decl nil sq "reals/") (sq_eq formula-decl nil sq "reals/") (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/") (sq_sqrt formula-decl nil sqrt "reals/") (sq_1 formula-decl nil sq "reals/") (sq_nz_pos judgement-tcc nil sq "reals/") (sq const-decl "nonneg_real" sq "reals/")) shostak)) (pythagorean 0 (pythagorean-1 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) ((nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (arc_sin_cos formula-decl nil trig_basic nil) (sin2_cos2 formula-decl nil trig_basic nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (sq const-decl "nonneg_real" sq "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (sin_2a 0 (sin_2a-1 nil 3265007761 ("" (skosimp*) (("" (lemma "sin_plus" ("a" "a!1" "b" "a!1")) (("" (assert) nil nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin_plus formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil)) shostak)) (cos_2a 0 (cos_2a-1 nil 3265007796 ("" (skosimp*) (("" (lemma "cos_plus" ("a" "a!1" "b" "a!1")) (("" (assert) nil nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (cos_plus formula-decl nil trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil)) shostak)) (cos_2a_cos 0 (cos_2a_cos-1 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) ((cos_2a formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (sin const-decl "real" trig_basic nil) (sq const-decl "nonneg_real" sq "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (sin2_cos2 formula-decl nil trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sq_rew formula-decl nil sq "reals/") (cos const-decl "real" trig_basic nil)) shostak)) (cos_2a_sin 0 (cos_2a_sin-1 nil 3265007915 ("" (skosimp*) (("" (lemma "sin2_cos2" ("a" "a!1")) (("" (rewrite "cos_2a") (("" (expand "sq") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin2_cos2 formula-decl nil trig_basic nil) (sq const-decl "nonneg_real" sq "reals/") (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_2a formula-decl nil trig_basic nil)) shostak)) (tan_2a_TCC1 0 (tan_2a_TCC1-1 nil 3264999490 ("" (skosimp*) (("" (expand "tan") (("" (assert) nil nil)) nil)) nil) ((sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (tan const-decl "real" trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (tan_2a 0 (tan_2a-1 nil 3265072074 ("" (skosimp*) (("" (lemma "tan_plus" ("a" "a!1" "b" "a!1")) (("" (assert) nil nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (tan_plus formula-decl nil trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (sin_period 0 (sin_period-4 nil 3279387961 ("" (case-replace "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" (case-replace "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" (case-replace "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) ((sin_plus formula-decl nil trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (cos_2pi formula-decl nil trig_basic nil) (sin_2pi formula-decl nil trig_basic nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nat_induction formula-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (minus_int_is_int application-judgement "int" integers nil) (sin_neg formula-decl nil trig_basic nil) (j!1 skolem-const-decl "integer" trig_basic nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (integer nonempty-type-from-decl nil integers nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sin const-decl "real" trig_basic nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil)) nil) (sin_period-3 nil 3279387942 ("" (case-replace "FORALL (a: real, j: nat): sin(a) = sin(a + 2 * j * PI)") (("1" (skosimp*) (("1" (case-replace "j!1 >= 0") (("1" (inst?) nil) ("2" (case-replace "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" (case-replace "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) (sin_period-2 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")) (("" (lemma "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) (sin_period-1 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")) (("" (lemma "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)) (cos_period 0 (cos_period-1 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) ((cos_sin formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_times_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (sin_period formula-decl nil trig_basic nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (integer nonempty-type-from-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil)) shostak)) (tan_period_TCC1 0 (tan_period_TCC1-4 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) ((Tan? const-decl "bool" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (cos_period formula-decl nil trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (neg_cos formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (odd? const-decl "bool" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (even? const-decl "bool" integers nil) (odd_or_even_int formula-decl nil naturalnumbers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (integer nonempty-type-from-decl nil integers nil)) nil) (tan_period_TCC1-3 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" (case-replace "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) (tan_period_TCC1-2 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" (case-replace "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) (tan_period_TCC1-1 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)) (tan_period 0 (tan_period-2 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) ((tan const-decl "real" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sin_period formula-decl nil trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (neg_cos formula-decl nil trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (neg_sin formula-decl nil trig_basic nil) (cos_period formula-decl nil trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (odd? const-decl "bool" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (even? const-decl "bool" integers nil) (odd_or_even_int formula-decl nil naturalnumbers nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (integer nonempty-type-from-decl nil integers nil)) nil) (tan_period-1 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)) (sin_k_pi 0 (sin_k_pi-2 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) ((integer nonempty-type-from-decl nil integers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (odd_or_even_int formula-decl nil naturalnumbers nil) (even? const-decl "bool" integers nil) (sin_0 formula-decl nil trig_basic nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (odd? const-decl "bool" integers nil) (sin_pi formula-decl nil trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sin_period formula-decl nil trig_basic nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil)) nil) (sin_k_pi-1 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)) (cos_2k_pi 0 (cos_2k_pi-1 nil 3265073272 ("" (skosimp*) (("" (lemma "cos_period" ("a" "0" "j" "k!1")) (("" (rewrite "cos_0") (("" (assert) nil nil)) nil)) nil)) nil) ((integer nonempty-type-from-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (cos_period formula-decl nil trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (cos_0 formula-decl nil trig_basic nil)) shostak)) (cos_k_pi 0 (cos_k_pi-1 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) ((integer nonempty-type-from-decl nil integers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (odd_or_even_int formula-decl nil naturalnumbers nil) (even_m1_pow formula-decl nil exponentiation nil) (cos_0 formula-decl nil trig_basic nil) (even? const-decl "bool" integers nil) (not_even_m1_pow formula-decl nil exponentiation nil) (even_iff_not_odd formula-decl nil naturalnumbers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (odd? const-decl "bool" integers nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (cos_period formula-decl nil trig_basic nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (rat_exp application-judgement "rat" exponentiation nil) (real_plus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (cos_pi formula-decl nil trig_basic nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil)) shostak)) (sin_k_pi2 0 (sin_k_pi2-1 nil 3265073635 ("" (skosimp*) (("" (lemma "cos_k_pi" ("k" "k!1")) (("" (rewrite "cos_sin") (("" (assert) nil nil)) nil)) nil)) nil) ((integer nonempty-type-from-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (cos_k_pi formula-decl nil trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (rat_exp application-judgement "rat" exponentiation nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (cos_sin formula-decl nil trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (tan_k_pi_TCC1 0 (tan_k_pi_TCC1-1 nil 3264999491 ("" (skosimp*) (("" (expand "Tan?") (("" (lemma "cos_k_pi" ("k" "k!1")) (("" (assert) nil nil)) nil)) nil)) nil) ((Tan? const-decl "bool" trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (rat_exp application-judgement "rat" exponentiation nil) (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (cos_k_pi formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (integer nonempty-type-from-decl nil integers nil)) shostak)) (tan_k_pi 0 (tan_k_pi-1 nil 3265072687 ("" (skosimp*) (("" (expand "tan") (("" (rewrite "sin_k_pi") (("" (assert) nil nil)) nil)) nil)) nil) ((tan const-decl "real" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (integer nonempty-type-from-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin_k_pi formula-decl nil trig_basic nil)) shostak)) (sin_eq_0 0 (sin_eq_0-2 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" (lemma "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" (inst + "2 * (floor(a!1 / (2 * pi))) +1") (("2" (assert) nil nil)) nil) ("3" (inst + "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)) / (2 * pi))) = 0") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (lemma "div_cancel1" ("x" "floor(a!1 / (2 * pi))" "n0z" "2*pi")) (("2" (replace -1) (("2" (lemma "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" (lemma "floor_val" ("i" "1+2*j!1" "j" "2" "k" "j!1")) (("1" (split -1) (("1" (replace -1) (("1" (assert) (("1" (lemma "sin_pi") (("1" (expand "sin") (("1" (lemma "div_cancel1" ("x" "1/2" "n0z" "pi")) (("1" (replace -1) (("1" (lemma "floor_val" ("i" "1" "j" "2" "k" "0")) (("1" (split -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" (lemma "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) (sin_eq_0-1 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" (lemma "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" (inst + "2 * floor(a!1 / (2 * pi))") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "pi") (("2" (inst + "2 * (floor(a!1 / (2 * pi))) +1") (("2" (assert) nil nil)) nil)) nil) ("3" (expand "pi") (("3" (inst + "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)) / (2 * pi))) = 0") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (lemma "div_cancel1" ("x" "floor(a!1 / (2 * pi))" "n0z" "2*pi")) (("2" (replace -1) (("2" (lemma "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" (hide -1 -2 -3) (("1" (lemma "floor_val" ("i" "1+2*j!1" "j" "2" "k" "j!1")) (("1" (split -1) (("1" (replace -1) (("1" (assert) (("1" (lemma "sin_pi") (("1" (expand "pi") (("1" (expand "sin") (("1" (lemma "div_cancel1" ("x" "1/2" "n0z" "pi")) (("1" (replace -1) (("1" (lemma "floor_val" ("i" "1" "j" "2" "k" "0")) (("1" (split -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" (lemma "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)) (cos_eq_0 0 (cos_eq_0-1 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) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (cos_sin formula-decl nil trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (int_minus_int_is_int application-judgement "int" integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_eq_0 formula-decl nil trig_basic nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil)) shostak)) (sin_eq_0_2pi 0 (sin_eq_0_2pi-4 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" (case-replace "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) ((sin_eq_0 formula-decl nil trig_basic nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (pos_times_ge formula-decl nil real_props nil) (sin_0 formula-decl nil trig_basic nil) (sin_pi formula-decl nil trig_basic nil) (sin_2pi formula-decl nil trig_basic nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil) (sin_eq_0_2pi-3 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" (hide -2) (("1" (inst - "0" "_") (("1" (rewrite "sin_value_0") (("1" (lemma "cos_value_strict_decreasing") (("1" (expand "strict_decreasing?") (("1" (inst - "_" "pi/2") (("1" (rewrite "cos_value_pi2") (("1" (lemma "phases_sin" ("x" "a!1")) (("1" (split -1) (("1" (rewrite "sin_q1" -5) (("1" (inst -3 "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" (inst -2 "a!1-pi/2") (("1" (assert) (("1" (flatten -1) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (rewrite "sin_q3" -5) (("3" (rewrite "phase_sin_q3") (("3" (flatten -1) (("3" (inst -4 "a!1-pi") (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (rewrite "sin_q4" -5) (("4" (rewrite "phase_sin_q4") (("4" (inst -2 "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" (name-replace "K1" "floor(a!1 / (2 * pi))") (("2" (lemma "trichotomy" ("x" "K1")) (("2" (split -1) (("1" (case "K1=1") (("1" (assert) nil nil) ("2" (case "K1>1") (("1" (lemma "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" (lemma "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) (sin_eq_0_2pi-2 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" (hide -2) (("1" (inst - "0" "_") (("1" (rewrite "sin_value_0") (("1" (lemma "cos_value_strict_decreasing") (("1" (expand "strict_decreasing?") (("1" (inst - "_" "pi/2") (("1" (rewrite "cos_value_pi2") (("1" (lemma "phases_sin" ("x" "a!1")) (("1" (split -1) (("1" (rewrite "sin_q1" -5) (("1" (inst -3 "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" (inst -2 "a!1-pi/2") (("1" (assert) (("1" (flatten -1) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (rewrite "sin_q3" -5) (("3" (rewrite "phase_sin_q3") (("3" (flatten -1) (("3" (inst -4 "a!1-pi") (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (rewrite "sin_q4" -5) (("4" (rewrite "phase_sin_q4") (("4" (inst -2 "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" (name-replace "K1" "floor(a!1 / (2 * pi))") (("2" (lemma "trichotomy" ("x" "K1")) (("2" (split -1) (("1" (case "K1=1") (("1" (assert) (("1" (postpone) nil nil)) nil) ("2" (case "K1>1") (("1" (lemma "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" (lemma "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) (sin_eq_0_2pi-1 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" (flatten) (("1" (hide -2) (("1" (inst - "0" "_") (("1" (rewrite "sin_value_0") (("1" (lemma "cos_value_strict_decreasing") (("1" (expand "strict_decreasing?") (("1" (inst - "_" "pi/2") (("1" (rewrite "cos_value_pi2") (("1" (lemma "phases_sin" ("x" "a!1")) (("1" (split -1) (("1" (rewrite "sin_q1" -5) (("1" (inst -3 "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" (inst -2 "a!1-pi/2") (("1" (assert) (("1" (flatten -1) (("1" (assert) nil nil)) nil)) nil) ("2" (flatten -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (rewrite "sin_q3" -5) (("3" (rewrite "phase_sin_q3") (("3" (flatten -1) (("3" (inst -4 "a!1-pi") (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (rewrite "sin_q4" -5) (("4" (rewrite "phase_sin_q4") (("4" (inst -2 "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" (name-replace "K1" "floor(a!1 / (2 * pi))") (("2" (lemma "trichotomy" ("x" "K1")) (("2" (split -1) (("1" (case "K1=1") (("1" (assert) nil nil) ("2" (case "K1>1") (("1" (lemma "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" (lemma "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)) (cos_eq_0_2pi 0 (cos_eq_0_2pi-1 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" (lemma "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) ((pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_eq_0_2pi formula-decl nil trig_basic nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_sin formula-decl nil trig_basic nil) (nzint_times_nzint_is_nzint application-judgement "nzint" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (integer nonempty-type-from-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (cos_period formula-decl nil trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cos_pi2 formula-decl nil trig_basic nil) (cos_3pi2 formula-decl nil trig_basic nil)) shostak)) (tan_eq_0 0 (tan_eq_0-1 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) ((sin_eq_0 formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (tan const-decl "real" trig_basic nil) (div_cancel3 formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (cos const-decl "real" trig_basic nil) (sin const-decl "real" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (Tan? const-decl "bool" trig_basic nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (sin_eq_1 0 (sin_eq_1-4 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" (case-replace "even?(i!1-1)") (("1" (expand "even?") (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "odd_iff_even_succ") (("2" (inst - "i!1-1") (("2" (assert) (("2" (hide 3) (("2" (lemma "odd_or_even_int") (("2" (inst?) (("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) ((sin const-decl "real" trig_basic nil) (sq const-decl "nonneg_real" sq "reals/") (sin2 formula-decl nil trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil) (zero_times3 formula-decl nil real_props nil) (cos_eq_0 formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (even? const-decl "bool" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_3pi2 formula-decl nil trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (odd_or_even_int formula-decl nil naturalnumbers nil) (int_plus_int_is_int application-judgement "int" integers nil) (odd_iff_even_succ formula-decl nil naturalnumbers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (integer nonempty-type-from-decl nil integers nil) (i!1 skolem-const-decl "int" trig_basic nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (sin_period formula-decl nil trig_basic nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_times_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (cos const-decl "real" trig_basic nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_plus formula-decl nil trig_basic nil) (cos_pi2 formula-decl nil trig_basic nil) (cos_2k_pi formula-decl nil trig_basic nil) (sin_pi2 formula-decl nil trig_basic nil)) nil) (sin_eq_1-3 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" (case-replace "even?(i!1-1)") (("1" (expand "even?") (("1" (skosimp*) (("1" (assert) nil))))) ("2" (hide 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) (sin_eq_1-2 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" (inst - "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)") (("1" (lemma "cos_value_bij") (("1" (expand "bijective?") (("1" (expand "injective?") (("1" (flatten -1) (("1" (hide -2) (("1" (lemma "sin_value_strict_increasing") (("1" (expand "strict_increasing?") (("1" (split -3) (("1" (rewrite "sin_q1" -6) (("1" (rewrite "phase_sin_q1" -1) (("1" (flatten -1) (("1" (inst -3 "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" (flatten -1) (("2" (inst -4 "-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" (flatten -1) (("3" (inst -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" (flatten -1) (("4" (inst -4 "pi" "-1 * (3 * pi / 2) - 2 * (floor(a!1 / (2 * pi)) * pi) + a!1") (("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) (sin_eq_1-1 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" (inst - "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)") (("1" (lemma "cos_value_bij") (("1" (expand "bijective?") (("1" (expand "injective?") (("1" (flatten -1) (("1" (hide -2) (("1" (lemma "sin_value_strict_increasing") (("1" (expand "strict_increasing?") (("1" (split -3) (("1" (rewrite "sin_q1" -6) (("1" (rewrite "phase_sin_q1" -1) (("1" (flatten -1) (("1" (inst -3 "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" (flatten -1) (("2" (inst -4 "-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" (flatten -1) (("3" (inst -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" (flatten -1) (("4" (inst -4 "pi" "-1 * (3 * pi / 2) - 2 * (floor(a!1 / (2 * pi)) * pi) + a!1") (("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)) (cos_eq_1 0 (cos_eq_1-1 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) ((cos_sin formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (sin_eq_1 formula-decl nil trig_basic nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil)) shostak)))
¤ Dauer der Verarbeitung: 0.297 Sekunden (vorverarbeitet am 2026-04-26) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26