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