YES Problem: a(d(x1)) -> d(b(x1)) a(x1) -> b(b(b(x1))) b(d(b(x1))) -> a(c(x1)) c(x1) -> d(x1) Proof: String Reversal Processor: d(a(x1)) -> b(d(x1)) a(x1) -> b(b(b(x1))) b(d(b(x1))) -> c(a(x1)) c(x1) -> d(x1) Matrix Interpretation Processor: dim=2 interpretation: [1 0] [0] [c](x0) = [0 2]x0 + [1], [1 1] [b](x0) = [0 1]x0, [1 3] [1] [a](x0) = [0 1]x0 + [0], [1 0] [0] [d](x0) = [0 2]x0 + [1] orientation: [1 3] [1] [1 2] [1] d(a(x1)) = [0 2]x1 + [1] >= [0 2]x1 + [1] = b(d(x1)) [1 3] [1] [1 3] a(x1) = [0 1]x1 + [0] >= [0 1]x1 = b(b(b(x1))) [1 3] [1] [1 3] [1] b(d(b(x1))) = [0 2]x1 + [1] >= [0 2]x1 + [1] = c(a(x1)) [1 0] [0] [1 0] [0] c(x1) = [0 2]x1 + [1] >= [0 2]x1 + [1] = d(x1) problem: d(a(x1)) -> b(d(x1)) b(d(b(x1))) -> c(a(x1)) c(x1) -> d(x1) Arctic Interpretation Processor: dimension: 2 interpretation: [1 0 ] [c](x0) = [3 -&]x0, [2 1 ] [b](x0) = [-& 2 ]x0, [3 -&] [a](x0) = [-& -&]x0, [1 -&] [d](x0) = [3 -&]x0 orientation: [4 -&] [4 -&] d(a(x1)) = [6 -&]x1 >= [5 -&]x1 = b(d(x1)) [6 5] [4 -&] b(d(b(x1))) = [7 6]x1 >= [6 -&]x1 = c(a(x1)) [1 0 ] [1 -&] c(x1) = [3 -&]x1 >= [3 -&]x1 = d(x1) problem: d(a(x1)) -> b(d(x1)) c(x1) -> d(x1) Arctic Interpretation Processor: dimension: 3 interpretation: [3 2 3] [c](x0) = [2 1 3]x0 [0 2 3] , [0 0 2 ] [b](x0) = [-& -& -&]x0 [0 -& 0 ] , [2 0 2 ] [a](x0) = [0 2 2 ]x0 [1 -& 1 ] , [0 0 0 ] [d](x0) = [1 0 2 ]x0 [-& 0 0 ] orientation: [2 2 2] [1 2 2 ] d(a(x1)) = [3 2 3]x1 >= [-& -& -&]x1 = b(d(x1)) [1 2 2] [0 0 0 ] [3 2 3] [0 0 0 ] c(x1) = [2 1 3]x1 >= [1 0 2 ]x1 = d(x1) [0 2 3] [-& 0 0 ] problem: d(a(x1)) -> b(d(x1)) Arctic Interpretation Processor: dimension: 3 interpretation: [0 0 -&] [b](x0) = [0 2 1 ]x0 [0 -& 0 ] , [2 0 2] [a](x0) = [1 2 0]x0 [3 3 3] , [1 0 0 ] [d](x0) = [0 -& 0 ]x0 [-& 0 0 ] orientation: [3 3 3] [1 0 0] d(a(x1)) = [3 3 3]x1 >= [2 1 2]x1 = b(d(x1)) [3 3 3] [1 0 0] problem: Qed