YES Problem: .(1(),x) -> x .(x,1()) -> x .(i(x),x) -> 1() .(x,i(x)) -> 1() i(1()) -> 1() i(i(x)) -> x .(i(y),.(y,z)) -> z .(y,.(i(y),z)) -> z .(.(x,y),z) -> .(x,.(y,z)) i(.(x,y)) -> .(i(y),i(x)) Proof: Matrix Interpretation Processor: dim=1 interpretation: [i](x0) = 4x0 + 1, [.](x0, x1) = x0 + x1 + 5, [1] = 6 orientation: .(1(),x) = x + 11 >= x = x .(x,1()) = x + 11 >= x = x .(i(x),x) = 5x + 6 >= 6 = 1() .(x,i(x)) = 5x + 6 >= 6 = 1() i(1()) = 25 >= 6 = 1() i(i(x)) = 16x + 5 >= x = x .(i(y),.(y,z)) = 5y + z + 11 >= z = z .(y,.(i(y),z)) = 5y + z + 11 >= z = z .(.(x,y),z) = x + y + z + 10 >= x + y + z + 10 = .(x,.(y,z)) i(.(x,y)) = 4x + 4y + 21 >= 4x + 4y + 7 = .(i(y),i(x)) problem: .(i(x),x) -> 1() .(x,i(x)) -> 1() .(.(x,y),z) -> .(x,.(y,z)) Matrix Interpretation Processor: dim=1 interpretation: [i](x0) = 4x0, [.](x0, x1) = 4x0 + x1 + 2, [1] = 2 orientation: .(i(x),x) = 17x + 2 >= 2 = 1() .(x,i(x)) = 8x + 2 >= 2 = 1() .(.(x,y),z) = 16x + 4y + z + 10 >= 4x + 4y + z + 4 = .(x,.(y,z)) problem: .(i(x),x) -> 1() .(x,i(x)) -> 1() Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [1] [i](x0) = [0 0 0]x0 + [0] [0 0 0] [0], [1 0 0] [1 0 0] [.](x0, x1) = [0 0 0]x0 + [0 0 0]x1 [0 0 0] [0 0 0] , [0] [1] = [0] [0] orientation: [2 0 0] [1] [0] .(i(x),x) = [0 0 0]x + [0] >= [0] = 1() [0 0 0] [0] [0] [2 0 0] [1] [0] .(x,i(x)) = [0 0 0]x + [0] >= [0] = 1() [0 0 0] [0] [0] problem: Qed