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