|
(trig_basic
(sin2_cos2 0
(sin2_cos2-1 nil 3265002048
("" (skosimp*)
(("" (expand "sin")
(("" (expand "cos")
(("" (lemma "floor_def" ("x" "a!1 / (2 * pi)"))
(("" (rewrite "div_mult_pos_le2" -1)
(("" (rewrite "div_mult_pos_lt1" -1)
(("" (flatten -1)
((""
(lemma "sin2_cos2_phase"
("x" "a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)"))
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
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)
(sin const-decl "real" sincos_def nil)
(pi const-decl "posreal" atan nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(floor_def formula-decl nil floor_ceil nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(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_minus_real_is_real application-judgement "real" reals nil)
(sin2_cos2_phase formula-decl nil sincos_phase nil)
(nnreal type-eq-decl nil real_types nil)
(trig_phase nonempty-type-eq-decl nil sincos_phase nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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) (<= 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)
(div_mult_pos_le2 formula-decl nil real_props nil)
(cos const-decl "real" sincos_def nil))
shostak))
(cos2 0
(cos2-1 nil 3265002167
("" (skosimp*)
(("" (lemma "sin2_cos2" ("a" "a!1")) (("" (assert) nil nil)) nil))
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)
(sin2_cos2 formula-decl nil trig_basic nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(sin2 0
(sin2-1 nil 3265002192
("" (skosimp*)
(("" (lemma "sin2_cos2" ("a" "a!1")) (("" (assert) nil nil)) nil))
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)
(sin2_cos2 formula-decl nil trig_basic nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_minus_real_is_real application-judgement "real" reals nil))
shostak))
(cos_0 0
(cos_0-1 nil 3265002205
("" (expand "cos")
(("" (rewrite "floor_int") (("" (rewrite "cos_phase_0") nil nil))
nil))
nil)
((AND const-decl "[bool, bool -> bool]" booleans nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(floor_int formula-decl nil floor_ceil 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 "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)
(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)
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(cos_phase_0 formula-decl nil sincos_phase nil)
(cos const-decl "real" sincos_def nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil 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))
shostak))
(sin_0 0
(sin_0-1 nil 3265002237
("" (expand "sin")
(("" (rewrite "floor_int") (("" (rewrite "sin_phase_0") nil nil))
nil))
nil)
((AND const-decl "[bool, bool -> bool]" booleans nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(floor_int formula-decl nil floor_ceil 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 "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)
(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)
(real_times_real_is_real application-judgement "real" reals nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(sin_phase_0 formula-decl nil sincos_phase nil)
(sin const-decl "real" sincos_def nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil 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))
shostak))
(sin_pi2 0
(sin_pi2-1 nil 3265002302
("" (expand "sin")
(("" (rewrite "div_div2")
(("" (lemma "div_cancel1" ("x" "1/4" "n0z" "pi"))
(("" (replace -1)
(("" (lemma "floor_val" ("i" "1" "j" "4" "k" "0"))
(("" (split -1)
(("1" (replace -1)
(("1" (rewrite "sin_phase_pi2") nil nil)) nil)
("2" (assert) nil nil) ("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((div_div2 formula-decl nil real_props 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)
(/= const-decl "boolean" notequal nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> 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)
(sin_phase_pi2 formula-decl nil sincos_phase nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(even_plus_odd_is_odd application-judgement "odd_int" integers nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer nonempty-type-from-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(floor_val formula-decl nil floor_ceil nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(div_cancel1 formula-decl nil real_props nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(sin const-decl "real" sincos_def nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
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))
shostak))
(cos_pi2 0
(cos_pi2-1 nil 3265002447
("" (lemma "sin2_cos2" ("a" "pi/2"))
(("" (rewrite "sin_pi2")
(("" (rewrite "sq_1")
(("" (lemma "sq_eq_0" ("a" "cos(pi/2)"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil)
((sin_pi2 formula-decl nil trig_basic nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(sq_eq_0 formula-decl nil sq "reals/")
(cos const-decl "real" sincos_def nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(sq_nz_pos application-judgement "posreal" sq "reals/")
(sq_1 formula-decl nil sq "reals/")
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin2_cos2 formula-decl nil trig_basic 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 "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))
shostak))
(tan_0_TCC1 0
(tan_0_TCC1-1 nil 3264999490
("" (expand "Tan?")
(("" (expand "cos")
(("" (rewrite "floor_int")
(("" (rewrite "cos_phase_0") (("" (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)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(cos const-decl "real" sincos_def nil)
(cos_phase_0 formula-decl nil sincos_phase nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_times_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)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(integer nonempty-type-from-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(floor_int formula-decl nil floor_ceil nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(Tan? const-decl "bool" sincos_def nil))
shostak))
(tan_0 0
(tan_0-1 nil 3265002274
("" (expand "tan")
(("" (rewrite "sin_0")
(("" (rewrite "cos_0") (("" (assert) nil nil)) nil)) nil))
nil)
((sin_0 formula-decl nil trig_basic nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(cos_0 formula-decl nil trig_basic nil)
(tan const-decl "real" sincos_def nil))
shostak))
(sin_neg 0
(sin_neg-1 nil 3265008367
("" (skosimp*)
(("" (expand "sin")
(("" (lemma "floor_neg" ("x" "a!1/(2*pi)"))
(("" (case "integer?(a!1 / (2 * pi))")
(("1" (assert)
(("1" (replace -2)
(("1" (lemma "floor_def" ("x" "-a!1 / (2 * pi)"))
(("1" (flatten -1)
(("1"
(lemma "div_mult_pos_le2"
("x" "floor(-a!1 / (2 * pi))" "z" "-a!1" "py"
"2 * pi"))
(("1" (replace -1 -2)
(("1"
(lemma "div_mult_pos_lt1"
("x" "floor(-a!1 / (2 * pi))+1" "z" "-a!1"
"py" "2 * pi"))
(("1" (replace -1 -4)
(("1" (hide -1 -2)
(("1" (rewrite "floor_int" -4)
(("1"
(case
"floor(-(a!1 / (2 * pi))) = -a!1/(2*pi)")
(("1"
(replace -1)
(("1"
(lemma
"div_cancel1"
("x" "a!1" "n0z" "2*pi"))
(("1"
(replace -1)
(("1"
(lemma
"div_cancel1"
("x" "-a!1" "n0z" "2*pi"))
(("1"
(replace -1)
(("1"
(simplify 1)
(("1"
(rewrite "sin_phase_0")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (replace -1 2)
(("2" (case "a!1 = - 2 * (floor(-a!1 / (2 * pi)) * pi)")
(("1" (assert) nil nil)
("2"
(lemma "sin_phase_neg"
("px" "-a!1 - 2 * (floor(-a!1 / (2 * pi)) * pi)"))
(("1" (assert) nil nil)
("2" (assert)
(("2" (lemma "floor_def" ("x" "-a!1 / (2 * pi)"))
(("2" (flatten -1)
(("2" (rewrite "div_mult_pos_le2" -1)
(("2" (rewrite "div_mult_pos_lt1" -2)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(minus_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(sin const-decl "real" sincos_def nil)
(integer? const-decl "bool" integers nil)
(floor_int formula-decl nil floor_ceil nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_phase_0 formula-decl nil sincos_phase 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)
(minus_even_is_even application-judgement "even_int" integers nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_cancel1 formula-decl nil real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(int_plus_int_is_int application-judgement "int" integers 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) (<= 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)
(div_mult_pos_le2 formula-decl nil real_props nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(floor_def formula-decl nil floor_ceil nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_int_is_int application-judgement "int" integers nil)
(sin_phase_neg formula-decl nil sincos_phase nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(floor_neg formula-decl nil floor_ceil 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 "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)
(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))
shostak))
(cos_neg 0
(cos_neg-1 nil 3265009425
("" (skosimp*)
(("" (expand "cos")
(("" (lemma "floor_neg" ("x" "a!1 / (2 * pi)"))
(("" (case "integer?(a!1 / (2 * pi))")
(("1" (assert) nil nil)
("2" (assert)
(("2" (replace -1)
(("2"
(case "-a!1 - 2 * (floor(-a!1 / (2 * pi)) * pi) = 0")
(("1" (assert) nil nil)
("2"
(lemma "cos_phase_neg"
("px" "-a!1 - 2 * (floor(-a!1 / (2 * pi)) * pi)"))
(("1" (assert) nil nil)
("2" (lemma "floor_def" ("x" "-a!1 / (2 * pi)"))
(("2" (flatten)
(("2" (rewrite "div_mult_pos_le2" -1)
(("2" (rewrite "div_mult_pos_lt1" -2)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(minus_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(cos const-decl "real" sincos_def nil)
(integer? const-decl "bool" integers nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_int_is_int application-judgement "int" integers nil)
(cos_phase_neg formula-decl nil sincos_phase nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(div_mult_pos_lt1 formula-decl nil real_props 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_plus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(floor_def formula-decl nil floor_ceil nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[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)
(integer nonempty-type-from-decl nil integers 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)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(floor_neg formula-decl nil floor_ceil 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 "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)
(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))
shostak))
(tan_neg_TCC1 0
(tan_neg_TCC1-1 nil 3264999490
("" (skosimp*)
(("" (typepred "a!1")
(("" (expand "Tan?")
(("" (lemma "cos_neg" ("a" "a!1")) (("" (assert) nil nil))
nil))
nil))
nil))
nil)
((Tan? const-decl "bool" sincos_def nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(cos_neg formula-decl nil trig_basic nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(minus_real_is_real application-judgement "real" reals nil))
shostak))
(tan_neg 0
(tan_neg-1 nil 3265006358
("" (skosimp*)
(("" (typepred "a!1")
(("" (expand "Tan?")
(("" (expand "tan")
(("" (rewrite "cos_neg")
(("" (rewrite "sin_neg") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((Tan? const-decl "bool" sincos_def nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(tan const-decl "real" sincos_def nil)
(sin_neg formula-decl nil trig_basic nil)
(minus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_neg formula-decl nil trig_basic nil))
shostak))
(cos_sin 0
(cos_sin-1 nil 3265009874
("" (skosimp*)
(("" (expand "cos")
(("" (expand "sin")
(("" (lemma "floor_def" ("x" "a!1 / (2 * pi)"))
(("" (rewrite "div_mult_pos_le2" -1)
(("" (rewrite "div_mult_pos_lt1" -1)
(("" (lemma "floor_def" ("x" "(pi/2+a!1 )/ (2 * pi)"))
(("" (rewrite "div_mult_pos_le2" -1)
(("" (rewrite "div_mult_pos_lt1" -1)
(("" (flatten)
((""
(lemma "cos_eqv_sin_phase"
("x"
"a!1 - 2 * (floor(a!1 / (2 * pi)) * pi)"))
(("1" (replace -1)
(("1" (hide -1)
(("1"
(lemma "floor_plus"
("x" "a!1 / (2 * pi)" "y" "1/4"))
(("1"
(lemma
"floor_val"
("i" "1" "j" "4" "k" "0"))
(("1"
(split -1)
(("1"
(replace -1)
(("1"
(lemma
"div_cancel1"
("x" "1/4" "n0z" "pi"))
(("1"
(lemma
"div_distributes"
("x"
"pi/2"
"y"
"a!1"
"n0z"
"2*pi"))
(("1"
(replace -2 -1)
(("1"
(replace -1 * rl)
(("1"
(replace -4)
(("1"
(assert)
(("1"
(replace -1)
(("1"
(name
"FL"
"floor(a!1 / (2 * pi))")
(("1"
(replace -1)
(("1"
(case
"fractional(1/4) = 1/4")
(("1"
(replace -1)
(("1"
(case
"fractional(a!1 / (2 * pi)) = a!1/(2*pi) - FL")
(("1"
(replace
-1)
(("1"
(case
"a!1 - 2 * (FL * pi) < 3 * pi / 2")
(("1"
(assert)
(("1"
(case
"floor(1 / 4 + a!1 / (2 * pi) - FL) = 0")
(("1"
(assert)
nil
nil)
("2"
(hide
2)
(("2"
(lemma
"floor_def"
("x"
"1 / 4 + a!1 / (2 * pi) - FL"))
(("2"
(flatten
-1)
(("2"
(name-replace
"K1"
"floor(1 / 4 + a!1 / (2 * pi) - FL)")
(("2"
(lemma
"trichotomy"
("x"
"K1"))
(("2"
(split
-1)
(("1"
(case
"K1=1")
(("1"
(replace
-1)
(("1"
(assert)
nil
nil))
nil)
("2"
(case
"K1>1")
(("1"
(assert)
nil
nil)
("2"
(assert)
nil
nil))
nil))
nil)
("2"
(propax)
nil
nil)
("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(case
"floor(1 / 4 + (a!1 / (2 * pi) - FL)) = 1")
(("1"
(replace
-1)
(("1"
(hide-all-but
(1
2))
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide
3)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand
"fractional"
1)
(("2"
(replace
-2)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand
"fractional"
1)
(("2"
(lemma
"floor_val"
("i"
"1"
"j"
"4"
"k"
"0"))
(("2"
(hide-all-but
(-1
1))
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(cos const-decl "real" sincos_def nil)
(pi const-decl "posreal" atan nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(floor_def formula-decl nil floor_ceil nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(div_mult_pos_lt1 formula-decl nil real_props nil)
(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)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(floor_plus formula-decl nil floor_ceil nil)
(div_cancel1 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(trichotomy formula-decl nil real_axioms nil)
(odd_plus_odd_is_even application-judgement "even_int" integers
nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(fractional const-decl "{x | 0 <= x & x < 1}" floor_ceil nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(div_distributes formula-decl nil real_props nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(even_plus_odd_is_odd application-judgement "odd_int" integers nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(floor_val formula-decl nil floor_ceil nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(trig_phase nonempty-type-eq-decl nil sincos_phase nil)
(nnreal type-eq-decl nil real_types nil)
(cos_eqv_sin_phase formula-decl nil sincos_phase nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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) (<= 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)
(div_mult_pos_le2 formula-decl nil real_props nil)
(sin const-decl "real" sincos_def nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil))
shostak))
(sin_cos 0
(sin_cos-1 nil 3265010005
("" (skosimp*)
(("" (lemma "cos_sin" ("a" "-(a!1+pi/2)"))
(("" (lemma "cos_neg" ("a" "a!1+pi/2"))
(("" (lemma "sin_neg" ("a" "a!1")) (("" (assert) nil nil))
nil))
nil))
nil))
nil)
((pi const-decl "posreal" atan nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(/ const-decl "[numfield, 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)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(cos_sin formula-decl nil trig_basic nil)
(minus_real_is_real application-judgement "real" reals nil)
(sin_neg formula-decl nil trig_basic nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_neg formula-decl nil trig_basic nil)
(real_plus_real_is_real application-judgement "real" reals nil))
shostak))
(sin_shift 0
(sin_shift-1 nil 3265074854
("" (skosimp*)
(("" (lemma "sin_neg" ("a" "pi/2-a!1"))
(("" (lemma "sin_cos" ("a" "a!1-pi/2")) (("" (assert) nil nil))
nil))
nil))
nil)
((pi const-decl "posreal" atan nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(/ const-decl "[numfield, 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)
(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)
(sin_neg formula-decl nil trig_basic nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(cos_range application-judgement "trig_range" sincos_def nil)
(minus_real_is_real application-judgement "real" reals 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)
(sin_range application-judgement "trig_range" sincos_def nil)
(sin_cos formula-decl nil trig_basic nil))
shostak))
(cos_shift 0
(cos_shift-1 nil 3265010327
("" (skosimp*)
(("" (lemma "sin_shift" ("a" "pi/2-a!1")) (("" (assert) nil nil))
nil))
nil)
((pi const-decl "posreal" atan nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(/ const-decl "[numfield, 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)
(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)
(sin_shift formula-decl nil trig_basic nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(cos_range application-judgement "trig_range" sincos_def nil))
shostak))
(neg_cos 0
(neg_cos-1 nil 3265010987
("" (skosimp*)
(("" (rewrite "cos_sin")
(("" (rewrite "sin_cos") (("" (assert) nil nil)) nil)) nil))
nil)
((cos_sin formula-decl nil trig_basic 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)
(cos_range application-judgement "trig_range" sincos_def nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sin_range application-judgement "trig_range" sincos_def nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(minus_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)
(bool nonempty-type-eq-decl nil booleans nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(sin_cos formula-decl nil trig_basic nil))
shostak))
(neg_sin 0
(neg_sin-1 nil 3265071739
("" (skosimp*)
(("" (rewrite "sin_cos")
(("" (rewrite "cos_sin") (("" (assert) nil nil)) nil)) nil))
nil)
((sin_cos formula-decl nil trig_basic 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)
(sin_range application-judgement "trig_range" sincos_def 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)
(cos_range application-judgement "trig_range" sincos_def nil)
(minus_real_is_real application-judgement "real" reals nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi const-decl "posreal" atan nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(cos_sin formula-decl nil trig_basic nil))
shostak))
(sin_pi 0
(sin_pi-1 nil 3265006547
("" (expand "sin")
(("" (lemma "div_cancel1" ("x" "1/2" "n0z" "pi"))
(("" (replace -1 1)
(("" (lemma "floor_val" ("i" "1" "j" "2" "k" "0"))
(("" (split -1)
(("1" (replace -1)
(("1" (assert)
(("1" (expand "sin_phase")
(("1" (lemma "div_cancel1" ("x" "2" "n0z" "pi"))
(("1" (replace -1)
(("1" (rewrite "sin_value_0")
(("1" (rewrite "floor_int" 1)
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil) ("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil 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)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(div_cancel1 formula-decl nil real_props nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(floor_val formula-decl nil floor_ceil nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(integer nonempty-type-from-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(even_plus_odd_is_odd application-judgement "odd_int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_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)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sin_phase const-decl "real_abs_le1" sincos_phase nil)
(floor_int formula-decl nil floor_ceil nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(sin_value_0 formula-decl nil sincos_quad nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(sin const-decl "real" sincos_def nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nonneg_floor_is_nat application-judgement "nat" floor_ceil 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))
shostak))
(cos_pi 0
(cos_pi-2 nil 3279154503
("" (expand "cos")
(("" (lemma "div_cancel1" ("x" "1/2" "n0z" "pi"))
(("" (replace -1)
(("" (lemma "floor_val" ("i" "1" "j" "2" "k" "0"))
(("" (split -1)
(("1" (replace -1)
(("1" (simplify 1)
(("1" (expand "cos_phase")
(("1" (rewrite "cos_value_pi") nil nil)) nil))
nil))
nil)
("2" (assert) nil nil) ("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(numfield nonempty-type-eq-decl nil 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)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(div_cancel1 formula-decl nil real_props nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(floor_val formula-decl nil floor_ceil nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.106Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
