fmod ENTRY is
  pr STRING .
  pr NAT .
  sort Entry .
  op < _ , _ > : String Nat -> Entry .
  op 1st : Entry -> String .
  op 2nd : Entry -> Nat .
  var S : String .
  var N : Nat .
  eq 1st(< S,N >) = S .
  eq 2nd(< S,N >) = N .
endfm

fmod TABLE2 is
  pr ENTRY .
  sort Table .
  subsort Entry < Table .
  ***
  op empty : -> Table .
  op _ _ : Table Table -> Table [assoc comm id: empty] .
  op singleton : String Nat -> Table .
  op update : String Nat Table -> Table .
  op delete : String Table -> Table .
  op lookup : [String] [Table] -> [Nat] .
  op enabled-update : String Nat Table -> Bool .
  op enabled-delete : String Table -> Bool .
  ***
  var S : String .
  vars N N' : Nat .
  var T : Table .
  *** singleton
  eq singleton(S,N) = < S,N > .
  *** update
  eq update(S,N,< S,N' > T) = < S,N > T .
  ceq update(S,N,T) = < S,N > T
      if enabled-update(S,N,T) =/= true .
  *** delete
  eq delete(S,< S,N' > T) = T .
  ceq delete(S,T) = T
      if enabled-delete(S,T) =/= true .
  *** lookup
  eq lookup(S,< S,N' > T) = N' .
  *** enabled-update
  eq enabled-update(S,N,< S,N' > T) = true .
  *** enabled-delete
  eq enabled-delete(S,< S,N' > T) = true .
endfm

fmod TEST2 is
  pr TABLE2 .
  op t : -> Table .
  eq t = update("c",2,update("b",1,update("a",0,empty))) .
endfm

red in TEST2 : empty .
red in TEST2 : singleton("a",0) .
red in TEST2 : t .
red in TEST2 : update("b",10,t) .
red in TEST2 : update("d",10,t) .
red in TEST2 : delete("b",t) .
red in TEST2 : delete("d",t) .
red in TEST2 : lookup("b",t) .
red in TEST2 : lookup("d",t) .