YES Problem: f(f(x)) -> f(g(f(x),x)) f(f(x)) -> f(h(f(x),f(x))) g(x,y) -> y h(x,x) -> g(x,0()) Proof: Matrix Interpretation Processor: dim=2 interpretation: [0] [0] = [0], [2 0] [1 0] [0] [h](x0, x1) = [0 0]x0 + [0 0]x1 + [2], [1 0] [1 1] [g](x0, x1) = [0 0]x0 + [0 1]x1, [1 1] [0] [f](x0) = [2 2]x0 + [2] orientation: [3 3] [2] [2 3] [0] f(f(x)) = [6 6]x + [6] >= [4 6]x + [2] = f(g(f(x),x)) [3 3] [2] [3 3] [2] f(f(x)) = [6 6]x + [6] >= [6 6]x + [6] = f(h(f(x),f(x))) [1 0] [1 1] g(x,y) = [0 0]x + [0 1]y >= y = y [3 0] [0] [1 0] h(x,x) = [0 0]x + [2] >= [0 0]x = g(x,0()) problem: f(f(x)) -> f(h(f(x),f(x))) g(x,y) -> y h(x,x) -> g(x,0()) Matrix Interpretation Processor: dim=3 interpretation: [0] [0] = [0] [0], [1 0 0] [1 0 0] [1] [h](x0, x1) = [0 0 1]x0 + [0 0 0]x1 + [0] [0 1 1] [0 0 1] [1], [1 0 0] [1 0 0] [g](x0, x1) = [0 0 1]x0 + [1 1 0]x1 [0 0 0] [1 0 1] , [1 1 0] [0] [f](x0) = [1 1 0]x0 + [1] [0 0 0] [0] orientation: [2 2 0] [1] [2 2 0] [1] f(f(x)) = [2 2 0]x + [2] >= [2 2 0]x + [2] = f(h(f(x),f(x))) [0 0 0] [0] [0 0 0] [0] [1 0 0] [1 0 0] g(x,y) = [0 0 1]x + [1 1 0]y >= y = y [0 0 0] [1 0 1] [2 0 0] [1] [1 0 0] h(x,x) = [0 0 1]x + [0] >= [0 0 1]x = g(x,0()) [0 1 2] [1] [0 0 0] problem: f(f(x)) -> f(h(f(x),f(x))) g(x,y) -> y Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [1 0 0] [h](x0, x1) = [0 1 0]x0 + [0 0 0]x1 [0 0 0] [0 0 0] , [1 0 0] [1 1 1] [1] [g](x0, x1) = [0 0 0]x0 + [1 1 1]x1 + [1] [0 0 0] [1 1 1] [1], [1 0 1] [0] [f](x0) = [0 1 0]x0 + [1] [1 0 1] [0] orientation: [2 0 2] [0] [2 0 2] [0] f(f(x)) = [0 1 0]x + [2] >= [0 1 0]x + [2] = f(h(f(x),f(x))) [2 0 2] [0] [2 0 2] [0] [1 0 0] [1 1 1] [1] g(x,y) = [0 0 0]x + [1 1 1]y + [1] >= y = y [0 0 0] [1 1 1] [1] problem: f(f(x)) -> f(h(f(x),f(x))) Matrix Interpretation Processor: dim=3 interpretation: [1 0 0] [1 0 0] [h](x0, x1) = [0 1 0]x0 + [0 1 1]x1 [0 0 0] [0 0 0] , [1 0 1] [0] [f](x0) = [0 0 0]x0 + [1] [1 0 1] [1] orientation: [2 0 2] [1] [2 0 2] [0] f(f(x)) = [0 0 0]x + [1] >= [0 0 0]x + [1] = f(h(f(x),f(x))) [2 0 2] [2] [2 0 2] [1] problem: Qed