spec LISTNAT = free type Nat ::= 0 | succ(Nat) op __+__: Nat*Nat->Nat vars m,n : Nat . %[addNat_0] 0 + m = m . %[addNat_succ] succ(n) + m = succ(n + m) sort Elem free type List ::= nil | __::__(Elem; List) op __++__: List * List -> List var x: Elem; K,L: List . %[app_nil] nil ++ K = K . %[app_cons] (x::K) ++ L = x ::(K++L) op rev: List -> List var x: Elem; L:List . %[rev_nil] rev(nil)= nil . %[rev_cons] rev (x::L) = rev(L) ++ (x::nil) op len: List -> Nat var x: Elem; L:List . %[len_nil] len(nil)=0 . %[len_cons] len(x::L) = succ(len(L)) end