Quelle to2pi.prf Sprache: Lisp

(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 "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (pi_lb const-decl "posreal" trig_basic 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 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)
 (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 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)
 (<= 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)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (pi_lb const-decl "posreal" trig_basic nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 nil)
 (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 nil))
 shostak))
(to2pi_period 0
 (to2pi_period-1 nil 3460907724
 ("" (skeep) (("" (expand "to2pi") (("" (assert) 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)
 (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)
 ((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 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_lb const-decl "posreal" trig_basic nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 nil)
 (sin_range application-judgement "trig_range" trig_basic 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)
 ((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 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_lb const-decl "posreal" trig_basic nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 nil)
 (cos_range application-judgement "trig_range" trig_basic 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)
 ((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 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_lb const-decl "posreal" trig_basic nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 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)
 ((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 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_lb const-decl "posreal" trig_basic nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 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)
 ((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 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_lb const-decl "posreal" trig_basic nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 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)
 ((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 "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (pi_lb const-decl "posreal" trig_basic 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 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)
 ((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 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_lb const-decl "posreal" trig_basic nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 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)
 (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)
 (to2pi const-decl "nnreal_lt_2pi" to2pi nil)
 (nnreal_lt_2pi nonempty-type-eq-decl nil atan2 nil)
 (nnreal type-eq-decl nil real_types nil)
 (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (< const-decl "bool" reals nil)
 (pi_lb const-decl "posreal" trig_basic nil)
 (AND const-decl "[bool, bool -> bool]" booleans 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)
 (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 numfield]" number_fields nil)
 (<= const-decl "bool" reals 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 "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (pi_lb const-decl "posreal" trig_basic nil)
 (AND const-decl "[bool, bool -> bool]" booleans 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)
 (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" trig_basic 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)
 (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" trig_basic 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 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 "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (pi_lb const-decl "posreal" trig_basic nil)
 (AND const-decl "[bool, bool -> bool]" booleans 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" trig_basic 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)
 (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" trig_basic 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 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 "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (pi_lb const-decl "posreal" trig_basic nil)
 (AND const-decl "[bool, bool -> bool]" booleans 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" trig_basic nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props 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)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (pi_lb const-decl "posreal" trig_basic nil)
 (< const-decl "bool" reals nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 nil)
 (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
 nil)
 (posreal_div_posreal_is_posreal application-judgement "posreal"
 real_types 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)
 (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" trig_basic nil)
 (sin_range application-judgement "trig_range" trig_basic 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)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (pi_lb const-decl "posreal" trig_basic nil)
 (< const-decl "bool" reals nil)
 (pi_ub const-decl "posreal" trig_basic nil)
 (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
 nil)
 (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
 nil)
 (posreal_div_posreal_is_posreal application-judgement "posreal"
 real_types 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 "[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" trig_basic nil)
 (sin_range application-judgement "trig_range" trig_basic 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)))

quality98%

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