YES(?,O(n^1))

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:
 Bounds Processor:
  bound: 2
  enrichment: match
  automaton:
   final states: {8}
   transitions:
    a1(24) -> 25*
    e1(23) -> 24*
    e1(13) -> 14*
    b1(56) -> 57*
    b1(21) -> 22*
    c1(15) -> 16*
    c1(42) -> 43*
    u1(12) -> 13*
    a2(65) -> 66*
    e2(64) -> 65*
    b2(58) -> 59*
    d0(8) -> 8*
    e0(8) -> 8*
    u0(8) -> 8*
    c0(8) -> 8*
    b0(8) -> 8*
    v0(8) -> 8*
    a0(8) -> 8*
    8 -> 23,21,15,12
    12 -> 64,58,56,42
    13 -> 8,21,12,15,23
    14 -> 8*
    16 -> 8*
    22 -> 16,8
    25 -> 22,8
    43 -> 8,21,12,15,23
    57 -> 8*
    59 -> 43,16,8
    66 -> 59,57,22,16
  problem:
   
  Qed