(VAR x y) (RULES a(0,b(0,x)) -> b(0,a(0,x)) a(0,x) -> b(0,b(0,x)) a(0,a(1,a(x,y))) -> a(1,a(0,a(x,y))) b(0,a(1,a(x,y))) -> b(1,a(0,a(x,y))) a(0,a(x,y)) -> a(1,a(1,a(x,y))) )