| products/Sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: arithmetic.pvs Sprache: LispOriginal von: PVS© |
|
||||||
|
(trig_ineq
(cos_gt_0 0 (cos_gt_0-1 nil 3321111622 ("" (skosimp) (("" (case "forall (x:posreal): x (("1" (lemma "trichotomy" ("x" "a!1")) (("1" (split -1) (("1" (inst - "a!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil) ("2" (replace -1) (("2" (rewrite "cos_0") (("2" (assert) nil nil)) nil)) nil) ("3" (inst - "-a!1") (("1" (assert) (("1" (rewrite "cos_neg") nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp) (("2" (expand "cos") (("2" (typepred "x!1") (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "x!1" "py" "2*pi")) (("2" (lemma "both_sides_div_pos_lt1" ("pz" "2*pi" "x" "x!1" "y" "pi/2")) (("2" (assert) (("2" (rewrite "div_div2" -1) (("2" (lemma "div_cancel1" ("n0z" "pi" "x" "1/4")) (("2" (replace -1) (("2" (hide -1) (("2" (lemma "floor_def" ("x" "x!1 / (2 * pi)")) (("2" (flatten) (("2" (lemma "trichotomy" ("x" "floor(x!1 / (2 * pi))")) (("2" (split -1) (("1" (assert) nil nil) ("2" (replace -1) (("2" (assert) (("2" (hide -1 -2 -3 -4 -5) (("2" (expand "cos_phase") (("2" (lemma "posreal_div_posreal_is_posreal" ("px" "x!1" "py" "pi")) (("2" (lemma "both_sides_div_pos_lt1" ("pz" "pi" "x" "x!1" "y" "pi/2")) (("2" (replace -5 -1) (("2" (lemma "div_cancel1" ("n0z" "pi" "x" "1/2")) (("2" (replace -1) (("2" (flatten -2) (("2" (hide -1) (("2" (lemma "floor_def" ("x" "x!1 / pi")) (("2" (flatten) (("2" (lemma "trichotomy" ("x" "floor(x!1 / pi)")) (("2" (split -1) (("1" (assert) nil nil) ("2" (replace -1) (("2" (lemma "cos_value_strict_decreasing") (("2" (expand "strict_decreasing?") (("2" (inst - "x!1" "pi/2") (("2" (assert) (("2" (rewrite "cos_value_pi2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cos const-decl "real" sincos_def nil) (pi const-decl "posreal" atan 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) (IMPLIES 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) (cos_range application-judgement "trig_range" sincos_def nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (a!1 skolem-const-decl "real" trig_ineq nil) (AND const-decl "[bool, bool -> bool]" 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) (cos_0 formula-decl nil trig_basic nil) (cos_neg formula-decl nil trig_basic nil) (- const-decl "[numfield -> numfield]" number_fields nil) (minus_real_is_real application-judgement "real" reals nil) (trichotomy formula-decl nil real_axioms nil) (NOT const-decl "[bool -> bool]" booleans nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_div2 formula-decl nil real_props nil) (floor_def 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) (<= 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) (cos_value_strict_decreasing formula-decl nil sincos_quad nil) (nnreal_le_pi nonempty-type-eq-decl nil acos nil) (nnreal type-eq-decl nil real_types nil) (cos_value_pi2 formula-decl nil sincos_quad nil) (strict_decreasing? const-decl "bool" real_fun_preds "reals/") (cos_phase const-decl "real_abs_le1" sincos_phase nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (div_cancel1 formula-decl nil real_props nil) (posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (real_minus_real_is_real application-judgement "real" reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (nnreal_times_nnreal_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)) shostak)) (sin_gt_0 0 (sin_gt_0-1 nil 3321113131 ("" (skosimp) (("" (lemma "cos_sin" ("a" "a!1-pi/2")) (("" (lemma "cos_gt_0" ("a" "a!1-pi/2")) (("" (assert) 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, 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) (cos_sin formula-decl nil trig_basic 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) (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_plus_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" sincos_def nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_range application-judgement "trig_range" sincos_def nil) (cos_gt_0 formula-decl nil trig_ineq nil)) shostak)) (sin_ge_0 0 (sin_ge_0-1 nil 3321111692 ("" (skosimp) (("" (expand "<=") (("" (split -1) (("1" (split -2) (("1" (lemma "sin_gt_0" ("a" "a!1")) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (rewrite "sin_pi") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (replace -1 1 rl) (("2" (rewrite "sin_0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" reals nil) (sin_0 formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" sincos_def nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sin_gt_0 formula-decl nil trig_ineq 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_pi formula-decl nil trig_basic nil)) shostak)) (cos_ge_0 0 (cos_ge_0-1 nil 3321111792 ("" (skosimp) (("" (expand "<=") (("" (split -1) (("1" (split -2) (("1" (lemma "cos_gt_0" ("a" "a!1")) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (rewrite "cos_pi2") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (lemma "cos_neg" ("a" "pi/2")) (("2" (rewrite "cos_pi2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (<= const-decl "bool" reals nil) (cos_neg formula-decl nil trig_basic 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) (cos_range application-judgement "trig_range" sincos_def nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" 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) (cos_gt_0 formula-decl nil trig_ineq 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_pi2 formula-decl nil trig_basic nil)) shostak)) (sin_lt_0 0 (sin_lt_0-1 nil 3321112483 ("" (skosimp) (("" (lemma "neg_sin" ("a" "a!1-pi")) (("" (lemma "sin_gt_0" ("a" "a!1-pi")) (("" (assert) 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) (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) (neg_sin formula-decl nil trig_basic 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_plus_real_is_real application-judgement "real" reals nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (sin_range application-judgement "trig_range" sincos_def nil) (minus_real_is_real application-judgement "real" reals nil) (sin_gt_0 formula-decl nil trig_ineq nil)) shostak)) (cos_lt_0 0 (cos_lt_0-1 nil 3321112640 ("" (skosimp) (("" (lemma "neg_cos" ("a" "a!1-pi")) (("" (assert) (("" (lemma "cos_gt_0" ("a" "a!1-pi")) (("" (assert) 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) (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) (neg_cos formula-decl nil trig_basic nil) (real_minus_real_is_real application-judgement "real" reals nil) (cos_gt_0 formula-decl nil trig_ineq nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" sincos_def nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (real_plus_real_is_real application-judgement "real" reals 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_le_0 0 (sin_le_0-1 nil 3321112929 ("" (skosimp) (("" (expand "<=" (-1 -2)) (("" (split -1) (("1" (split -2) (("1" (lemma "sin_lt_0" ("a" "a!1")) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (rewrite "sin_2pi") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1 1 rl) (("2" (rewrite "sin_pi") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (<= const-decl "bool" reals nil) (sin_pi formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" sincos_def 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sin_lt_0 formula-decl nil trig_ineq 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_2pi formula-decl nil trig_basic nil)) shostak)) (cos_le_0 0 (cos_le_0-1 nil 3321113009 ("" (skosimp) (("" (expand "<=" (-1 -2)) (("" (split -1) (("1" (split -2) (("1" (lemma "cos_lt_0" ("a" "a!1")) (("1" (assert) nil nil)) nil) ("2" (replace -1) (("2" (rewrite "cos_3pi2") (("2" (assert) nil nil)) nil)) nil)) nil) ("2" (replace -1 * rl) (("2" (rewrite "cos_pi2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (<= const-decl "bool" reals nil) (cos_pi2 formula-decl nil trig_basic nil) (cos_range application-judgement "trig_range" sincos_def 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (cos_lt_0 formula-decl nil trig_ineq 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_3pi2 formula-decl nil trig_basic nil)) shostak)) (tan_gt_0_TCC1 0 (tan_gt_0_TCC1-1 nil 3321111953 ("" (skosimp) (("" (expand "Tan?") (("" (lemma "cos_eq_0_2pi" ("a" "a!1")) (("" (assert) nil nil)) nil)) nil)) nil) ((Tan? const-decl "bool" sincos_def 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) (cos_range application-judgement "trig_range" sincos_def nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx 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) (cos_eq_0_2pi 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_gt_0 0 (tan_gt_0-1 nil 3321112029 ("" (skosimp) (("" (expand "tan") (("" (lemma "sin_gt_0" ("a" "a!1")) (("" (lemma "cos_gt_0" ("a" "a!1")) (("" (assert) (("" (lemma "posreal_div_posreal_is_posreal" ("px" "sin(a!1)" "py" "cos(a!1)")) (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tan const-decl "real" sincos_def nil) (cos_gt_0 formula-decl nil trig_ineq nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types 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) (sin const-decl "real" sincos_def nil) (cos const-decl "real" sincos_def nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" sincos_def nil) (cos_range application-judgement "trig_range" sincos_def nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sin_gt_0 formula-decl nil trig_ineq 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_lt_0_TCC1 0 (tan_lt_0_TCC1-1 nil 3321111953 ("" (skosimp) (("" (expand "Tan?") (("" (lemma "cos_eq_0_2pi" ("a" "-a!1")) (("" (assert) (("" (rewrite "cos_neg") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((Tan? const-decl "bool" sincos_def 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) (cos_range application-judgement "trig_range" sincos_def nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (cos_neg formula-decl nil trig_basic nil) (minus_real_is_real application-judgement "real" reals nil) (cos_eq_0_2pi formula-decl nil trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil)) shostak)) (tan_lt_0 0 (tan_lt_0-1 nil 3321112133 ("" (skosimp) (("" (lemma "tan_gt_0" ("a" "-a!1")) (("" (assert) (("" (rewrite "tan_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) (tan_gt_0 formula-decl nil trig_ineq nil) (minus_real_is_real application-judgement "real" reals nil) (Tan? const-decl "bool" sincos_def nil) (bool nonempty-type-eq-decl nil booleans nil) (tan_neg formula-decl nil trig_basic 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) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil)) shostak)) (tan_pi2_def 0 (tan_pi2_def-1 nil 3312284516 ("" (skeep) (("" (expand "Tan?") (("" (case "cos(a)>0") (("1" (assert) nil nil) ("2" (rewrite "cos_gt_0") nil nil)) nil)) nil)) nil) ((Tan? const-decl "bool" sincos_def nil) (cos_gt_0 formula-decl nil trig_ineq nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (cos_range application-judgement "trig_range" sincos_def nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" 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) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (cos const-decl "real" sincos_def nil)) shostak)) (tan_npi_def 0 (tan_npi_def-1 nil 3323008626 ("" (skeep) (("" (expand "Tan?") (("" (lemma "cos_k_pi") (("" (inst -1 "n") (("" (replaces -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((Tan? const-decl "bool" sincos_def 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) (int nonempty-type-eq-decl nil integers nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (nzreal_exp application-judgement "nzreal" exponentiation nil) (rat_exp application-judgement "rat" exponentiation nil) (cos_k_pi formula-decl nil trig_basic nil)) shostak)) (cos_ge_0_3pi2 0 (cos_ge_0_3pi2-1 nil 3279136307 ("" (skosimp*) (("" (name "BB" "a!1 - 2 * pi") (("" (case-replace "a!1 = BB + 2*pi") (("1" (hide -1 -2) (("1" (assert) (("1" (case-replace "-pi/2 <= BB AND BB <= 0") (("1" (hide -2 -3) (("1" (rewrite "cos_plus") (("1" (rewrite "cos_2pi") (("1" (rewrite "sin_2pi") (("1" (flatten) (("1" (assert) (("1" (lemma "cos_gt_0") (("1" (inst?) (("1" (lemma "cos_pi2") (("1" (lemma "cos_neg") (("1" (inst -1 "pi/2") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (assert) 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) (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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-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) (real_minus_real_is_real application-judgement "real" reals 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) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (cos_plus formula-decl nil trig_basic nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sin_range application-judgement "trig_range" sincos_def nil) (real_times_real_is_real application-judgement "real" reals nil) (sin_2pi formula-decl nil trig_basic nil) (cos_neg formula-decl nil trig_basic 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) (cos_pi2 formula-decl nil trig_basic nil) (cos_gt_0 formula-decl nil trig_ineq nil) (cos_2pi formula-decl nil trig_basic 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (cos_range application-judgement "trig_range" sincos_def nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (minus_nzint_is_nzint application-judgement "nzint" integers nil) (minus_even_is_even application-judgement "even_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)) nil)) (sin_increasing_imp 0 (sin_increasing_imp-1 nil 3279136307 ("" (skosimp) (("" (case "sin(a!1) - sin(b!1) > 0") (("1" (assert) nil nil) ("2" (hide 2) (("2" (assert) (("2" (lemma "sin_plus") (("2" (inst -1 "(a!1+b!1)/2" "(a!1-b!1)/2") (("2" (lemma "sin_minus") (("2" (inst -1 "(a!1+b!1)/2" "(a!1-b!1)/2") (("2" (replace -2 * lr) (("2" (replace -1 * lr) (("2" (hide -2 -1) (("2" (assert) (("2" (assert) (("2" (lemma "pos_times_gt") (("2" (inst -1 "2" "sin((a!1 - b!1) / 2) * cos((a!1 + b!1) / 2)") (("2" (replace -1 * lr) (("2" (hide -1) (("2" (flatten) (("2" (hide 1) (("2" (rewrite "pos_times_gt" 1) (("2" (assert) (("2" (flatten) (("2" (hide 1) (("2" (rewrite "sin_gt_0") (("2" (rewrite "cos_gt_0") 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) ((sin const-decl "real" sincos_def nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (> const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sin_range application-judgement "trig_range" sincos_def 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) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (real_ge_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_div_nzreal_is_real application-judgement "real" 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) (pos_times_gt formula-decl nil real_props nil) (sin_gt_0 formula-decl nil trig_ineq nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (cos_gt_0 formula-decl nil trig_ineq nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (cos const-decl "real" sincos_def nil) (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" sincos_def nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (sin_minus formula-decl nil trig_basic nil) (sin_plus formula-decl nil trig_basic nil)) nil)) (sin_increasing 0 (sin_increasing-1 nil 3279136307 ("" (skosimp) (("" (prop) (("1" (lemma "sin_increasing_imp") (("1" (inst -1 "b!1" "a!1") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "sin_increasing_imp") 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (sin_range application-judgement "trig_range" sincos_def 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) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (real_ge_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) (sin_increasing_imp formula-decl nil trig_ineq nil)) nil)) (sin_decreasing 0 (sin_decreasing-1 nil 3279136307 ("" (lemma "sin_increasing") (("" (skosimp) (("" (inst -1 "pi-b!1" "pi-a!1") (("" (rewrite "sin_minus") (("" (rewrite "sin_pi") (("" (rewrite "cos_pi") (("" (rewrite "sin_minus") (("" (rewrite "sin_pi") (("" (rewrite "cos_pi") (("" (assert) (("" (case-replace "-1 * (sin(b!1) * -1) = sin(b!1)") (("1" (hide -1) (("1" (case-replace "-1 * (sin(a!1) * -1) = sin(a!1)") (("1" (hide -1) (("1" (ground) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sin_minus formula-decl nil trig_basic nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_range application-judgement "trig_range" sincos_def nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (sin_range application-judgement "trig_range" sincos_def nil) (real_times_real_is_real application-judgement "real" reals nil) (cos_pi formula-decl nil trig_basic nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (real_ge_is_total_order name-judgement "(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) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield -> numfield]" number_fields nil) (sin const-decl "real" sincos_def nil) (sin_pi formula-decl nil trig_basic 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) (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_minus_real_is_real application-judgement "real" reals nil) (sin_increasing formula-decl nil trig_ineq nil)) nil)) (cos_increasing 0 (cos_increasing-1 nil 3279136307 ("" (skosimp) (("" (lemma "sin_increasing") (("" (inst -1 "a!1-3*pi/2" "b!1-3*pi/2") (("" (assert) (("" (rewrite "sin_minus") (("" (rewrite "cos_3pi2") (("" (rewrite "sin_3pi2") (("" (rewrite "sin_minus") (("" (rewrite "cos_3pi2") (("" (rewrite "sin_3pi2") (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sin_increasing formula-decl nil trig_ineq nil) (cos_range application-judgement "trig_range" sincos_def nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (cos_3pi2 formula-decl nil trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sin_3pi2 formula-decl nil trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" sincos_def nil) (sin_minus formula-decl nil trig_basic 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) (/ 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) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (cos_decreasing 0 (cos_decreasing-1 nil 3279136307 ("" (skosimp) (("" (lemma "sin_increasing") (("" (inst -1 "a!1-pi/2" "b!1-pi/2") (("" (assert) (("" (rewrite "sin_minus") (("" (rewrite "sin_pi2") (("" (rewrite "cos_pi2") (("" (assert) (("" (rewrite "sin_minus") (("" (rewrite "sin_pi2") (("" (rewrite "cos_pi2") (("" (assert) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sin_increasing formula-decl nil trig_ineq nil) (cos_range application-judgement "trig_range" sincos_def nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}" atan_approx nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sin_pi2 formula-decl nil trig_basic nil) (cos_pi2 formula-decl nil trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (sin_range application-judgement "trig_range" sincos_def nil) (sin_minus formula-decl nil trig_basic 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, 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) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (tan_increasing_imp_TCC1 0 (tan_increasing_imp_TCC1-1 nil 3279136307 ("" (skosimp) (("" (rewrite "tan_pi2_def") nil nil)) nil) ((tan_pi2_def formula-decl nil trig_ineq 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)) nil)) (tan_increasing_imp_TCC2 0 (tan_increasing_imp_TCC2-2 nil 3312284395 ("" (skosimp) (("" (rewrite "tan_pi2_def") nil nil)) nil) ((tan_pi2_def formula-decl nil trig_ineq 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)) nil)) (tan_increasing_imp 0 (tan_increasing_imp-1 nil 3279136307 ("" (skosimp) (("" (expand "tan") (("" (lemma "cos_gt_0") (("" (inst -1 "a!1") (("" (lemma "cos_gt_0") (("" (inst -1 "b!1") (("" (assert) (("" (case "a!1>0" "b!1<0") (("1" (case "EXISTS (d: real): sin(a!1) / cos(a!1) > d AND d >= sin(b!1) / cos(b!1)") (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (inst 1 "0") (("2" (rewrite "pos_div_gt" 1) (("2" (rewrite "sin_gt_0") (("2" (rewrite "neg_div_ge" 1) (("2" (lemma "sin_gt_0") (("2" (inst -1 "-b!1") (("2" (rewrite "sin_neg" -1) (("2" (case "0 < -b!1 AND -b!1 < pi IMPLIES sin(b!1) < 0") (("1" (hide -2) (("1" (assert) nil nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "EXISTS (d: real): sin(a!1) / cos(a!1) > d AND d >= sin(b!1) / cos(b!1)") (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (hide 3) (("2" (inst + "sin(b!1)/cos(a!1)") (("2" (split) (("1" (lemma "both_sides_div_pos_lt1") (("1" (inst -1 "cos(a!1)" "sin(b!1)" "sin(a!1)") (("1" (assert) (("1" (lemma "sin_increasing") (("1" (inst -1 "a!1" "b!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "(sin(b!1) = 0 OR sin(b!1) > 0 AND cos(a!1) <= cos(b!1) OR sin(b!1) < 0 AND cos(a!1) >= cos(b!1))") (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (lemma "both_sides_div_pos_le2") (("1" (inst -1 "cos(b!1)" "cos(a!1)" "sin(b!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lemma "both_sides_div_pos_le3") (("2" (inst -1 "sin(b!1)" "cos(b!1)" "cos(a!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "cos_decreasing") (("2" (inst -1 "a!1" "b!1") (("2" (assert) (("2" (lemma "sin_ge_0") (("2" (inst -1 "b!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "EXISTS (d: real): sin(a!1) / cos(a!1) > d AND d >= sin(b!1) / cos(b!1)") (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (hide 3) (("2" (inst + "sin(b!1)/cos(a!1)") (("2" (split) (("1" (lemma "both_sides_div_pos_gt1") (("1" (inst -1 "cos(a!1)" "sin(a!1)" "sin(b!1)") (("1" (assert) (("1" (hide 2) (("1" (rewrite "sin_increasing") nil nil)) nil)) nil)) nil)) nil) ("2" (case "(sin(b!1) = 0 OR sin(b!1) > 0 AND cos(a!1) <= cos(b!1) OR sin(b!1) < 0 AND cos(a!1) >= cos(b!1))") (("1" (assert) (("1" (split -1) (("1" (flatten) (("1" (lemma "both_sides_div_pos_le2") (("1" (inst -1 "cos(b!1)" "cos(a!1)" "sin(b!1)") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (lemma "both_sides_div_pos_le3") (("2" (inst -1 "sin(b!1)" "cos(b!1)" "cos(a!1)") (("1" (assert) nil nil) ("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "sin_gt_0") (("2" (inst -1 "-b!1") (("2" (rewrite "sin_neg" -1) (("2" (case "0 < -b!1 AND -b!1 < pi IMPLIES sin(b!1) < 0") (("1" (hide -2) (("1" (assert) (("1" (lemma "cos_decreasing") (("1" (inst -1 "-b!1" "-a!1") (("1" (rewrite "cos_neg" -1) (("1" (rewrite "cos_neg" -1) (("1" (assert) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.121 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 |
