|
(acosx
(acos_lemma 0
(acos_lemma-1 nil 3288613766
("" (skosimp*)
(("" (expand "acos")
(("" (expand "cauchy_acos")
(("" (lemma "pi_lemma")
((""
(lemma "lemma_div2n" ("x" "pi" "cx" "cauchy_pi" "n" "1"))
(("" (lemma "asin_lemma" ("x" "x!1" "cx" "cx!1"))
(("" (assert)
(("" (expand "div2n")
(("" (rewrite "expt_x1")
((""
(lemma "sub_lemma"
("x" "pi/2" "y" "asin(x!1)" "cx"
"cauchy_div2n(cauchy_pi, 1)" "cy"
"cauchy_asin(cx!1)"))
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((acos const-decl "nnreal_le_pi" acos "trig_fnd/")
(pi_lemma formula-decl nil atanx nil)
(asin_lemma formula-decl nil asinx nil)
(cauchy_real_abs_le1? const-decl "bool" asinx nil)
(cauchy_real_abs_le1 nonempty-type-eq-decl nil asinx nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(real_abs_le1 nonempty-type-eq-decl nil asin "trig_fnd/")
(div2n const-decl "real" shift nil)
(sub_lemma formula-decl nil sub nil)
(cauchy_div2n const-decl "cauchy_real" shift nil)
(cauchy_asin const-decl "cauchy_real" asinx nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(real_abs_le_pi2 nonempty-type-eq-decl nil asin "trig_fnd/")
(asin const-decl "real_abs_le_pi2" asin "trig_fnd/")
(posint_exp application-judgement "posint" exponentiation nil)
(expt_x1 formula-decl nil exponentiation nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(lemma_div2n formula-decl nil shift 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)
(cauchy_real? const-decl "bool" cauchy nil)
(cauchy_real nonempty-type-eq-decl nil cauchy nil)
(cauchy_pi const-decl "cauchy_real" atanx 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 "trig_fnd/")
(cauchy_acos const-decl "cauchy_real" acosx nil))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.20Angebot
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
|
