YES Problem: strict: g(s(x)) -> f(x) f(0()) -> s(0()) f(s(x)) -> s(s(g(x))) g(0()) -> 0() weak: rand(x) -> x rand(x) -> rand(s(x)) Proof: Arctic Interpretation Processor: dimension: 1 interpretation: [rand](x0) = 8x0, [g](x0) = x0, [0] = 12, [s](x0) = x0, [f](x0) = x0 orientation: g(s(x)) = x >= x = f(x) f(0()) = 12 >= 12 = s(0()) f(s(x)) = x >= x = s(s(g(x))) g(0()) = 12 >= 12 = 0() rand(x) = 8x >= x = x rand(x) = 8x >= 8x = rand(s(x)) problem: strict: g(s(x)) -> f(x) f(0()) -> s(0()) f(s(x)) -> s(s(g(x))) g(0()) -> 0() weak: rand(x) -> rand(s(x)) Arctic Interpretation Processor: dimension: 2 interpretation: [4 3] [rand](x0) = [1 0]x0, [3 -&] [g](x0) = [7 -&]x0, [1] [0] = [6], [0 -&] [s](x0) = [1 -&]x0, [3 -&] [f](x0) = [7 -&]x0 orientation: [3 -&] [3 -&] g(s(x)) = [7 -&]x >= [7 -&]x = f(x) [4] [1] f(0()) = [8] >= [2] = s(0()) [3 -&] [3 -&] f(s(x)) = [7 -&]x >= [4 -&]x = s(s(g(x))) [4] [1] g(0()) = [8] >= [6] = 0() [4 3] [4 -&] rand(x) = [1 0]x >= [1 -&]x = rand(s(x)) problem: strict: g(s(x)) -> f(x) f(s(x)) -> s(s(g(x))) weak: rand(x) -> rand(s(x)) String Reversal Processor: strict: s(g(x)) -> f(x) s(f(x)) -> g(s(s(x))) weak: rand(x) -> s(rand(x)) Matrix Interpretation Processor: dim=5 interpretation: [1 0 0 0 1] [0] [1 0 0 1 1] [1] [rand](x0) = [0 0 0 0 0]x0 + [0] [0 0 0 0 0] [0] [0 0 0 0 0] [0], [1 0 0 0 0] [0] [0 0 0 0 0] [0] [g](x0) = [0 0 1 1 0]x0 + [0] [0 0 0 1 0] [0] [0 0 0 0 1] [1], [1 0 0 1 1] [1 0 0 0 0] [s](x0) = [0 0 0 0 1]x0 [0 0 0 1 0] [0 0 1 0 1] , [1 0 0 1 1] [0] [1 0 0 0 0] [0] [f](x0) = [0 0 0 0 1]x0 + [1] [0 0 0 1 0] [0] [0 0 1 1 1] [0] orientation: [1 0 0 1 1] [1] [1 0 0 1 1] [0] [1 0 0 0 0] [0] [1 0 0 0 0] [0] s(g(x)) = [0 0 0 0 1]x + [1] >= [0 0 0 0 1]x + [1] = f(x) [0 0 0 1 0] [0] [0 0 0 1 0] [0] [0 0 1 1 1] [1] [0 0 1 1 1] [0] [1 0 1 3 2] [0] [1 0 1 2 2] [0] [1 0 0 1 1] [0] [0 0 0 0 0] [0] s(f(x)) = [0 0 1 1 1]x + [0] >= [0 0 1 1 1]x + [0] = g(s(s(x))) [0 0 0 1 0] [0] [0 0 0 1 0] [0] [0 0 1 1 2] [1] [0 0 1 0 2] [1] [1 0 0 0 1] [0] [1 0 0 0 1] [1 0 0 1 1] [1] [1 0 0 0 1] rand(x) = [0 0 0 0 0]x + [0] >= [0 0 0 0 0]x = s(rand(x)) [0 0 0 0 0] [0] [0 0 0 0 0] [0 0 0 0 0] [0] [0 0 0 0 0] problem: strict: s(f(x)) -> g(s(s(x))) weak: rand(x) -> s(rand(x)) Arctic Interpretation Processor: dimension: 3 interpretation: [2 3 0 ] [rand](x0) = [0 -& 0 ]x0 [0 -& 0 ] , [0 -& -&] [g](x0) = [-& -& 0 ]x0 [-& -& -&] , [0 0 0 ] [s](x0) = [-& 0 0 ]x0 [-& 0 -&] , [1 1 0 ] [f](x0) = [0 0 0 ]x0 [-& 2 1 ] orientation: [1 2 1] [0 0 0 ] s(f(x)) = [0 2 1]x >= [-& 0 0 ]x = g(s(s(x))) [0 0 0] [-& -& -&] [2 3 0 ] [2 3 0 ] rand(x) = [0 -& 0 ]x >= [0 -& 0 ]x = s(rand(x)) [0 -& 0 ] [0 -& 0 ] problem: strict: weak: rand(x) -> s(rand(x)) Qed