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

The program

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