YES Problem: d(x) -> e(u(x)) d(u(x)) -> c(x) c(u(x)) -> b(x) v(e(x)) -> x b(u(x)) -> a(e(x)) Proof: Arctic Interpretation Processor: dimension: 2 interpretation: [0 -&] [a](x0) = [-& -&]x0, [0 -&] [v](x0) = [1 -&]x0, [2 1] [b](x0) = [0 0]x0, [2 1] [c](x0) = [2 1]x0, [0 1] [e](x0) = [0 2]x0, [2 -&] [u](x0) = [1 0 ]x0, [2 2] [d](x0) = [3 2]x0 orientation: [2 2] [2 1] d(x) = [3 2]x >= [3 2]x = e(u(x)) [4 2] [2 1] d(u(x)) = [5 2]x >= [2 1]x = c(x) [4 1] [2 1] c(u(x)) = [4 1]x >= [0 0]x = b(x) [0 1] v(e(x)) = [1 2]x >= x = x [4 1] [0 1 ] b(u(x)) = [2 0]x >= [-& -&]x = a(e(x)) problem: d(x) -> e(u(x)) c(u(x)) -> b(x) v(e(x)) -> x b(u(x)) -> a(e(x)) Arctic Interpretation Processor: dimension: 2 interpretation: [0 -&] [a](x0) = [0 -&]x0, [0 2 ] [v](x0) = [-& 0 ]x0, [0 -&] [b](x0) = [0 0 ]x0, [1 -&] [c](x0) = [0 2 ]x0, [0 -&] [e](x0) = [-& 2 ]x0, [0 0] [u](x0) = [1 0]x0, [0 0] [d](x0) = [3 2]x0 orientation: [0 0] [0 0] d(x) = [3 2]x >= [3 2]x = e(u(x)) [1 1] [0 -&] c(u(x)) = [3 2]x >= [0 0 ]x = b(x) [0 4 ] v(e(x)) = [-& 2 ]x >= x = x [0 0] [0 -&] b(u(x)) = [1 0]x >= [0 -&]x = a(e(x)) problem: d(x) -> e(u(x)) v(e(x)) -> x b(u(x)) -> a(e(x)) Arctic Interpretation Processor: dimension: 2 interpretation: [0 -&] [a](x0) = [0 -&]x0, [0 2] [v](x0) = [0 0]x0, [2 1] [b](x0) = [1 3]x0, [0 -&] [e](x0) = [0 1 ]x0, [1 0 ] [u](x0) = [2 -&]x0, [2 1] [d](x0) = [3 0]x0 orientation: [2 1] [1 0] d(x) = [3 0]x >= [3 0]x = e(u(x)) [2 3] v(e(x)) = [0 1]x >= x = x [3 2] [0 -&] b(u(x)) = [5 1]x >= [0 -&]x = a(e(x)) problem: d(x) -> e(u(x)) Arctic Interpretation Processor: dimension: 3 interpretation: [0 0 1 ] [e](x0) = [-& -& 0 ]x0 [0 2 1 ] , [0 2 0 ] [u](x0) = [0 0 -&]x0 [0 1 0 ] , [2 3 2] [d](x0) = [2 2 2]x0 [3 3 2] orientation: [2 3 2] [1 2 1] d(x) = [2 2 2]x >= [0 1 0]x = e(u(x)) [3 3 2] [2 2 1] problem: Qed