| products/sources/formale sprachen/PVS/trig_fnd/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: LispOriginal von: PVS© |
|
||||||
|
(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 (("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 --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.59 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
