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