(VAR x y z)
(RULES
f(x,nil) -> g(nil,x)
f(x,g(y,z)) -> g(f(x,y),z)
++(x,nil) -> x
++(x,g(y,z)) -> g(++(x,y),z)
null(nil) -> true
null(g(x,y)) -> false
mem(nil,y) -> false
mem(g(x,y),z) -> or(=(y,z),mem(x,z))
mem(x,max(x)) -> not(null(x))
max(g(g(nil,x),y)) -> max'(x,y)
max(g(g(g(x,y),z),u)) -> max'(max(g(g(x,y),z)),u)
)

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