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) Usable Rule Processor: DPs: a#() -> g#(c()) f#(g(X),b()) -> a#() f#(g(X),b()) -> f#(a(),X) TRS: a() -> g(c()) Arctic Interpretation Processor: dimension: 1 usable rules: a() -> g(c()) interpretation: [f#](x0, x1) = -6x0 + x1 + 4, [g#](x0) = 2x0 + 1, [a#] = 4, [b] = 5, [g](x0) = 7x0 + 2, [c] = 0, [a] = 8 orientation: a#() = 4 >= 2 = g#(c()) f#(g(X),b()) = 1X + 5 >= 4 = a#() f#(g(X),b()) = 1X + 5 >= X + 4 = f#(a(),X) a() = 8 >= 7 = g(c()) problem: DPs: TRS: a() -> g(c()) Qed