YES

We show the termination of the TRS R:

  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))

-- SCC decomposition.

Consider the dependency pair problem (P, R), where P consists of

p1: d#(u(x)) -> c#(x)
p2: c#(u(x)) -> b#(x)

and R consists of:

r1: d(x) -> e(u(x))
r2: d(u(x)) -> c(x)
r3: c(u(x)) -> b(x)
r4: v(e(x)) -> x
r5: b(u(x)) -> a(e(x))

The estimated dependency graph contains the following SCCs:

  (no SCCs)