Problem: c() -> b() a() -> a() b() -> b() f(f(a())) -> c() Proof: Church Rosser Transformation Processor (critical pair closing system, Thm 2.4): f(f(a())) -> c() critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [f](x0) = x0 + 5, [c] = 0, [a] = 5 orientation: f(f(a())) = 15 >= 0 = c() problem: Qed