[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
[Table of Contents] [Index]