(from AG01 4.2) (VAR x y) (RULES f(g(x),s(0),y) -> f(y,y,g(x)) g(s(x)) -> s(g(x)) g(0) -> 0 )