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)) Usable Rule Processor: DPs: d#(u(x)) -> c#(x) c#(u(x)) -> b#(x) TRS: Arctic Interpretation Processor: dimension: 4 usable rules: interpretation: [b#](x0) = [0 -1 -2 -2]x0, [c#](x0) = [-& -& 0 0 ]x0 + [0], [d#](x0) = [-& 0 0 -&]x0 + [1], [-2 0 0 0 ] [0 ] [-1 0 -2 -2] [-2] [u](x0) = [1 0 1 1 ]x0 + [0 ] [0 0 1 1 ] [0 ] orientation: d#(u(x)) = [1 0 1 1]x + [1] >= [-& -& 0 0 ]x + [0] = c#(x) c#(u(x)) = [1 0 1 1]x + [0] >= [0 -1 -2 -2]x = b#(x) problem: DPs: TRS: Qed