|
finite_bags_lems[T: TYPE]: THEORY
%------------------------------------------------------------------------
%
% This theory establishes some more useful lemmas about finite bags
%
% Authors: Rick Butler NASA Langley
% David Griffioen (CWI Amsterdam and KUN)
% Lee Pike NASA Langley
%------------------------------------------------------------------------
BEGIN
IMPORTING finite_bags[T], finite_bags_inductions[T]
A,B : VAR finite_bag
x : VAR T
card_bag_plus : THEOREM card(plus(A,B)) = card(A) + card(B)
card_bag_union : THEOREM card(union(A,B)) = card(A) + card(B) -
card(intersection(A,B))
card_bag_disj_union : THEOREM disjoint?(A,B) IMPLIES
card(union(A,B)) = card(A) + card(B)
card_subbag_strict : THEOREM subbag?(A,B) AND member(x, B) AND NOT member(x, A) IMPLIES
card(A) < card(B)
card_subbag_strict2 : THEOREM subbag?(A,B) AND A(x) < B(x) IMPLIES
card(A) < card(B)
END finite_bags_lems
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
