|
(trig_degree
(rad_deg 0
(rad_deg-1 nil 3269434094 ("" (grind) nil nil)
((real_times_real_is_real application-judgement "real" reals 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)
(toRad const-decl "real" trig_degree nil)
(toDeg const-decl "real" trig_degree nil))
nil))
(deg_rad 0
(deg_rad-1 nil 3269434094 ("" (grind) nil nil)
((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(toDeg const-decl "real" trig_degree nil)
(toRad const-decl "real" trig_degree nil))
nil))
(tand_TCC1 0
(tand_TCC1-1 nil 3269434094 ("" (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)
(cos_range application-judgement "trig_range" trig_basic nil)
(toRad const-decl "real" trig_degree nil)
(/= const-decl "boolean" notequal nil)
(Tan? const-decl "bool" trig_basic nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx nil)
(real_times_real_is_real application-judgement "real" reals nil)
(real_div_nzreal_is_real application-judgement "real" reals nil))
nil))
(sq_sin_cos_d_one 0
(sq_sin_cos_d_one-1 nil 3269434094
("" (skolem 1 "a")
(("" (expand "sind")
(("" (expand "cosd")
(("" (lemma "sin2_cos2")
(("" (inst?) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil)
((sind const-decl "real" trig_degree 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" trig_basic nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(toRad const-decl "real" trig_degree 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)
(cosd const-decl "real" trig_degree nil))
nil))
(sind_bounds 0
(sind_bounds-2 nil 3321628718
("" (skeep)
(("" (expand "sind")
(("" (expand "toRad")
(("" (case "sin(a * pi / 180) >= sin(a*pi_lb/180)")
(("1"
(case "sin(a * pi_lb / 180)>= sin_lb(a * pi_lb / 180,n)")
(("1" (ground) nil nil)
("2" (hide 2)
(("2" (lemma "sin_bounds")
(("2" (inst -1 "a * pi_lb / 180" "n")
(("2" (ground) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (case "a=0")
(("1" (replace -1 :hide? t) (("1" (ground) nil nil)) nil)
("2" (case "a > 0")
(("1" (hide 1)
(("1" (lemma "sin_increasing")
(("1" (inst -1 " a * pi / 180" "a * pi_lb / 180")
(("1" (ground)
(("1" (hide 2 3)
(("1" (cross-mult 1)
(("1" (cancel-by 1 "a*180") nil nil)) nil))
nil)
("2" (cross-mult)
(("2" (hide 2)
(("2" (cancel-by 1 "2*pi") nil nil)) nil))
nil)
("3" (cross-mult)
(("3" (hide 2)
(("3" (cancel-by 1 "2*pi") nil nil)) nil))
nil)
("4" (hide 2)
(("4" (cross-mult 1)
(("4" (cancel-by 1 "2")
(("4" (grind-reals) nil nil)) nil))
nil))
nil)
("5" (hide 2)
(("5" (cross-mult)
(("5" (cancel-by 1 "2")
(("5"
(typepred "pi")
(("5" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sind const-decl "real" trig_degree 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 "[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)
(sin const-decl "real" trig_basic 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_div_nzreal_is_real application-judgement "real" reals nil)
(sin_bounds formula-decl nil trig_approx nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sin_range application-judgement "trig_range" trig_basic nil)
(real_times_real_is_real application-judgement "real" reals 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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(sin_lb const-decl "real" trig_approx nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(minus_even_is_even application-judgement "even_int" integers nil)
(minus_nzint_is_nzint application-judgement "nzint" integers nil)
(neg_mult formula-decl nil extra_tegies nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(posint nonempty-type-eq-decl nil integers nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(le_times_le_pos formula-decl nil real_props nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(div_mult_pos_ge2 formula-decl nil real_props nil)
(both_sides_times_pos_ge1 formula-decl nil real_props nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(both_sides_times_pos_le1 formula-decl nil real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(zero_times1 formula-decl nil real_props nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(CBD_12 skolem-const-decl "real" trig_degree nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(div_mult_pos_gt2 formula-decl nil extra_real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(times_div2 formula-decl nil real_props nil)
(div_mult_pos_gt1 formula-decl nil extra_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)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(sin_increasing formula-decl nil trig_ineq nil)
(toRad const-decl "real" trig_degree nil))
nil))
(cosd_bounds 0
(cosd_bounds-1 nil 3321628868
("" (skeep)
(("" (expand "cosd")
(("" (expand "toRad")
(("" (case "cos(a * pi / 180) <= cos(a*pi_lb/180)")
(("1"
(case "cos(a * pi_lb / 180) <= cos_ub(a * pi_lb / 180,n)")
(("1" (ground) nil nil)
("2" (hide 2)
(("2" (lemma "cos_bounds")
(("2" (inst -1 "a * pi_lb / 180" "n")
(("2" (ground) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "cos_decreasing")
(("2" (inst -1 "a * pi / 180" "a * pi_lb / 180")
(("2" (ground)
(("1" (hide 2 3)
(("1" (cross-mult 1)
(("1" (case "a=0")
(("1" (replace -1) (("1" (ground) nil nil))
nil)
("2" (cancel-by 2 "180*a") nil nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (cross-mult 1)
(("2" (cancel-by 1 "pi") nil nil)) nil))
nil)
("3" (hide 2)
(("3" (cross-mult 1)
(("3" (typepred "pi")
(("3" (grind-reals) nil nil)) nil))
nil))
nil)
("4" (hide 2)
(("4" (cross-mult)
(("4" (typepred "pi")
(("4" (swap-rel -3)
(("4" (mult-ineq -3 -6)
(("4" (assert)
(("4"
(mult-ineq -4 -8)
(("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("5" (hide 2)
(("5" (cross-mult 1) (("5" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cosd const-decl "real" trig_degree 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)
(* 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)
(cos const-decl "real" trig_basic 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_div_nzreal_is_real application-judgement "real" reals nil)
(cos_bounds formula-decl nil trig_approx nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(cos_range application-judgement "trig_range" trig_basic nil)
(real_times_real_is_real application-judgement "real" reals nil)
(pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
atan_approx 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(cos_ub const-decl "real" trig_approx nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(cos_decreasing formula-decl nil trig_ineq 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_gt1 formula-decl nil extra_real_props nil)
(times_div2 formula-decl nil real_props nil)
(nonzero_real nonempty-type-eq-decl nil reals nil)
(div_mult_pos_gt2 formula-decl nil extra_real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(div_mult_pos_ge1 formula-decl nil real_props nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(CBD_17 skolem-const-decl "real" trig_degree nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(both_sides_times_pos_le1 formula-decl nil 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)
(pos_times_ge formula-decl nil real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(abs_nat formula-decl nil abs_lems "reals/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(lt_times_lt_any1 formula-decl nil extra_real_props nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(toRad const-decl "real" trig_degree nil))
nil)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.32Angebot
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
|
