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