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 TABLE1 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 .
  ***
  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 .
  eq update(S,N,T) = < S,N > T [owise] .
  *** delete
  eq delete(S,< S,N' > T) = T .
  eq delete(S,T) = T [owise] .
  *** lookup
  eq lookup(S,< S,N' > T) = N' .
endfm

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

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