/home/nowonder/forschung/aprove/TPDB05/TRS/HM/t004.trs

The program

(VAR x)
(RULES
f(s(x)) -> s(f(f(p(s(x)))))
f(0) -> 0
p(s(x)) -> x
)

(COMMENT
Identity function. Example in \cite{DH95}.
)