YES Problem: Proof: Church Rosser Transformation Processor: critical peaks: joinable Qed