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