/home/nowonder/forschung/aprove/TPDB05/TRS/SK90/4.11.trs

The program

(VAR x y z)
(RULES
+(x,0) -> x
+(x,s(y)) -> s(+(x,y))
+(0,s(y)) -> s(y)
s(+(0,y)) -> s(y)
)
(COMMENT Example 4.11 (Addition) in \cite{SK90})