Quelle sincos_def.prf Sprache: Lisp

(sincos_def
(sin_TCC1 0
  (sin_TCC1-1 nil 3294919158
   ("" (skosimp)
    (("" (name "DRL1" "floor(x!1 / (2 * pi))")
      (("" (lemma "floor_div" ("x" "x!1" "py" "2*pi" "i" "DRL1"))
        (("" (replace -2) (("" (flatten) (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((pi const-decl "posreal" atan nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (integer nonempty-type-from-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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals 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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (floor_div formula-decl nil floor_ceil nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil))
   shostak))
(sin_range 0
  (sin_range-1 nil 3294919299
   ("" (expand "sin")
    (("" (skosimp)
      (("" (name "DRL1" "floor(a!1 / (2 * pi))")
        (("" (lemma "floor_div" ("x" "a!1" "py" "2*pi" "i" "DRL1"))
          (("" (replace -2)
            (("" (flatten)
              (("" (name-replace "DRL2" "a!1 - 2 * (DRL1 * pi)")
                (("" (typepred "sin_phase(DRL2)")
                  (("1" (case-replace "sin_phase(DRL2) < 0")
                    (("1" (assert) nil nil) ("2" (assert) nil nil)
                     ("3" (assert) nil nil))
                    nil)
                   ("2" (hide 2)
                    (("2" (expand "DRL2") (("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((floor_div formula-decl nil floor_ceil nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (trig_phase nonempty-type-eq-decl nil sincos_phase nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (sin_phase const-decl "real_abs_le1" sincos_phase 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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (DRL2 skolem-const-decl "real" sincos_def nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (integer nonempty-type-from-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan nil)
    (sin const-decl "real" sincos_def nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil))
   shostak))
(cos_range 0
  (cos_range-1 nil 3294919466
   ("" (skosimp)
    (("" (expand "cos")
      (("" (name "DRL1" "floor(a!1 / (2 * pi))")
        (("" (lemma "floor_div" ("x" "a!1" "py" "2*pi" "i" "DRL1"))
          (("" (replace -2)
            (("" (flatten)
              (("" (name "DRL2" "a!1 - 2 * (DRL1 * pi)")
                (("" (replace -1)
                  (("" (typepred "cos_phase(DRL2)")
                    (("1" (case-replace "cos_phase(DRL2) < 0")
                      (("1" (assert) nil nil) ("2" (assert) nil nil)
                       ("3" (assert) nil nil))
                      nil)
                     ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (cos const-decl "real" sincos_def nil)
    (floor_div formula-decl nil floor_ceil nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (cos_phase const-decl "real_abs_le1" sincos_phase nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (trig_phase nonempty-type-eq-decl nil sincos_phase nil)
    (nnreal type-eq-decl nil real_types nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (integer nonempty-type-from-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan nil))
   shostak))
(sin_range_ax 0
  (sin_range_ax-1 nil 3294919642
   ("" (lemma "sin_range") (("" (propax) nil nil)) nil)
   ((sin_range judgement-tcc nil sincos_def nil)) shostak))
(cos_range_ax 0
  (cos_range_ax-1 nil 3294919653
   ("" (lemma "cos_range") (("" (propax) nil nil)) nil)
   ((cos_range judgement-tcc nil sincos_def nil)) shostak))
(tan_TCC1 0
  (tan_TCC1-1 nil 3294919572
   ("" (skosimp)
    (("" (typepred "a!1")
      (("" (expand "Tan?") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((Tan? const-decl "bool" sincos_def 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)
    (cos_range application-judgement "trig_range" sincos_def nil))
   shostak))
(tan_rew 0
  (tan_rew-1 nil 3294925610
   ("" (expand "tan") (("" (propax) nil nil)) nil)
   ((tan const-decl "real" sincos_def nil)
    (cos_range application-judgement "trig_range" sincos_def nil)
    (sin_range application-judgement "trig_range" sincos_def nil))
   shostak))
(sin_sin_phase_TCC1 0
  (sin_sin_phase_TCC1-1 nil 3294920258
   ("" (skosimp) (("" (assert) nil nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
(sin_sin_phase 0
  (sin_sin_phase-1 nil 3294920287
   ("" (skolem 1 ("a"))
    (("" (flatten)
      (("" (expand "sin")
        (("" (lemma "floor_0" ("x" "a/(2*pi)"))
          (("" (rewrite "div_mult_pos_lt1" -1)
            (("" (assert) (("" (rewrite "div_mult_pos_le2" 1) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((pi const-decl "posreal" atan nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (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)
    (floor_0 formula-decl nil floor_ceil nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (sin const-decl "real" sincos_def nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil))
   shostak))
(cos_cos_phase 0
  (cos_cos_phase-1 nil 3294920464
   ("" (skolem 1 ("a"))
    (("" (flatten)
      (("" (expand "cos")
        (("" (lemma "floor_0" ("x" "a/(2*pi)"))
          (("" (rewrite "div_mult_pos_le2" -1)
            (("" (rewrite "div_mult_pos_lt1" -1)
              (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((pi const-decl "posreal" atan nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (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)
    (floor_0 formula-decl nil floor_ceil nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (cos const-decl "real" sincos_def nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil))
   shostak))
(sin_sin_value_TCC1 0
  (sin_sin_value_TCC1-1 nil 3294920613
   ("" (expand "abs")
    (("" (skosimp)
      (("" (case-replace "a!1<0")
        (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (< const-decl "bool" reals 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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   shostak))
(sin_sin_value 0
  (sin_sin_value-1 nil 3294920637
   ("" (skosimp*)
    (("" (case "0<=a!1")
      (("1" (rewrite "sin_sin_phase")
        (("1" (expand "sin_phase")
          (("1" (lemma "floor_0" ("x" "(2 * a!1) / pi"))
            (("1" (rewrite "div_mult_pos_le2" -4)
              (("1" (rewrite "div_mult_pos_le2" -1)
                (("1" (rewrite "div_mult_pos_lt1" -1)
                  (("1" (assert)
                    (("1" (case-replace "a!1=pi/2")
                      (("1" (assert) nil nil)
                       ("2" (rewrite "div_cancel4" 1)
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (expand "sin")
        (("2" (lemma "floor_div" ("x" "a!1" "py" "2*pi" "i" "-1"))
          (("2" (assert)
            (("2" (replace -1)
              (("2" (assert)
                (("2" (case "a!1<0")
                  (("1" (hide -2 -4 1)
                    (("1" (expand "sin_phase")
                      (("1"
                        (lemma "floor_div"
                         ("x" "2*a!1+4*pi" "py" "pi" "i" "3"))
                        (("1" (assert)
                          (("1" (rewrite "sin_value_neg" 1 :dir rl)
                            (("1" (assert) nil nil)
                             ("2" (expand "abs")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sin_phase const-decl "real_abs_le1" sincos_phase nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (div_cancel4 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (floor_0 formula-decl nil floor_ceil 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)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sin_sin_phase formula-decl nil sincos_def nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (integer nonempty-type-from-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)
    (floor_div formula-decl nil floor_ceil nil)
    (< const-decl "bool" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (sin_value_neg formula-decl nil sincos_quad nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (odd_plus_odd_is_even application-judgement "even_int" integers
     nil)
    (sin const-decl "real" sincos_def nil))
   shostak))
(cos_cos_value_TCC1 0
  (cos_cos_value_TCC1-1 nil 3294920613
   ("" (skosimp) (("" (assert) nil nil)) nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
(cos_cos_value 0
  (cos_cos_value-1 nil 3294921311
   ("" (skosimp*)
    (("" (rewrite "cos_cos_phase")
      (("" (expand "cos_phase")
        (("" (lemma "floor_0" ("x" "a!1/pi"))
          (("" (rewrite "div_mult_pos_lt1")
            (("" (rewrite "div_mult_pos_le2")
              (("" (case-replace "a!1=pi")
                (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cos_cos_phase formula-decl nil 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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pi const-decl "posreal" atan nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (floor_0 formula-decl nil floor_ceil nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (cos_phase const-decl "real_abs_le1" sincos_phase nil))
   shostak))
(tan_value_TCC 0
  (tan_value_TCC-1 nil 3294928867
   ("" (expand "Tan?")
    (("" (skosimp)
      (("" (case "0<=a!1")
        (("1" (lemma "cos_cos_value" ("a" "a!1"))
          (("1" (assert)
            (("1" (lemma "cos_value_strict_decreasing")
              (("1" (expand "strict_decreasing?")
                (("1" (inst - "a!1" "pi/2")
                  (("1" (rewrite "cos_value_pi2")
                    (("1" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (case-replace "a!1=0")
          (("1" (rewrite "cos_cos_value")
            (("1" (rewrite "cos_value_0") (("1" (assert) nil nil))
              nil))
            nil)
           ("2" (expand "cos")
            (("2" (lemma "floor_div" ("x" "a!1" "py" "2*pi" "i" "-1"))
              (("2" (lemma "cos_phase_neg" ("px" "-a!1"))
                (("1" (lemma "cos_cos_phase" ("a" "-a!1"))
                  (("1" (lemma "cos_cos_value" ("a" "-a!1"))
                    (("1" (lemma "cos_value_strict_decreasing")
                      (("1" (expand "strict_decreasing?")
                        (("1" (inst - "-a!1" "pi/2")
                          (("1" (rewrite "cos_value_pi2")
                            (("1" (assert) nil nil)) nil)
                           ("2" (assert) nil nil)
                           ("3" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((= const-decl "[T, T -> boolean]" equalities nil)
    (cos_value_0 formula-decl nil sincos_quad nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (integer nonempty-type-from-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)
    (floor_div formula-decl nil floor_ceil nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (cos_cos_phase formula-decl nil sincos_def nil)
    (a!1 skolem-const-decl "real" sincos_def nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (odd_plus_odd_is_even application-judgement "even_int" integers
     nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" reals nil)
    (cos_phase_neg formula-decl nil sincos_phase nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (cos const-decl "real" sincos_def nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (cos_cos_value formula-decl nil sincos_def nil)
    (cos_value_strict_decreasing formula-decl nil sincos_quad nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan nil)
    (nnreal_le_pi nonempty-type-eq-decl nil acos 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)
    (cos_value_pi2 formula-decl nil sincos_quad nil)
    (strict_decreasing? const-decl "bool" real_fun_preds "reals/")
    (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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (cos_range application-judgement "trig_range" 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (<= const-decl "bool" reals nil)
    (Tan? const-decl "bool" sincos_def nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   shostak))
(tan_tan_value_TCC1 0
  (tan_tan_value_TCC1-1 nil 3294926396
   ("" (lemma "tan_value_TCC")
    (("" (skosimp) (("" (inst - "a!1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (tan_value_TCC formula-decl nil sincos_def nil))
   shostak))
(tan_tan_value_TCC2 0
  (tan_tan_value_TCC2-1 nil 3294926396
   ("" (skosimp)
    (("" (expand "abs")
      (("" (case-replace "a!1<0")
        (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (< const-decl "bool" reals nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil))
   shostak))
(tan_tan_value 0
  (tan_tan_value-1 nil 3294927207
   ("" (skosimp)
    (("" (expand "tan")
      (("" (rewrite "tan_value_def")
        (("1" (rewrite "sin_sin_value")
          (("1" (case-replace "cos(a!1) = cos_value(abs(a!1))")
            (("1" (hide 2)
              (("1" (expand "abs")
                (("1" (case-replace "a!1<0")
                  (("1" (expand "cos")
                    (("1"
                      (lemma "floor_div"
                       ("x" "a!1" "py" "2*pi" "i" "-1"))
                      (("1" (assert)
                        (("1" (replace -1)
                          (("1" (lemma "cos_phase_neg" ("px" "-a!1"))
                            (("1" (replace -1)
                              (("1"
                                (lemma "cos_cos_phase" ("a" "-a!1"))
                                (("1"
                                  (lemma "cos_cos_value" ("a" "-a!1"))
                                  (("1" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (rewrite "cos_cos_value")
                    (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (expand "abs")
              (("2" (case-replace "a!1<0")
                (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (expand "abs")
          (("2" (case-replace "a!1<0")
            (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((tan const-decl "real" sincos_def nil)
    (sin_sin_value formula-decl nil sincos_def 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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (floor_div formula-decl nil floor_ceil nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (integer nonempty-type-from-decl nil integers nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (cos_cos_value formula-decl nil sincos_def nil)
    (cos_cos_phase formula-decl nil sincos_def nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (cos_phase_neg formula-decl nil sincos_phase nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (odd_plus_odd_is_even application-judgement "even_int" integers
     nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (cos const-decl "real" sincos_def nil)
    (nnreal type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (nnreal_le_pi nonempty-type-eq-decl nil acos nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad
     nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (cos_range application-judgement "trig_range" sincos_def nil)
    (sin_range application-judgement "trig_range" sincos_def nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (pi const-decl "posreal" atan nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (tan_value_def formula-decl nil tan_quad nil))
   shostak))
(sin_asin 0
  (sin_asin-1 nil 3294919880
   ("" (skosimp)
    (("" (typepred "asin(x!1)")
      (("" (expand "abs")
        (("" (lemma "sin_phase_asin" ("xa" "x!1"))
          (("" (case-replace "x!1<0")
            (("1" (lemma "asin_strict_increasing")
              (("1" (expand "strict_increasing?")
                (("1" (inst - "x!1" "0")
                  (("1" (rewrite "asin_0")
                    (("1" (assert)
                      (("1" (expand "sin")
                        (("1"
                          (lemma "floor_div"
                           ("x" "asin(x!1)" "py" "2*pi" "i" "-1"))
                          (("1" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil)
                   ("2" (expand "abs") (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (assert)
              (("2" (expand "sin")
                (("2" (typepred "asin(x!1)")
                  (("2" (expand "abs")
                    (("2" (lemma "asin_strict_increasing")
                      (("2" (expand "strict_increasing?")
                        (("2" (case-replace "x!1=0")
                          (("1" (rewrite "asin_0")
                            (("1" (assert) nil nil)) nil)
                           ("2" (inst - "0" "x!1")
                            (("1" (rewrite "asin_0")
                              (("1"
                                (assert)
                                (("1"
                                  (lemma
                                   "floor_0"
                                   ("x" "asin(x!1) / (2 * pi)"))
                                  (("1"
                                    (rewrite "div_mult_pos_lt1" -1)
                                    (("1"
                                      (rewrite "div_mult_pos_le2" -1)
                                      (("1"
                                        (flatten)
                                        (("1"
                                          (replace -1)
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "abs")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((trig_range type-eq-decl nil sincos_def nil)
    (asin const-decl "real_abs_le_pi2" asin nil)
    (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pi const-decl "posreal" atan nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (<= const-decl "bool" reals 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)
    (< const-decl "bool" reals nil)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (asin_0 formula-decl nil asin nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sin const-decl "real" sincos_def nil)
    (odd_plus_odd_is_even application-judgement "even_int" integers
     nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (integer nonempty-type-from-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)
    (floor_div formula-decl nil floor_ceil nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sin_range application-judgement "trig_range" sincos_def nil)
    (asin_strict_increasing formula-decl nil asin nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (floor_0 formula-decl nil floor_ceil nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (sin_phase_asin formula-decl nil sincos_phase nil))
   shostak))
(cos_acos 0
  (cos_acos-1 nil 3294922021
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (typepred "acos(x!1)")
        (("1" (expand "cos")
          (("1" (lemma "floor_0" ("x" "acos(x!1) / (2 * pi)"))
            (("1" (rewrite "div_mult_pos_lt1" -1)
              (("1" (rewrite "div_mult_pos_le2" -1)
                (("1" (assert)
                  (("1" (replace -1)
                    (("1" (assert)
                      (("1" (rewrite "cos_phase_acos") nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (expand "abs")
          (("2" (case-replace "x!1<0")
            (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((trig_range type-eq-decl nil sincos_def nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (<= const-decl "bool" reals 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)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (cos const-decl "real" sincos_def nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (cos_phase_acos formula-decl nil sincos_phase nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (floor_0 formula-decl nil floor_ceil nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (>= const-decl "bool" reals nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (nnreal type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan nil)
    (nnreal_le_pi nonempty-type-eq-decl nil acos nil)
    (acos const-decl "nnreal_le_pi" acos nil))
   shostak))
(tan_atan_TCC1 0
  (tan_atan_TCC1-1 nil 3294924365
   ("" (skosimp)
    (("" (typepred "atan(a!1)")
      (("" (lemma "tan_value_TCC" ("a" "atan(a!1)"))
        (("" (expand "abs")
          (("" (expand "pi")
            (("" (expand "atan")
              (("" (case-replace "atan_value(a!1) < 0")
                (("1" (assert) nil nil)
                 ("2" (assert) (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((atan const-decl "real_abs_lt_pi2" atan nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pi const-decl "posreal" atan nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals 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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (atan_value const-decl "real" atan nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (tan_value_TCC formula-decl nil sincos_def nil))
   shostak))
(tan_atan 0
  (tan_atan-3 nil 3408979506
   ("" (skosimp)
    (("" (typepred "atan(a!1)")
      (("" (case-replace "2 * atan_value(1)=pi/2")
        (("1" (lemma "tan_tan_value" ("a" "atan(a!1)"))
          (("1" (split -1)
            (("1" (expand "tan_value")
              (("1" (lemma "atan_bij")
                (("1" (replace -2 1)
                  (("1" (hide -2 -3)
                    (("1"
                      (lemma "comp_inverse_left[real, real_abs_lt_pi2]"
                       ("f" "atan" "x" "a!1"))
                      (("1" (propax) nil nil) ("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (propax) nil nil) ("3" (propax) nil nil))
            nil))
          nil)
         ("2" (expand "pi")
          (("2" (expand "atan") (("2" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((atan const-decl "real_abs_lt_pi2" atan nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pi const-decl "posreal" atan nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals 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)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (tan_tan_value formula-decl nil sincos_def nil)
    (tan_value const-decl "[real_abs_lt_pi2 -> real]" tan_quad nil)
    (comp_inverse_left formula-decl nil function_inverse nil)
    (bijective? const-decl "bool" functions nil)
    (atan_bij formula-decl nil atan nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (atan_value const-decl "real" atan nil))
   nil)
  (tan_atan-2 nil 3408966474
   ("" (skosimp)
    (("" (typepred "atan(a!1)")
      (("" (case-replace "2 * atan_value(1)=pi/2")
        (("1" (lemma "tan_tan_value" ("a" "atan(a!1)"))
          (("1" (split -1)
            (("1" (expand "tan_value")
              (("1" (lemma "atan_bij")
                (("1" (replace -2 1)
                  (("1" (hide -2 -3)
                    (("1"
                      (lemma "comp_inverse_left[real, real_abs_lt_pi]"
                       ("f" "atan" "x" "a!1"))
                      (("1" (propax) nil nil) ("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (propax) nil nil) ("3" (propax) nil nil))
            nil))
          nil)
         ("2" (expand "pi")
          (("2" (expand "atan") (("2" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((atan_value const-decl "real" atan nil)
    (atan_bij formula-decl nil atan nil)
    (tan_value const-decl "[real_abs_lt_pi2 -> real]" tan_quad nil)
    (pi const-decl "posreal" atan nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (atan const-decl "real_abs_lt_pi2" atan nil))
   nil)
  (tan_atan-1 nil 3294923216
   ("" (skosimp)
    (("" (typepred "atan(a!1)")
      (("" (case-replace "2 * atan_value(1)=pi/2")
        (("1" (lemma "tan_tan_value" ("a" "atan(a!1)"))
          (("1" (split -1)
            (("1" (expand "tan_value")
              (("1" (lemma "atan_bij")
                (("1" (replace -2 1)
                  (("1" (hide -2 -3)
                    (("1"
                      (lemma "comp_inverse_left[real, real_mpi_ppi]"
                       ("f" "atan" "x" "a!1"))
                      (("1" (propax) nil nil) ("2" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand "abs")
              (("2" (case-replace "atan(a!1) < 0")
                (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
              nil)
             ("3" (expand "abs")
              (("3" (case-replace "atan(a!1) < 0")
                (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (expand "pi")
          (("2" (expand "atan") (("2" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((pi const-decl "posreal" atan nil)
    (atan const-decl "real_abs_lt_pi2" atan nil)
    (atan_value const-decl "real" atan nil)
    (tan_value const-decl "[real_abs_lt_pi2 -> real]" tan_quad nil)
    (atan_bij formula-decl nil atan nil))
   shostak))
(asin_sin 0
  (asin_sin-2 nil 3323081477
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (lemma "asin_bij")
        ((""
          (lemma "bijective_inverse[real_abs_le1, real_abs_le_pi2]"
           ("f" "asin" "y" "x!1" "x" "sin(x!1)"))
          (("1" (assert)
            (("1" (hide 2)
              (("1" (rewrite "sin_sin_value" 1)
                (("1" (expand "sin_value") (("1" (propax) nil nil))
                  nil)
                 ("2" (expand "abs") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (propax) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pi const-decl "posreal" atan nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (<= const-decl "bool" reals 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)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (asin const-decl "real_abs_le_pi2" asin nil)
    (bijective? const-decl "bool" functions nil)
    (sin const-decl "real" sincos_def nil)
    (bijective_inverse formula-decl nil function_inverse nil)
    (sin_range application-judgement "trig_range" sincos_def nil)
    (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]"
     sincos_quad nil)
    (sin_sin_value formula-decl nil sincos_def nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (asin_bij formula-decl nil asin nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   nil))
(acos_cos 0
  (acos_cos-1 nil 3294927744
   ("" (skosimp)
    (("" (lemma "acos_bij")
      (("" (typepred "x!1")
        (("" (typepred "cos(x!1)")
          ((""
            (lemma "bijective_inverse[real_abs_le1, nnreal_le_pi]"
             ("f" "acos" "x" "cos(x!1)" "y" "x!1"))
            (("1" (assert)
              (("1" (hide 2)
                (("1" (rewrite "cos_cos_value" 1)
                  (("1" (expand "cos_value") (("1" (propax) nil nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (propax) nil nil)
             ("3" (expand "abs")
              (("3" (case-replace "cos(x!1) < 0")
                (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((acos_bij formula-decl nil acos nil)
    (cos const-decl "real" sincos_def nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (cos_range application-judgement "trig_range" sincos_def nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (cos_cos_value formula-decl nil sincos_def nil)
    (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad
     nil)
    (bijective_inverse formula-decl nil function_inverse nil)
    (bijective? const-decl "bool" functions nil)
    (acos const-decl "nnreal_le_pi" acos nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin 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 "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan nil)
    (nnreal_le_pi nonempty-type-eq-decl nil acos nil))
   shostak))
(atan_tan_TCC1 0
  (atan_tan_TCC1-1 nil 3294926402
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (lemma "tan_value_TCC" ("a" "x!1"))
        (("" (expand "abs")
          (("" (case-replace "x!1<0")
            (("1" (assert) nil nil)
             ("2" (assert) (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pi const-decl "posreal" atan nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals 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)
    (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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (tan_value_TCC formula-decl nil sincos_def nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   shostak))
(atan_tan 0
  (atan_tan-3 nil 3408979532
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (case "-pi/2 < x!1 & x!1 < pi/2")
        (("1" (flatten)
          (("1" (lemma "atan_bij")
            (("1"
              (lemma "bijective_inverse[real, real_abs_lt_pi2]"
               ("f" "atan" "x" "tan(x!1)" "y" "x!1"))
              (("1" (assert)
                (("1" (hide 2)
                  (("1" (rewrite "tan_tan_value" 1)
                    (("1" (expand "tan_value") (("1" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (propax) nil nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (case-replace "x!1<0")
            (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pi const-decl "posreal" atan nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals 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)
    (atan const-decl "real_abs_lt_pi2" atan nil)
    (bijective? const-decl "bool" functions nil)
    (tan const-decl "real" sincos_def nil)
    (Tan? const-decl "bool" sincos_def nil)
    (bijective_inverse formula-decl nil function_inverse nil)
    (tan_value const-decl "[real_abs_lt_pi2 -> real]" tan_quad nil)
    (tan_tan_value formula-decl nil sincos_def nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (atan_bij formula-decl nil atan nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil))
   nil)
  (atan_tan-2 nil 3408966519
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (case "-pi/2 < x!1 & x!1 < pi/2")
        (("1" (flatten)
          (("1" (lemma "atan_bij")
            (("1"
              (lemma "bijective_inverse[real, real_abs_lt_pi]"
               ("f" "atan" "x" "tan(x!1)" "y" "x!1"))
              (("1" (assert)
                (("1" (hide 2)
                  (("1" (rewrite "tan_tan_value" 1)
                    (("1" (expand "tan_value") (("1" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (propax) nil nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (case-replace "x!1<0")
            (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((atan_bij formula-decl nil atan nil)
--> --------------------

--> maximum size reached

--> --------------------

quality100%

¤ Dauer der Verarbeitung: 0.41 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.