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