|
(riesz_linear_functionals
(additive_op?_TCC1 0
(additive_op?_TCC1-1 nil 3492864848
("" (lemma "funs_sum_closed") (("" (propax) nil nil)) nil)
((funs_sum_closed formula-decl nil riesz_linear_functionals nil))
nil))
(const_inv_op?_TCC1 0
(const_inv_op?_TCC1-1 nil 3492864848
("" (lemma "funs_const_closed") (("" (propax) nil nil)) nil)
((funs_const_closed formula-decl nil riesz_linear_functionals nil))
nil))
(linear_op_zero_TCC1 0
(linear_op_zero_TCC1-1 nil 3492874942
("" (lemma "funs_contain_zero") (("" (assert) nil nil)) nil)
((funs_contain_zero formula-decl nil riesz_linear_functionals nil))
nil))
(linear_op_zero 0
(linear_op_zero-1 nil 3492874942
("" (skeep)
(("" (expand "linear_op?")
(("" (flatten)
(("" (expand "const_inv_op?")
(("" (inst - "LAMBDA (y:INTab): 0" "0")
(("1" (expand "*") (("1" (assert) nil nil)) nil)
("2" (lemma "funs_contain_zero") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((linear_op? const-decl "bool" riesz_linear_functionals nil)
(const_inv_op? const-decl "bool" riesz_linear_functionals nil)
(funs_contain_zero formula-decl nil riesz_linear_functionals nil)
(* const-decl "[T -> real]" real_fun_ops "reals/")
(real_times_real_is_real application-judgement "real" reals nil)
(Funs formal-subtype-decl nil riesz_linear_functionals 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(a formal-const-decl "real" riesz_linear_functionals nil)
(< const-decl "bool" reals nil)
(b formal-const-decl "{bb: real | a < bb}" riesz_linear_functionals
nil)
(INTab type-eq-decl nil riesz_interval_funs nil)
(Funs_pred const-decl "[[INTab[a, b] -> real] -> boolean]"
riesz_linear_functionals nil))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot
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
|
