*** file: /net/cs/htdocs/users/goguen/kumo/bset/bset.duck
***************************************************
style: beijing
***************************************************
spec: /net/cs/htdocs/users/goguen/kumo/bset/bset.bob
***************************************************

proof: <<AssocUnion>>
  goal: assoc-of _U_ []

proof: <<CommUnion>>
  goal: comm-of _U_ []

proof: <<IdemUnion>>
  goal: (forall S : Set) S U S = S . []

proof: <<UnitUnion>>
  goal: (forall S : Set) empty U S = S . []

proof: <<AssocIntersect>>
  goal: assoc-of _&_ []

proof: <<CommIntersect>>
  goal: comm-of _&_ []

proof: <<IdemIntersect>>
  goal: (forall S : Set) S & S = S . []
 
proof: <<ZeroIntersect>>
  goal: (forall S : Set) empty & S = empty . []

proof: <<DeMorgen>>
  goal: ((forall S1 S2 : Set) neg(S1 U S2) = neg(S1) & neg(S2)) and
        ((forall S1 S2 : Set) neg(S1 & S2) = neg(S1) U neg(S2)) .
[]


******************************************************
spec: /net/cs/htdocs/users/goguen/kumo/bset/list.bob
******************************************************
proof: <<ListRefinesSet>>
  goal: ((forall L : List N : Nat) N in nil = false)  and 
        (forall L : List M N : Nat) (N in cons(M, L) = N == M \or N in L ) .
[]
******************************************************

display: <<ListRefinesSet AssocUnion CommUnion IdemUnion UnitUnion
            AssocIntersect CommIntersect IdemIntersect ZeroIntersect
            DeMorgen>>
   title: "Behavioral Properties of Set"
   dir: /net/cs/htdocs/groups/tatami/kumo/exs/bset
   homepage: /net/cs/htdocs/users/goguen/kumo/bset/home
   specexpl: /net/cs/htdocs/users/goguen/kumo/bset/bsetspec.exp

   <<ListRefinesSet>>
      subtitle: "LIST is a Behavioral Refinement of SET"
      expl: exp1 

   <<AssocUnion>>
      subtitle: "Union"
      expl: exp2
      intro: "Associativity of union"
      [;]    
   <<CommUnion>>
      intro: "Commutativity of union"
      [;]
   <<IdemUnion>>
      intro: "Idempotency of union"
      [;]
   <<UnitUnion>>
      intro: "The empty set is a unit for union"

   <<AssocIntersect>>
      subtitle: "Intersection"
      intro: "Associativity of intersection"
      expl: exp2
      [;]
   <<CommIntersect>>
      intro: "Commutativity of intersection"
      [;]
   <<IdemIntersect>>
      intro: "Idempotence of intersection"
      [;]
   <<ZeroIntersect>>
      intro: "The empty set is a zero for intersection"

   <<DeMorgen>>
      subtitle: "The De Morgen laws"

[]