YES Problem: d(x) -> e(u(x)) d(u(x)) -> c(x) c(u(x)) -> b(x) v(e(x)) -> x b(u(x)) -> a(e(x)) Proof: DP Processor: DPs: d#(u(x)) -> c#(x) c#(u(x)) -> b#(x) TRS: d(x) -> e(u(x)) d(u(x)) -> c(x) c(u(x)) -> b(x) v(e(x)) -> x b(u(x)) -> a(e(x)) Arctic Interpretation Processor: dimension: 1 interpretation: [b#](x0) = -16x0 + 0, [c#](x0) = -8x0 + 1, [d#](x0) = 1x0 + 8, [a](x0) = x0, [v](x0) = x0 + 0, [b](x0) = 6x0 + -5, [c](x0) = 12x0 + 15, [e](x0) = 1x0 + -2, [u](x0) = -2x0 + 1, [d](x0) = 15x0 + 3 orientation: d#(u(x)) = -1x + 8 >= -8x + 1 = c#(x) c#(u(x)) = -10x + 1 >= -16x + 0 = b#(x) d(x) = 15x + 3 >= -1x + 2 = e(u(x)) d(u(x)) = 13x + 16 >= 12x + 15 = c(x) c(u(x)) = 10x + 15 >= 6x + -5 = b(x) v(e(x)) = 1x + 0 >= x = x b(u(x)) = 4x + 7 >= 1x + -2 = a(e(x)) problem: DPs: TRS: d(x) -> e(u(x)) d(u(x)) -> c(x) c(u(x)) -> b(x) v(e(x)) -> x b(u(x)) -> a(e(x)) Qed