Problem: f(g(x)) -> h(g(x),g(x)) f(s(x)) -> h(s(x),s(x)) g(x) -> s(x) Proof: Church Rosser Transformation Processor (kb): f(g(x)) -> h(g(x),g(x)) f(s(x)) -> h(s(x),s(x)) g(x) -> s(x) critical peaks: joinable Matrix Interpretation Processor: dim=1 interpretation: [s](x0) = x0, [h](x0, x1) = 2x0 + 2x1, [f](x0) = 5x0 + 3, [g](x0) = 4x0 + 2 orientation: f(g(x)) = 20x + 13 >= 16x + 8 = h(g(x),g(x)) f(s(x)) = 5x + 3 >= 4x = h(s(x),s(x)) g(x) = 4x + 2 >= x = s(x) problem: Qed