YES Problem: a(p(x1)) -> p(a(A(x1))) a(A(x1)) -> A(a(x1)) p(A(A(x1))) -> a(p(x1)) Proof: String Reversal Processor: p(a(x1)) -> A(a(p(x1))) A(a(x1)) -> a(A(x1)) A(A(p(x1))) -> p(a(x1)) Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [1] [A](x0) = [0 1 0]x0 + [1] [0 1 0] [0], [0] [a](x0) = x0 + [1] [1], [1 1 0] [0] [p](x0) = [0 1 1]x0 + [1] [0 1 1] [0] orientation: [1 1 0] [1] [1 1 0] [1] p(a(x1)) = [0 1 1]x1 + [3] >= [0 1 1]x1 + [3] = A(a(p(x1))) [0 1 1] [2] [0 1 1] [2] [1 0 0] [1] [1 0 0] [1] A(a(x1)) = [0 1 0]x1 + [2] >= [0 1 0]x1 + [2] = a(A(x1)) [0 1 0] [1] [0 1 0] [1] [1 1 0] [2] [1 1 0] [1] A(A(p(x1))) = [0 1 1]x1 + [3] >= [0 1 1]x1 + [3] = p(a(x1)) [0 1 1] [2] [0 1 1] [2] problem: p(a(x1)) -> A(a(p(x1))) A(a(x1)) -> a(A(x1)) String Reversal Processor: a(p(x1)) -> p(a(A(x1))) a(A(x1)) -> A(a(x1)) Matrix Interpretation Processor: dim=3 interpretation: [1] [A](x0) = x0 + [0] [1], [1 1 1] [1] [a](x0) = [0 1 0]x0 + [0] [0 1 1] [1], [1 1 0] [0] [p](x0) = [0 1 0]x0 + [1] [0 0 1] [1] orientation: [1 2 1] [3] [1 2 1] [3] a(p(x1)) = [0 1 0]x1 + [1] >= [0 1 0]x1 + [1] = p(a(A(x1))) [0 1 1] [3] [0 1 1] [3] [1 1 1] [3] [1 1 1] [2] a(A(x1)) = [0 1 0]x1 + [0] >= [0 1 0]x1 + [0] = A(a(x1)) [0 1 1] [2] [0 1 1] [2] problem: a(p(x1)) -> p(a(A(x1))) Arctic Interpretation Processor: dimension: 3 interpretation: [0 -& -&] [A](x0) = [0 -& 0 ]x0 [-& -& -&] , [0 -& 1 ] [a](x0) = [-& 1 1 ]x0 [0 0 1 ] , [0 -& 0 ] [p](x0) = [-& -& -&]x0 [0 -& 0 ] orientation: [1 -& 1 ] [0 -& 0 ] a(p(x1)) = [1 -& 1 ]x1 >= [-& -& -&]x1 = p(a(A(x1))) [1 -& 1 ] [0 -& 0 ] problem: Qed