(from AG01 3.16) (VAR x y) (RULES times(x,0) -> 0 times(x,s(y)) -> plus(times(x,y),x) plus(x,0) -> x plus(0,x) -> x plus(x,s(y)) -> s(plus(x,y)) plus(s(x),y) -> s(plus(x,y)) )