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