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