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