(VAR x y z) (RULES +(0,y) -> y +(x,0) -> x +(s(x),y) -> s(+(x,y)) +(x,s(y)) -> s(+(x,y)) +(x,+(y,z)) -> +(+(x,y),z) +(x,y) -> +(y,x) ) (COMMENT R3 of \cite{AT2012})