YES Problem: f(0()) -> s(0()) f(s(x)) -> g(s(s(x))) g(0()) -> s(0()) g(s(0())) -> s(0()) g(s(s(x))) -> f(x) Proof: DP Processor: DPs: f#(s(x)) -> g#(s(s(x))) g#(s(s(x))) -> f#(x) TRS: f(0()) -> s(0()) f(s(x)) -> g(s(s(x))) g(0()) -> s(0()) g(s(0())) -> s(0()) g(s(s(x))) -> f(x) Arctic Interpretation Processor: dimension: 1 interpretation: [g#](x0) = -1x0 + 0, [f#](x0) = 2x0, [g](x0) = x0 + 3, [s](x0) = 2x0 + 1, [f](x0) = 3x0 + -16, [0] = 0 orientation: f#(s(x)) = 4x + 3 >= 3x + 2 = g#(s(s(x))) g#(s(s(x))) = 3x + 2 >= 2x = f#(x) f(0()) = 3 >= 2 = s(0()) f(s(x)) = 5x + 4 >= 4x + 3 = g(s(s(x))) g(0()) = 3 >= 2 = s(0()) g(s(0())) = 3 >= 2 = s(0()) g(s(s(x))) = 4x + 3 >= 3x + -16 = f(x) problem: DPs: TRS: f(0()) -> s(0()) f(s(x)) -> g(s(s(x))) g(0()) -> s(0()) g(s(0())) -> s(0()) g(s(s(x))) -> f(x) Qed