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