| products/Sources/formale Sprachen/PVS/trig/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: sigma_nat.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(trig_basic
(pi_TCC1 0 (pi_TCC1-1 nil 3279386567 ("" (inst + "(pi_lb+pi_ub)/2") (("" (assert) (("" (case "(pi_lb + pi_ub) / 2 > 0 ") (("1" (assert) (("1" (prop) (("1" (cross-mult 1) (("1" (assert) (("1" (grind) nil nil)) nil)) nil) ("2" (cross-mult 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (cross-mult 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (div_mult_pos_gt1 formula-decl nil extra_real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (trig_phase_TCC1 0 (trig_phase_TCC1-1 nil 3294394361 ("" (assert) nil nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (sin_range_ax 0 (sin_range_ax-1 nil 3264999679 ("" (skosimp*) (("" (expand "sin") (("" (lemma "floor_def" ("x" "a!1 / (2 * pi)")) (("" (flatten) (("" (rewrite "div_mult_pos_le2" -1) (("" (rewrite "div_mult_pos_lt1" -2) (("" (typepred "sin_phase(a!1 - 2 * (floor(a!1 / (2 * pi)) * pi))") (("1" (expand "abs") (("1" (case "sin_phase(a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)) < 0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (cos_range_ax 0 (cos_range_ax-1 nil 3265001911 ("" (skosimp*) (("" (expand "cos") (("" (lemma "floor_def" ("x" "a!1 / (2 * pi)")) (("" (rewrite "div_mult_pos_le2" -1) (("" (rewrite "div_mult_pos_lt1" -1) (("" (flatten) (("" (typepred "cos_phase(a!1 - 2 * (floor(a!1 / (2 * pi)) * pi))") (("1" (expand "abs") (("1" (case "cos_phase(a!1 - 2 * (floor(a!1 / (2 * pi)) * pi))<0") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (sin_range 0 (sin_range-1 nil 3264999490 ("" (skosimp*) (("" (rewrite "sin_range_ax") nil nil)) nil) ((sin_range_ax formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil)) shostak)) (cos_range 0 (cos_range-1 nil 3264999490 ("" (skosimp*) (("" (rewrite "cos_range_ax") nil nil)) nil) ((cos_range_ax formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil)) shostak)) (tan_TCC1 0 (tan_TCC1-1 nil 3264999490 ("" (skosimp*) (("" (typepred "a!1") (("" (expand "Tan?") (("" (assert) nil nil)) nil)) nil)) nil) ((Tan? const-decl "bool" trig_basic nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (cos_range application-judgement "trig_range" trig_basic nil)) shostak)) (sin2_cos2 0 (sin2_cos2-1 nil 3265002048 ("" (skosimp*) (("" (expand "sin") (("" (expand "cos") (("" (lemma "floor_def" ("x" "a!1 / (2 * pi)")) (("" (rewrite "div_mult_pos_le2" -1) (("" (rewrite "div_mult_pos_lt1" -1) (("" (flatten -1) (("" (lemma "sin2_cos2_phase" ("x" "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)")) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (cos2 0 (cos2-1 nil 3265002167 ("" (skosimp*) (("" (lemma "sin2_cos2" ("a" "a!1")) (("" (assert) nil nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin2_cos2 formula-decl nil trig_basic nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (sin2 0 (sin2-1 nil 3265002192 ("" (skosimp*) (("" (lemma "sin2_cos2" ("a" "a!1")) (("" (assert) nil nil)) nil)) nil) ((real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin2_cos2 formula-decl nil trig_basic nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil)) shostak)) (cos_0 0 (cos_0-1 nil 3265002205 ("" (expand "cos") (("" (rewrite "floor_int") (("" (rewrite "cos_phase_0") nil nil)) nil)) nil) nil shostak)) (sin_0 0 (sin_0-2 nil 3279387338 ("" (lemma "sin2_cos2") (("" (inst?) (("" (rewrite "cos_0") (("" (expand "sq") (("" (rewrite "zero_times3") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (sq const-decl "nonneg_real" sq "reals/") (zero_times3 formula-decl nil real_props nil) (sin const-decl "real" trig_basic nil) (cos_0 formula-decl nil trig_basic nil) (sin2_cos2 formula-decl nil trig_basic nil)) nil) (sin_0-1 nil 3265002237 ("" (expand "sin") (("" (rewrite "floor_int") (("" (rewrite "sin_phase_0") nil nil)) nil)) nil) nil shostak)) (sin_pi2 0 (sin_pi2-1 nil 3265002302 ("" (expand "sin") (("" (rewrite "div_div2") (("" (lemma "div_cancel1" ("x" "1/4" "n0z" "pi")) (("" (replace -1) (("" (lemma "floor_val" ("i" "1" "j" "4" "k" "0")) (("" (split -1) (("1" (replace -1) (("1" (rewrite "sin_phase_pi2") nil nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (cos_pi2 0 (cos_pi2-1 nil 3265002447 ("" (lemma "sin2_cos2" ("a" "pi/2")) (("" (rewrite "sin_pi2") (("" (rewrite "sq_1") (("" (lemma "sq_eq_0" ("a" "cos(pi/2)")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((sin_pi2 formula-decl nil trig_basic nil) (sq_eq_0 formula-decl nil sq "reals/") (cos const-decl "real" trig_basic nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (cos_range application-judgement "trig_range" trig_basic nil) (sq_nz_pos application-judgement "posreal" sq "reals/") (sq_1 formula-decl nil sq "reals/") (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin2_cos2 formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil)) shostak)) (tan_0_TCC1 0 (tan_0_TCC1-1 nil 3264999490 ("" (expand "Tan?") (("" (rewrite "cos_0") (("" (assert) nil nil)) nil)) nil) ((cos_0 formula-decl nil trig_basic nil) (Tan? const-decl "bool" trig_basic nil)) shostak)) (tan_0 0 (tan_0-1 nil 3265002274 ("" (expand "tan") (("" (rewrite "sin_0") (("" (rewrite "cos_0") (("" (assert) nil nil)) nil)) nil)) nil) ((sin_0 formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (cos_0 formula-decl nil trig_basic nil) (tan const-decl "real" trig_basic nil)) shostak)) (sin_neg 0 (sin_neg-1 nil 3265008367 ("" (skosimp*) (("" (expand "sin") (("" (lemma "floor_neg" ("x" "a!1/(2*pi)")) (("" (case "integer?(a!1 / (2 * pi))") (("1" (assert) (("1" (replace -2) (("1" (lemma "floor_def" ("x" "-a!1 / (2 * pi)")) (("1" (flatten -1) (("1" (lemma "div_mult_pos_le2" ("x" "floor(-a!1 / (2 * pi))" "z" "-a!1" "py" "2 * pi")) (("1" (replace -1 -2) (("1" (lemma "div_mult_pos_lt1" ("x" "floor(-a!1 / (2 * pi))+1" "z" "-a!1" "py" "2 * pi")) (("1" (replace -1 -4) (("1" (hide -1 -2) (("1" (rewrite "floor_int" -4) (("1" (case "floor(-(a!1 / (2 * pi))) = -a!1/(2*pi)") (("1" (replace -1) (("1" (lemma "div_cancel1" ("x" "a!1" "n0z" "2*pi")) (("1" (replace -1) (("1" (lemma "div_cancel1" ("x" "-a!1" "n0z" "2*pi")) (("1" (replace -1) (("1" (simplify 1) (("1" (rewrite "sin_phase_0") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (replace -1 2) (("2" (case "a!1 = - 2 * (floor(-a!1 / (2 * pi)) * pi)") (("1" (assert) nil nil) ("2" (lemma "sin_phase_neg" ("px" "-a!1 - 2 * (floor(-a!1 / (2 * pi)) * pi)")) (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "floor_def" ("x" "-a!1 / (2 * pi)")) (("2" (flatten -1) (("2" (rewrite "div_mult_pos_le2" -1) (("2" (rewrite "div_mult_pos_lt1" -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (cos_neg 0 (cos_neg-1 nil 3265009425 ("" (skosimp*) (("" (expand "cos") (("" (lemma "floor_neg" ("x" "a!1 / (2 * pi)")) (("" (case "integer?(a!1 / (2 * pi))") (("1" (assert) nil nil) ("2" (assert) (("2" (replace -1) (("2" (case "-a!1 - 2 * (floor(-a!1 / (2 * pi)) * pi) = 0") (("1" (assert) nil nil) ("2" (lemma "cos_phase_neg" ("px" "-a!1 - 2 * (floor(-a!1 / (2 * pi)) * pi)")) (("1" (assert) nil nil) ("2" (lemma "floor_def" ("x" "-a!1 / (2 * pi)")) (("2" (flatten) (("2" (rewrite "div_mult_pos_le2" -1) (("2" (rewrite "div_mult_pos_lt1" -2) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (tan_neg_TCC1 0 (tan_neg_TCC1-1 nil 3264999490 ("" (skosimp*) (("" (typepred "a!1") (("" (expand "Tan?") (("" (lemma "cos_neg" ("a" "a!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((Tan? const-decl "bool" trig_basic nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (cos_neg formula-decl nil trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (minus_real_is_real application-judgement "real" reals nil)) shostak)) (tan_neg 0 (tan_neg-1 nil 3265006358 ("" (skosimp*) (("" (typepred "a!1") (("" (expand "Tan?") (("" (expand "tan") (("" (rewrite "cos_neg") (("" (rewrite "sin_neg") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Tan? const-decl "bool" trig_basic nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (tan const-decl "real" trig_basic nil) (sin_neg formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_neg formula-decl nil trig_basic nil)) shostak)) (cos_sin 0 (cos_sin-1 nil 3265009874 ("" (skosimp*) (("" (expand "cos") (("" (expand "sin") (("" (lemma "floor_def" ("x" "a!1 / (2 * pi)")) (("" (rewrite "div_mult_pos_le2" -1) (("" (rewrite "div_mult_pos_lt1" -1) (("" (lemma "floor_def" ("x" "(pi/2+a!1 )/ (2 * pi)")) (("" (rewrite "div_mult_pos_le2" -1) (("" (rewrite "div_mult_pos_lt1" -1) (("" (flatten) (("" (lemma "cos_eqv_sin_phase" ("x" "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)")) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "floor_plus" ("x" "a!1 / (2 * pi)" "y" "1/4")) (("1" (lemma "floor_val" ("i" "1" "j" "4" "k" "0")) (("1" (split -1) (("1" (replace -1) (("1" (lemma "div_cancel1" ("x" "1/4" "n0z" "pi")) (("1" (lemma "div_distributes" ("x" "pi/2" "y" "a!1" "n0z" "2*pi")) (("1" (replace -2 -1) (("1" (replace -1 * rl) (("1" (replace -4) (("1" (assert) (("1" (replace -1) (("1" (name "FL" "floor(a!1 / (2 * pi))") (("1" (replace -1) (("1" (case "fractional(1/4) = 1/4") (("1" (replace -1) (("1" (case "fractional(a!1 / (2 * pi)) = a!1/(2*pi) - FL") (("1" (replace -1) (("1" (case "a!1 - 2 * (FL * pi) < 3 * pi / 2") (("1" (assert) (("1" (case "floor(1 / 4 + a!1 / (2 * pi) - FL) = 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (lemma "floor_def" ("x" "1 / 4 + a!1 / (2 * pi) - FL")) (("2" (flatten -1) (("2" (name-replace "K1" "floor(1 / 4 + a!1 / (2 * pi) - FL)") (("2" (lemma "trichotomy" ("x" "K1")) (("2" (split -1) (("1" (case "K1=1") (("1" (replace -1) (("1" (assert) nil nil)) nil) ("2" (case "K1>1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (propax) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "floor(1 / 4 + (a!1 / (2 * pi) - FL)) = 1") (("1" (replace -1) (("1" (hide-all-but (1 2)) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 3) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "fractional" 1) (("2" (replace -2) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "fractional" 1) (("2" (lemma "floor_val" ("i" "1" "j" "4" "k" "0")) (("2" (hide-all-but (-1 1)) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (sin_cos 0 (sin_cos-1 nil 3265010005 ("" (skosimp*) (("" (lemma "cos_sin" ("a" "-(a!1+pi/2)")) (("" (lemma "cos_neg" ("a" "a!1+pi/2")) (("" (lemma "sin_neg" ("a" "a!1")) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (cos_sin formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (sin_neg formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_neg formula-decl nil trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (sin_shift 0 (sin_shift-1 nil 3265074854 ("" (skosimp*) (("" (lemma "sin_neg" ("a" "pi/2-a!1")) (("" (lemma "sin_cos" ("a" "a!1-pi/2")) (("" (assert) nil nil)) nil)) nil)) nil) ((pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin_neg formula-decl nil trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (sin_range application-judgement "trig_range" trig_basic nil) (sin_cos formula-decl nil trig_basic nil)) shostak)) (cos_shift 0 (cos_shift-1 nil 3265010327 ("" (skosimp*) (("" (lemma "sin_shift" ("a" "pi/2-a!1")) (("" (assert) nil nil)) nil)) nil) ((pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin_shift formula-decl nil trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_range application-judgement "trig_range" trig_basic nil)) shostak)) (neg_cos 0 (neg_cos-1 nil 3265010987 ("" (skosimp*) (("" (rewrite "cos_sin") (("" (rewrite "sin_cos") (("" (assert) nil nil)) nil)) nil)) nil) ((cos_sin formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sin_cos formula-decl nil trig_basic nil)) shostak)) (neg_sin 0 (neg_sin-1 nil 3265071739 ("" (skosimp*) (("" (rewrite "sin_cos") (("" (rewrite "cos_sin") (("" (assert) nil nil)) nil)) nil)) nil) ((sin_cos formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (cos_sin formula-decl nil trig_basic nil)) shostak)) (sin_pi 0 (sin_pi-2 nil 3279387666 ("" (case "pi=pi/2 + pi/2") (("1" (replace -1 :hide? t) (("1" (lemma "sin_minus") (("1" (inst -1 "pi/2" "-pi/2") (("1" (case "pi / 2 - -pi / 2 = pi / 2 + pi / 2") (("1" (replace -1 :hide? t) (("1" (replace -1 :hide? t) (("1" (case "(pi / 2 + pi / 2) / 2 = pi/2") (("1" (replace -1 :hide? t) (("1" (case "-(pi / 2 + pi / 2)/2 = -(pi/2)") (("1" (replace -1 :hide? t) (("1" (rewrite "sin_neg") (("1" (rewrite "cos_neg") (("1" (rewrite "sin_pi2") (("1" (rewrite "cos_pi2") (("1" (ground) nil))))))))))) ("2" (ground) nil))))) ("2" (ground) nil))))))) ("2" (ground) nil))))))))) ("2" (ground) nil)) nil) nil nil) (sin_pi-1 nil 3265006547 ("" (expand "sin") (("" (lemma "div_cancel1" ("x" "1/2" "n0z" "pi")) (("" (replace -1 1) (("" (lemma "floor_val" ("i" "1" "j" "2" "k" "0")) (("" (split -1) (("1" (replace -1) (("1" (assert) (("1" (expand "sin_phase") (("1" (lemma "div_cancel1" ("x" "2" "n0z" "pi")) (("1" (replace -1) (("1" (rewrite "sin_value_0") (("1" (rewrite "floor_int" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (cos_pi 0 (cos_pi-2 nil 3279154503 ("" (expand "cos") (("" (lemma "div_cancel1" ("x" "1/2" "n0z" "pi")) (("" (replace -1) (("" (lemma "floor_val" ("i" "1" "j" "2" "k" "0")) (("" (split -1) (("1" (replace -1) (("1" (simplify 1) (("1" (expand "cos_phase") (("1" (rewrite "cos_value_pi") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) nil nil) (cos_pi-1 nil 3265008251 ("" (expand "pi") (("" (expand "cos") (("" (lemma "div_cancel1" ("x" "1/2" "n0z" "pi")) (("" (replace -1) (("" (lemma "floor_val" ("i" "1" "j" "2" "k" "0")) (("" (split -1) (("1" (replace -1) (("1" (simplify 1) (("1" (expand "cos_phase") (("1" (rewrite "cos_value_pi") nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (tan_pi_TCC1 0 (tan_pi_TCC1-1 nil 3264999490 ("" (expand "Tan?") (("" (rewrite "cos_pi") (("" (assert) nil nil)) nil)) nil) ((cos_pi formula-decl nil trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (Tan? const-decl "bool" trig_basic nil)) shostak)) (tan_pi 0 (tan_pi-1 nil 3265006469 ("" (expand "tan") (("" (rewrite "sin_pi") (("" (rewrite "cos_pi") (("" (assert) nil nil)) nil)) nil)) nil) ((sin_pi formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (cos_pi formula-decl nil trig_basic nil) (tan const-decl "real" trig_basic nil)) shostak)) (sin_3pi2 0 (sin_3pi2-1 nil 3265010743 ("" (lemma "neg_sin" ("a" "pi/2")) (("" (rewrite "sin_pi2") (("" (assert) nil nil)) nil)) nil) ((sin_pi2 formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (neg_sin formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil)) shostak)) (cos_3pi2 0 (cos_3pi2-1 nil 3265010800 ("" (lemma "neg_cos" ("a" "pi/2")) (("" (rewrite "cos_pi2") (("" (assert) nil nil)) nil)) nil) ((cos_pi2 formula-decl nil trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_even_is_even application-judgement "even_int" integers nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (neg_cos formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil)) shostak)) (sin_2pi 0 (sin_2pi-2 nil 3279154535 ("" (expand "sin") (("" (rewrite "div_simp") (("" (rewrite "floor_int") (("" (assert) (("" (rewrite "sin_phase_0") nil nil)) nil)) nil)) nil)) nil) nil nil) (sin_2pi-1 nil 3265010441 ("" (expand "pi") (("" (expand "sin") (("" (rewrite "div_simp") (("" (rewrite "floor_int") (("" (assert) (("" (rewrite "sin_phase_0") nil nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (cos_2pi 0 (cos_2pi-2 nil 3279154560 ("" (expand "cos") (("" (rewrite "div_simp") (("" (rewrite "floor_int") (("" (assert) (("" (rewrite "cos_phase_0") nil nil)) nil)) nil)) nil)) nil) nil nil) (cos_2pi-1 nil 3265010493 ("" (expand "cos") (("" (expand "pi") (("" (rewrite "div_simp") (("" (rewrite "floor_int") (("" (assert) (("" (rewrite "cos_phase_0") nil nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (tan_2pi_TCC1 0 (tan_2pi_TCC1-1 nil 3264999491 ("" (expand "Tan?") (("" (rewrite "cos_2pi") (("" (assert) nil nil)) nil)) nil) ((cos_2pi formula-decl nil trig_basic nil) (Tan? const-decl "bool" trig_basic nil)) shostak)) (tan_2pi 0 (tan_2pi-1 nil 3265006491 ("" (expand "tan") (("" (rewrite "sin_2pi") (("" (rewrite "cos_2pi") (("" (assert) nil nil)) nil)) nil)) nil) ((sin_2pi formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (cos_2pi formula-decl nil trig_basic nil) (tan const-decl "real" trig_basic nil)) shostak)) (sin_plus 0 (sin_plus-1 nil 3265083493 ("" (skosimp*) (("" (expand "sin") (("" (expand "cos") (("" (name "FLA" "floor(a!1 / (2 * pi))") (("" (name "FLB" "floor(b!1 / (2 * pi))") (("" (replace -1) (("" (replace -2) (("" (lemma "floor_plus" ("x" "a!1/(2*pi)" "y" "b!1/(2*pi)")) (("" (replace -2) (("" (replace -3) (("" (lemma "sin_phase_sum" ("x" "a!1 - 2 * (FLA * pi)" "y" "b!1 - 2 * (FLB * pi)")) (("1" (replace -1 1) (("1" (hide -1) (("1" (case "a!1 - 2 * (FLA * pi) + (b!1 - 2 * (FLB * pi)) < 2 * pi") (("1" (assert) (("1" (case "floor(fractional(a!1 / (2 * pi)) + fractional(b!1 / (2 * pi))) = 0") (("1" (assert) nil nil) ("2" (hide -2 2) (("2" (lemma "floor_def" ("x" "fractional(a!1 / (2 * pi)) + fractional(b!1 / (2 * pi))")) (("2" (flatten) (("2" (expand "fractional") (("2" (replace -4) (("2" (replace -5) (("2" (lemma "both_sides_times_pos_le1" ("x" "floor(a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB)" "y" "a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB" "pz" "2*pi")) (("2" (lemma "both_sides_times_pos_lt1" ("y" "1+floor(a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB)" "x" "a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB" "pz" "2*pi")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (case "floor((a!1 + b!1) / (2 * pi)) = FLA+FLB+1") (("1" (assert) nil nil) ("2" (hide 3) (("2" (case "floor(fractional(a!1 / (2 * pi)) + fractional(b!1 / (2 * pi))) = 1") (("1" (assert) nil nil) ("2" (hide 2) (("2" (expand "fractional" 1) (("2" (replace -2) (("2" (replace -3) (("2" (hide -1) (("2" (lemma "floor_def" ("x" "a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB")) (("2" (lemma "both_sides_times_pos_lt1" ("y" "1+floor(a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB)" "x" "a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB" "pz" "2*pi")) (("2" (lemma "both_sides_times_pos_lt1" ("x" "floor(a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB)" "y" "a!1 / (2 * pi) + b!1 / (2 * pi) - FLA - FLB" "pz" "2*pi")) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "floor_def" ("x" "b!1/(2*pi)")) (("2" (rewrite "div_mult_pos_lt1" -1) (("2" (rewrite "div_mult_pos_le2" -1) (("2" (flatten) (("2" (replace -4) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (expand "FLA") (("3" (lemma "floor_def" ("x" "a!1/(2*pi)")) (("3" (rewrite "div_mult_pos_lt1" -1) (("3" (rewrite "div_mult_pos_le2" -1) (("3" (flatten) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (sin_minus 0 (sin_minus-1 nil 3265007645 ("" (skosimp*) (("" (lemma "sin_plus" ("a" "a!1" "b" "-b!1")) (("" (rewrite "sin_neg") (("" (rewrite "cos_neg") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((- const-decl "[numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin_plus formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (cos_neg formula-decl nil trig_basic nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (sin_neg formula-decl nil trig_basic nil)) shostak)) (cos_plus 0 (cos_plus-1 nil 3265071786 ("" (skosimp*) (("" (rewrite "cos_sin") (("" (rewrite "cos_sin") (("" (lemma "sin_cos" ("a" "a!1")) (("" (lemma "sin_plus" ("a" "pi/2+a!1" "b" "b!1")) (("" (assert) nil nil)) nil)) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 1.124 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 |
