fmod SET-HIERARCHY is
  sorts Set Elt EltList .
  subsorts Set < Elt < EltList .
  op {} : -> Set .
  op _,_ : EltList EltList -> EltList [assoc comm] .
  op {_} : EltList -> Set .
  ops _\/_ : Set Set -> Set [assoc comm id: {}] .
  ops _/\_ : Set Set -> Set [assoc comm] .
  op _\_ : Set Set -> Set .
  op _in_ : Elt Set -> Bool .
  op 2^_ : Set -> Set .
  op augment : Set Set -> Set .
  ops a b c d e : -> Elt .
  ops u v w x : -> Set .

vars L M : EltList .
vars E F : Elt .
vars S T : Set .

*** equations between constructors to eliminate duplicate elements
  eq {L, L, M} = {L, M} .
  eq {L, L} = {L} .

*** set union
  eq {L} \/ {M} = {L, M} .

*** set membership
  eq E in {} = false .
  eq E in {F} = (E == F) .
  eq E in {F, L} = if E == F then true else E in {L} fi .

*** set intersection
  eq {} /\ S = {} .
  eq {E} /\ S = if E in S then {E} else {} fi .
  eq {E, L} /\ S = ({E} /\ S) \/ ({L} /\ S) .

*** asymmetric set difference
  eq {} \ S = {} .
  eq {E} \ S = if E in S then {} else {E} fi .
  eq {E, L} \ S = ({E} \ S) \/ ({L} \ S) .

*** power set (defined using auxiliary function "augment")
  eq 2^{} = {{}} .
  eq 2^{E} = {{}, {E}} .
  eq 2^{E, L} = 2^{L} \/ augment(2^{L}, {E}) .
  eq augment({}, T) = {} .
  eq augment({S}, T) = {S \/ T} .
  eq augment({S, L}, T) = {S \/ T} \/ augment({L}, T) .

*** some specific sets
  eq u = 2^ (2^{a, b, c} \/ 2^{b, d} \/ {e}).
  eq v = 2^ 2^{a, b} .
  eq w = 2^ 2^{a, c} .
  eq x = 2^ 2^{b, c} .
endfm

red u \ (v \/ w) == (u \ v) /\ (u \ w) .