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