| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/trig_fnd/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 306 kB |
|
Quelle sincos_phase.prfSprache: Lisp |
|||||||||||||||
|
(sincos_phase (trig_phase_TCC1 0 (trig_phase_TCC1-1 nil 3264603198 ("" (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_phase_TCC1 0 (sin_phase_TCC1-1 nil 3264597671 ("" (skosimp*) (("" (replace -2) (("" (hide -2) (("" (lemma "floor_def" ("x" "(2*x!1)/pi")) (("" (flatten) (("" (assert) (("" (replace -3) (("" (hide -3) (("" (expand "abs") (("" (lemma "div_mult_pos_le1" ("z" "x!1" "x" "1" "py" "pi/2")) (("" (replace -1 1 rl) (("" (hide -1) (("" (rewrite "div_div1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (nnreal 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) (/ 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) (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) (floor_def formula-decl nil floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_div1 formula-decl nil real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (div_mult_pos_le1 formula-decl nil real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (sin_phase_TCC2 0 (sin_phase_TCC2-1 nil 3264597671 ("" (skosimp*) (("" (replace -2) (("" (hide -2 1) (("" (lemma "floor_def" ("x" "(2 * x!1) / pi")) (("" (replace -2 * rl) (("" (flatten) (("" (replace -3) (("" (hide -3) (("" (expand "abs") (("" (lemma "div_mult_pos_lt1" ("x" "1" "z" "x!1" "py" "pi")) (("" (lemma "both_sides_times_pos_lt1" ("x" "x!1/pi" "y" "1" "pz" "2")) (("" (replace -1 -2 rl) (("" (replace -4 -2) (("" (flatten -2) (("" (hide -1 -4) (("" (assert) (("" (lemma "div_mult_pos_le2" ("x" "1" "z" "2*x!1" "py" "pi")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (nnreal 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) (/ 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) (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) (floor_def formula-decl nil floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (int_times_even_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (div_mult_pos_le2 formula-decl nil real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (sin_phase_TCC3 0 (sin_phase_TCC3-1 nil 3264597671 ("" (skosimp*) (("" (replace -2) (("" (hide -2 1 2) (("" (lemma "floor_def" ("x" "(2*x!1)/pi")) (("" (flatten) (("" (replace -3) (("" (hide -3) (("" (lemma "div_mult_pos_le2" ("x" "2" "z" "2*x!1" "py" "pi")) (("" (lemma "both_sides_times_pos_le1" ("x" "pi" "y" "x!1" "pz" "2")) (("" (expand "abs" 1) (("" (assert) (("" (lemma "div_mult_pos_lt1" ("z" "2*x!1" "py" "pi" "x" "3")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (nnreal 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) (/ 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) (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) (floor_def formula-decl nil floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (div_mult_pos_le2 formula-decl nil real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (sin_phase_TCC4 0 (owre "fix" 3399981374 ("" (skosimp*) (("" (case "floor((2 * x!1) / pi) = 0") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (case "floor((2 * x!1) / pi) = 1") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (case "floor((2 * x!1) / pi) = 2") (("1" (rewrite "abs_neg") (("1" (assert) nil nil)) nil) ("2" (lemma "floor_def" ("x" "(2*x!1)/pi")) (("2" (flatten) (("2" (replace -3) (("2" (lemma "div_mult_pos_le2" ("z" "2*x!1" "py" "pi" "x" "2")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (nnreal 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) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (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) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (floor_def formula-decl nil floor_ceil nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (div_mult_pos_le2 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak) (sin_phase_TCC4-2 nil 3399981363 (";;; Proof sin_phase_TCC4-2 for formula sincos_phase.sin_phase_TCC4" (skosimp*) ((";;; Proof sin_phase_TCC4-2 for formula sincos_phase.sin_phase_TCC4" (case "floor((2 * x!1) / pi) = 0") (("1" (replace -1) (("1" (propax) nil))) ("2" (assert) (("2" (case "floor((2 * x!1) / pi) = 1") (("1" (replace -1) (("1" (propax) nil))) ("2" (case "floor((2 * x!1) / pi) = 2") (("1" (rewrite "abs_neg") (("1" (assert) nil))) ("2" (lemma "floor_def" ("x" "(2*x!1)/pi")) (("2" (flatten) (("2" (replace -3) (("2" (lemma "div_mult_pos_le2" ("z" "2*x!1" "py" "pi" "x" "2")) (("2" (assert) nil)))))))))))))))))) ";;; developed with shostak decision procedures") ((real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil) (pi const-decl "posreal" atan nil)) nil) (sin_phase_TCC4-1 nil 3264597671 ("" (skosimp*) (("" (lemma "floor_def" ("x" "(2 * x!1) / pi")) (("" (replace -2 * rl) (("" (flatten) (("" (hide -3) (("" (lemma "div_mult_pos_le2" ("x" "i!1" "py" "pi" "z" "2*x!1")) (("" (lemma "div_mult_pos_lt1" ("x" "i!1+1" "py" "pi" "z" "2*x!1")) (("" (typepred "x!1") (("" (replace -6) (("" (replace -5) (("" (flatten) (("" (expand "abs") (("" (lemma "both_sides_times_pos_lt1" ("x" "x!1" "y" "2*pi" "pz" "2")) (("" (replace -3 -1) (("" (flatten) (("" (lemma "div_mult_pos_le2" ("z" "pi" "py" "2" "x" "2*pi-x!1")) (("" (replace -1 4) (("" (hide -1) (("" (lemma "both_sides_plus_le1" ("x" "(2*pi-x!1)*2" "y" "pi" "z" "2*x!1-pi")) (("" (replace -1 4 rl) (("" (hide -1) (("" (assert) (("" (case "i!1 < 0") (("1" (assert) nil nil) ("2" (case "i!1 = 3") (("1" (assert) nil nil) ("2" (case "i!1=4") (("1" (assert) nil nil) ("2" (case "i!1>4") (("1" (assert) (("1" (lemma "div_mult_pos_le2" ("x" "4" "z" "2*x!1" "py" "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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pi const-decl "posreal" atan nil)) shostak)) (sin_phase_TCC5 0 (sin_phase_TCC5-2 nil 3399981395 ("" (skosimp*) (("" (lemma "floor_def" ("x" "(2 * x!1) / pi")) (("" (replace -2 * rl) (("" (flatten) (("" (hide -3) (("" (lemma "div_mult_pos_le2" ("x" "i!1" "py" "pi" "z" "2*x!1")) (("" (lemma "div_mult_pos_lt1" ("x" "i!1+1" "py" "pi" "z" "2*x!1")) (("" (typepred "x!1") (("" (replace -6) (("" (replace -5) (("" (flatten) (("" (expand "abs") (("" (lemma "both_sides_times_pos_lt1" ("x" "x!1" "y" "2*pi" "pz" "2")) (("" (replace -3 -1) (("" (flatten) (("" (lemma "div_mult_pos_le2" ("z" "pi" "py" "2" "x" "2*pi-x!1")) (("" (replace -1 4) (("" (hide -1) (("" (lemma "both_sides_plus_le1" ("x" "(2*pi-x!1)*2" "y" "pi" "z" "2*x!1-pi")) (("" (replace -1 4 rl) (("" (hide -1) (("" (assert) (("" (case "i!1 < 0") (("1" (assert) nil nil) ("2" (case "i!1 = 3") (("1" (assert) nil nil) ("2" (case "i!1=4") (("1" (assert) nil nil) ("2" (case "i!1>4") (("1" (assert) (("1" (lemma "div_mult_pos_le2" ("x" "4" "z" "2*x!1" "py" "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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (nnreal 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) (/ 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) (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) (floor_def formula-decl nil floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" 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) (div_mult_pos_le2 formula-decl nil real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (both_sides_plus_le1 formula-decl nil real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_minus_real_is_real application-judgement "real" reals nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) nil) (sin_phase_TCC5-1 nil 3264597671 ("" (skosimp*) (("" (case "floor((2 * x!1) / pi) = 0") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (case "floor((2 * x!1) / pi) = 1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (case "floor((2 * x!1) / pi) = 2") (("1" (assert) (("1" (assert) (("1" (rewrite "abs_neg") (("1" (assert) nil nil) ("2" (lemma "floor_def" ("x" "(2*x!1)/pi")) (("2" (flatten) (("2" (replace -3) (("2" (lemma "div_mult_pos_le2" ("z" "2*x!1" "py" "pi" "x" "2")) (("2" (expand "abs" 1) (("2" (assert) (("2" (lemma "div_mult_pos_lt1" ("z" "x!1" "py" "pi/2" "x" "3")) (("2" (rewrite "div_div1" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (typepred "x!1") (("2" (case "floor((2 * x!1) / pi) = 3") (("1" (lemma "floor_def" ("x" "(2*x!1)/pi")) (("1" (flatten) (("1" (replace -3) (("1" (lemma "div_mult_pos_lt1" ("z" "x!1" "py" "pi/2" "x" "4")) (("1" (lemma "div_mult_pos_le2" ("z" "x!1" "py" "pi/2" "x" "3")) (("1" (rewrite "div_div1") (("1" (replace -4) (("1" (replace -3) (("1" (flatten) (("1" (rewrite "abs_neg") (("1" (typepred "sin_value(2 * pi - x!1)") (("1" (propax) nil nil) ("2" (expand "abs" 1) (("2" (assert) 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 5) (("2" (case "floor((2 * x!1) / pi) < 0") (("1" (lemma "floor_def" ("x" "(2*x!1)/pi")) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "floor_def" ("x" "(2*x!1)/pi")) (("2" (flatten) (("2" (case "floor((2 * x!1) / pi) = 4") (("1" (replace -1) (("1" (rewrite "div_mult_pos_le2") nil nil)) nil) ("2" (case "floor((2 * x!1) / pi) > 4") (("1" (lemma "div_mult_pos_le2" ("x" "4" "z" "x!1" "py" "pi/2")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pi const-decl "posreal" atan nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil)) shostak)) (sin_phase_TCC6 0 (sin_phase_TCC6-2 nil 3399981423 ("" (skosimp*) (("" (case "floor((2 * x!1) / pi) = 0") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (assert) (("2" (case "floor((2 * x!1) / pi) = 1") (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (case "floor((2 * x!1) / pi) = 2") (("1" (assert) nil nil) ("2" (rewrite "abs_neg") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (nnreal 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) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (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) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) nil) (sin_phase_TCC6-1 nil 3399976753 ("" (subtype-tcc) nil nil) nil nil)) (cos_phase_TCC1 0 (cos_phase_TCC1-1 nil 3264597671 ("" (skosimp*) (("" (replace -2) (("" (lemma "floor_def" ("x" "x!1/pi")) (("" (flatten) (("" (replace -3 * rl) (("" (rewrite "div_mult_pos_lt1" -2) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" 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) (div_mult_pos_lt1 formula-decl nil real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (floor_def formula-decl nil floor_ceil 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil)) shostak)) (cos_phase_TCC2 0 (cos_phase_TCC2-1 nil 3264597671 ("" (skosimp*) (("" (case "i!1 = 1") (("1" (replace -1) (("1" (lemma "floor_def" ("x" "x!1/pi")) (("1" (replace -3 * rl) (("1" (flatten) (("1" (rewrite "div_mult_pos_le2") (("1" (lemma "div_mult_pos_lt1" ("z" "x!1" "py" "pi" "x" "2")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "i!1<0") (("1" (assert) nil nil) ("2" (case "i!1 = 2") (("1" (lemma "floor_def" ("x" "x!1/pi")) (("1" (replace -3 * rl) (("1" (replace -2) (("1" (flatten) (("1" (rewrite "div_mult_pos_le2" -1) nil nil)) nil)) nil)) nil)) nil) ("2" (case "i!1>2") (("1" (lemma "floor_def" ("x" "x!1/pi")) (("1" (replace -3 -1 rl) (("1" (flatten) (("1" (rewrite "div_mult_pos_le2" -1) (("1" (rewrite "div_mult_pos_lt1" -2) (("1" (assert) (("1" (lemma "both_sides_times_pos_lt1" ("x" "2" "y" "i!1" "pz" "pi")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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 "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (AND const-decl "[bool, bool -> bool]" booleans 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) (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) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (floor_def formula-decl nil floor_ceil nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (div_mult_pos_le2 formula-decl nil real_props nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (int_plus_int_is_int application-judgement "int" integers nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil)) shostak)) (phase_sin_q1 0 (phase_sin_q1-1 nil 3264623984 ("" (skosimp*) (("" (lemma "floor_def" ("x" "(2 * x!1) / pi")) (("" (flatten) (("" (name-replace "K1" "floor((2 * x!1) / pi)") (("" (lemma "trichotomy" ("x" "K1")) (("" (split -1) (("1" (case "K1=1") (("1" (replace -1) (("1" (lemma "div_mult_pos_le2" ("x" "1" "z" "2*x!1" "py" "pi")) (("1" (lemma "div_mult_pos_lt1" ("x" "2" "z" "2*x!1" "py" "pi")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (case "K1>1") (("1" (assert) (("1" (rewrite "div_mult_pos_le2") (("1" (lemma "both_sides_times_pos_lt1" ("x" "1" "y" "K1" "pz" "pi")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (replace -1) (("2" (rewrite "div_mult_pos_le2") (("2" (rewrite "div_mult_pos_lt1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (nnreal 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) (/ 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) (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) (floor_def formula-decl nil floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (= const-decl "[T, T -> boolean]" equalities 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (div_mult_pos_le2 formula-decl nil real_props nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (trichotomy formula-decl nil real_axioms nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (phase_sin_q2 0 (phase_sin_q2-1 nil 3264624534 ("" (skosimp*) (("" (lemma "floor_def" ("x" "(2 * x!1) / pi")) (("" (flatten) (("" (name-replace "K1" "floor((2 * x!1) / pi)") (("" (lemma "trich_lt" ("x" "K1" "y" "1")) (("" (split -1) (("1" (assert) (("1" (flatten) (("1" (rewrite "div_mult_pos_le2") (("1" (rewrite "div_mult_pos_lt1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (rewrite "div_mult_pos_lt1") (("2" (rewrite "div_mult_pos_le2") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (assert) (("3" (rewrite "div_mult_pos_le2") (("3" (rewrite "div_mult_pos_lt1") (("3" (assert) (("3" (flatten) (("3" (lemma "both_sides_times_pos_lt1" ("x" "1" "y" "K1" "pz" "pi")) (("3" (assert) (("3" (case "K1=2") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (case "K1>2") (("1" (lemma "both_sides_times_pos_lt1" ("x" "2" "y" "K1" "pz" "pi")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (nnreal 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) (/ 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) (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) (floor_def formula-decl nil floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (= const-decl "[T, T -> boolean]" equalities 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (div_mult_pos_le2 formula-decl nil real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (trich_lt formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (phase_sin_q3 0 (phase_sin_q3-1 nil 3264675279 ("" (skosimp*) (("" (lemma "floor_def" ("x" "(2*x!1)/pi")) (("" (flatten) (("" (name-replace "K1" "floor((2 * x!1) / pi)") (("" (rewrite "div_mult_pos_le2" -1) (("" (lemma "both_sides_times_pos_le1" ("x" "pi" "y" "x!1" "pz" "2")) (("" (replace -1 1 rl) (("" (rewrite "div_mult_pos_lt1" -3) (("" (rewrite "div_mult_pos_lt2" 1) (("" (lemma "trich_lt" ("x" "K1" "y" "2")) (("" (split -1) (("1" (lemma "both_sides_times_pos_lt1" ("x" "K1" "y" "2" "pz" "pi")) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) nil nil)) nil) ("3" (case "3=K1") (("1" (replace -1 * rl) (("1" (assert) nil nil)) nil) ("2" (case "3<K1") (("1" (lemma "both_sides_times_pos_lt1" ("x" "K1" "y" "3" "pz" "pi")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (nnreal 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) (/ 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) (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) (floor_def formula-decl nil floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (= const-decl "[T, T -> boolean]" equalities 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (trich_lt formula-decl nil real_props nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (div_mult_pos_lt2 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (div_mult_pos_le2 formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (phase_sin_q4 0 (phase_sin_q4-1 nil 3264675711 ("" (skosimp*) (("" (lemma "floor_def" ("x" "(2*x!1)/pi")) (("" (flatten) (("" (name-replace "K1" "floor((2 * x!1) / pi)") (("" (lemma "trich_lt" ("x" "K1" "y" "3")) (("" (rewrite "div_mult_pos_le2" -2) (("" (rewrite "div_mult_pos_lt1" -3) (("" (rewrite "div_mult_pos_le1" 1) (("" (split -1) (("1" (lemma "both_sides_times_pos_lt1" ("x" "K1" "y" "3" "pz" "pi")) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (assert) nil nil)) nil) ("3" (case "K1=4") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (case "K1>4") (("1" (lemma "both_sides_times_pos_lt1" ("x" "K1" "y" "4" "pz" "pi")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (nnreal 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) (/ 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) (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) (floor_def formula-decl nil floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (= const-decl "[T, T -> boolean]" equalities 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (div_mult_pos_le2 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (div_mult_pos_le1 formula-decl nil real_props 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) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (trich_lt formula-decl nil real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (phases_sin 0 (phases_sin-1 nil 3264623778 ("" (skosimp*) (("" (rewrite "phase_sin_q1") (("" (rewrite "phase_sin_q2") (("" (rewrite "phase_sin_q3") (("" (rewrite "phase_sin_q4") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((phase_sin_q1 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (phase_sin_q3 formula-decl nil sincos_phase nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (phase_sin_q4 formula-decl nil sincos_phase nil) (phase_sin_q2 formula-decl nil sincos_phase nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (sin_q1_TCC1 0 (sin_q1_TCC1-1 nil 3264686873 ("" (skosimp*) (("" (rewrite "phase_sin_q1") (("" (expand "abs") (("" (assert) nil nil)) nil)) nil)) nil) ((phase_sin_q1 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (sin_q1 0 (sin_q1-1 nil 3264683531 ("" (skosimp*) (("" (expand "sin_phase") (("" (assert) nil nil)) nil)) nil) ((sin_phase const-decl "real_abs_le1" sincos_phase nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (sin_q2_TCC1 0 (sin_q2_TCC1-1 nil 3264686873 ("" (skosimp*) (("" (rewrite "phase_sin_q2") (("" (assert) (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((phase_sin_q2 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (sin_q2 0 (sin_q2-1 nil 3264683552 ("" (skosimp*) (("" (expand "sin_phase") (("" (assert) (("" (rewrite "phase_sin_q2") (("" (flatten) (("" (rewrite "sin_eqv_cos_value" 1) (("1" (lemma "cos_value_neg" ("xc" "x!1-pi/2")) (("1" (replace -1 1) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_phase const-decl "real_abs_le1" sincos_phase nil) (phase_sin_q2 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sin_eqv_cos_value formula-decl nil sincos_quad nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (cos_value_neg formula-decl nil sincos_quad nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (sin_q3_TCC1 0 (sin_q3_TCC1-1 nil 3264686874 ("" (skosimp*) (("" (rewrite "phase_sin_q3") (("" (flatten) (("" (expand "abs") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((phase_sin_q3 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (sin_q3 0 (sin_q3-1 nil 3264683931 ("" (skosimp*) (("" (expand "sin_phase") (("" (assert) nil nil)) nil)) nil) ((sin_phase const-decl "real_abs_le1" sincos_phase nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (sin_q4_TCC1 0 (sin_q4_TCC1-1 nil 3264686875 ("" (skosimp*) (("" (rewrite "phase_sin_q4") (("" (assert) nil nil)) nil)) nil) ((phase_sin_q4 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase 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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (sin_q4 0 (sin_q4-1 nil 3264683957 ("" (skosimp*) (("" (expand "sin_phase") (("" (assert) (("" (rewrite "phase_sin_q4") (("" (lemma "sin_eqv_cos_value" ("xs" "2*pi-x!1")) (("1" (replace -1 1) (("1" (lemma "cos_value_neg" ("xc" "x!1-3*pi/2")) (("1" (replace -1 1) (("1" (propax) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_phase const-decl "real_abs_le1" sincos_phase nil) (phase_sin_q4 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (cos_value_neg formula-decl nil sincos_quad nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (- const-decl "[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) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sin_eqv_cos_value formula-decl nil sincos_quad nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (phase_cos_q1 0 (phase_cos_q1-1 nil 3264616587 ("" (skosimp*) (("" (lemma "floor_def" ("x" "x!1/pi")) (("" (flatten) (("" (name-replace "K1" "floor(x!1/pi)") (("" (rewrite "div_mult_pos_le2" -1) (("" (rewrite "div_mult_pos_lt1" -2) (("" (lemma "trichotomy" ("x" "K1")) (("" (split -1) (("1" (case "K1=1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (case "K1>1") (("1" (lemma "both_sides_times_pos_lt1" ("x" "1" "y" "K1" "pz" "pi")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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 "bool" reals nil) (nnreal 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) (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) (floor_def formula-decl nil floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (= const-decl "[T, T -> boolean]" equalities 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (both_sides_times_pos_lt1 formula-decl nil real_props 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) (trichotomy formula-decl nil real_axioms nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (div_mult_pos_le2 formula-decl nil real_props nil)) shostak)) (phase_cos_q2 0 (phase_cos_q2-1 nil 3264617408 ("" (skosimp*) (("" (typepred "x!1") (("" (replace -2) (("" (lemma "floor_def" ("x" "x!1/pi")) (("" (flatten) (("" (name-replace "K1" "floor(x!1/pi)") (("" (rewrite "div_mult_pos_le2" -1) (("" (lemma "div_mult_pos_lt1" ("z" "x!1" "py" "pi" "x" "K1+1")) (("" (replace -3 -1) (("" (flatten -1) (("" (case "K1<1") (("1" (assert) nil nil) ("2" (case "K1=1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (case "K1>1") (("1" (case "K1=2") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (case "K1>2") (("1" (lemma "both_sides_times_pos_lt1" ("x" "2" "y" "K1" "pz" "pi")) (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (floor_def formula-decl nil floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (= const-decl "[T, T -> boolean]" equalities 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (div_mult_pos_le2 formula-decl nil real_props nil)) shostak)) (phases_cos 0 (phases_cos-1 nil 3264616276 ("" (skosimp*) (("" (rewrite "phase_cos_q1") (("" (rewrite "phase_cos_q2") (("" (assert) nil nil)) nil)) nil)) nil) ((phase_cos_q1 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (phase_cos_q2 formula-decl nil sincos_phase nil)) shostak)) (cos_q1_TCC1 0 (cos_q1_TCC1-1 nil 3264686878 ("" (skosimp*) (("" (rewrite "phase_sin_q1") (("" (assert) nil nil)) nil)) nil) ((phase_sin_q1 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (cos_q1 0 (cos_q1-1 nil 3264684459 ("" (skosimp*) (("" (expand "cos_phase") (("" (assert) (("" (rewrite "phase_sin_q1") (("" (rewrite "phase_cos_q1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((cos_phase const-decl "real_abs_le1" sincos_phase nil) (phase_sin_q1 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (phase_cos_q1 formula-decl nil sincos_phase nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (cos_q2_TCC1 0 (cos_q2_TCC1-1 nil 3264686878 ("" (skosimp*) (("" (rewrite "phase_sin_q2") (("" (flatten) (("" (expand "abs") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((phase_sin_q2 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (cos_q2 0 (cos_q2-1 nil 3264684553 ("" (skosimp*) (("" (expand "cos_phase") (("" (rewrite "phase_sin_q2") (("" (flatten) (("" (rewrite "phase_cos_q1") (("" (assert) (("" (lemma "sin_eqv_cos_value" ("xs" "x!1-pi/2")) (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_eqv_cos_value formula-decl nil sincos_quad nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (phase_cos_q1 formula-decl nil sincos_phase nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal 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) (phase_sin_q2 formula-decl nil sincos_phase nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (cos_q3_TCC1 0 (cos_q3_TCC1-1 nil 3264686878 ("" (skosimp*) (("" (rewrite "phase_sin_q3") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil) ((phase_sin_q3 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (cos_q3 0 (cos_q3-1 nil 3264685624 ("" (skosimp*) (("" (rewrite "phase_sin_q3" -1) (("" (flatten) (("" (expand "cos_phase") (("" (lemma "phase_cos_q1" ("x" "x!1")) (("" (replace -1 1) (("" (assert) (("" (lemma "cos_value_neg" ("xc" "x!1-pi")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((phase_sin_q3 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil) (cos_value_neg formula-decl nil sincos_quad nil) (<= const-decl "bool" reals nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (phase_cos_q1 formula-decl nil sincos_phase nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (cos_q4_TCC1 0 (cos_q4_TCC1-1 nil 3264686878 ("" (skosimp*) (("" (rewrite "phase_sin_q4") (("" (expand "abs") (("" (assert) nil nil)) nil)) nil)) nil) ((phase_sin_q4 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase 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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (cos_q4 0 (cos_q4-1 nil 3264685991 ("" (skosimp*) (("" (expand "cos_phase") (("" (rewrite "phase_sin_q4") (("" (rewrite "phase_cos_q1") (("" (assert) (("" (lemma "sin_value_neg" ("xs" "3*pi/2-x!1")) (("1" (replace -1) (("1" (lemma "sin_eqv_cos_value" ("xs" "3*pi/2-x!1")) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "abs") (("2" (assert) (("2" (expand "<=" -1) (("2" (split -1) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil) (phase_cos_q1 formula-decl nil sincos_phase nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (- const-decl "[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) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sin_value_neg formula-decl nil sincos_quad nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sin_eqv_cos_value formula-decl nil sincos_quad nil) (minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal 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) (phase_sin_q4 formula-decl nil sincos_phase nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (sin_h2_TCC1 0 (sin_h2_TCC1-1 nil 3264838737 ("" (skosimp*) (("" (rewrite "phase_cos_q2") (("" (assert) nil nil)) nil)) nil) ((phase_cos_q2 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (sin_h2 0 (sin_h2-1 nil 3264837795 ("" (skosimp*) (("" (rewrite "phase_cos_q2") (("" (lemma "phases_sin" ("x" "x!1")) (("" (split -1) (("1" (rewrite "phase_sin_q1") (("1" (assert) nil nil)) nil) ("2" (rewrite "phase_sin_q2") (("2" (assert) nil nil)) nil) ("3" (lemma "sin_q3" ("x" "x!1")) (("3" (assert) (("3" (lemma "sin_q1" ("x" "x!1-pi")) (("3" (rewrite "phase_sin_q1") (("3" (rewrite "phase_sin_q3") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (lemma "sin_q4" ("x" "x!1")) (("4" (assert) (("4" (lemma "sin_q2" ("x" "x!1-pi")) (("4" (rewrite "phase_sin_q4") (("4" (rewrite "phase_sin_q2") (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((phase_cos_q2 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (phase_sin_q1 formula-decl nil sincos_phase nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (phase_sin_q2 formula-decl nil sincos_phase nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (real_times_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (phase_sin_q3 formula-decl nil sincos_phase nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (sin_q1 formula-decl nil sincos_phase nil) (sin_q3 formula-decl nil sincos_phase nil) (phase_sin_q4 formula-decl nil sincos_phase nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sin_q2 formula-decl nil sincos_phase nil) (sin_q4 formula-decl nil sincos_phase nil) (phases_sin formula-decl nil sincos_phase nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) shostak)) (sin_h1_TCC1 0 (sin_h1_TCC1-1 nil 3264838765 ("" (skosimp*) (("" (rewrite "phase_cos_q1") (("" (assert) nil nil)) nil)) nil) ((phase_cos_q1 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (sin_h1 0 (sin_h1-1 nil 3264838368 ("" (skosimp*) (("" (lemma "sin_h2" ("x" "x!1+pi")) (("1" (rewrite "phase_cos_q1") (("1" (rewrite "phase_cos_q2") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (rewrite "phase_cos_q1") nil nil)) nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal 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) (sin_h2 formula-decl nil sincos_phase nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (phase_cos_q2 formula-decl nil sincos_phase nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (phase_cos_q1 formula-decl nil sincos_phase nil)) shostak)) (cos_h1 0 (cos_h1-1 nil 3264838539 ("" (skosimp*) (("" (expand "cos_phase") (("" (assert) (("" (rewrite "phase_cos_q1") (("" (rewrite "phase_cos_q1") (("" (rewrite "cos_value_neg") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil) (phase_cos_q1 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (<= const-decl "bool" reals nil) (cos_value_neg formula-decl nil sincos_quad nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (cos_h2 0 (cos_h2-1 nil 3264838643 ("" (skosimp*) (("" (rewrite "phase_cos_q2") (("" (lemma "cos_h1" ("x" "x!1-pi")) (("1" (rewrite "phase_cos_q1") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((phase_cos_q2 formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (phase_cos_q1 formula-decl nil sincos_phase nil) (minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (cos_h1 formula-decl nil sincos_phase nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (sin_phase_neg_TCC1 0 (sin_phase_neg_TCC1-1 nil 3264604314 ("" (skosimp*) (("" (typepred "px!1") (("" (assert) nil nil)) nil)) nil) ((pi const-decl "posreal" atan nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals 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) (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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (sin_phase_neg 0 (sin_phase_neg-1 nil 3264603635 ("" (skosimp*) (("" (typepred "px!1") (("" (hide -1) (("" (expand "sin_phase") (("" (lemma "phases_sin" ("x" "px!1")) (("" (split -1) (("1" (assert) (("1" (lemma "phase_sin_q1" ("x" "px!1")) (("1" (replace -2) (("1" (flatten -1) (("1" (lemma "phase_sin_q4" ("x" "2*pi-px!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "floor_def" ("x" "(2 * px!1) / pi")) (("2" (replace -2) (("2" (flatten -1) (("2" (expand "<=" -1) (("2" (split -1) (("1" (lemma "phase_sin_q3" ("x" "2*pi-px!1")) (("1" (assert) nil nil)) nil) ("2" (lemma "both_sides_times1" ("x" "1" "y" "(2 * px!1) / pi" "n0z" "pi/2")) (("2" (flatten -1) (("2" (replace -3 -2 rl) (("2" (hide -1) (("2" (replace -1 * rl) (("2" (lemma "minus_div2" ("x" "4*pi" "y" "2*px!1" "n0x" "pi")) (("2" (replace -1 * rl) (("2" (replace -2 * rl) (("2" (lemma "div_cancel1" ("x" "4" "n0z" "pi")) (("2" (replace -1) (("2" (rewrite "floor_int" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (lemma "floor_def" ("x" "(2 * px!1) / pi")) (("3" (flatten) (("3" (replace -3) (("3" (rewrite "div_mult_pos_le2" -1) (("3" (rewrite "div_mult_pos_lt1" -2) (("3" (expand "<=" -1) (("3" (split -1) (("1" (lemma "phase_sin_q2" ("x" "2*pi-px!1")) (("1" (assert) nil nil)) nil) ("2" (replace -1 * rl) (("2" (simplify 1) (("2" (lemma "div_cancel1" ("x" "2" "n0z" "pi")) (("2" (replace -1) (("2" (rewrite "floor_int" 1) (("2" (assert) (("2" (lemma "sin_value_neg" ("xs" "px!1-pi")) (("1" (replace -1 1) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert) (("4" (lemma "floor_def" ("x" "(2 * px!1) / pi")) (("4" (flatten) (("4" (replace -3) (("4" (rewrite "div_mult_pos_le2" -1) (("4" (lemma "div_mult_pos_lt1" ("z" "2*px!1" "py" "pi" "x" "4")) (("4" (replace -3 -1) (("4" (flatten -1) (("4" (lemma "phase_sin_q1" ("x" "2*pi-px!1")) (("4" (expand "<=" -3) (("4" (split -3) (("1" (assert) nil nil) ("2" (replace -1 * rl) (("2" (simplify 1) (("2" (rewrite "div_simp" 1) (("2" (rewrite "floor_int" 1) (("2" (simplify 1) (("2" (lemma "both_sides_div1" ("x" "3 * pi" "y" "2 * px!1" "n0z" "2")) (("2" (flatten -1) (("2" (lemma "div_cancel1" ("x" "px!1" "n0z" "2")) (("2" (replace -1) (("2" (replace -4 -3 rl) (("2" (hide -1 -2) (("2" (replace -1 * rl) (("2" (simplify 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pi const-decl "posreal" atan nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals 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) (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) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (sin_phase const-decl "real_abs_le1" sincos_phase nil) (phase_sin_q1 formula-decl nil sincos_phase nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (phase_sin_q4 formula-decl nil sincos_phase nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (floor_def formula-decl nil floor_ceil nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (phase_sin_q3 formula-decl nil sincos_phase nil) (minus_div2 formula-decl nil real_props nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (floor_int formula-decl nil floor_ceil 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) (div_cancel1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (both_sides_times1 formula-decl nil real_props nil) (<= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (phase_sin_q2 formula-decl nil sincos_phase nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields nil) (sin_value_neg formula-decl nil sincos_quad nil) (div_mult_pos_le2 formula-decl nil real_props nil) (div_simp formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (both_sides_div1 formula-decl nil real_props nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (nnreal type-eq-decl nil real_types nil) (phases_sin formula-decl nil sincos_phase nil)) shostak)) (cos_phase_neg 0 (cos_phase_neg-1 nil 3264622320 ("" (skosimp*) (("" (expand "cos_phase") (("" (lemma "phases_cos" ("x" "px!1")) (("" (split -1) (("1" (assert) (("1" (lemma "phase_cos_q1" ("x" "px!1")) (("1" (replace -2 -1) (("1" (flatten -1) (("1" (typepred "px!1") (("1" (hide -1 -4) (("1" (hide -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "phase_cos_q2" ("x" "px!1")) (("2" (assert) (("2" (typepred "px!1") (("2" (assert) (("2" (expand ">=") (("2" (expand "<=" -4) (("2" (split -4) (("1" (lemma "phase_cos_q1" ("x" "2*pi-px!1")) (("1" (assert) nil nil)) nil) ("2" (replace -1 * rl) (("2" (simplify 1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil) (phase_cos_q1 formula-decl nil sincos_phase nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (phase_cos_q2 formula-decl nil sincos_phase nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (phases_cos formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil)) shostak)) (sin_eqv_cos_phase_TCC1 0 (sin_eqv_cos_phase_TCC1-1 nil 3264605210 ("" (skosimp*) (("" (assert) nil nil)) nil) ((posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (sin_eqv_cos_phase_TCC2 0 (sin_eqv_cos_phase_TCC2-1 nil 3264605272 ("" (skosimp*) (("" (typepred "x!1") (("" (assert) nil nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props 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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (sin_eqv_cos_phase 0 (sin_eqv_cos_phase-1 nil 3264610766 ("" (skosimp*) (("" (expand "sin_phase") (("" (expand "cos_phase") (("" (lemma "phases_sin" ("x" "x!1")) (("" (split -1) (("1" (replace -1) (("1" (lemma "phase_sin_q1" ("x" "x!1")) (("1" (replace -2) (("1" (flatten -1) (("1" (lemma "phase_cos_q1" ("x" "pi/2+x!1")) (("1" (assert) (("1" (rewrite "sin_eqv_cos_value") (("1" (expand "abs" 1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1 1) (("2" (simplify 1) (("2" (lemma "phase_sin_q2" ("x" "x!1")) (("2" (replace -2 -1) (("2" (flatten -1) (("2" (assert) (("2" (lemma "phase_cos_q2" ("x" "pi/2+x!1")) (("2" (assert) (("2" (lemma "sin_eqv_cos_value" ("xs" "pi - x!1")) (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (lemma "phase_sin_q3" ("x" "x!1")) (("3" (replace -2 -1) (("3" (flatten -1) (("3" (lemma "phase_cos_q2" ("x" "x!1+pi/2")) (("1" (assert) (("1" (lemma "sin_value_neg" ("xs" "pi-x!1")) (("1" (replace -1 1) (("1" (rewrite "sin_eqv_cos_value" 1) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (expand "<=" -2) (("2" (split -2) (("1" (assert) nil nil) ("2" (replace -1 * rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (assert) (("4" (lemma "phase_sin_q4" ("x" "x!1")) (("4" (replace -2 -1) (("4" (flatten -1) (("4" (assert) (("4" (expand "<=" -1) (("4" (split -1) (("1" (lemma "sin_value_neg" ("xs" "2*pi-x!1")) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (rewrite "sin_eqv_cos_value" 1) (("1" (simplify 1) (("1" (assert) nil nil)) nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (simplify 1) (("2" (rewrite "floor_int" 1) (("2" (rewrite "cos_value_0") (("2" (rewrite "sin_value_pi2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_phase const-decl "real_abs_le1" sincos_phase nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal 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) (phases_sin formula-decl nil sincos_phase nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cos_value_0 formula-decl nil sincos_quad nil) (sin_value_pi2 formula-decl nil sincos_quad nil) (floor_int formula-decl nil floor_ceil 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) (minus_odd_is_odd application-judgement "odd_int" integers nil) (phase_sin_q4 formula-decl nil sincos_phase nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_value_neg formula-decl nil sincos_quad nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (phase_sin_q3 formula-decl nil sincos_phase nil) (phase_sin_q2 formula-decl nil sincos_phase nil) (phase_cos_q2 formula-decl nil sincos_phase nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (phase_cos_q1 formula-decl nil sincos_phase 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sin_eqv_cos_value formula-decl nil sincos_quad nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (phase_sin_q1 formula-decl nil sincos_phase nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (cos_eqv_sin_phase 0 (cos_eqv_sin_phase-1 nil 3264846233 ("" (skosimp*) (("" (case "x!1 < 3 * pi / 2") (("1" (assert) (("1" (lemma "sin_eqv_cos_phase" ("x" "pi/2+x!1")) (("1" (case "x!1<pi") (("1" (assert) (("1" (lemma "div_cancel1" ("x" "pi" "n0z" "2")) (("1" (replace -1) (("1" (replace -3 1) (("1" (hide -1 -3 -4) (("1" (expand "cos_phase") (("1" (rewrite "phase_cos_q1") (("1" (rewrite "phase_cos_q1") (("1" (lemma "cos_value_neg" ("xc" "x!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "pi / 2 - 3 * pi / 2 + x!1 = x!1-pi") (("1" (replace -1) (("1" (replace -2) (("1" (case "x!1>=pi") (("1" (hide -2 -3 1) (("1" (expand "cos_phase") (("1" (rewrite "phase_cos_q1") (("1" (rewrite "phase_cos_q1") (("1" (lemma "cos_value_neg" ("xc" "x!1-pi")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "sin_eqv_cos_phase" ("x" "x!1-3 * pi / 2")) (("2" (assert) (("2" (replace -1 2) (("2" (case "x!1>=3*pi/2") (("1" (case "pi / 2 - 3 * pi / 2 + x!1 = x!1-pi") (("1" (replace -1) (("1" (hide -1 -3 1) (("1" (expand "cos_phase") (("1" (rewrite "phase_cos_q1") (("1" (rewrite "phase_cos_q1") (("1" (lemma "cos_value_neg" ("xc" "x!1-pi")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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_eqv_cos_phase formula-decl nil sincos_phase nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (phase_cos_q1 formula-decl nil sincos_phase nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (cos_value_neg formula-decl nil sincos_quad nil) (<= const-decl "bool" reals nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel1 formula-decl nil real_props 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) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (sin_phase_inv_TCC1 0 (sin_phase_inv_TCC1-1 nil 3264852379 ("" (skosimp*) (("" (assert) nil nil)) nil) ((posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (sin_phase_inv_TCC2 0 (sin_phase_inv_TCC2-1 nil 3264852379 ("" (skosimp*) (("" (assert) nil nil)) nil) ((real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (sin_phase_inv 0 (sin_phase_inv-1 nil 3264852009 ("" (skosimp*) (("" (rewrite "sin_eqv_cos_phase") (("" (case "x!1<pi") (("1" (assert) (("1" (rewrite "cos_eqv_sin_phase") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (case "x!1 < 3 * pi / 2") (("1" (assert) (("1" (rewrite "cos_eqv_sin_phase") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (rewrite "cos_eqv_sin_phase") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sin_eqv_cos_phase formula-decl nil sincos_phase 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) (nnreal type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (cos_eqv_sin_phase formula-decl nil sincos_phase 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)) shostak)) (cos_phase_inv 0 (cos_phase_inv-1 nil 3264852196 ("" (skosimp*) (("" (case "x!1<pi") (("1" (rewrite "cos_eqv_sin_phase") (("1" (assert) (("1" (rewrite "sin_eqv_cos_phase") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "cos_eqv_sin_phase") (("2" (case "x!1 < 3 * pi / 2") (("1" (assert) (("1" (rewrite "sin_eqv_cos_phase") (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (rewrite "sin_eqv_cos_phase") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (sin_eqv_cos_phase formula-decl nil sincos_phase 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cos_eqv_sin_phase formula-decl nil sincos_phase nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (sin_phase_3pi2_TCC1 0 (sin_phase_3pi2_TCC1-1 nil 3264621137 ("" (assert) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (sin_phase_3pi2 0 (sin_phase_3pi2-1 nil 3264621852 ("" (expand "sin_phase") (("" (lemma "div_cancel1" ("x" "3*pi" "n0z" "2")) (("" (replace -1) (("" (lemma "div_cancel2" ("x" "3" "n0z" "pi")) (("" (replace -1) (("" (rewrite "floor_int" 1) (("" (assert) (("" (rewrite "sin_value_pi2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pi const-decl "posreal" atan 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) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (div_cancel1 formula-decl nil real_props nil) (div_cancel2 formula-decl nil real_props 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) (floor_int formula-decl nil floor_ceil nil) (sin_value_pi2 formula-decl nil sincos_quad nil) (minus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sin_phase const-decl "real_abs_le1" sincos_phase nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (sin_phase_0 0 (sin_phase_0-1 nil 3264603991 ("" (expand "sin_phase") (("" (rewrite "sin_value_0") (("" (lemma "floor_int" ("i" "0")) (("" (replace -1) (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((sin_value_0 formula-decl nil sincos_quad nil) (floor_int formula-decl nil floor_ceil 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) (sin_phase const-decl "real_abs_le1" sincos_phase nil)) shostak)) (sin_phase_pi4_TCC1 0 (sin_phase_pi4_TCC1-1 nil 3264605320 ("" (assert) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (sin_phase_pi4 0 (sin_phase_pi4-1 nil 3264620487 ("" (rewrite "sin_phase") (("" (rewrite "sin_value_pi4") (("" (lemma "div_cancel1" ("x" "2/4" "n0z" "pi")) (("" (replace -1 1) (("" (lemma "floor_val" ("i" "2" "j" "4" "k" "0")) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((sin_value_pi4 formula-decl nil sincos_quad nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_times_even_is_even application-judgement "even_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (int nonempty-type-eq-decl nil integers 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) (floor_val formula-decl nil floor_ceil nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel1 formula-decl nil real_props nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal 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) (sin_phase const-decl "real_abs_le1" sincos_phase nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (sin_phase_pi2_TCC1 0 (sin_phase_pi2_TCC1-1 nil 3264605328 ("" (assert) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (sin_phase_pi2 0 (sin_phase_pi2-1 nil 3264621187 ("" (expand "sin_phase") (("" (lemma "div_cancel1" ("x" "pi" "n0z" "2")) (("" (replace -1) (("" (rewrite "div_simp") (("" (rewrite "floor_int") (("" (rewrite "sin_value_pi2") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pi const-decl "posreal" atan 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) (nonzero_real nonempty-type-eq-decl nil reals nil) (/= const-decl "boolean" notequal 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) (div_cancel1 formula-decl nil real_props nil) (div_simp formula-decl nil real_props nil) (sin_value_pi2 formula-decl nil sincos_quad nil) (floor_int formula-decl nil floor_ceil 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) (sin_phase const-decl "real_abs_le1" sincos_phase nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (cos_phase_0 0 (cos_phase_0-1 nil 3264621060 ("" (expand "cos_phase") (("" (rewrite "floor_int") (("1" (rewrite "cos_value_0") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ((AND const-decl "[bool, bool -> bool]" booleans nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (floor_int formula-decl nil floor_ceil 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) (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) (pi const-decl "posreal" atan nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (cos_value_0 formula-decl nil sincos_quad nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil)) shostak)) (cos_phase_pi4 0 (cos_phase_pi4-1 nil 3264621363 ("" (expand "cos_phase") (("" (rewrite "div_div2" 1) (("" (lemma "div_cancel1" ("x" "1/4" "n0z" "pi")) (("" (replace -1 1) (("" (lemma "floor_val" ("i" "1" "j" "4" "k" "0")) (("" (assert) (("" (rewrite "cos_value_pi4") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((div_div2 formula-decl nil real_props 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) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-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) (pi const-decl "posreal" atan nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (sqrt_pos application-judgement "posreal" sqrt "reals/") (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (int_times_even_is_even application-judgement "even_int" integers nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (cos_value_pi4 formula-decl nil sincos_quad nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (int nonempty-type-eq-decl nil integers 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) (floor_val formula-decl nil floor_ceil nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (div_cancel1 formula-decl nil real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (cos_phase_pi2 0 (cos_phase_pi2-1 nil 3264621525 ("" (expand "cos_phase") (("" (rewrite "div_div2") (("" (lemma "floor_val" ("i" "1" "j" "2" "k" "0")) (("" (lemma "div_cancel1" ("x" "1/2" "n0z" "pi")) (("" (rewrite "div_div2") (("" (replace -1 1) (("" (assert) (("" (rewrite "cos_value_pi2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((div_div2 formula-decl nil real_props 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) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-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) (pi const-decl "posreal" atan nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (div_cancel1 formula-decl nil real_props nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (cos_value_pi2 formula-decl nil sincos_quad nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (int_times_even_is_even application-judgement "even_int" integers nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (int nonempty-type-eq-decl nil integers 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) (floor_val formula-decl nil floor_ceil nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (cos_phase_pi_TCC1 0 (cos_phase_pi_TCC1-1 nil 3264605342 ("" (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)) (cos_phase_pi 0 (cos_phase_pi-1 nil 3264621665 ("" (expand "cos_phase") (("" (rewrite "cos_value_pi") nil nil)) nil) ((cos_value_pi formula-decl nil sincos_quad nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil)) shostak)) (sin_phase_asin_TCC1 0 (sin_phase_asin_TCC1-1 nil 3264625616 ("" (skosimp*) (("" (typepred "xa!1") (("" (expand "abs") (("" (assert) (("" (lemma "asin_strict_increasing") (("" (expand "strict_increasing?") (("" (inst-cp - "xa!1" "0") (("1" (rewrite "asin_0") (("1" (case "xa!1=-1") (("1" (replace -1) (("1" (rewrite "asin_minus1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst - "-1" "xa!1") (("1" (rewrite "asin_minus1") (("1" (assert) nil nil)) nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_abs_le1 nonempty-type-eq-decl nil asin nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals 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) (asin_strict_increasing formula-decl nil asin nil) (= const-decl "[T, T -> boolean]" equalities nil) (asin_minus1 formula-decl nil asin nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (asin_0 formula-decl nil asin nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) shostak)) (sin_phase_asin_TCC2 0 (sin_phase_asin_TCC2-1 nil 3264628114 ("" (skosimp*) (("" (lemma "asin_strict_increasing") (("" (expand "strict_increasing?") (("" (case "xa!1=0") (("1" (replace -1) (("1" (rewrite "asin_0") (("1" (assert) (("1" (typepred "pi") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst - "0" "xa!1") (("1" (rewrite "asin_0") (("1" (assert) (("1" (typepred "asin(xa!1)") (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((asin_strict_increasing formula-decl nil asin nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (asin_0 formula-decl nil asin nil) (NOT const-decl "[bool -> bool]" 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) (pi const-decl "posreal" atan nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/")) shostak)) (sin_phase_asin 0 (sin_phase_asin-1 nil 3264628447 ("" (skosimp*) (("" (case "xa!1<0") (("1" (assert) (("1" (expand "sin_phase") (("1" (typepred "asin(xa!1)") (("1" (lemma "asin_strict_increasing") (("1" (expand "strict_increasing?") (("1" (inst-cp - "xa!1" "0") (("1" (rewrite "asin_0") (("1" (assert) (("1" (lemma "phase_sin_q4" ("x" "2*pi+asin(xa!1)")) (("1" (assert) (("1" (lemma "sin_value_neg" ("xs" "asin(xa!1)")) (("1" (replace -1 1) (("1" (rewrite "sin_value_asin" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "sin_phase") (("2" (typepred "asin(xa!1)") (("2" (lemma "asin_strict_increasing") (("2" (expand "strict_increasing?") (("2" (case "xa!1=0") (("1" (replace -1) (("1" (rewrite "asin_0") (("1" (rewrite "sin_value_0") (("1" (assert) (("1" (rewrite "floor_int" 2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst-cp - "0" "xa!1") (("2" (inst - "xa!1" "1") (("2" (rewrite "asin_1") (("2" (rewrite "asin_0") (("2" (assert) (("2" (expand "<=" -4) (("2" (split -4) (("1" (lemma "phase_sin_q1" ("x" "asin(xa!1)")) (("1" (assert) (("1" (rewrite "sin_value_asin") nil nil)) nil)) nil) ("2" (case "floor((2 * asin(xa!1)) / pi) = 1") (("1" (assert) (("1" (lemma "asin_1") (("1" (lemma "asin_bij") (("1" (expand "bijective?") (("1" (expand "injective?") (("1" (flatten) (("1" (inst - "xa!1" "1") (("1" (assert) (("1" (replace -5) (("1" (rewrite "sin_value_pi2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4) (("2" (replace -1 1) (("2" (lemma "div_cancel1" ("x" "pi" "n0z" "2")) (("2" (replace -1) (("2" (rewrite "div_simp" 1) (("2" (rewrite "floor_int" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_abs_le1 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (real_times_real_is_real application-judgement "real" reals nil) (sin_phase const-decl "real_abs_le1" sincos_phase nil) (asin_strict_increasing formula-decl nil asin nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (sin_value_asin formula-decl nil sincos_quad nil) (sin_value_neg formula-decl nil sincos_quad nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal type-eq-decl nil real_types nil) (phase_sin_q4 formula-decl nil sincos_phase nil) (asin_0 formula-decl nil asin nil) (strict_increasing? const-decl "bool" real_fun_preds "reals/") (NOT const-decl "[bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields 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) (pi const-decl "posreal" atan nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (asin const-decl "real_abs_le_pi2" asin nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (floor_int formula-decl nil floor_ceil 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) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" 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) (sin_value_0 formula-decl nil sincos_quad nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (bijective? const-decl "bool" functions nil) (sin_value_pi2 formula-decl nil sincos_quad nil) (injective? const-decl "bool" functions nil) (asin_bij formula-decl nil asin nil) (real_minus_real_is_real application-judgement "real" reals nil) (div_simp formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_cancel1 formula-decl nil real_props nil) (phase_sin_q1 formula-decl nil sincos_phase nil) (asin_1 formula-decl nil asin nil)) shostak)) (cos_phase_acos_TCC1 0 (cos_phase_acos_TCC1-1 nil 3264625616 ("" (skosimp*) (("" (typepred "acos(xa!1)") (("" (assert) nil nil)) nil)) nil) ((acos const-decl "nnreal_le_pi" acos nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (pi const-decl "posreal" atan 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) (nnreal type-eq-decl nil real_types nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (>= const-decl "bool" reals 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props 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)) (cos_phase_acos 0 (cos_phase_acos-1 nil 3264677087 ("" (skosimp*) (("" (typepred "xa!1") (("" (typepred "acos(xa!1)") (("" (expand "cos_phase") (("" (rewrite "phase_cos_q1" 1) (("" (expand ">=") (("" (replace -1) (("" (expand "<=" -2) (("" (split) (("1" (assert) (("1" (rewrite "cos_value_acos") nil nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (rewrite "cos_value_pi") (("2" (lemma "acos_bij") (("2" (expand "bijective?") (("2" (expand "injective?") (("2" (flatten) (("2" (inst - "-1" "xa!1") (("1" (rewrite "acos_minus1") (("1" (assert) nil nil)) nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_abs_le1 nonempty-type-eq-decl nil asin nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals 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_phase const-decl "real_abs_le1" sincos_phase nil) (cos_value_pi formula-decl nil sincos_quad nil) (bijective? const-decl "bool" functions nil) (acos_minus1 formula-decl nil acos nil) (injective? const-decl "bool" functions nil) (acos_bij formula-decl nil acos nil) (real_minus_real_is_real application-judgement "real" reals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cos_value_acos formula-decl nil sincos_quad nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (< const-decl "bool" reals nil) (phase_cos_q1 formula-decl nil sincos_phase 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) (>= const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types 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) (pi const-decl "posreal" atan nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (acos const-decl "nnreal_le_pi" acos nil)) shostak)) (sin2_cos2_phase 0 (sin2_cos2_phase-1 nil 3264625668 ("" (skosimp*) (("" (expand "sin_phase") (("" (expand "cos_phase") (("" (lemma "phases_sin" ("x" "x!1")) (("" (split -1) (("1" (lemma "phase_sin_q1" ("x" "x!1")) (("1" (replace -2) (("1" (flatten -1) (("1" (lemma "phase_cos_q1" ("x" "x!1")) (("1" (assert) (("1" (lemma "sin2_cos2_value" ("q1" "x!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "phase_sin_q2" ("x" "x!1")) (("2" (replace -2) (("2" (flatten -1) (("2" (lemma "phase_cos_q1" ("x" "x!1")) (("2" (assert) (("2" (lemma "sin2_cos2_value" ("q1" "pi-x!1")) (("2" (rewrite "cos_value_neg" -1) (("2" (rewrite "sq_neg") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "phase_sin_q3" ("x" "x!1")) (("3" (replace -2) (("3" (flatten -1) (("3" (lemma "phase_cos_q2" ("x" "x!1")) (("3" (assert) (("3" (lemma "sin2_cos2_value" ("q1" "x!1-pi")) (("3" (lemma "cos_value_neg" ("xc" "x!1-pi")) (("3" (replace -1 1) (("3" (rewrite "sq_neg" 1) (("3" (assert) (("3" (rewrite "sq_neg" 1) (("3" (expand "abs" 1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (lemma "phase_sin_q4" ("x" "x!1")) (("4" (replace -2) (("4" (flatten -1) (("4" (lemma "phase_cos_q2" ("x" "x!1")) (("4" (assert) (("4" (lemma "sin2_cos2_value" ("q1" "2*pi-x!1")) (("4" (assert) (("4" (rewrite "sq_neg" 1) (("4" (expand "abs" 1) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sin_phase const-decl "real_abs_le1" sincos_phase nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal 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) (phases_sin formula-decl nil sincos_phase nil) (phase_sin_q4 formula-decl nil sincos_phase nil) (phase_sin_q3 formula-decl nil sincos_phase nil) (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (phase_cos_q2 formula-decl nil sincos_phase nil) (phase_sin_q2 formula-decl nil sincos_phase nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (cos_value_neg formula-decl nil sincos_quad nil) (minus_real_is_real application-judgement "real" reals nil) (sq_neg formula-decl nil sq "reals/") (- const-decl "[numfield -> numfield]" number_fields nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (phase_sin_q1 formula-decl nil sincos_phase nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_quad1_closed nonempty-type-eq-decl nil sincos_quad 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 "bool" reals nil) (sin2_cos2_value formula-decl nil sincos_quad nil) (phase_cos_q1 formula-decl nil sincos_phase nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil)) shostak)) (sin_phase_diff_TCC1 0 (sin_phase_diff_TCC1-1 nil 3264625616 ("" (skosimp*) (("" (typepred "x!1") (("" (typepred "y!1") (("" (assert) nil nil)) nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (sin_phase_diff_TCC2 0 (sin_phase_diff_TCC2-1 nil 3264628358 ("" (skosimp*) (("" (typepred "x!1") (("" (typepred "y!1") (("" (assert) nil nil)) nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (sin_phase_diff 0 (sin_phase_diff-1 nil 3264836972 ("" (case "FORALL (x,y:{x:nnreal|x<pi}): sin_phase(x) * cos_phase(y) - cos_phase(x) * sin_phas IF x - y < 0 THEN sin_phase(x - y + 2 * pi) ELSE sin_phase(x - y) ENDIF") (("1" (skosimp*) (("1" (lemma "phases_cos" ("x" "x!1")) (("1" (lemma "phases_cos" ("x" "y!1")) (("1" (split -1) (("1" (split -2) (("1" (inst - "x!1" "y!1") (("1" (rewrite "phase_cos_q1" -2) (("1" (case "x!1 - y!1 < 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (rewrite "phase_cos_q1" -1) (("2" (rewrite "phase_cos_q1" -2) nil nil)) nil) ("3" (rewrite "phase_cos_q1" -1) nil nil)) nil) ("2" (inst - "x!1-pi" "y!1") (("1" (lemma "cos_h2" ("x" "x!1")) (("1" (lemma "sin_h2" ("x" "x!1")) (("1" (assert) (("1" (replace -1 1) (("1" (replace -2 1) (("1" (case "x!1<y!1") (("1" (assert) (("1" (lemma "sin_h1" ("x" "pi - y!1 + x!1")) (("1" (rewrite "phase_cos_q1") (("1" (rewrite "phase_cos_q1") (("1" (rewrite "phase_cos_q2") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "phase_cos_q2") nil nil)) nil) ("2" (rewrite "phase_cos_q2") (("2" (rewrite "phase_cos_q1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "x!1-y!1<pi") (("1" (assert) (("1" (lemma "phase_cos_q1" ("x" "x!1-y!1")) (("1" (replace -2 -1) (("1" (case "0 <= x!1-y!1") (("1" (replace -1 -2) (("1" (flatten -2) (("1" (lemma "sin_h1" ("x" "x!1-y!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "phase_cos_q2" ("x" "x!1-y!1")) (("2" (assert) (("2" (lemma "sin_h2" ("x" "x!1-y!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_cos_q1" -2) nil nil) ("3" (rewrite "phase_cos_q2" -1) (("3" (assert) nil nil)) nil)) nil)) nil) ("2" (split -2) (("1" (inst - "x!1" "y!1-pi") (("1" (lemma "sin_h2" ("x" "y!1")) (("1" (lemma "cos_h1" ("x" "x!1")) (("1" (assert) (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (rewrite "phase_cos_q1" -1) (("1" (rewrite "phase_cos_q2" -2) (("1" (assert) (("1" (lemma "cos_h2" ("x" "y!1")) (("1" (rewrite "phase_cos_q2" -1) (("1" (replace -1) (("1" (hide -1) (("1" (case "pi - y!1 + x!1 < 0") (("1" (assert) (("1" (lemma "sin_h2" ("x" "3 * pi - y!1 + x!1")) (("1" (rewrite "phase_cos_q2" -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "sin_h1" ("x" "pi - y!1 + x!1")) (("2" (rewrite "phase_cos_q1" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_cos_q2" -2) (("2" (assert) nil nil)) nil) ("3" (rewrite "phase_cos_q1" -1) nil nil)) nil) ("2" (inst - "x!1-pi" "y!1-pi") (("1" (lemma "sin_h2" ("x" "x!1")) (("1" (lemma "cos_h2" ("x" "x!1")) (("1" (lemma "cos_h2" ("x" "y!1")) (("1" (lemma "sin_h2" ("x" "y!1")) (("1" (assert) (("1" (replace -1) (("1" (replace -2) (("1" (replace -3) (("1" (replace -4) (("1" (hide (-1 -2 -3 -4)) (("1" (case "x!1<y!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_cos_q2" -2) (("2" (assert) nil nil)) nil) ("3" (rewrite "phase_cos_q2" -1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (typepred "x!1") (("2" (typepred "y!1") (("2" (expand "cos_phase") (("2" (rewrite "phase_cos_q1") (("2" (rewrite "phase_cos_q1") (("2" (lemma "phases_sin" ("x" "x!1")) (("2" (split -1) (("1" (lemma "sin_q1" ("x" "x!1")) (("1" (assert) (("1" (replace -1) (("1" (lemma "phases_sin" ("x" "y!1")) (("1" (split -1) (("1" (lemma "sin_q1" ("x" "y!1")) (("1" (assert) (("1" (replace -1) (("1" (lemma "sin_value_diff" ("q1" "x!1" "q2" "y!1")) (("1" (replace -1 1 rl) (("1" (case "x!1-y!1<0") (("1" (assert) (("1" (lemma "phase_sin_q4" ("x" "2 * pi - y!1 + x!1")) (("1" (rewrite "phase_sin_q1" -5) (("1" (rewrite "phase_sin_q1" -7) (("1" (assert) (("1" (lemma "sin_q4" ("x" "2 * pi - y!1 + x!1")) (("1" (assert) (("1" (replace -1 1) (("1" (replace -1 1 rl) (("1" (lemma "sin_phase_neg" ("px" "y!1-x!1")) (("1" (replace -1 1) (("1" (lemma "sin_value_neg" ("xs" "y!1-x!1")) (("1" (replace -1 1) (("1" (lemma "sin_q1" ("x" "y!1-x!1")) (("1" (rewrite "phase_sin_q1" -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "sin_q1" ("x" "x!1-y!1")) (("2" (rewrite "phase_sin_q1" -1) (("2" (assert) (("2" (rewrite "phase_sin_q1" -3) (("2" (rewrite "phase_sin_q1" -4) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_sin_q1" -2) (("2" (assert) nil nil)) nil) ("3" (rewrite "phase_sin_q1" -4) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (case "x!1<pi/2") (("1" (case "pi/2<=y!1") (("1" (hide -5 -8) (("1" (lemma "sin_q2" ("x" "y!1")) (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "sin_phase_neg" ("px" "y!1-x!1")) (("1" (replace -1 1) (("1" (hide -1) (("1" (case "y!1-x!1<pi/2") (("1" (lemma "sin_q1" ("x" "y!1-x!1")) (("1" (rewrite "phase_sin_q1" -1) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (case "cos_value(y!1) = -sin_value(y!1 - pi / 2)") (("1" (replace -1 1) (("1" (hide -1) (("1" (lemma "cos_value_diff" ("q1" "x!1" "q2" "y!1-pi/2")) (("1" (assert) (("1" (lemma "sin_eqv_cos_quad" ("q1" "y!1-x!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -6 1)) (("2" (lemma "cos_value_neg" ("xc" "y!1")) (("2" (lemma "cos_eqv_sin_quad" ("q1" "pi-y!1")) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (expand "abs" 1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sin_q2" ("x" "y!1-x!1")) (("2" (rewrite "phase_sin_q2" -1) (("2" (assert) (("2" (replace -1 2) (("2" (hide -1) (("2" (case "cos_value(y!1) = -sin_value(y!1 - pi / 2)") (("1" (replace -1 2) (("1" (lemma "cos_value_diff" ("q1" "x!1" "q2" "y!1-pi/2")) (("1" (assert) (("1" (case "pi / 2 - y!1 + x!1 < 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 -5 1)) (("2" (lemma "cos_value_neg" ("xc" "y!1")) (("2" (lemma "cos_eqv_sin_quad" ("q1" "pi-y!1")) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (expand "abs" 1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_sin_q2" -2) nil nil)) nil) ("2" (rewrite "phase_sin_q1" -2) nil nil)) nil)) nil) ("3" (rewrite "phase_sin_q3" -1) nil nil) ("4" (rewrite "phase_sin_q4" -1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sin_q2" ("x" "x!1")) (("2" (assert) (("2" (replace -1 1) (("2" (case "pi/2<= x!1") (("1" (hide -6 -2) (("1" (lemma "phases_sin" ("x" "y!1")) (("1" (split -1) (("1" (case "y!1<pi/2") (("1" (hide -6) (("1" (assert) (("1" (case "cos_value(x!1) = -sin_value(x!1 - pi / 2)") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sin_q1" ("x" "y!1")) (("1" (assert) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "cos_value_diff" ("q1" "x!1-pi/2" "q2" "y!1")) (("1" (case "x!1 - pi / 2 - y!1 < 0") (("1" (assert) (("1" (replace -2 1 rl) (("1" (hide -2) (("1" (lemma "sin_q1" ("x" "x!1-y!1")) (("1" (rewrite "phase_sin_q1" -1) (("1" (rewrite "sin_eqv_cos_quad" -1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1 2 rl) (("2" (hide -1) (("2" (lemma "sin_q2" ("x" "x!1-y!1")) (("2" (rewrite "phase_sin_q2" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 -6 1)) (("2" (lemma "cos_value_neg" ("xc" "x!1")) (("2" (lemma "cos_eqv_sin_quad" ("q1" "pi-x!1")) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (expand "abs" 1) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_sin_q1" -1) nil nil)) nil) ("2" (case "pi/2<= y!1") (("1" (hide -5) (("1" (lemma "sin_q2" ("x" "y!1")) (("1" (assert) (("1" (replace -1 1) (("1" (hide -1) (("1" (case "FORALL (x:real): pi/2<=x & x < pi => cos_value(x) = -sin_value(x-pi/2)") (("1" (inst-cp - "x!1") (("1" (inst - "y!1") (("1" (assert) (("1" (replace -1) (("1" (replace -2) (("1" (lemma "sin_value_diff" ("q1" "x!1-pi/2" "q2" "y!1-pi/2")) (("1" (case "x!1<y!1") (("1" (lemma "sin_phase_neg" ("px" "y!1-x!1")) (("1" (assert) (("1" (replace -1 1) (("1" (lemma "sin_q1" ("x" "y!1-x!1")) (("1" (rewrite "phase_sin_q1" -1) (("1" (lemma "sin_value_neg" ("xs" "y!1-x!1")) (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) (("2" (lemma "sin_q1" ("x" "x!1-y!1")) (("2" (rewrite "phase_sin_q1" -1) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "cos_value_neg" ("xc" "x!2")) (("1" (lemma "cos_eqv_sin_quad" ("q1" "pi-x!2")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "abs" 1) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_sin_q2" -1) nil nil)) nil) ("3" (rewrite "phase_sin_q3" -1) nil nil) ("4" (rewrite "phase_sin_q4" -1) nil nil)) nil)) nil)) nil) ("2" (rewrite "phase_sin_q2" -2) nil nil)) nil)) nil)) nil)) nil) ("3" (rewrite "phase_sin_q3" -1) nil nil) ("4" (rewrite "phase_sin_q4" -1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (hide 2) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil) ((phase_sin_q3 formula-decl nil sincos_phase nil) (sin_q2 formula-decl nil sincos_phase nil) (phase_sin_q2 formula-decl nil sincos_phase nil) (cos_eqv_sin_quad formula-decl nil sincos_quad nil) (cos_value_neg formula-decl nil sincos_quad nil) (cos_value_diff formula-decl nil sincos_quad nil) (sin_eqv_cos_quad formula-decl nil sincos_quad nil) (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]" sincos_quad nil) (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (phase_sin_q1 formula-decl nil sincos_phase nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (sin_value_neg formula-decl nil sincos_quad nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sin_phase_neg formula-decl nil sincos_phase nil) (sin_q4 formula-decl nil sincos_phase nil) (phase_sin_q4 formula-decl nil sincos_phase nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nnreal_quad1_closed nonempty-type-eq-decl nil sincos_quad nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (sin_value_diff formula-decl nil sincos_quad nil) (sin_q1 formula-decl nil sincos_phase nil) (phases_sin formula-decl nil sincos_phase nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (cos_h1 formula-decl nil sincos_phase nil) (phase_cos_q1 formula-decl nil sincos_phase nil) (real_times_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (y!1 skolem-const-decl "trig_phase" sincos_phase nil) (x!1 skolem-const-decl "trig_phase" sincos_phase nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (cos_h2 formula-decl nil sincos_phase nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (phase_cos_q2 formula-decl nil sincos_phase nil) (sin_h1 formula-decl nil sincos_phase nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sin_h2 formula-decl nil sincos_phase nil) (phases_cos formula-decl nil sincos_phase nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals 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) (nnreal 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) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil) (= const-decl "[T, T -> boolean]" equalities 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) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (sin_phase const-decl "real_abs_le1" sincos_phase nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (cos_phase_sum_TCC1 0 (cos_phase_sum_TCC1-1 nil 3264625616 ("" (skosimp*) (("" (typepred "x!1") (("" (typepred "y!1") (("" (assert) nil nil)) nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals 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) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (cos_phase_sum 0 (cos_phase_sum-1 nil 3264629773 ("" (case "FORALL (x,y:{x:nnreal|x<pi}): cos_phase(x) * cos_phase(y) - sin_phase(x) * sin_phas (("1" (skosimp*) (("1" (lemma "phases_cos" ("x" "x!1")) (("1" (lemma "phases_cos" ("x" "y!1")) (("1" (split -2) (("1" (split -2) (("1" (case "x!1<pi") (("1" (case "y!1<pi") (("1" (inst - "x!1" "y!1") (("1" (assert) nil nil)) nil) ("2" (rewrite "phase_cos_q1" -2) nil nil)) nil) ("2" (rewrite "phase_cos_q1" -2) nil nil)) nil) ("2" (case "pi<=y!1") (("1" (case "x!1<pi") (("1" (inst - "x!1" "y!1-pi") (("1" (case "cos_phase(y!1 - pi) = -cos_phase(y!1)") (("1" (case "sin_phase(y!1 - pi) = -sin_phase(y!1)") (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (case "x!1+y!1<2*pi") (("1" (assert) (("1" (case "cos_phase(x!1 + y!1)=-cos_phase(x!1 - pi + y!1)") (("1" (assert) nil nil) ("2" (hide -6 2) (("2" (rewrite "cos_phase_inv" 1) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "cos_phase_inv" ("x" "x!1 - pi + y!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "sin_phase_inv" 1) nil nil)) nil) ("3" (assert) nil nil)) nil) ("2" (hide 2) (("2" (rewrite "cos_phase_inv" 1) nil nil)) nil) ("3" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (rewrite "phase_cos_q1" -3) nil nil)) nil) ("2" (rewrite "phase_cos_q2" -1) nil nil)) nil)) nil) ("2" (case "pi<=x!1") (("1" (split -3) (("1" (case "y!1< pi") (("1" (case "x!1 + y!1 < 2 * pi") (("1" (assert) (("1" (inst - "x!1-pi" "y!1") (("1" (lemma "cos_phase_inv" ("x" "x!1-pi")) (("1" (lemma "sin_phase_inv" ("x" "x!1-pi")) (("1" (lemma "cos_phase_inv" ("x" "x!1+y!1")) (("1" (assert) (("1" (replace -2) (("1" (replace -3) (("1" (replace -1) (("1" (replace -9 1 rl) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst - "x!1-pi" "y!1") (("1" (lemma "cos_phase_inv" ("x" "x!1-pi")) (("1" (lemma "sin_phase_inv" ("x" "x!1-pi")) (("1" (lemma "cos_phase_inv" ("x" "x!1+y!1-pi")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (rewrite "phase_cos_q1" -1) nil nil)) nil) ("2" (case "pi<=y!1") (("1" (inst - "x!1-pi" "y!1-pi") (("1" (assert) (("1" (lemma "sin_phase_inv" ("x" "x!1")) (("1" (lemma "cos_phase_inv" ("x" "x!1")) (("1" (lemma "sin_phase_inv" ("x" "y!1")) (("1" (lemma "cos_phase_inv" ("x" "y!1")) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil) ("2" (rewrite "phase_cos_q2" -1) nil nil)) nil)) nil) ("2" (rewrite "phase_cos_q2" -1) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (lemma "phases_sin" ("x" "x!1")) (("2" (split -1) (("1" (case "x!1<pi/2") (("1" (lemma "phases_sin" ("x" "y!1")) (("1" (split -1) (("1" (case "y!1<pi/2") (("1" (lemma "sin_q1" ("x" "x!1")) (("1" (lemma "sin_q1" ("x" "y!1")) (("1" (lemma "cos_q1" ("x" "x!1")) (("1" (lemma "cos_q1" ("x" "y!1")) (("1" (assert) (("1" (replace -1) (("1" (replace -2) (("1" (replace -3) (("1" (replace -4) (("1" (hide -1 -2 -3 -4) (("1" (lemma "cos_value_sum" ("q1" "x!1" "q2" "y!1")) (("1" (replace -1 1 rl) (("1" (hide -1) (("1" (expand "cos_phase" 1) (("1" (rewrite "phase_cos_q1" 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_sin_q1" -1) nil nil)) nil) ("2" (case "pi/2<= y!1") (("1" (lemma "sin_q1" ("x" "x!1")) (("1" (lemma "cos_q1" ("x" "x!1")) (("1" (lemma "sin_q2" ("x" "y!1")) (("1" (lemma "cos_q2" ("x" "y!1")) (("1" (assert) (("1" (replace -1) (("1" (replace -2) (("1" (replace -3) (("1" (replace -4) (("1" (hide -1 -2 -3 -4) (("1" (lemma "sin_value_sum" ("q1" "x!1" "q2" "y!1-pi/2")) (("1" (expand "cos_phase" 1) (("1" (rewrite "phase_cos_q1" 1) (("1" (lemma "trich_lt" ("x" "x!1+y!1" "y" "pi")) (("1" (split -1) (("1" (assert) (("1" (lemma "sin_eqv_cos_value" ("xs" "x!1 - pi / 2 + y!1")) (("1" (assert) nil nil) ("2" (expand "abs" 1) (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (assert) (("2" (lemma "sin_value_pi2") (("2" (case "x!1=pi-y!1") (("1" (replace -1) (("1" (simplify (-4 1)) (("1" (rewrite "cos_value_pi") (("1" (replace -2) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (assert) (("3" (lemma "cos_value_neg" ("xc" "x!1+y!1-pi")) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "phase_sin_q2" -1) nil nil)) nil) ("3" (rewrite "phase_sin_q3" -1) nil nil) ("4" (rewrite "phase_sin_q4" -1) nil nil)) nil)) nil) ("2" (rewrite "phase_sin_q1" -1) nil nil)) nil) ("2" (case "pi/2<=x!1") (("1" (lemma "phases_sin" ("x" "y!1")) (("1" (split -1) (("1" (case "y!1<pi/2") (("1" (lemma "sin_q2" ("x" "x!1")) (("1" (lemma "cos_q2" ("x" "x!1")) (("1" (lemma "sin_q1" ("x" "y!1")) (("1" (lemma "cos_q1" ("x" "y!1")) (("1" (assert) (("1" (lemma "cos_q2" ("x" "x!1+y!1")) (("1" (lemma "cos_q3" ("x" "x!1+y!1")) (("1" (replace -3) (("1" (replace -4) (("1" (replace -5) (("1" (replace -6) (("1" (rewrite "phase_sin_q2" -2) (("1" (rewrite "phase_sin_q3" -1) (("1" (case "x!1+y!1<pi") (("1" (assert) (("1" (hide -2 -4 -5 -6 -7) (("1" (lemma "sin_value_sum" ("q1" "x!1-pi/2" "q2" "y!1")) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide -2 -3 -4 -5 -6) (("2" (lemma "sin_value_sum" ("q1" "x!1-pi/2" "q2" "y!1")) (("2" (assert) (("2" (case "x!1=pi-y!1") (("1" (replace -1) (("1" (assert) (("1" (rewrite "sin_value_pi2" -2) (("1" (rewrite "cos_value_0") (("1" (assert) nil nil)) nil)) nil)) 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" (rewrite "phase_sin_q1" -1) nil nil)) nil) ("2" (case "pi/2<=y!1") (("1" (lemma "cos_value_sum" ("q1" "x!1-pi/2" "q2" "y!1-pi/2")) (("1" (simplify -1) (("1" (lemma "div_cancel1" ("x" "pi" "n0z" "2")) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "sin_q2" ("x" "x!1")) (("1" (lemma "cos_q2" ("x" "x!1")) (("1" (lemma "sin_q2" ("x" "y!1")) (("1" (lemma "cos_q2" ("x" "y!1")) (("1" (assert) (("1" (replace -1) (("1" (replace -2) (("1" (replace -3) (("1" (replace -4) (("1" (rewrite "cos_phase_inv" 1) (("1" (hide -1 -2 -3 -4) (("1" (expand "cos_phase" 1) (("1" (rewrite "phase_cos_q1" 1) (("1" (assert) nil nil)) 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) ("2" (rewrite "phase_sin_q2" -1) nil nil)) nil) ("3" (rewrite "phase_sin_q3" -1) nil nil) ("4" (rewrite "phase_sin_q4" -1) nil nil)) nil)) nil) ("2" (rewrite "phase_sin_q2" -1) nil nil)) nil) ("3" (rewrite "phase_sin_q3" -1) nil nil) ("4" (rewrite "phase_sin_q4" -1) nil nil)) nil)) nil)) nil)) nil)) nil) ((nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (phases_sin formula-decl nil sincos_phase nil) (cos_q3 formula-decl nil sincos_phase nil) (cos_value_0 formula-decl nil sincos_quad nil) (div_cancel1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (phase_sin_q1 formula-decl nil sincos_phase nil) (sin_q1 formula-decl nil sincos_phase nil) (cos_q1 formula-decl nil sincos_phase nil) (cos_value_sum formula-decl nil sincos_quad nil) (nnreal_quad1_closed nonempty-type-eq-decl nil sincos_quad nil) (phase_sin_q2 formula-decl nil sincos_phase nil) (sin_q2 formula-decl nil sincos_phase nil) (sin_value_sum formula-decl nil sincos_quad nil) (sin_eqv_cos_value formula-decl nil sincos_quad nil) (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cos_value_pi formula-decl nil sincos_quad nil) (sin_value_pi2 formula-decl nil sincos_quad nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (cos_value_neg formula-decl nil sincos_quad nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (trich_lt formula-decl nil real_props nil) (cos_q2 formula-decl nil sincos_phase nil) (phase_sin_q3 formula-decl nil sincos_phase nil) (phase_sin_q4 formula-decl nil sincos_phase nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (y!1 skolem-const-decl "trig_phase" sincos_phase nil) (x!1 skolem-const-decl "trig_phase" sincos_phase nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (phase_cos_q1 formula-decl nil sincos_phase nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (phase_cos_q2 formula-decl nil sincos_phase nil) (minus_real_is_real application-judgement "real" reals nil) (sin_phase_inv formula-decl nil sincos_phase nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (cos_phase_inv formula-decl nil sincos_phase nil) (minus_even_is_even application-judgement "even_int" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (phases_cos formula-decl nil sincos_phase nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types 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) (nnreal 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) (posreal nonempty-type-eq-decl nil real_types nil) (pi const-decl "posreal" atan nil) (= const-decl "[T, T -> boolean]" equalities 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) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (real_abs_le1 nonempty-type-eq-decl nil asin nil) (cos_phase const-decl "real_abs_le1" sincos_phase nil) (sin_phase const-decl "real_abs_le1" sincos_phase nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (cos_phase_diff 0 (cos_phase_diff-1 nil 3264848363 ("" (skosimp*) (("" (case "y!1=0") (("1" (replace -1) (("1" (rewrite "cos_phase_0") (("1" (rewrite "sin_phase_0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "cos_phase_sum" ("x" "x!1" "y" "2*pi-y!1")) (("1" (lemma "sin_phase_neg" ("px" "y!1")) (("1" (lemma "cos_phase_neg" ("px" "y!1")) (("1" (replace -1) (("1" (replace -2) (("1" (hide -1 -2) (("1" (replace -1 2) (("1" (case "x!1 - y!1 >= 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal 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) (= const-decl "[T, T -> boolean]" equalities nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (cos_phase_0 formula-decl nil sincos_phase nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_phase_0 formula-decl nil sincos_phase nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (sin_phase_neg formula-decl nil sincos_phase nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (minus_real_is_real application-judgement "real" reals nil) (cos_phase_neg formula-decl nil sincos_phase nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (cos_phase_sum formula-decl nil sincos_phase nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil)) shostak)) (sin_phase_sum 0 (sin_phase_sum-1 nil 3264847615 ("" (skosimp*) (("" (lemma "sin_phase_diff" ("x" "x!1" "y" "2*pi-y!1")) (("1" (case "x!1 + y!1 < 2 * pi") (("1" (assert) (("1" (case "y!1=0") (("1" (replace -1) (("1" (rewrite "sin_phase_0") (("1" (rewrite "cos_phase_0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "sin_phase_neg" ("px" "y!1")) (("1" (lemma "cos_phase_neg" ("px" "y!1")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (typepred "y!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (lemma "sin_phase_neg" ("px" "y!1")) (("2" (lemma "cos_phase_neg" ("px" "y!1")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "y!1=0") (("1" (replace -1) (("1" (rewrite "cos_phase_0") (("1" (rewrite "sin_phase_0") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (trig_phase nonempty-type-eq-decl nil sincos_phase nil) (pi const-decl "posreal" atan 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) (numfield nonempty-type-eq-decl nil number_fields nil) (< const-decl "bool" reals nil) (nnreal 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) (sin_phase_diff formula-decl nil sincos_phase nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (sin_phase_neg formula-decl nil sincos_phase nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_real_is_real application-judgement "real" reals nil) (cos_phase_neg formula-decl nil sincos_phase nil) (NOT const-decl "[bool -> bool]" booleans nil) (cos_phase_0 formula-decl nil sincos_phase nil) (sin_phase_0 formula-decl nil sincos_phase nil) (= const-decl "[T, T -> boolean]" equalities nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil)) shostak)))
¤ Dauer der Verarbeitung: 0.318 Sekunden (vorverarbeitet am 2026-04-27) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26