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: Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [1] [g](x0) = [1 0 1]x0 + [1] [0 0 0] [0], [1 0 0] [n__d](x0) = [0 0 0]x0 [0 0 0] , [1 1 1] [1] [h](x0) = [0 1 0]x0 + [1] [0 0 1] [1], [1 0 0] [d](x0) = [0 0 0]x0 [0 0 0] , [activate](x0) = x0 , [1 0 0] [0] [c](x0) = [0 0 0]x0 + [0] [0 0 0] [1], [1 0 0] [1] [n__g](x0) = [1 0 1]x0 + [1] [0 0 0] [0], [1 0 1] [0] [n__f](x0) = [1 1 0]x0 + [0] [0 0 1] [1], [1 0 1] [0] [f](x0) = [1 1 0]x0 + [0] [0 0 1] [1] orientation: [1 0 2] [1] [1 0 1] [1] f(f(X)) = [2 1 1]X + [0] >= [0 0 0]X + [0] = c(n__f(n__g(n__f(X)))) [0 0 1] [2] [0 0 0] [1] [1 0 0] [0] [1 0 0] c(X) = [0 0 0]X + [0] >= [0 0 0]X = d(activate(X)) [0 0 0] [1] [0 0 0] [1 1 1] [1] [1 0 0] [0] h(X) = [0 1 0]X + [1] >= [0 0 0]X + [0] = c(n__d(X)) [0 0 1] [1] [0 0 0] [1] [1 0 1] [0] [1 0 1] [0] f(X) = [1 1 0]X + [0] >= [1 1 0]X + [0] = n__f(X) [0 0 1] [1] [0 0 1] [1] [1 0 0] [1] [1 0 0] [1] g(X) = [1 0 1]X + [1] >= [1 0 1]X + [1] = n__g(X) [0 0 0] [0] [0 0 0] [0] [1 0 0] [1 0 0] d(X) = [0 0 0]X >= [0 0 0]X = n__d(X) [0 0 0] [0 0 0] [1 0 1] [0] [1 0 1] [0] activate(n__f(X)) = [1 1 0]X + [0] >= [1 1 0]X + [0] = f(activate(X)) [0 0 1] [1] [0 0 1] [1] [1 0 0] [1] [1 0 0] [1] activate(n__g(X)) = [1 0 1]X + [1] >= [1 0 1]X + [1] = g(X) [0 0 0] [0] [0 0 0] [0] [1 0 0] [1 0 0] activate(n__d(X)) = [0 0 0]X >= [0 0 0]X = d(X) [0 0 0] [0 0 0] 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 Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [g](x0) = [1 0 0]x0 [0 0 0] , [1 0 0] [n__d](x0) = [0 0 0]x0 [0 0 0] , [1 0 0] [d](x0) = [0 0 0]x0 [0 0 0] , [1 1 0] [0] [activate](x0) = [1 1 0]x0 + [0] [0 0 1] [1], [1 1 0] [1] [c](x0) = [0 0 0]x0 + [0] [0 0 0] [1], [1 0 0] [n__g](x0) = [0 0 0]x0 [0 0 0] , [1 1 0] [0] [n__f](x0) = [1 1 0]x0 + [1] [0 0 0] [0], [1 1 0] [1] [f](x0) = [1 1 0]x0 + [1] [0 0 0] [1] orientation: [2 2 0] [3] [2 2 0] [2] f(f(X)) = [2 2 0]X + [3] >= [0 0 0]X + [0] = c(n__f(n__g(n__f(X)))) [0 0 0] [1] [0 0 0] [1] [1 1 0] [1] [1 1 0] c(X) = [0 0 0]X + [0] >= [0 0 0]X = d(activate(X)) [0 0 0] [1] [0 0 0] [1 1 0] [1] [1 1 0] [0] f(X) = [1 1 0]X + [1] >= [1 1 0]X + [1] = n__f(X) [0 0 0] [1] [0 0 0] [0] [1 0 0] [1 0 0] g(X) = [1 0 0]X >= [0 0 0]X = n__g(X) [0 0 0] [0 0 0] [1 0 0] [1 0 0] d(X) = [0 0 0]X >= [0 0 0]X = n__d(X) [0 0 0] [0 0 0] [2 2 0] [1] [2 2 0] [1] activate(n__f(X)) = [2 2 0]X + [1] >= [2 2 0]X + [1] = f(activate(X)) [0 0 0] [1] [0 0 0] [1] [1 0 0] [0] [1 0 0] activate(n__g(X)) = [1 0 0]X + [0] >= [1 0 0]X = g(X) [0 0 0] [1] [0 0 0] [1 0 0] [0] [1 0 0] activate(n__d(X)) = [1 0 0]X + [0] >= [0 0 0]X = d(X) [0 0 0] [1] [0 0 0] [1 1 0] [0] activate(X) = [1 1 0]X + [0] >= X = X [0 0 1] [1] problem: 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 String Reversal Processor: g(X) -> n__g(X) d(X) -> n__d(X) n__f(activate(X)) -> activate(f(X)) n__g(activate(X)) -> g(X) n__d(activate(X)) -> d(X) activate(X) -> X KBO Processor: weight function: w0 = 1 w(g) = w(n__d) = w(d) = w(activate) = w(n__f) = w(f) = 1 w(n__g) = 0 precedence: n__g > d > n__d > g > n__f > activate > f problem: Qed