NO Problem: h(X,Z) -> f(X,s(X),Z) f(X,Y,g(X,Y)) -> h(0(),g(X,Y)) g(0(),Y) -> 0() g(X,s(Y)) -> g(X,Y) Proof: Matrix Interpretation Processor: dimension: 1 interpretation: [0] = 0, [g](x0, x1) = 4x0 + x1 + 1, [f](x0, x1, x2) = 4x0 + x1 + x2 + 1, [s](x0) = x0, [h](x0, x1) = 5x0 + x1 + 1 orientation: h(X,Z) = 5X + Z + 1 >= 5X + Z + 1 = f(X,s(X),Z) f(X,Y,g(X,Y)) = 8X + 2Y + 2 >= 4X + Y + 2 = h(0(),g(X,Y)) g(0(),Y) = Y + 1 >= 0 = 0() g(X,s(Y)) = 4X + Y + 1 >= 4X + Y + 1 = g(X,Y) problem: h(X,Z) -> f(X,s(X),Z) f(X,Y,g(X,Y)) -> h(0(),g(X,Y)) g(X,s(Y)) -> g(X,Y) Matrix Interpretation Processor: dimension: 2 interpretation: [0] [0] = [0], [2 3] [2 1] [g](x0, x1) = [0 1]x0 + [2 0]x1, [1 2] [1 0] [1 0] [f](x0, x1, x2) = [0 0]x0 + [0 0]x1 + [1 2]x2, [1 0] [0] [s](x0) = [2 1]x0 + [1], [3 2] [1 0] [h](x0, x1) = [0 0]x0 + [1 2]x1 orientation: [3 2] [1 0] [2 2] [1 0] h(X,Z) = [0 0]X + [1 2]Z >= [0 0]X + [1 2]Z = f(X,s(X),Z) [3 5] [3 1] [2 3] [2 1] f(X,Y,g(X,Y)) = [2 5]X + [6 1]Y >= [2 5]X + [6 1]Y = h(0(),g(X,Y)) [2 3] [4 1] [1] [2 3] [2 1] g(X,s(Y)) = [0 1]X + [2 0]Y + [0] >= [0 1]X + [2 0]Y = g(X,Y) problem: h(X,Z) -> f(X,s(X),Z) f(X,Y,g(X,Y)) -> h(0(),g(X,Y)) Unfolding Processor: loop length: 2 terms: h(0(),g(0(),s(0()))) f(0(),s(0()),g(0(),s(0()))) context: [] substitution: Qed