|
finite_bags_aux[T: TYPE]: THEORY
%-------------------------------------------------------------------------
%
% Additional properties of finite bags.
%
% Author: David Griffioen (CWI Amsterdam and KUN)
%
%-------------------------------------------------------------------------
BEGIN
IMPORTING finite_bags[T], bags_aux[T]
x,e: VAR T
b: VAR finite_bag
p: VAR pred[T]
n,xn: VAR nat
finite_bag_rest: LEMMA is_finite(rest[T](b))
JUDGEMENT rest(b) HAS_TYPE finite_bag
card_bag_rest : LEMMA nonempty_bag?(b) IMPLIES
card(b) = card(rest(b)) + 1
%% ===== on finite bags and filters =====
finite_filter : THEOREM is_finite(filter(b,p))
JUDGEMENT filter(b,p) HAS_TYPE finite_bag
card_filter_insert: LEMMA card(filter(insert(x,b),p)) =
card(filter(b,p)) + IF p(x) THEN 1 ELSE 0 ENDIF
card_filter_delete: LEMMA card(filter(delete(x,b,n),p)) =
card(filter(b,p)) - IF p(x) THEN min(b(x),n)
ELSE 0 ENDIF
END finite_bags_aux
¤ 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
|
