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