YES Problem: g(0()) -> 0() g(s(x)) -> f(g(x)) f(0()) -> 0() Proof: Matrix Interpretation Processor: dim=1 interpretation: [f](x0) = x0 + 3, [s](x0) = x0 + 3, [g](x0) = x0, [0] = 4 orientation: g(0()) = 4 >= 4 = 0() g(s(x)) = x + 3 >= x + 3 = f(g(x)) f(0()) = 7 >= 4 = 0() problem: g(0()) -> 0() g(s(x)) -> f(g(x)) Matrix Interpretation Processor: dim=1 interpretation: [f](x0) = x0, [s](x0) = x0 + 3, [g](x0) = x0, [0] = 6 orientation: g(0()) = 6 >= 6 = 0() g(s(x)) = x + 3 >= x = f(g(x)) problem: g(0()) -> 0() Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [1] [g](x0) = [0 0 0]x0 + [0] [0 0 0] [0], [0] [0] = [0] [0] orientation: [1] [0] g(0()) = [0] >= [0] = 0() [0] [0] problem: Qed