YES Problem: f(f(X)) -> c(n__f(g(n__f(X)))) c(X) -> d(activate(X)) h(X) -> c(n__d(X)) f(X) -> n__f(X) d(X) -> n__d(X) activate(n__f(X)) -> f(X) activate(n__d(X)) -> d(X) activate(X) -> X Proof: Arctic Interpretation Processor: dimension: 2 interpretation: [0 1 ] [n__d](x0) = [-& 0 ]x0, [3 3] [h](x0) = [2 1]x0, [0 2 ] [d](x0) = [-& 0 ]x0, [2 2] [activate](x0) = [0 0]x0, [2 3] [c](x0) = [0 0]x0, [0 0] [g](x0) = [0 1]x0, [1 0 ] [n__f](x0) = [-& 0 ]x0, [3 1] [f](x0) = [0 0]x0 orientation: [6 4] [4 4] f(f(X)) = [3 1]X >= [2 1]X = c(n__f(g(n__f(X)))) [2 3] [2 2] c(X) = [0 0]X >= [0 0]X = d(activate(X)) [3 3] [2 3] h(X) = [2 1]X >= [0 1]X = c(n__d(X)) [3 1] [1 0 ] f(X) = [0 0]X >= [-& 0 ]X = n__f(X) [0 2 ] [0 1 ] d(X) = [-& 0 ]X >= [-& 0 ]X = n__d(X) [3 2] [3 1] activate(n__f(X)) = [1 0]X >= [0 0]X = f(X) [2 3] [0 2 ] activate(n__d(X)) = [0 1]X >= [-& 0 ]X = d(X) [2 2] activate(X) = [0 0]X >= X = X problem: f(f(X)) -> c(n__f(g(n__f(X)))) c(X) -> d(activate(X)) h(X) -> c(n__d(X)) f(X) -> n__f(X) d(X) -> n__d(X) activate(n__f(X)) -> f(X) activate(X) -> X Arctic Interpretation Processor: dimension: 1 interpretation: [n__d](x0) = x0, [h](x0) = 8x0, [d](x0) = x0, [activate](x0) = 1x0, [c](x0) = 1x0, [g](x0) = x0, [n__f](x0) = x0, [f](x0) = 1x0 orientation: f(f(X)) = 2X >= 1X = c(n__f(g(n__f(X)))) c(X) = 1X >= 1X = d(activate(X)) h(X) = 8X >= 1X = c(n__d(X)) f(X) = 1X >= X = n__f(X) d(X) = X >= X = n__d(X) activate(n__f(X)) = 1X >= 1X = f(X) activate(X) = 1X >= X = X problem: c(X) -> d(activate(X)) d(X) -> n__d(X) activate(n__f(X)) -> f(X) Arctic Interpretation Processor: dimension: 3 interpretation: [0 -& -&] [n__d](x0) = [0 -& -&]x0 [-& 2 0 ] , [0 0 2] [d](x0) = [2 1 1]x0 [0 2 1] , [0 -& 0 ] [activate](x0) = [0 0 1 ]x0 [1 1 -&] , [3 3 1] [c](x0) = [2 2 2]x0 [2 2 3] , [1 0 0] [n__f](x0) = [0 0 1]x0 [0 2 1] , [0 0 -&] [f](x0) = [-& 0 0 ]x0 [0 -& -&] orientation: [3 3 1] [3 3 1] c(X) = [2 2 2]X >= [2 2 2]X = d(activate(X)) [2 2 3] [2 2 3] [0 0 2] [0 -& -&] d(X) = [2 1 1]X >= [0 -& -&]X = n__d(X) [0 2 1] [-& 2 0 ] [1 2 1] [0 0 -&] activate(n__f(X)) = [1 3 2]X >= [-& 0 0 ]X = f(X) [2 1 2] [0 -& -&] problem: c(X) -> d(activate(X)) d(X) -> n__d(X) Arctic Interpretation Processor: dimension: 3 interpretation: [0 -& -&] [n__d](x0) = [-& -& -&]x0 [-& -& -&] , [1 -& -&] [d](x0) = [2 -& 0 ]x0 [-& 0 2 ] , [1 0 -&] [activate](x0) = [0 2 -&]x0 [0 1 0 ] , [2 1 0] [c](x0) = [3 2 2]x0 [2 3 2] orientation: [2 1 0] [2 1 -&] c(X) = [3 2 2]X >= [3 2 0 ]X = d(activate(X)) [2 3 2] [2 3 2 ] [1 -& -&] [0 -& -&] d(X) = [2 -& 0 ]X >= [-& -& -&]X = n__d(X) [-& 0 2 ] [-& -& -&] problem: c(X) -> d(activate(X)) Arctic Interpretation Processor: dimension: 3 interpretation: [0 0 1 ] [d](x0) = [-& -& 0 ]x0 [0 2 1 ] , [0 2 0 ] [activate](x0) = [0 0 -&]x0 [0 1 0 ] , [2 3 2] [c](x0) = [2 2 2]x0 [3 3 2] orientation: [2 3 2] [1 2 1] c(X) = [2 2 2]X >= [0 1 0]X = d(activate(X)) [3 3 2] [2 2 1] problem: Qed