Problem: a() -> a() b() -> h(f(f(f(b()))),h(b(),f(a()))) Proof: Church Rosser Transformation Processor: critical peaks: joinable Qed