YES Problem: a() -> b() f(a()) -> g(a()) f(b()) -> g(b()) Proof: Uncurry Processor: a() -> b() f4(f(),a()) -> f4(g(),a()) f4(f(),b()) -> f4(g(),b()) Ground Confluence Processor: confluent by decision procedure.