fmod SET is
  pr NAT .
  sorts Elt NeSet Set .
  subsort Elt < NeSet < Set .

  vars S T : Set .
  vars E F : Elt .
  var N : NeSet .

  op empty : -> Set .
  op _,_ : Set Set -> Set [assoc comm id: empty] .
  op _,_ : NeSet Set -> NeSet [assoc comm id: empty] .

  eq N, N = N .

  op _in_ : Elt Set -> Bool .
  eq E in (E, S) = true .
  eq E in S = false [owise] .

  op |_| : Set -> Nat .
  eq | empty | = 0 .
  eq | N, N, S | = | N, S | .
  eq | E, S | = 1 + | S | [owise] .

  op union : Set Set -> Set .
  eq union(S, T) = S, T .

  op intersect : Set Set -> Set .
  eq intersect((E, S), T) = 
    if E in T then E, intersect(S, T) else intersect(S, T) fi .
  eq intersect(empty, T) = empty .

  op _\_ : Set Set -> Set .
  eq (E, S) \ T =  if E in T then S \ T else E, (S \ T) fi .
  eq empty \ T = empty .
endfm

fmod SET-TEST is
  inc SET .
  subsort Nat < Elt .

  op twoMult : Nat -> Set .
  op threeMult : Nat -> Set .

var N : Nat .
  eq twoMult(0) = 0 .
  eq twoMult(s N) = ((s N) * 2) , twoMult(N) .

  eq threeMult(0) = 0 .
  eq threeMult(s N) = ((s N) * 3) , threeMult(N) .
endfm

red | intersect(twoMult(100000), threeMult(100000)) | .

red | twoMult(100000) \ threeMult(100000) | .