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