YES
TRS:
 {a(f(), a(s(), x)) -> a(d(), a(f(), a(p(), a(s(), x)))),
        a(f(), 0()) -> a(s(), 0()),
  a(d(), a(s(), x)) -> a(s(), a(s(), a(d(), a(p(), a(s(), x))))),
        a(d(), 0()) -> 0(),
  a(p(), a(s(), x)) -> x}
 DP:
  Strict:
   {a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x))),
    a#(f(), a(s(), x)) -> a#(d(), a(f(), a(p(), a(s(), x)))),
    a#(f(), a(s(), x)) -> a#(p(), a(s(), x)),
          a#(f(), 0()) -> a#(s(), 0()),
    a#(d(), a(s(), x)) -> a#(s(), a(s(), a(d(), a(p(), a(s(), x))))),
    a#(d(), a(s(), x)) -> a#(s(), a(d(), a(p(), a(s(), x)))),
    a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x))),
    a#(d(), a(s(), x)) -> a#(p(), a(s(), x))}
  Weak:
  {a(f(), a(s(), x)) -> a(d(), a(f(), a(p(), a(s(), x)))),
         a(f(), 0()) -> a(s(), 0()),
   a(d(), a(s(), x)) -> a(s(), a(s(), a(d(), a(p(), a(s(), x))))),
         a(d(), 0()) -> 0(),
   a(p(), a(s(), x)) -> x}
  EDG:
   {(a#(f(), a(s(), x)) -> a#(d(), a(f(), a(p(), a(s(), x)))), a#(d(), a(s(), x)) -> a#(p(), a(s(), x)))
    (a#(f(), a(s(), x)) -> a#(d(), a(f(), a(p(), a(s(), x)))), a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x))))
    (a#(f(), a(s(), x)) -> a#(d(), a(f(), a(p(), a(s(), x)))), a#(d(), a(s(), x)) -> a#(s(), a(d(), a(p(), a(s(), x)))))
    (a#(f(), a(s(), x)) -> a#(d(), a(f(), a(p(), a(s(), x)))), a#(d(), a(s(), x)) -> a#(s(), a(s(), a(d(), a(p(), a(s(), x))))))
    (a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x))), a#(d(), a(s(), x)) -> a#(s(), a(s(), a(d(), a(p(), a(s(), x))))))
    (a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x))), a#(d(), a(s(), x)) -> a#(s(), a(d(), a(p(), a(s(), x)))))
    (a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x))), a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x))))
    (a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x))), a#(d(), a(s(), x)) -> a#(p(), a(s(), x)))
    (a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x))), a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x))))
    (a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x))), a#(f(), a(s(), x)) -> a#(d(), a(f(), a(p(), a(s(), x)))))
    (a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x))), a#(f(), a(s(), x)) -> a#(p(), a(s(), x)))
    (a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x))), a#(f(), 0()) -> a#(s(), 0()))}
   SCCS:
    Scc:
     {a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x)))}
    Scc:
     {a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x)))}
    SCC:
     Strict:
      {a#(d(), a(s(), x)) -> a#(d(), a(p(), a(s(), x)))}
     Weak:
     {a(f(), a(s(), x)) -> a(d(), a(f(), a(p(), a(s(), x)))),
            a(f(), 0()) -> a(s(), 0()),
      a(d(), a(s(), x)) -> a(s(), a(s(), a(d(), a(p(), a(s(), x))))),
            a(d(), 0()) -> 0(),
      a(p(), a(s(), x)) -> x}
     UR:
      {a(p(), a(s(), x)) -> x}
      BOUND:
       Bound: match(-raise)-bounded by 0
       Automaton:
        {     b_0() -> 1*
              p_0() -> 4*
              d_0() -> 3*
              s_0() -> 5*
         a#_0(3, 7) -> 2*
          a_0(5, 1) -> 6*
          a_0(4, 6) -> 7*
                  1 -> 7*}
       Strict:
        {}
       Qed
    SCC:
     Strict:
      {a#(f(), a(s(), x)) -> a#(f(), a(p(), a(s(), x)))}
     Weak:
     {a(f(), a(s(), x)) -> a(d(), a(f(), a(p(), a(s(), x)))),
            a(f(), 0()) -> a(s(), 0()),
      a(d(), a(s(), x)) -> a(s(), a(s(), a(d(), a(p(), a(s(), x))))),
            a(d(), 0()) -> 0(),
      a(p(), a(s(), x)) -> x}
     UR:
      {a(p(), a(s(), x)) -> x}
      BOUND:
       Bound: match(-raise)-bounded by 0
       Automaton:
        {     c_0() -> 1*
              p_0() -> 4*
              f_0() -> 3*
              s_0() -> 5*
         a#_0(3, 7) -> 2*
          a_0(5, 1) -> 6*
          a_0(4, 6) -> 7*
                  1 -> 7*}
       Strict:
        {}
       Qed