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}
     BOUND:
      Bound: match(-raise)-DP-bounded by 0
      Automaton:
       {     b_0() -> 5*
             p_0() -> 3*
             d_0() -> 2*
             s_0() -> 4*
        a#_0(2, 7) -> 1*
         a_0(4, 5) -> 6*
         a_0(3, 6) -> 7*
                 5 -> 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}
     BOUND:
      Bound: match(-raise)-DP-bounded by 0
      Automaton:
       {     c_0() -> 5*
             p_0() -> 3*
             f_0() -> 2*
             s_0() -> 4*
        a#_0(2, 7) -> 1*
         a_0(4, 5) -> 6*
         a_0(3, 6) -> 7*
                 5 -> 7*}
      Strict:
       {}
      Qed