Problem: f(b()) -> c() c() -> c() f(c()) -> b() a() -> b() Proof: sorted: (order-sorted) 0:f(b()) -> c() c() -> c() f(c()) -> b() 1:a() -> b() ----- sorts [0>2, 1>4, 2>3, 2>4] sort attachment (non-strict) f : 2 -> 0 b : 4 c : 3 a : 1 ----- 0:f(b()) -> c() c() -> c() f(c()) -> b() Church Rosser Transformation Processor (critical pair closing system, Thm 2.4): f(c()) -> b() critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [f](x0) = x0 + 1, [b] = 0, [c] = 4 orientation: f(c()) = 5 >= 0 = b() problem: Qed 1:a() -> b() Church Rosser Transformation Processor: critical peaks: joinable Qed