YES Problem: a(x1) -> g(d(x1)) b(b(b(x1))) -> c(d(c(x1))) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) Proof: Arctic Interpretation Processor: dimension: 1 interpretation: [c](x0) = 4x0, [b](x0) = 3x0, [g](x0) = 2x0, [d](x0) = x0, [a](x0) = 2x0 orientation: a(x1) = 2x1 >= 2x1 = g(d(x1)) b(b(b(x1))) = 9x1 >= 8x1 = c(d(c(x1))) b(b(x1)) = 6x1 >= 6x1 = a(g(g(x1))) c(d(x1)) = 4x1 >= 4x1 = g(g(x1)) g(g(g(x1))) = 6x1 >= 6x1 = b(b(x1)) problem: a(x1) -> g(d(x1)) b(b(x1)) -> a(g(g(x1))) c(d(x1)) -> g(g(x1)) g(g(g(x1))) -> b(b(x1)) Arctic Interpretation Processor: dimension: 2 interpretation: [3 1] [c](x0) = [3 2]x0, [1 2] [b](x0) = [0 0]x0, [0 1] [g](x0) = [0 1]x0, [0 0 ] [d](x0) = [-& -&]x0, [1 1] [a](x0) = [0 0]x0 orientation: [1 1] [0 0] a(x1) = [0 0]x1 >= [0 0]x1 = g(d(x1)) [2 3] [2 3] b(b(x1)) = [1 2]x1 >= [1 2]x1 = a(g(g(x1))) [3 3] [1 2] c(d(x1)) = [3 3]x1 >= [1 2]x1 = g(g(x1)) [2 3] [2 3] g(g(g(x1))) = [2 3]x1 >= [1 2]x1 = b(b(x1)) problem: a(x1) -> g(d(x1)) b(b(x1)) -> a(g(g(x1))) g(g(g(x1))) -> b(b(x1)) Arctic Interpretation Processor: dimension: 2 interpretation: [0 1] [b](x0) = [0 1]x0, [0 0] [g](x0) = [0 1]x0, [0 -&] [d](x0) = [-& -&]x0, [0 -&] [a](x0) = [0 -&]x0 orientation: [0 -&] [0 -&] a(x1) = [0 -&]x1 >= [0 -&]x1 = g(d(x1)) [1 2] [0 1] b(b(x1)) = [1 2]x1 >= [0 1]x1 = a(g(g(x1))) [1 2] [1 2] g(g(g(x1))) = [2 3]x1 >= [1 2]x1 = b(b(x1)) problem: a(x1) -> g(d(x1)) g(g(g(x1))) -> b(b(x1)) Arctic Interpretation Processor: dimension: 2 interpretation: [0 0] [b](x0) = [0 0]x0, [0 0] [g](x0) = [0 1]x0, [1 0] [d](x0) = [0 1]x0, [1 2] [a](x0) = [2 3]x0 orientation: [1 2] [1 1] a(x1) = [2 3]x1 >= [1 2]x1 = g(d(x1)) [1 2] [0 0] g(g(g(x1))) = [2 3]x1 >= [0 0]x1 = b(b(x1)) problem: a(x1) -> g(d(x1)) Arctic Interpretation Processor: dimension: 3 interpretation: [0 0 1 ] [g](x0) = [-& -& 0 ]x0 [0 2 1 ] , [0 2 0 ] [d](x0) = [0 0 -&]x0 [0 1 0 ] , [2 3 2] [a](x0) = [2 2 2]x0 [3 3 2] orientation: [2 3 2] [1 2 1] a(x1) = [2 2 2]x1 >= [0 1 0]x1 = g(d(x1)) [3 3 2] [2 2 1] problem: Qed