YES Problem: add(0(),x) -> x add(s(x),y) -> s(add(x,y)) Proof: Matrix Interpretation Processor: dim=1 interpretation: [s](x0) = x0, [add](x0, x1) = x0 + x1 + 6, [0] = 1 orientation: add(0(),x) = x + 7 >= x = x add(s(x),y) = x + y + 6 >= x + y + 6 = s(add(x,y)) problem: add(s(x),y) -> s(add(x,y)) Matrix Interpretation Processor: dim=1 interpretation: [s](x0) = x0 + 1, [add](x0, x1) = 2x0 + 2x1 + 5 orientation: add(s(x),y) = 2x + 2y + 7 >= 2x + 2y + 6 = s(add(x,y)) problem: Qed