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