YES Problem: f(i(x),g(a())) -> f(j(x,x),g(b())) b() -> a() i(x) -> j(x,x) Proof: Church Rosser Transformation Processor (kb): f(i(x),g(a())) -> f(j(x,x),g(b())) b() -> a() i(x) -> j(x,x) critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [j](x0, x1) = x0 + 6x1 + 2, [a] = 0, [f](x0, x1) = x0 + 2x1 + 3, [b] = 0, [i](x0) = 7x0 + 4, [g](x0) = 4x0 orientation: f(i(x),g(a())) = 7x + 7 >= 7x + 5 = f(j(x,x),g(b())) b() = 0 >= 0 = a() i(x) = 7x + 4 >= 7x + 2 = j(x,x) problem: b() -> a() Matrix Interpretation Processor: dim=1 interpretation: [a] = 0, [b] = 1 orientation: b() = 1 >= 0 = a() problem: Qed