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 1
      Automaton:
       {       p_1() -> 20*
               p_0() -> 16*
               d_1() -> 19*
               d_0() -> 15*
               f_0() -> 14*
               0_0() -> 13 | 11
               s_1() -> 21*
               s_0() -> 12*
        a#_1(19, 23) -> 8*
        a#_0(15, 18) -> 8*
         a_1(21, 18) -> 22*
         a_1(21, 17) -> 22*
         a_1(21, 16) -> 22*
         a_1(21, 15) -> 22*
         a_1(21, 14) -> 22*
         a_1(21, 13) -> 22*
         a_1(21, 12) -> 22*
         a_1(21, 11) -> 22*
         a_1(20, 22) -> 23*
         a_0(18, 18) -> 11*
         a_0(18, 17) -> 11*
         a_0(18, 16) -> 11*
         a_0(18, 15) -> 11*
         a_0(18, 14) -> 11*
         a_0(18, 13) -> 11*
         a_0(18, 12) -> 11*
         a_0(18, 11) -> 11*
         a_0(17, 18) -> 11*
         a_0(17, 17) -> 11*
         a_0(17, 16) -> 11*
         a_0(17, 15) -> 11*
         a_0(17, 14) -> 11*
         a_0(17, 13) -> 11*
         a_0(17, 12) -> 11*
         a_0(17, 11) -> 11*
         a_0(16, 18) -> 11*
         a_0(16, 17) -> 18*
         a_0(16, 16) -> 11*
         a_0(16, 15) -> 11*
         a_0(16, 14) -> 11*
         a_0(16, 13) -> 11*
         a_0(16, 12) -> 11*
         a_0(16, 11) -> 11*
         a_0(15, 18) -> 11*
         a_0(15, 17) -> 11*
         a_0(15, 16) -> 11*
         a_0(15, 15) -> 11*
         a_0(15, 14) -> 11*
         a_0(15, 13) -> 11*
         a_0(15, 12) -> 11*
         a_0(15, 11) -> 11*
         a_0(14, 18) -> 11*
         a_0(14, 17) -> 11*
         a_0(14, 16) -> 11*
         a_0(14, 15) -> 11*
         a_0(14, 14) -> 11*
         a_0(14, 13) -> 11*
         a_0(14, 12) -> 11*
         a_0(14, 11) -> 11*
         a_0(13, 18) -> 11*
         a_0(13, 17) -> 11*
         a_0(13, 16) -> 11*
         a_0(13, 15) -> 11*
         a_0(13, 14) -> 11*
         a_0(13, 13) -> 11*
         a_0(13, 12) -> 11*
         a_0(13, 11) -> 11*
         a_0(12, 18) -> 17*
         a_0(12, 17) -> 17*
         a_0(12, 16) -> 17*
         a_0(12, 15) -> 17*
         a_0(12, 14) -> 17*
         a_0(12, 13) -> 17*
         a_0(12, 12) -> 17*
         a_0(12, 11) -> 17*
         a_0(11, 18) -> 11*
         a_0(11, 17) -> 11*
         a_0(11, 16) -> 11*
         a_0(11, 15) -> 11*
         a_0(11, 14) -> 11*
         a_0(11, 13) -> 11*
         a_0(11, 12) -> 11*
         a_0(11, 11) -> 11*
                  18 -> 11*
                  17 -> 18 | 11
                  16 -> 18 | 11
                  15 -> 18 | 11
                  14 -> 18 | 11
                  13 -> 18 | 11
                  12 -> 18 | 11
                  11 -> 23 | 18}
      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 1
      Automaton:
       {       p_1() -> 20*
               p_0() -> 16*
               d_0() -> 15*
               f_1() -> 19*
               f_0() -> 14*
               0_0() -> 13 | 11
               s_1() -> 21*
               s_0() -> 12*
        a#_1(19, 23) -> 8*
        a#_0(14, 18) -> 8*
         a_1(21, 18) -> 22*
         a_1(21, 17) -> 22*
         a_1(21, 16) -> 22*
         a_1(21, 15) -> 22*
         a_1(21, 14) -> 22*
         a_1(21, 13) -> 22*
         a_1(21, 12) -> 22*
         a_1(21, 11) -> 22*
         a_1(20, 22) -> 23*
         a_0(18, 18) -> 11*
         a_0(18, 17) -> 11*
         a_0(18, 16) -> 11*
         a_0(18, 15) -> 11*
         a_0(18, 14) -> 11*
         a_0(18, 13) -> 11*
         a_0(18, 12) -> 11*
         a_0(18, 11) -> 11*
         a_0(17, 18) -> 11*
         a_0(17, 17) -> 11*
         a_0(17, 16) -> 11*
         a_0(17, 15) -> 11*
         a_0(17, 14) -> 11*
         a_0(17, 13) -> 11*
         a_0(17, 12) -> 11*
         a_0(17, 11) -> 11*
         a_0(16, 18) -> 11*
         a_0(16, 17) -> 18*
         a_0(16, 16) -> 11*
         a_0(16, 15) -> 11*
         a_0(16, 14) -> 11*
         a_0(16, 13) -> 11*
         a_0(16, 12) -> 11*
         a_0(16, 11) -> 11*
         a_0(15, 18) -> 11*
         a_0(15, 17) -> 11*
         a_0(15, 16) -> 11*
         a_0(15, 15) -> 11*
         a_0(15, 14) -> 11*
         a_0(15, 13) -> 11*
         a_0(15, 12) -> 11*
         a_0(15, 11) -> 11*
         a_0(14, 18) -> 11*
         a_0(14, 17) -> 11*
         a_0(14, 16) -> 11*
         a_0(14, 15) -> 11*
         a_0(14, 14) -> 11*
         a_0(14, 13) -> 11*
         a_0(14, 12) -> 11*
         a_0(14, 11) -> 11*
         a_0(13, 18) -> 11*
         a_0(13, 17) -> 11*
         a_0(13, 16) -> 11*
         a_0(13, 15) -> 11*
         a_0(13, 14) -> 11*
         a_0(13, 13) -> 11*
         a_0(13, 12) -> 11*
         a_0(13, 11) -> 11*
         a_0(12, 18) -> 17*
         a_0(12, 17) -> 17*
         a_0(12, 16) -> 17*
         a_0(12, 15) -> 17*
         a_0(12, 14) -> 17*
         a_0(12, 13) -> 17*
         a_0(12, 12) -> 17*
         a_0(12, 11) -> 17*
         a_0(11, 18) -> 11*
         a_0(11, 17) -> 11*
         a_0(11, 16) -> 11*
         a_0(11, 15) -> 11*
         a_0(11, 14) -> 11*
         a_0(11, 13) -> 11*
         a_0(11, 12) -> 11*
         a_0(11, 11) -> 11*
                  18 -> 11*
                  17 -> 18 | 11
                  16 -> 18 | 11
                  15 -> 18 | 11
                  14 -> 18 | 11
                  13 -> 18 | 11
                  12 -> 18 | 11
                  11 -> 23 | 18}
      Strict:
       {}
      Qed