|
deriv_domain_def[T : TYPE FROM real]: THEORY
BEGIN
deriv_domain?: bool = FORALL (e: posreal, x:T):
EXISTS (y: {u: nzreal | T_pred(u + x)}): abs(y) < e
not_one_element?: bool = (FORALL (x: T): EXISTS (y: T): x /= y)
connected?: bool = FORALL (x, y : T), (z : real): x <= z AND z <= y IMPLIES T_pred(z)
connected_deriv_domain: LEMMA connected? AND not_one_element?
IMPLIES deriv_domain?
del_neigh_all?: bool = FORALL (a: T): EXISTS (del: posreal): FORALL (xx:real):
abs(xx-a) < del IMPLIES T_pred(xx)
% The following lemma shows that our derivative domain is more general than just
% having a delta neighborhood around every point.
del_neigh_all_lem : LEMMA del_neigh_all? IMPLIES deriv_domain?
END deriv_domain_def
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.60Angebot
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
|
