tan_approx.prf  Interaktion und
Portierbarkeitunbekannt

(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)))