YES Problem: a() -> g(c()) g(a()) -> b() f(g(X),b()) -> f(a(),X) Proof: DP Processor: DPs: a#() -> g#(c()) f#(g(X),b()) -> a#() f#(g(X),b()) -> f#(a(),X) TRS: a() -> g(c()) g(a()) -> b() f(g(X),b()) -> f(a(),X) Arctic Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = -3x0 + -2x1 + 0, [g#](x0) = x0 + 0, [a#] = 1, [f](x0, x1) = x0 + 2x1 + 0, [b] = 4, [g](x0) = 3x0 + 0, [c] = 0, [a] = 4 orientation: a#() = 1 >= 0 = g#(c()) f#(g(X),b()) = X + 2 >= 1 = a#() f#(g(X),b()) = X + 2 >= -2X + 1 = f#(a(),X) a() = 4 >= 3 = g(c()) g(a()) = 7 >= 4 = b() f(g(X),b()) = 3X + 6 >= 2X + 4 = f(a(),X) problem: DPs: TRS: a() -> g(c()) g(a()) -> b() f(g(X),b()) -> f(a(),X) Qed