YES Problem: -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) f(0()) -> 0() f(s(x)) -> -(s(x),g(f(x))) g(0()) -> s(0()) g(s(x)) -> -(s(x),f(g(x))) Proof: DP Processor: DPs: -#(s(x),s(y)) -> -#(x,y) f#(s(x)) -> f#(x) f#(s(x)) -> g#(f(x)) f#(s(x)) -> -#(s(x),g(f(x))) g#(s(x)) -> g#(x) g#(s(x)) -> f#(g(x)) g#(s(x)) -> -#(s(x),f(g(x))) TRS: -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) f(0()) -> 0() f(s(x)) -> -(s(x),g(f(x))) g(0()) -> s(0()) g(s(x)) -> -(s(x),f(g(x))) Matrix Interpretation Processor: dim=1 interpretation: [g#](x0) = 4x0 + 3, [f#](x0) = 6x0, [-#](x0, x1) = x0, [g](x0) = 2x0 + 1, [f](x0) = 3x0, [s](x0) = 3x0 + 1, [-](x0, x1) = 2x0 + 1, [0] = 0 orientation: -#(s(x),s(y)) = 3x + 1 >= x = -#(x,y) f#(s(x)) = 18x + 6 >= 6x = f#(x) f#(s(x)) = 18x + 6 >= 12x + 3 = g#(f(x)) f#(s(x)) = 18x + 6 >= 3x + 1 = -#(s(x),g(f(x))) g#(s(x)) = 12x + 7 >= 4x + 3 = g#(x) g#(s(x)) = 12x + 7 >= 12x + 6 = f#(g(x)) g#(s(x)) = 12x + 7 >= 3x + 1 = -#(s(x),f(g(x))) -(x,0()) = 2x + 1 >= x = x -(0(),s(y)) = 1 >= 0 = 0() -(s(x),s(y)) = 6x + 3 >= 2x + 1 = -(x,y) f(0()) = 0 >= 0 = 0() f(s(x)) = 9x + 3 >= 6x + 3 = -(s(x),g(f(x))) g(0()) = 1 >= 1 = s(0()) g(s(x)) = 6x + 3 >= 6x + 3 = -(s(x),f(g(x))) problem: DPs: TRS: -(x,0()) -> x -(0(),s(y)) -> 0() -(s(x),s(y)) -> -(x,y) f(0()) -> 0() f(s(x)) -> -(s(x),g(f(x))) g(0()) -> s(0()) g(s(x)) -> -(s(x),f(g(x))) Qed