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=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] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] [1 0 0] .(.(x,y),z) = [0 0 0]x + [0 0 0]y + [0 0 0]z >= [0 0 0]x + [0 0 0]y + [0 0 0]z = .(x,.(y,z)) [0 0 0] [0 0 0] [0 0 0] [0 0 0] [0 0 0] [0 0 0] problem: .(.(x,y),z) -> .(x,.(y,z)) Matrix Interpretation Processor: dim=1 interpretation: [.](x0, x1) = 2x0 + x1 + 1 orientation: .(.(x,y),z) = 4x + 2y + z + 3 >= 2x + 2y + z + 2 = .(x,.(y,z)) problem: Qed