Quelle tan_approx.prf Sprache: Lisp

(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" sincos_def 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" sincos_def nil)
    (cos_range application-judgement "trig_range" sincos_def nil)
    (tan const-decl "real" sincos_def 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" sincos_def 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 sincos_def 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" sincos_def 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" 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)
    (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" sincos_def nil)
    (Tan? const-decl "bool" sincos_def 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" 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)
    (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" sincos_def 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" sincos_def 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" sincos_def nil)
    (cos_range application-judgement "trig_range" sincos_def nil)
    (tan const-decl "real" sincos_def 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" sincos_def 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 sincos_def 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" sincos_def 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" sincos_def 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" 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)
    (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" sincos_def 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" sincos_def 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" sincos_def 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)))

quality100%

¤ Dauer der Verarbeitung: 0.30 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.