Problem: f(a()) -> b() f(a()) -> f(c()) a() -> d() f(d()) -> b() f(c()) -> b() d() -> c() Proof: Uncurry Processor: f5(f(),a()) -> b() f5(f(),a()) -> f5(f(),c()) a() -> d() f5(f(),d()) -> b() f5(f(),c()) -> b() d() -> c() Church Rosser Transformation Processor: strict: weak: critical peaks: 0 Qed