[PostScript]
Set (E, C): trait
% Common set operators
includes
SetBasics,
Integer,
DerivedOrders (C, \subseteq for <=, \supseteq for >=,
\subset for <, \supset for >)
introduces
__\notin __: E, C -> Bool
delete: E, C -> C
{__}: E -> C
__ \U __, __ \I __, __-__: C, C -> C
size: C -> Int
asserts
forall e, e1, e2: E, s, s1, s2: C
e \notin s == ~(e \in s);
{ e } == insert(e, {});
e1 \in delete(e2, s) == e1 \neq e2 /\ e1 \in s;
e \in (s1 \U s2) == e \in s1 \/ e \in s2;
e \in (s1 \I s2) == e \in s1 /\ e \in s2;
e \in (s1 - s2)  == e \in s1 /\ e \notin s2;
size({}) == 0;
size(insert(e, s)) ==
if e \notin s then size(s) + 1 else size(s);
s1 \subseteq s2 == s1 - s2 = {}
implies
AbelianMonoid (\U for \circ, {} for unit, C for T),
AC (\I, C),
JoinOp (\U, {} for empty),
MemberOp ({} for empty),
PartialOrder (C, \subseteq for <=, \supseteq for >=,
\subset for <, \supset for >)
C generated by {}, {__}, \U
forall e: E, s, s1, s2: C
s1 \subseteq s2 => (e \in s1 => e \in s2);
size(s) >= 0
converts
\in, \notin, {__}, delete, size, \U, \I, -:C,C->C,
\subseteq, \supseteq, \subset, \supset