products/sources/formale Sprachen/C/Lyx/src/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: to2pi.prf   Sprache: Unknown

(to2pi
 (to2pi_TCC1 0
  (to2pi_TCC1-2 nil 3460903442
   ("" (skeep)
    (("" (typepred "floor(a/(2*pi))")
      (("" (name-replace "ff" "floor(a/(2*pi))")
        (("" (grind-reals) 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)
    (AND const-decl "[bool, bool -> bool]" 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)
    (<= 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)
    (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)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (neg_times_lt formula-decl nil real_props nil)
    (neg_times_le formula-decl nil real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil))
   nil)
  (to2pi_TCC1-1 nil 3460903434 ("" (subtype-tcc) nil nil) nil nil))
 (to2pi_id 0
  (to2pi_id-1 nil 3460907374
   ("" (skeep)
    (("" (expand "to2pi")
      (("" (typepred "alpha")
        (("" (typepred "floor(alpha / (2 * pi))")
          (("" (div-by -5 "2*pi")
            (("" (div-by -4 "2*pi")
              (("" (name-replace "aa" "alpha/(2*pi)")
                (("" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (to2pi const-decl "nnreal_lt_2pi" to2pi 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)
    (AND const-decl "[bool, bool -> bool]" 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)
    (<= const-decl "bool" reals nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (both_sides_div_pos_ge1 formula-decl nil real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_simp formula-decl nil real_props nil)
    (both_sides_div_pos_lt1 formula-decl nil real_props 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields 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_lt_2pi nonempty-type-eq-decl nil atan2 nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   shostak))
 (to2pi_period 0
  (to2pi_period-1 nil 3460907724
   ("" (skeep) (("" (expand "to2pi") (("" (assert) nil nil)) nil)) nil)
   ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (to2pi const-decl "nnreal_lt_2pi" to2pi nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (sin_id_to2pi 0
  (sin_id_to2pi-1 nil 3461066796
   ("" (skeep)
    (("" (expand "to2pi")
      (("" (lemma "sin_period")
        (("" (inst -1 "a" "-(floor(a / (2 * pi)))")
          (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (to2pi const-decl "nnreal_lt_2pi" to2pi nil)
    (minus_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)
    (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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields 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)
    (+ 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_range application-judgement "trig_range" sincos_def nil)
    (real_plus_real_is_real application-judgement "real" reals 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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sin_period formula-decl nil trig_basic nil))
   shostak))
 (cos_id_to2pi 0
  (cos_id_to2pi-1 nil 3461066841
   ("" (skeep)
    (("" (expand "to2pi")
      (("" (lemma "cos_period")
        (("" (inst -1 "a" "-(floor(a / (2 * pi)))")
          (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (to2pi const-decl "nnreal_lt_2pi" to2pi nil)
    (minus_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)
    (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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields 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)
    (+ 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)
    (cos_range application-judgement "trig_range" sincos_def nil)
    (real_plus_real_is_real application-judgement "real" reals 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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (cos_period formula-decl nil trig_basic nil))
   shostak))
 (to2pi_to2pi 0
  (to2pi_to2pi-1 nil 3460907618
   ("" (skeep)
    (("" (expand "to2pi" 1 2)
      (("" (lemma "to2pi_period")
        (("" (inst -1 "a+b" "-floor(a / (2 * pi))")
          (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (to2pi const-decl "nnreal_lt_2pi" to2pi nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields 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 "[numfield -> numfield]" number_fields 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)
    (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)
    (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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (to2pi_period formula-decl nil to2pi nil))
   shostak))
 (to2pi_to2pi_sub 0
  (to2pi_to2pi_sub-1 nil 3578251257
   ("" (skosimp*)
    (("" (expand "to2pi" 1 2)
      (("" (lemma "to2pi_period")
        (("" (inst -1 "b!1 - a!1" "floor((a!1 / (2 * pi)))")
          (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (to2pi const-decl "nnreal_lt_2pi" to2pi nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (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)
    (+ 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)
    (real_plus_real_is_real application-judgement "real" reals 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)
    (to2pi_period formula-decl nil to2pi nil))
   shostak))
 (to2pi_neg 0
  (to2pi_neg-1 nil 3460909105
   ("" (skeep)
    (("" (expand "to2pi")
      (("" (typepred "floor(a / (2 * pi))")
        (("" (div-by -3 "2*pi")
          (("" (div-by -4 "2*pi") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (to2pi const-decl "nnreal_lt_2pi" to2pi nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (both_sides_div_pos_le1 formula-decl nil real_props nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nnreal_div_posreal_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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (int_plus_int_is_int application-judgement "int" integers 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)
    (both_sides_div_pos_lt1 formula-decl nil real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals 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)
    (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)
    (AND const-decl "[bool, bool -> bool]" booleans 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))
 (to2pi_equal 0
  (to2pi_equal-2 nil 3601824842
   ("" (skosimp*)
    (("" (expand "to2pi")
      (("" (inst 1 "floor(a!1/(2*pi)-floor(b!1/(2*pi)))")
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (to2pi const-decl "nnreal_lt_2pi" to2pi nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (real_plus_real_is_real application-judgement "real" reals 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (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)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil)
  (to2pi_equal-1 nil 3601824780
   ("" (skosimp*)
    (("" (expand "to2pi")
      (("" (inst 1 "floor(alpha!1/(2*pi)-floor(beta!1/(2*pi)))")
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((nnreal_lt_2pi nonempty-type-eq-decl nil atan2 nil)) nil))
 (to2pi_to2pi_add 0
  (to2pi_to2pi_add-1 nil 3578320604
   ("" (skosimp*)
    (("" (expand "to2pi" 1 2)
      (("" (lemma "to2pi_period")
        (("" (inst - "a!1+b!1" "-floor(a!1/(2*pi))")
          (("" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (to2pi const-decl "nnreal_lt_2pi" to2pi nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields 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 "[numfield -> numfield]" number_fields 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)
    (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)
    (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)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (to2pi_period formula-decl nil to2pi nil))
   shostak))
 (to2pi_closed_diff 0
  (to2pi_closed_diff-1 nil 3569609817
   ("" (skeep)
    (("" (lemma "abs_lt") (("" (inst?) (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((abs_lt formula-decl nil abs_lems "reals/")
    (minus_nzreal_is_nzreal application-judgement "nzreal" 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (to2pi const-decl "nnreal_lt_2pi" to2pi nil)
    (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 nil)
    (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (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)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (to2pi_eq 0
  (to2pi_eq-1 nil 3578945120
   ("" (skosimp*)
    (("" (replace -1)
      (("" (lemma "to2pi_period")
        (("" (inst -1 "b!1" "k!1") (("" (assert) nil 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)
    (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)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals 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)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (to2pi_period formula-decl nil to2pi nil))
   shostak))
 (to2pi_sep 0
  (to2pi_sep-1 nil 3578908896
   ("" (skosimp*)
    (("" (case "a!1 < 2*pi*floor(b!1/(2*pi))")
      (("1" (inst 1 "floor(b!1 / (2 * pi))")
        (("1" (hide 2)
          (("1" (split)
            (("1" (assert) nil nil)
             ("2" (typepred "floor(b!1 / (2 * pi))")
              (("2" (hide -2 -3 -4 -5)
                (("2" (mult-by -1 "2*pi") (("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (inst 2 "floor(b!1 / (2 * pi))")
          (("2" (typepred "floor(b!1 / (2 * pi))")
            (("2" (mult-by -2 "2*pi")
              (("2" (mult-by -1 "2*pi")
                (("2" (split)
                  (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" 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)
    (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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (posreal_times_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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
     nil)
    (div_cancel2 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int nonempty-type-eq-decl nil integers nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil))
   shostak))
 (sin_gt_to2pi 0
  (sin_gt_to2pi-1 nil 3460984720
   ("" (skeep)
    (("" (lemma "sin_gt")
      (("" (inst -1 "to2pi(a+pi/2)-pi/2" "b")
        (("" (assert)
          (("" (typepred "to2pi(pi / 2 + a)")
            (("" (assert)
              (("" (replaces -3 :dir rl)
                ((""
                  (case-replace "sin(a) = sin(to2pi(pi/2+a) - pi/2)")
                  (("1" (assert) nil nil)
                   ("2" (hide-all-but 1)
                    (("2" (expand "to2pi")
                      (("2" (lemma "sin_period")
                        (("2"
                          (inst -1 "a"
                           "-floor((pi / 2 + a) / (2 * pi))")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sin_gt formula-decl nil trig_ineq nil)
    (sin_range application-judgement "trig_range" sincos_def nil)
    (real_gt_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_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)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sin const-decl "real" sincos_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (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)
    (sin_period formula-decl nil trig_basic nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (to2pi const-decl "nnreal_lt_2pi" to2pi nil)
    (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 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 "[numfield, numfield -> numfield]" number_fields nil)
    (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (sin_lt_to2pi 0
  (sin_lt_to2pi-1 nil 3460984754
   ("" (skeep)
    (("" (lemma "sin_lt")
      (("" (inst -1 "to2pi(a+pi/2)-pi/2" "b")
        (("" (assert)
          (("" (typepred "to2pi(pi / 2 + a)")
            (("" (assert)
              (("" (replaces -3 :dir rl)
                ((""
                  (case-replace "sin(a) = sin(to2pi(pi/2+a) - pi/2)")
                  (("1" (assert) nil nil)
                   ("2" (hide-all-but 1)
                    (("2" (expand "to2pi")
                      (("2" (lemma "sin_period")
                        (("2"
                          (inst -1 "a"
                           "-floor((pi / 2 + a) / (2 * pi))")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sin_lt formula-decl nil trig_ineq nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sin_range application-judgement "trig_range" sincos_def 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)
    (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)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sin const-decl "real" sincos_def nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (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)
    (sin_period formula-decl nil trig_basic nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (to2pi const-decl "nnreal_lt_2pi" to2pi nil)
    (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 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 "[numfield, numfield -> numfield]" number_fields nil)
    (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   nil))
 (sin_ge_to2pi 0
  (sin_ge_to2pi-1 nil 3460994922
   ("" (skeep)
    (("" (lemma "sin_lt_to2pi")
      (("" (inst -1 "a" "b") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((sin_lt_to2pi formula-decl nil to2pi nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sin_range application-judgement "trig_range" sincos_def nil)
    (real_ge_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_plus_real_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)
    (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))
 (cos_pos_to2pi 0
  (cos_pos_to2pi-1 nil 3461066356
   ("" (skeep)
    (("" (name-replace "bb" "a+pi/2" :hide? nil)
      (("" (move-terms -1 l 2)
        (("" (replaces -1)
          (("" (rewrite "cos_minus")
            (("" (rewrite "cos_pi2")
              (("" (rewrite "sin_pi2")
                (("" (assert)
                  (("" (rewrite "sin_id_to2pi" :dir rl)
                    (("" (split 1)
                      (("1" (flatten)
                        (("1" (split)
                          (("1" (typepred "to2pi(bb)")
                            (("1" (case-replace "to2pi(bb) = 0")
                              (("1"
                                (rewrite "sin_0")
                                (("1" (assert) nil nil))
                                nil)
                               ("2" (assert) nil nil))
                              nil))
                            nil)
                           ("2" (lemma "sin_le_0")
                            (("2" (inst?) (("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (flatten)
                        (("2" (lemma "sin_gt_0")
                          (("2" (inst?) (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_plus_real_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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" 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)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     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)
    (cos_pi2 formula-decl nil trig_basic 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_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sin_0 formula-decl nil trig_basic nil)
    (to2pi const-decl "nnreal_lt_2pi" to2pi nil)
    (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sin_le_0 formula-decl nil trig_ineq nil)
    (sin_gt_0 formula-decl nil trig_ineq nil)
    (sin_id_to2pi formula-decl nil to2pi nil)
    (sin_pi2 formula-decl nil trig_basic nil)
    (real_times_real_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)
    (cos_minus formula-decl nil trig_basic nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields
       nil))
   shostak))
 (cos_nneg_to2pi 0
  (cos_nneg_to2pi-1 nil 3461081667
   ("" (skeep)
    (("" (name-replace "bb" "a+pi/2" :hide? nil)
      (("" (move-terms -1 l 2)
        (("" (replaces -1)
          (("" (rewrite "cos_minus")
            (("" (rewrite "cos_pi2")
              (("" (rewrite "sin_pi2")
                (("" (assert)
                  (("" (rewrite "sin_id_to2pi" :dir rl)
                    (("" (split 1)
                      (("1" (flatten)
                        (("1" (lemma "sin_lt_0")
                          (("1" (inst?) (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (flatten)
                        (("2" (lemma "sin_ge_0")
                          (("2" (inst?) (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_plus_real_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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" 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)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     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)
    (cos_pi2 formula-decl nil trig_basic nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sin_lt_0 formula-decl nil trig_ineq 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)
    (nnreal type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 nil)
    (to2pi const-decl "nnreal_lt_2pi" to2pi nil)
    (sin_ge_0 formula-decl nil trig_ineq nil)
    (sin_id_to2pi formula-decl nil to2pi nil)
    (sin_pi2 formula-decl nil trig_basic nil)
    (real_times_real_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)
    (cos_minus formula-decl nil trig_basic nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields
       nil))
   nil)))

[ Dauer der Verarbeitung: 0.20 Sekunden  (vorverarbeitet)  ]