Problem: b() -> a() b() -> c() c() -> b() c() -> d() Proof: Uncurry Processor: b() -> a() b() -> c() c() -> b() c() -> d() Church Rosser Transformation Processor: b() -> a() b() -> c() c() -> b() c() -> d() critical peaks: joinable Qed