YES Problem: s(a()) -> a() s(s(x)) -> x s(f(x,y)) -> f(s(y),s(x)) s(g(x,y)) -> g(s(x),s(y)) f(x,a()) -> x f(a(),y) -> y f(g(x,y),g(u,v)) -> g(f(x,u),f(y,v)) g(a(),a()) -> a() Proof: Matrix Interpretation Processor: dim=1 interpretation: [g](x0, x1) = x0 + 4x1 + 1, [f](x0, x1) = 2x0 + 2x1, [s](x0) = x0, [a] = 6 orientation: s(a()) = 6 >= 6 = a() s(s(x)) = x >= x = x s(f(x,y)) = 2x + 2y >= 2x + 2y = f(s(y),s(x)) s(g(x,y)) = x + 4y + 1 >= x + 4y + 1 = g(s(x),s(y)) f(x,a()) = 2x + 12 >= x = x f(a(),y) = 2y + 12 >= y = y f(g(x,y),g(u,v)) = 2u + 8v + 2x + 8y + 4 >= 2u + 8v + 2x + 8y + 1 = g(f(x,u),f(y,v)) g(a(),a()) = 31 >= 6 = a() problem: s(a()) -> a() s(s(x)) -> x s(f(x,y)) -> f(s(y),s(x)) s(g(x,y)) -> g(s(x),s(y)) Matrix Interpretation Processor: dim=1 interpretation: [g](x0, x1) = 2x0 + 2x1 + 4, [f](x0, x1) = 4x0 + 4x1 + 2, [s](x0) = 5x0, [a] = 0 orientation: s(a()) = 0 >= 0 = a() s(s(x)) = 25x >= x = x s(f(x,y)) = 20x + 20y + 10 >= 20x + 20y + 2 = f(s(y),s(x)) s(g(x,y)) = 10x + 10y + 20 >= 10x + 10y + 4 = g(s(x),s(y)) problem: s(a()) -> a() s(s(x)) -> x Matrix Interpretation Processor: dim=3 interpretation: [1 0 1] [s](x0) = [0 0 1]x0 [0 1 0] , [0] [a] = [1] [1] orientation: [1] [0] s(a()) = [1] >= [1] = a() [1] [1] [1 1 1] s(s(x)) = [0 1 0]x >= x = x [0 0 1] problem: s(s(x)) -> x Matrix Interpretation Processor: dim=3 interpretation: [1 1 0] [0] [s](x0) = [0 0 1]x0 + [1] [0 1 0] [0] orientation: [1 1 1] [1] s(s(x)) = [0 1 0]x + [1] >= x = x [0 0 1] [1] problem: Qed