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