NO Problem: f(x,x) -> f(i(x),g(g(x))) f(x,y) -> x g(x) -> i(x) f(x,i(x)) -> f(x,x) f(i(x),i(g(x))) -> a() Proof: Matrix Interpretation Processor: dimension: 1 interpretation: [a] = 2, [g](x0) = x0, [i](x0) = x0, [f](x0, x1) = 2x0 + 2x1 + 2 orientation: f(x,x) = 4x + 2 >= 4x + 2 = f(i(x),g(g(x))) f(x,y) = 2x + 2y + 2 >= x = x g(x) = x >= x = i(x) f(x,i(x)) = 4x + 2 >= 4x + 2 = f(x,x) f(i(x),i(g(x))) = 4x + 2 >= 2 = a() problem: f(x,x) -> f(i(x),g(g(x))) g(x) -> i(x) f(x,i(x)) -> f(x,x) f(i(x),i(g(x))) -> a() Matrix Interpretation Processor: dimension: 1 interpretation: [a] = 0, [g](x0) = x0, [i](x0) = x0, [f](x0, x1) = x0 + x1 + 5 orientation: f(x,x) = 2x + 5 >= 2x + 5 = f(i(x),g(g(x))) g(x) = x >= x = i(x) f(x,i(x)) = 2x + 5 >= 2x + 5 = f(x,x) f(i(x),i(g(x))) = 2x + 5 >= 0 = a() problem: f(x,x) -> f(i(x),g(g(x))) g(x) -> i(x) f(x,i(x)) -> f(x,x) Unfolding Processor: loop length: 4 terms: f(x92,x92) f(i(x92),g(g(x92))) f(i(x92),i(g(x92))) f(i(x92),i(i(x92))) context: [] substitution: x92 -> i(x92) Qed