| products/Sources/formale Sprachen/PVS/power/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: tan_approx.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(tan_approx
(tan_lb_ub_TCC1 0 (tan_lb_ub_TCC1-1 nil 3285095221 ("" (skosimp :preds? t) nil nil) ((cos_ub const-decl "real" trig_approx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (/= const-decl "boolean" notequal nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (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)) shostak)) (tan_ub_lb_TCC1 0 (tan_ub_lb_TCC1-1 nil 3320436455 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (/= const-decl "boolean" notequal nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (cos_lb const-decl "real" trig_approx nil) (cos_approx const-decl "real" trig_approx nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil)) nil)) (tan_lb_ub_neg_TCC1 0 (tan_lb_ub_neg_TCC1-1 nil 3285095378 ("" (skeep) (("" (rewrite "cos_ub_neg") nil nil)) nil) ((cos_ub_neg formula-decl nil trig_approx 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) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (tan_lb_ub_neg 0 (tan_lb_ub_neg-1 nil 3285095182 ("" (skeep) (("" (expand* "tan_lb_ub" "tan_ub_ub") (("" (rewrite "sin_lb_neg") (("" (rewrite "cos_ub_neg") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((tan_ub_ub const-decl "real" tan_approx nil) (tan_lb_ub const-decl "real" tan_approx nil) (cos_ub_neg formula-decl nil trig_approx nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin_lb_neg formula-decl nil trig_approx nil)) shostak)) (tan_ub_lb_neg_TCC1 0 (tan_ub_lb_neg_TCC1-1 nil 3320436749 ("" (skeep) (("" (rewrite "cos_lb_neg") nil nil)) nil) ((cos_lb_neg formula-decl nil trig_approx 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) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) nil)) (tan_ub_lb_neg 0 (tan_ub_lb_neg-2 nil 3320436789 ("" (skeep) (("" (expand* "tan_ub_lb" "tan_lb_lb") (("" (rewrite "sin_ub_neg") (("" (rewrite "cos_lb_neg") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((tan_lb_lb const-decl "real" tan_approx nil) (tan_ub_lb const-decl "real" tan_approx nil) (cos_lb_neg formula-decl nil trig_approx nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin_ub_neg formula-decl nil trig_approx nil)) nil)) (tan_lb_lb_neg 0 (tan_lb_lb_neg-1 nil 3285095124 ("" (skeep) (("" (expand* "tan_lb_lb" "tan_ub_lb") (("" (rewrite "sin_lb_neg") (("" (rewrite "cos_lb_neg") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((tan_ub_lb const-decl "real" tan_approx nil) (tan_lb_lb const-decl "real" tan_approx nil) (cos_lb_neg formula-decl nil trig_approx nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin_lb_neg formula-decl nil trig_approx nil)) shostak)) (tan_ub_ub_neg 0 (tan_ub_ub_neg-1 nil 3285095094 ("" (skeep) (("" (expand* "tan_ub_ub" "tan_lb_ub") (("" (rewrite "sin_ub_neg") (("" (rewrite "cos_ub_neg") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((tan_lb_ub const-decl "real" tan_approx nil) (tan_ub_ub const-decl "real" tan_approx nil) (cos_ub_neg formula-decl nil trig_approx nil) (minus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (sin_ub_neg formula-decl nil trig_approx nil)) shostak)) (tan_bounds_0_pi2_TCC1 0 (tan_bounds_0_pi2_TCC1-1 nil 3285095421 ("" (skeep) (("" (lemma "cos_bounds") (("" (inst?) (("" (assert) (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((cos_bounds formula-decl nil trig_approx nil) (cos_range application-judgement "trig_range" trig_basic 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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (tan_bounds_0_pi2_TCC2 0 (tan_bounds_0_pi2_TCC2-1 nil 3285095537 ("" (skeep) (("" (rewrite "tan_pi2_def") nil nil)) 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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (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)) shostak)) (tan_bounds_0_pi2_TCC3 0 (tan_bounds_0_pi2_TCC3-1 nil 3285095563 ("" (skeep) (("" (assert) nil nil)) 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) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (tan_bounds_0_pi2 0 (tan_bounds_0_pi2-2 nil 3285094898 ("" (skeep) (("" (expand "tan") (("" (expand "tan_lb_ub") (("" (expand "tan_ub_lb") (("" (case "cos(a) > 0") (("1" (case "sin(a) >= 0") (("1" (lemma "sin_bounds") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (lemma "cos_bounds") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (split) (("1" (cross-mult 1) (("1" (case "sin_lb(a, n) * cos(a) <= sin(a) * cos(a)" "sin(a) * cos(a) <= sin(a) * cos_ub(a, n)") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (cancel-by 1 "sin(a)") nil nil)) nil) ("3" (hide 2) (("3" (cancel-by 1 "cos(a)") nil nil)) nil)) nil)) nil) ("2" (cross-mult 1) (("2" (case "sin(a) * cos_lb(a, n) <= sin(a) * cos(a)" "sin(a) * cos(a) <= sin_ub(a, n) * cos(a)") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (cancel-by 1 "cos(a)") nil nil)) nil) ("3" (hide 2) (("3" (cancel-by 1 "sin(a)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sin_ge_0") nil nil)) nil) ("2" (rewrite "cos_gt_0") nil nil)) nil)) nil)) nil)) nil)) nil) ((sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (tan const-decl "real" trig_basic nil) (tan_ub_lb const-decl "real" tan_approx nil) (minus_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (cos_gt_0 formula-decl nil trig_ineq nil) (>= const-decl "bool" reals nil) (sin const-decl "real" trig_basic nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (sin_ub const-decl "real" trig_approx nil) (cos_lb const-decl "real" trig_approx nil) (CBD_7 skolem-const-decl "trig_range" tan_approx nil) (CBD_6 skolem-const-decl "trig_range" tan_approx nil) (div_mult_pos_le1 formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types 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) (sin_lb const-decl "real" trig_approx nil) (n skolem-const-decl "nat" tan_approx nil) (a skolem-const-decl "real" tan_approx nil) (cos_ub const-decl "real" trig_approx nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (real_times_real_is_real application-judgement "real" reals nil) (times_div2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_le2 formula-decl nil real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (CBD_5 skolem-const-decl "trig_range" tan_approx nil) (= const-decl "[T, T -> boolean]" equalities nil) (- const-decl "[numfield -> numfield]" number_fields nil) (trig_range type-eq-decl nil trig_basic nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (CBD_4 skolem-const-decl "trig_range" tan_approx nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (pos_div_gt formula-decl nil real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (zero_times1 formula-decl nil real_props nil) (<= const-decl "bool" reals nil) (cos_bounds formula-decl nil trig_approx nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_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_div_nzreal_is_real application-judgement "real" reals nil) (sin_bounds formula-decl nil trig_approx nil) (sin_ge_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) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (cos const-decl "real" trig_basic nil) (tan_lb_ub const-decl "real" tan_approx nil)) nil)) (tan_bounds_npi2_0_TCC1 0 (tan_bounds_npi2_0_TCC1-1 nil 3285095576 ("" (skeep) (("" (assert) 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) (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) (real_le_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)) shostak)) (tan_bounds_npi2_0_TCC2 0 (tan_bounds_npi2_0_TCC2-1 nil 3285095608 ("" (skeep) (("" (rewrite "tan_pi2_def") nil nil)) nil) ((real_le_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) (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) (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)) shostak)) (tan_bounds_npi2_0_TCC3 0 (tan_bounds_npi2_0_TCC3-1 nil 3285095637 ("" (skeep) (("" (lemma "cos_bounds") (("" (inst?) (("" (assert) (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((cos_bounds formula-decl nil trig_approx nil) (cos_range application-judgement "trig_range" trig_basic 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) (real_le_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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (tan_bounds_npi2_0 0 (tan_bounds_npi2_0-2 nil 3321627681 ("" (skeep) (("" (lemma "tan_bounds_0_pi2") (("" (inst -1 "-a" "n") (("" (assert) (("" (rewrite "cos_lb_neg") (("" (assert) (("" (flatten) (("" (lemma "cos_bounds") (("" (inst?) (("" (assert) (("" (flatten) (("" (rewrite "tan_neg") (("1" (rewrite "tan_lb_ub_neg") (("1" (rewrite "tan_ub_lb_neg") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "Tan?") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tan_bounds_0_pi2 formula-decl nil tan_approx 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_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) (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_bounds formula-decl nil trig_approx nil) (cos_range application-judgement "trig_range" trig_basic nil) (Tan? const-decl "bool" trig_basic nil) (tan_neg formula-decl nil trig_basic nil) (tan_ub_lb_neg formula-decl nil tan_approx nil) (tan_lb_ub_neg formula-decl nil tan_approx nil) (cos_lb_neg formula-decl nil trig_approx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield -> numfield]" 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) (minus_real_is_real application-judgement "real" reals nil)) nil)) (tan_bounds_pi2_pi_TCC1 0 (tan_bounds_pi2_pi_TCC1-1 nil 3285095674 ("" (skeep) (("" (assert) nil nil)) 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (tan_bounds_pi2_pi_TCC2 0 (tan_bounds_pi2_pi_TCC2-1 nil 3285095683 ("" (skeep) (("" (expand "Tan?") (("" (lemma "cos_bounds") (("" (inst?) (("" (assert) 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) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (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" trig_basic nil) (cos_bounds formula-decl nil trig_approx nil)) shostak)) (tan_bounds_pi2_pi_TCC3 0 (tan_bounds_pi2_pi_TCC3-1 nil 3285095728 ("" (skeep) (("" (lemma "cos_bounds") (("" (inst?) (("" (assert) (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((cos_bounds formula-decl nil trig_approx nil) (cos_range application-judgement "trig_range" trig_basic 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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (tan_bounds_pi2_pi 0 (tan_bounds_pi2_pi-2 nil 3321627705 ("" (skeep) (("" (expand "tan") (("" (expand "tan_ub_ub") (("" (expand "tan_lb_lb") (("" (case "cos(a) < 0") (("1" (case "sin(a) >= 0") (("1" (lemma "cos_bounds") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (lemma "sin_bounds") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (split) (("1" (cross-mult 1) (("1" (case "sin_ub(a, n) * cos(a) <= sin(a) * cos(a)" "sin(a) * cos(a) <= sin(a) * cos_ub(a, n)") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (cancel-by 1 "sin(a)") nil nil)) nil) ("3" (hide 2) (("3" (cancel-by 1 "cos(a)") nil nil)) nil)) nil)) nil) ("2" (cross-mult 1) (("2" (case "sin(a) * cos_lb(a, n) <= sin(a) * cos(a)" "sin(a) * cos(a) <= sin_lb(a, n) * cos(a)") (("1" (assert) nil nil) ("2" (hide -1 2) (("2" (cancel-by 1 "cos(a)") nil nil)) nil) ("3" (hide 2) (("3" (cancel-by 1 "sin(a)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "sin_ge_0") nil nil)) nil) ("2" (rewrite "cos_lt_0") nil nil)) nil)) nil)) nil)) nil)) nil) ((sin_range application-judgement "trig_range" trig_basic nil) (cos_range application-judgement "trig_range" trig_basic nil) (tan const-decl "real" trig_basic nil) (tan_lb_lb const-decl "real" tan_approx nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (cos_lt_0 formula-decl nil trig_ineq nil) (>= const-decl "bool" reals nil) (sin const-decl "real" trig_basic nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (sin_lb const-decl "real" trig_approx nil) (cos_lb const-decl "real" trig_approx nil) (CBD_11 skolem-const-decl "trig_range" tan_approx nil) (CBD_10 skolem-const-decl "trig_range" tan_approx nil) (div_mult_neg_le1 formula-decl nil real_props nil) (<= const-decl "bool" reals nil) (nonpos_real nonempty-type-eq-decl nil real_types nil) (negreal nonempty-type-eq-decl nil real_types nil) (cos_ub const-decl "real" trig_approx 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) (sin_ub const-decl "real" trig_approx nil) (real_times_real_is_real application-judgement "real" reals nil) (times_div2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_times_neg_le1 formula-decl nil real_props nil) (CBD_9 skolem-const-decl "trig_range" tan_approx nil) (div_mult_neg_lt1 formula-decl nil real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield -> numfield]" number_fields nil) (trig_range type-eq-decl nil trig_basic nil) (> const-decl "bool" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (both_sides_times_pos_le1 formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (CBD_8 skolem-const-decl "trig_range" tan_approx nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (pos_div_gt formula-decl nil real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (zero_times1 formula-decl nil real_props nil) (sin_bounds formula-decl nil trig_approx nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (posreal_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_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (cos_bounds formula-decl nil trig_approx nil) (sin_ge_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) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" reals nil) (cos const-decl "real" trig_basic nil) (tan_ub_ub const-decl "real" tan_approx nil)) nil)) (tan_bounds_npi_npi2_TCC1 0 (tan_bounds_npi_npi2_TCC1-1 nil 3285095758 ("" (skeep) (("" (lemma "cos_bounds") (("" (inst?) (("" (assert) (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((cos_bounds formula-decl nil trig_approx nil) (cos_range application-judgement "trig_range" trig_basic 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) (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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (tan_bounds_npi_npi2_TCC2 0 (tan_bounds_npi_npi2_TCC2-1 nil 3285095780 ("" (skeep) (("" (expand "Tan?") (("" (lemma "cos_bounds") (("" (inst?) (("" (assert) 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) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (cos_range application-judgement "trig_range" trig_basic nil) (cos_bounds formula-decl nil trig_approx nil)) shostak)) (tan_bounds_npi_npi2_TCC3 0 (tan_bounds_npi_npi2_TCC3-1 nil 3285095806 ("" (skeep) (("" (assert) nil nil)) 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) (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)) shostak)) (tan_bounds_npi_npi2 0 (tan_bounds_npi_npi2-2 nil 3321627736 ("" (skeep) (("" (lemma "tan_bounds_pi2_pi") (("" (inst -1 "-a" "n") (("" (assert) (("" (rewrite "cos_ub_neg") (("" (assert) (("" (rewrite "tan_neg") (("1" (rewrite "tan_ub_ub_neg") (("1" (rewrite "tan_lb_lb_neg") (("1" (flatten) (("1" (assert) nil nil)) nil) ("2" (hide -1 2) (("2" (lemma "cos_bounds") (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "Tan?") (("2" (lemma "cos_bounds") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((tan_bounds_pi2_pi formula-decl nil tan_approx nil) (posreal_div_posreal_is_posreal application-judgement "posreal" 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) (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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (tan_ub_ub_neg formula-decl nil tan_approx nil) (cos_range application-judgement "trig_range" trig_basic nil) (cos_bounds formula-decl nil trig_approx nil) (tan_lb_lb_neg formula-decl nil tan_approx nil) (tan_neg formula-decl nil trig_basic nil) (Tan? const-decl "bool" trig_basic nil) (cos_ub_neg formula-decl nil trig_approx nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (- const-decl "[numfield -> numfield]" 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) (minus_real_is_real application-judgement "real" reals nil)) nil))) ¤ Dauer der Verarbeitung: 0.18 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 |
