(VAR x y z)
(RULES
norm(nil) -> 0
norm(g(x,y)) -> s(norm(x))
f(x,nil) -> g(nil,x)
f(x,g(y,z)) -> g(f(x,y),z)
rem(nil,y) -> nil
rem(g(x,y),0) -> g(x,y)
rem(g(x,y),s(z)) -> rem(x,z)
)

(COMMENT Example 2.41 (Finite Sequences of Natural Numbers) in \cite{SK90})