Problem: b() -> c() a() -> a() Proof: sorted: (order-sorted) 0:b() -> c() 1:a() -> a() ----- sorts [0>1] sort attachment (non-strict) b : 0 c : 1 a : 2 ----- 0:b() -> c() Church Rosser Transformation Processor: critical peaks: joinable Qed 1:a() -> a() Church Rosser Transformation Processor: critical peaks: joinable Qed