| products/Sources/formale Sprachen/PVS/trig/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: trig_ineq.prf 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_neg formula-decl nil trig_basic nil) (cos_0 formula-decl nil trig_basic 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 "{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) (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" trig_basic nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_range application-judgement "trig_range" trig_basic 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" trig_basic nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (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) ((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) (AND const-decl "[bool, bool -> bool]" booleans nil) (pi_lb const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (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 "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (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) (sin_range application-judgement "trig_range" trig_basic 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 "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (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" trig_basic 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) ((<= const-decl "bool" reals nil) (sin_pi formula-decl nil trig_basic nil) (sin_range application-judgement "trig_range" trig_basic 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) ((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" 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_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" trig_basic 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" trig_basic 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" trig_basic 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" trig_basic nil) (cos const-decl "real" trig_basic 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) (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" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic 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" trig_basic 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" trig_basic 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" trig_basic 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) (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" trig_basic nil) (cos_gt_0 formula-decl nil trig_ineq nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types 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" trig_basic 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" trig_basic nil)) shostak)) (tan_npi_def 0 (tan_npi_def-1 nil 3323008332 ("" (skeep) (("" (expand "Tan?") (("" (lemma "cos_k_pi") (("" (inst -1 "n") (("" (replaces -1) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((Tan? const-decl "bool" trig_basic nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (integer nonempty-type-from-decl nil integers nil) (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 "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (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) (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" trig_basic 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" trig_basic 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" trig_basic 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" 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) (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" trig_basic nil) (real_times_real_is_real application-judgement "real" reals nil) (cos_range application-judgement "trig_range" trig_basic nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_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" 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) (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" trig_basic nil) (sin_range application-judgement "trig_range" trig_basic 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" trig_basic nil) (sin_pi formula-decl nil trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (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" trig_basic 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) (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" trig_basic nil) (sin_minus formula-decl nil trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (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" trig_basic 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) (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" trig_basic nil) (sin_minus formula-decl nil trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (< const-decl "bool" reals nil) (pi_lb const-decl "posreal" trig_basic nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (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) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tan const-decl "real" 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) (< const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (pos_div_gt formula-decl nil real_props nil) (neg_div_ge formula-decl nil real_props nil) (minus_real_is_real application-judgement "real" reals nil) (- const-decl "[numfield -> numfield]" number_fields nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (pi_lb const-decl "posreal" trig_basic nil) (pi_ub const-decl "posreal" trig_basic nil) (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic nil) (sin_neg formula-decl nil trig_basic nil) (sin_gt_0 formula-decl nil trig_ineq nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (>= const-decl "bool" reals nil) (cos const-decl "real" trig_basic nil) (sin const-decl "real" trig_basic 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (sin_increasing formula-decl nil trig_ineq nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (cos_decreasing formula-decl nil trig_ineq nil) (sin_ge_0 formula-decl nil trig_ineq nil) (negreal nonempty-type-eq-decl nil real_types nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (both_sides_div_pos_le3 formula-decl nil real_props nil) (b!1 skolem-const-decl "real" trig_ineq nil) (both_sides_div_pos_le2 formula-decl nil real_props nil) (<= const-decl "bool" reals nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (both_sides_div_pos_gt1 formula-decl nil real_props nil) (cos_neg formula-decl nil trig_basic nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.93 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 |
