|
(tan_approx
(tan_lb_ub_TCC1 0
(tan_lb_ub_TCC1-1 nil 3285095221 ("" (skosimp :preds? t) nil nil)
((cos_ub const-decl "real" trig_approx nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(/= const-decl "boolean" notequal nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(tan_ub_lb_TCC1 0
(tan_ub_lb_TCC1-1 nil 3320436455 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(even_plus_odd_is_odd application-judgement "odd_int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(cos_lb const-decl "real" trig_approx nil)
(cos_approx const-decl "real" trig_approx nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil))
nil))
(tan_lb_ub_neg_TCC1 0
(tan_lb_ub_neg_TCC1-1 nil 3285095378
("" (skeep) (("" (rewrite "cos_ub_neg") nil nil)) nil)
((cos_ub_neg formula-decl nil trig_approx nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
shostak))
(tan_lb_ub_neg 0
(tan_lb_ub_neg-1 nil 3285095182
("" (skeep)
(("" (expand* "tan_lb_ub" "tan_ub_ub")
(("" (rewrite "sin_lb_neg")
(("" (rewrite "cos_ub_neg") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((tan_ub_ub const-decl "real" tan_approx nil)
(tan_lb_ub const-decl "real" tan_approx nil)
(cos_ub_neg formula-decl nil trig_approx nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sin_lb_neg formula-decl nil trig_approx nil))
shostak))
(tan_ub_lb_neg_TCC1 0
(tan_ub_lb_neg_TCC1-1 nil 3320436749
("" (skeep) (("" (rewrite "cos_lb_neg") nil nil)) nil)
((cos_lb_neg formula-decl nil trig_approx nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(tan_ub_lb_neg 0
(tan_ub_lb_neg-2 nil 3320436789
("" (skeep)
(("" (expand* "tan_ub_lb" "tan_lb_lb")
(("" (rewrite "sin_ub_neg")
(("" (rewrite "cos_lb_neg") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((tan_lb_lb const-decl "real" tan_approx nil)
(tan_ub_lb const-decl "real" tan_approx nil)
(cos_lb_neg formula-decl nil trig_approx nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sin_ub_neg formula-decl nil trig_approx nil))
nil))
(tan_lb_lb_neg 0
(tan_lb_lb_neg-1 nil 3285095124
("" (skeep)
(("" (expand* "tan_lb_lb" "tan_ub_lb")
(("" (rewrite "sin_lb_neg")
(("" (rewrite "cos_lb_neg") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((tan_ub_lb const-decl "real" tan_approx nil)
(tan_lb_lb const-decl "real" tan_approx nil)
(cos_lb_neg formula-decl nil trig_approx nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sin_lb_neg formula-decl nil trig_approx nil))
shostak))
(tan_ub_ub_neg 0
(tan_ub_ub_neg-1 nil 3285095094
("" (skeep)
(("" (expand* "tan_ub_ub" "tan_lb_ub")
(("" (rewrite "sin_ub_neg")
(("" (rewrite "cos_ub_neg") (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((tan_lb_ub const-decl "real" tan_approx nil)
(tan_ub_ub const-decl "real" tan_approx nil)
(cos_ub_neg formula-decl nil trig_approx nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(sin_ub_neg formula-decl nil trig_approx nil))
shostak))
(tan_bounds_0_pi2_TCC1 0
(tan_bounds_0_pi2_TCC1-1 nil 3285095421
("" (skeep)
(("" (lemma "cos_bounds")
(("" (inst?)
(("" (assert) (("" (flatten) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((cos_bounds formula-decl nil trig_approx nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(tan_bounds_0_pi2_TCC2 0
(tan_bounds_0_pi2_TCC2-1 nil 3285095537
("" (skeep) (("" (rewrite "tan_pi2_def") nil nil)) nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(tan_pi2_def formula-decl nil trig_ineq nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil))
shostak))
(tan_bounds_0_pi2_TCC3 0
(tan_bounds_0_pi2_TCC3-1 nil 3285095563
("" (skeep) (("" (assert) nil nil)) nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(tan_bounds_0_pi2 0
(tan_bounds_0_pi2-2 nil 3285094898
("" (skeep)
(("" (expand "tan")
(("" (expand "tan_lb_ub")
(("" (expand "tan_ub_lb")
(("" (case "cos(a) > 0")
(("1" (case "sin(a) >= 0")
(("1" (lemma "sin_bounds")
(("1" (inst?)
(("1" (assert)
(("1" (flatten)
(("1" (lemma "cos_bounds")
(("1" (inst?)
(("1" (assert)
(("1" (flatten)
(("1"
(split)
(("1"
(cross-mult 1)
(("1"
(case
"sin_lb(a, n) * cos(a) <= sin(a) * cos(a)"
"sin(a) * cos(a) <= sin(a) * cos_ub(a, n)")
(("1" (assert) nil nil)
("2"
(hide -1 2)
(("2"
(cancel-by 1 "sin(a)")
nil
nil))
nil)
("3"
(hide 2)
(("3"
(cancel-by 1 "cos(a)")
nil
nil))
nil))
nil))
nil)
("2"
(cross-mult 1)
(("2"
(case
"sin(a) * cos_lb(a, n) <= sin(a) * cos(a)"
"sin(a) * cos(a) <= sin_ub(a, n) * cos(a)")
(("1" (assert) nil nil)
("2"
(hide -1 2)
(("2"
(cancel-by 1 "cos(a)")
nil
nil))
nil)
("3"
(hide 2)
(("3"
(cancel-by 1 "sin(a)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sin_ge_0") nil nil))
nil)
("2" (rewrite "cos_gt_0") nil nil))
nil))
nil))
nil))
nil))
nil)
((sin_range application-judgement "trig_range" trig_basic nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(tan const-decl "real" trig_basic nil)
(tan_ub_lb const-decl "real" tan_approx nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(cos_gt_0 formula-decl nil trig_ineq nil)
(>= const-decl "bool" reals nil)
(sin const-decl "real" trig_basic nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(sin_ub const-decl "real" trig_approx nil)
(cos_lb const-decl "real" trig_approx nil)
(CBD_7 skolem-const-decl "trig_range" tan_approx nil)
(CBD_6 skolem-const-decl "trig_range" tan_approx nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(sin_lb const-decl "real" trig_approx nil)
(n skolem-const-decl "nat" tan_approx nil)
(a skolem-const-decl "real" tan_approx nil)
(cos_ub const-decl "real" trig_approx nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_times_real_is_real application-judgement "real" reals nil)
(times_div2 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(CBD_5 skolem-const-decl "trig_range" tan_approx nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(trig_range type-eq-decl nil trig_basic nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(CBD_4 skolem-const-decl "trig_range" tan_approx nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(pos_div_gt formula-decl nil real_props nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(zero_times1 formula-decl nil real_props nil)
(<= const-decl "bool" reals nil)
(cos_bounds formula-decl nil trig_approx nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(sin_bounds formula-decl nil trig_approx nil)
(sin_ge_0 formula-decl nil trig_ineq nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals nil)
(cos const-decl "real" trig_basic nil)
(tan_lb_ub const-decl "real" tan_approx nil))
nil))
(tan_bounds_npi2_0_TCC1 0
(tan_bounds_npi2_0_TCC1-1 nil 3285095576
("" (skeep) (("" (assert) nil nil)) nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(tan_bounds_npi2_0_TCC2 0
(tan_bounds_npi2_0_TCC2-1 nil 3285095608
("" (skeep) (("" (rewrite "tan_pi2_def") nil nil)) nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(tan_pi2_def formula-decl nil trig_ineq nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil))
shostak))
(tan_bounds_npi2_0_TCC3 0
(tan_bounds_npi2_0_TCC3-1 nil 3285095637
("" (skeep)
(("" (lemma "cos_bounds")
(("" (inst?)
(("" (assert) (("" (flatten) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((cos_bounds formula-decl nil trig_approx nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(tan_bounds_npi2_0 0
(tan_bounds_npi2_0-2 nil 3321627681
("" (skeep)
(("" (lemma "tan_bounds_0_pi2")
(("" (inst -1 "-a" "n")
(("" (assert)
(("" (rewrite "cos_lb_neg")
(("" (assert)
(("" (flatten)
(("" (lemma "cos_bounds")
(("" (inst?)
(("" (assert)
(("" (flatten)
(("" (rewrite "tan_neg")
(("1" (rewrite "tan_lb_ub_neg")
(("1" (rewrite "tan_ub_lb_neg")
(("1" (assert) nil nil)) nil))
nil)
("2" (expand "Tan?")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((tan_bounds_0_pi2 formula-decl nil tan_approx nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(cos_bounds formula-decl nil trig_approx nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(Tan? const-decl "bool" trig_basic nil)
(tan_neg formula-decl nil trig_basic nil)
(tan_ub_lb_neg formula-decl nil tan_approx nil)
(tan_lb_ub_neg formula-decl nil tan_approx nil)
(cos_lb_neg formula-decl nil trig_approx nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(minus_real_is_real application-judgement "real" reals nil))
nil))
(tan_bounds_pi2_pi_TCC1 0
(tan_bounds_pi2_pi_TCC1-1 nil 3285095674
("" (skeep) (("" (assert) nil nil)) nil)
((posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(tan_bounds_pi2_pi_TCC2 0
(tan_bounds_pi2_pi_TCC2-1 nil 3285095683
("" (skeep)
(("" (expand "Tan?")
(("" (lemma "cos_bounds")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((Tan? const-decl "bool" 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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(cos_bounds formula-decl nil trig_approx nil))
shostak))
(tan_bounds_pi2_pi_TCC3 0
(tan_bounds_pi2_pi_TCC3-1 nil 3285095728
("" (skeep)
(("" (lemma "cos_bounds")
(("" (inst?)
(("" (assert) (("" (flatten) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((cos_bounds formula-decl nil trig_approx nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(tan_bounds_pi2_pi 0
(tan_bounds_pi2_pi-2 nil 3321627705
("" (skeep)
(("" (expand "tan")
(("" (expand "tan_ub_ub")
(("" (expand "tan_lb_lb")
(("" (case "cos(a) < 0")
(("1" (case "sin(a) >= 0")
(("1" (lemma "cos_bounds")
(("1" (inst?)
(("1" (assert)
(("1" (flatten)
(("1" (lemma "sin_bounds")
(("1" (inst?)
(("1" (assert)
(("1" (flatten)
(("1"
(split)
(("1"
(cross-mult 1)
(("1"
(case
"sin_ub(a, n) * cos(a) <= sin(a) * cos(a)"
"sin(a) * cos(a) <= sin(a) * cos_ub(a, n)")
(("1" (assert) nil nil)
("2"
(hide -1 2)
(("2"
(cancel-by 1 "sin(a)")
nil
nil))
nil)
("3"
(hide 2)
(("3"
(cancel-by 1 "cos(a)")
nil
nil))
nil))
nil))
nil)
("2"
(cross-mult 1)
(("2"
(case
"sin(a) * cos_lb(a, n) <= sin(a) * cos(a)"
"sin(a) * cos(a) <= sin_lb(a, n) * cos(a)")
(("1" (assert) nil nil)
("2"
(hide -1 2)
(("2"
(cancel-by 1 "cos(a)")
nil
nil))
nil)
("3"
(hide 2)
(("3"
(cancel-by 1 "sin(a)")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "sin_ge_0") nil nil))
nil)
("2" (rewrite "cos_lt_0") nil nil))
nil))
nil))
nil))
nil))
nil)
((sin_range application-judgement "trig_range" trig_basic nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(tan const-decl "real" trig_basic nil)
(tan_lb_lb const-decl "real" tan_approx nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(cos_lt_0 formula-decl nil trig_ineq nil)
(>= const-decl "bool" reals nil)
(sin const-decl "real" trig_basic nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(sin_lb const-decl "real" trig_approx nil)
(cos_lb const-decl "real" trig_approx nil)
(CBD_11 skolem-const-decl "trig_range" tan_approx nil)
(CBD_10 skolem-const-decl "trig_range" tan_approx nil)
(div_mult_neg_le1 formula-decl nil real_props nil)
(<= const-decl "bool" reals nil)
(nonpos_real nonempty-type-eq-decl nil real_types nil)
(negreal nonempty-type-eq-decl nil real_types nil)
(cos_ub const-decl "real" trig_approx nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(sin_ub const-decl "real" trig_approx nil)
(real_times_real_is_real application-judgement "real" reals nil)
(times_div2 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(both_sides_times_neg_le1 formula-decl nil real_props nil)
(CBD_9 skolem-const-decl "trig_range" tan_approx nil)
(div_mult_neg_lt1 formula-decl nil real_props nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(trig_range type-eq-decl nil trig_basic nil)
(> const-decl "bool" reals nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(CBD_8 skolem-const-decl "trig_range" tan_approx nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(pos_div_gt formula-decl nil real_props nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(zero_times1 formula-decl nil real_props nil)
(sin_bounds formula-decl nil trig_approx nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(cos_bounds formula-decl nil trig_approx nil)
(sin_ge_0 formula-decl nil trig_ineq nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(< const-decl "bool" reals nil)
(cos const-decl "real" trig_basic nil)
(tan_ub_ub const-decl "real" tan_approx nil))
nil))
(tan_bounds_npi_npi2_TCC1 0
(tan_bounds_npi_npi2_TCC1-1 nil 3285095758
("" (skeep)
(("" (lemma "cos_bounds")
(("" (inst?)
(("" (assert) (("" (flatten) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((cos_bounds formula-decl nil trig_approx nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
shostak))
(tan_bounds_npi_npi2_TCC2 0
(tan_bounds_npi_npi2_TCC2-1 nil 3285095780
("" (skeep)
(("" (expand "Tan?")
(("" (lemma "cos_bounds")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((Tan? const-decl "bool" 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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(cos_bounds formula-decl nil trig_approx nil))
shostak))
(tan_bounds_npi_npi2_TCC3 0
(tan_bounds_npi_npi2_TCC3-1 nil 3285095806
("" (skeep) (("" (assert) nil nil)) nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(tan_bounds_npi_npi2 0
(tan_bounds_npi_npi2-2 nil 3321627736
("" (skeep)
(("" (lemma "tan_bounds_pi2_pi")
(("" (inst -1 "-a" "n")
(("" (assert)
(("" (rewrite "cos_ub_neg")
(("" (assert)
(("" (rewrite "tan_neg")
(("1" (rewrite "tan_ub_ub_neg")
(("1" (rewrite "tan_lb_lb_neg")
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (hide -1 2)
(("2" (lemma "cos_bounds")
(("2" (inst?)
(("2" (assert)
(("2" (flatten) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 2)
(("2" (expand "Tan?")
(("2" (lemma "cos_bounds")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((tan_bounds_pi2_pi formula-decl nil tan_approx nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(tan_ub_ub_neg formula-decl nil tan_approx nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(cos_bounds formula-decl nil trig_approx nil)
(tan_lb_lb_neg formula-decl nil tan_approx nil)
(tan_neg formula-decl nil trig_basic nil)
(Tan? const-decl "bool" trig_basic nil)
(cos_ub_neg formula-decl nil trig_approx nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(minus_real_is_real application-judgement "real" reals nil))
nil)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.45Angebot
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
|
