YES
TRS:
 {           a__f(X) -> f(X),
           a__f(0()) -> cons(0(), f(s(0()))),
        a__f(s(0())) -> a__f(a__p(s(0()))),
             a__p(X) -> p(X),
          a__p(s(X)) -> mark(X),
  mark(cons(X1, X2)) -> cons(mark(X1), X2),
           mark(0()) -> 0(),
          mark(f(X)) -> a__f(mark(X)),
          mark(s(X)) -> s(mark(X)),
          mark(p(X)) -> a__p(mark(X))}
 DP:
  Strict:
   {      a__f#(s(0())) -> a__f#(a__p(s(0()))),
          a__f#(s(0())) -> a__p#(s(0())),
            a__p#(s(X)) -> mark#(X),
    mark#(cons(X1, X2)) -> mark#(X1),
            mark#(f(X)) -> a__f#(mark(X)),
            mark#(f(X)) -> mark#(X),
            mark#(s(X)) -> mark#(X),
            mark#(p(X)) -> a__p#(mark(X)),
            mark#(p(X)) -> mark#(X)}
  Weak:
  {           a__f(X) -> f(X),
            a__f(0()) -> cons(0(), f(s(0()))),
         a__f(s(0())) -> a__f(a__p(s(0()))),
              a__p(X) -> p(X),
           a__p(s(X)) -> mark(X),
   mark(cons(X1, X2)) -> cons(mark(X1), X2),
            mark(0()) -> 0(),
           mark(f(X)) -> a__f(mark(X)),
           mark(s(X)) -> s(mark(X)),
           mark(p(X)) -> a__p(mark(X))}
  EDG:
   {(mark#(cons(X1, X2)) -> mark#(X1), mark#(p(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(f(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(f(X)) -> a__f#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (a__p#(s(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (a__p#(s(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (a__p#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__p#(s(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
    (a__p#(s(X)) -> mark#(X), mark#(f(X)) -> a__f#(mark(X)))
    (a__p#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(f(X)) -> a__f#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(f(X)) -> a__f#(mark(X)), a__f#(s(0())) -> a__p#(s(0())))
    (mark#(f(X)) -> a__f#(mark(X)), a__f#(s(0())) -> a__f#(a__p(s(0()))))
    (mark#(p(X)) -> a__p#(mark(X)), a__p#(s(X)) -> mark#(X))
    (mark#(p(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(p(X)) -> mark#(X), mark#(f(X)) -> a__f#(mark(X)))
    (mark#(p(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
    (mark#(p(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(p(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(p(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (mark#(f(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(f(X)) -> mark#(X), mark#(f(X)) -> a__f#(mark(X)))
    (mark#(f(X)) -> mark#(X), mark#(f(X)) -> mark#(X))
    (mark#(f(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(f(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
    (mark#(f(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
    (a__f#(s(0())) -> a__f#(a__p(s(0()))), a__f#(s(0())) -> a__f#(a__p(s(0()))))
    (a__f#(s(0())) -> a__f#(a__p(s(0()))), a__f#(s(0())) -> a__p#(s(0())))
    (a__f#(s(0())) -> a__p#(s(0())), a__p#(s(X)) -> mark#(X))}
   SCCS:
    Scc:
     {      a__f#(s(0())) -> a__f#(a__p(s(0()))),
            a__f#(s(0())) -> a__p#(s(0())),
              a__p#(s(X)) -> mark#(X),
      mark#(cons(X1, X2)) -> mark#(X1),
              mark#(f(X)) -> a__f#(mark(X)),
              mark#(f(X)) -> mark#(X),
              mark#(s(X)) -> mark#(X),
              mark#(p(X)) -> a__p#(mark(X)),
              mark#(p(X)) -> mark#(X)}
    SCC:
     Strict:
      {      a__f#(s(0())) -> a__f#(a__p(s(0()))),
             a__f#(s(0())) -> a__p#(s(0())),
               a__p#(s(X)) -> mark#(X),
       mark#(cons(X1, X2)) -> mark#(X1),
               mark#(f(X)) -> a__f#(mark(X)),
               mark#(f(X)) -> mark#(X),
               mark#(s(X)) -> mark#(X),
               mark#(p(X)) -> a__p#(mark(X)),
               mark#(p(X)) -> mark#(X)}
     Weak:
     {           a__f(X) -> f(X),
               a__f(0()) -> cons(0(), f(s(0()))),
            a__f(s(0())) -> a__f(a__p(s(0()))),
                 a__p(X) -> p(X),
              a__p(s(X)) -> mark(X),
      mark(cons(X1, X2)) -> cons(mark(X1), X2),
               mark(0()) -> 0(),
              mark(f(X)) -> a__f(mark(X)),
              mark(s(X)) -> s(mark(X)),
              mark(p(X)) -> a__p(mark(X))}
     POLY:
      Argument Filtering:
       pi(p) = 0, pi(mark#) = 0, pi(mark) = 0, pi(a__p#) = 0, pi(a__p) = 0, pi(a__f#) = [], pi(a__f) = [0], pi(s) = 0, pi(f) = [0], pi(0) = [], pi(cons) = [0,1]
      Usable Rules:
       {}
      Interpretation:
       [a__f#] = 0,
       [cons](x0, x1) = x0 + x1,
       [f](x0) = x0 + 1,
       [0] = 0
      Strict:
       {      a__f#(s(0())) -> a__f#(a__p(s(0()))),
              a__f#(s(0())) -> a__p#(s(0())),
                a__p#(s(X)) -> mark#(X),
        mark#(cons(X1, X2)) -> mark#(X1),
                mark#(s(X)) -> mark#(X),
                mark#(p(X)) -> a__p#(mark(X)),
                mark#(p(X)) -> mark#(X)}
      Weak:
       {           a__f(X) -> f(X),
                 a__f(0()) -> cons(0(), f(s(0()))),
              a__f(s(0())) -> a__f(a__p(s(0()))),
                   a__p(X) -> p(X),
                a__p(s(X)) -> mark(X),
        mark(cons(X1, X2)) -> cons(mark(X1), X2),
                 mark(0()) -> 0(),
                mark(f(X)) -> a__f(mark(X)),
                mark(s(X)) -> s(mark(X)),
                mark(p(X)) -> a__p(mark(X))}
      EDG:
       {(mark#(cons(X1, X2)) -> mark#(X1), mark#(p(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(p(X)) -> a__p#(mark(X)))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
        (mark#(s(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
        (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(p(X)) -> a__p#(mark(X)), a__p#(s(X)) -> mark#(X))
        (a__f#(s(0())) -> a__f#(a__p(s(0()))), a__f#(s(0())) -> a__f#(a__p(s(0()))))
        (a__f#(s(0())) -> a__f#(a__p(s(0()))), a__f#(s(0())) -> a__p#(s(0())))
        (mark#(p(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(p(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (mark#(p(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
        (mark#(p(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
        (a__p#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (a__p#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (a__p#(s(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
        (a__p#(s(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
        (a__f#(s(0())) -> a__p#(s(0())), a__p#(s(X)) -> mark#(X))}
       SCCS:
        Scc:
         {        a__p#(s(X)) -> mark#(X),
          mark#(cons(X1, X2)) -> mark#(X1),
                  mark#(s(X)) -> mark#(X),
                  mark#(p(X)) -> a__p#(mark(X)),
                  mark#(p(X)) -> mark#(X)}
        Scc:
         {a__f#(s(0())) -> a__f#(a__p(s(0())))}
        SCC:
         Strict:
          {        a__p#(s(X)) -> mark#(X),
           mark#(cons(X1, X2)) -> mark#(X1),
                   mark#(s(X)) -> mark#(X),
                   mark#(p(X)) -> a__p#(mark(X)),
                   mark#(p(X)) -> mark#(X)}
         Weak:
         {           a__f(X) -> f(X),
                   a__f(0()) -> cons(0(), f(s(0()))),
                a__f(s(0())) -> a__f(a__p(s(0()))),
                     a__p(X) -> p(X),
                  a__p(s(X)) -> mark(X),
          mark(cons(X1, X2)) -> cons(mark(X1), X2),
                   mark(0()) -> 0(),
                  mark(f(X)) -> a__f(mark(X)),
                  mark(s(X)) -> s(mark(X)),
                  mark(p(X)) -> a__p(mark(X))}
         POLY:
          Argument Filtering:
           pi(p) = 0, pi(mark#) = [0], pi(mark) = [0], pi(a__p#) = 0, pi(a__p) = 0, pi(a__f) = [], pi(s) = [0], pi(f) = [], pi(0) = [], pi(cons) = 0
          Usable Rules:
           {}
          Interpretation:
           [mark#](x0) = x0 + 1,
           [mark](x0) = x0 + 1,
           [s](x0) = x0 + 1
          Strict:
           {        a__p#(s(X)) -> mark#(X),
            mark#(cons(X1, X2)) -> mark#(X1),
                    mark#(p(X)) -> a__p#(mark(X)),
                    mark#(p(X)) -> mark#(X)}
          Weak:
           {           a__f(X) -> f(X),
                     a__f(0()) -> cons(0(), f(s(0()))),
                  a__f(s(0())) -> a__f(a__p(s(0()))),
                       a__p(X) -> p(X),
                    a__p(s(X)) -> mark(X),
            mark(cons(X1, X2)) -> cons(mark(X1), X2),
                     mark(0()) -> 0(),
                    mark(f(X)) -> a__f(mark(X)),
                    mark(s(X)) -> s(mark(X)),
                    mark(p(X)) -> a__p(mark(X))}
          EDG:
           {(mark#(p(X)) -> mark#(X), mark#(p(X)) -> mark#(X))
            (mark#(p(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
            (mark#(p(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(p(X)) -> a__p#(mark(X)), a__p#(s(X)) -> mark#(X))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(p(X)) -> a__p#(mark(X)))
            (mark#(cons(X1, X2)) -> mark#(X1), mark#(p(X)) -> mark#(X))
            (a__p#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
            (a__p#(s(X)) -> mark#(X), mark#(p(X)) -> a__p#(mark(X)))
            (a__p#(s(X)) -> mark#(X), mark#(p(X)) -> mark#(X))}
           SCCS:
            Scc:
             {        a__p#(s(X)) -> mark#(X),
              mark#(cons(X1, X2)) -> mark#(X1),
                      mark#(p(X)) -> a__p#(mark(X)),
                      mark#(p(X)) -> mark#(X)}
            SCC:
             Strict:
              {        a__p#(s(X)) -> mark#(X),
               mark#(cons(X1, X2)) -> mark#(X1),
                       mark#(p(X)) -> a__p#(mark(X)),
                       mark#(p(X)) -> mark#(X)}
             Weak:
             {           a__f(X) -> f(X),
                       a__f(0()) -> cons(0(), f(s(0()))),
                    a__f(s(0())) -> a__f(a__p(s(0()))),
                         a__p(X) -> p(X),
                      a__p(s(X)) -> mark(X),
              mark(cons(X1, X2)) -> cons(mark(X1), X2),
                       mark(0()) -> 0(),
                      mark(f(X)) -> a__f(mark(X)),
                      mark(s(X)) -> s(mark(X)),
                      mark(p(X)) -> a__p(mark(X))}
             POLY:
              Argument Filtering:
               pi(p) = [0], pi(mark#) = [0], pi(mark) = [0], pi(a__p#) = [0], pi(a__p) = [0], pi(a__f) = [], pi(s) = [0], pi(f) = [], pi(0) = [], pi(cons) = [0]
              Usable Rules:
               {}
              Interpretation:
               [mark#](x0) = x0 + 1,
               [a__p#](x0) = x0 + 1,
               [cons](x0) = x0 + 1,
               [p](x0) = x0 + 1,
               [mark](x0) = x0 + 1,
               [s](x0) = x0 + 1
              Strict:
               {mark#(p(X)) -> a__p#(mark(X))}
              Weak:
               {           a__f(X) -> f(X),
                         a__f(0()) -> cons(0(), f(s(0()))),
                      a__f(s(0())) -> a__f(a__p(s(0()))),
                           a__p(X) -> p(X),
                        a__p(s(X)) -> mark(X),
                mark(cons(X1, X2)) -> cons(mark(X1), X2),
                         mark(0()) -> 0(),
                        mark(f(X)) -> a__f(mark(X)),
                        mark(s(X)) -> s(mark(X)),
                        mark(p(X)) -> a__p(mark(X))}
              EDG:
               {}
               SCCS:
                
                Qed
        SCC:
         Strict:
          {a__f#(s(0())) -> a__f#(a__p(s(0())))}
         Weak:
         {           a__f(X) -> f(X),
                   a__f(0()) -> cons(0(), f(s(0()))),
                a__f(s(0())) -> a__f(a__p(s(0()))),
                     a__p(X) -> p(X),
                  a__p(s(X)) -> mark(X),
          mark(cons(X1, X2)) -> cons(mark(X1), X2),
                   mark(0()) -> 0(),
                  mark(f(X)) -> a__f(mark(X)),
                  mark(s(X)) -> s(mark(X)),
                  mark(p(X)) -> a__p(mark(X))}
         BOUND:
          Bound: match(-raise)-DP-bounded by 0
          Automaton:
           {       p_0(22) -> 20 | 18
                   p_0(21) -> 20 | 18
                   p_0(20) -> 20 | 18
                   p_0(19) -> 20 | 19 | 18
                   p_0(18) -> 20 | 19 | 18
                   p_0(17) -> 20 | 18
                   p_0(16) -> 20 | 18
                   p_0(15) -> 22 | 20
                   p_0(14) -> 20 | 18
                   p_0(13) -> 20 | 18
                mark_0(22) -> 19 | 18
                mark_0(21) -> 22 | 19
                mark_0(20) -> 19 | 18
                mark_0(19) -> 19 | 18
                mark_0(18) -> 19 | 18
                mark_0(17) -> 19 | 18
                mark_0(16) -> 19 | 18
                mark_0(15) -> 19 | 18
                mark_0(14) -> 19 | 18
                mark_0(13) -> 19 | 18
                a__p_0(22) -> 18*
                a__p_0(21) -> 18*
                a__p_0(20) -> 18*
                a__p_0(19) -> 19 | 18
                a__p_0(18) -> 19 | 18
                a__p_0(17) -> 18*
                a__p_0(16) -> 18*
                a__p_0(15) -> 22*
                a__p_0(14) -> 18*
                a__p_0(13) -> 18*
               a__f#_0(22) -> 10*
                a__f_0(22) -> 17*
                a__f_0(21) -> 17*
                a__f_0(20) -> 17*
                a__f_0(19) -> 19 | 18 | 17
                a__f_0(18) -> 19 | 18 | 17
                a__f_0(17) -> 17*
                a__f_0(16) -> 17*
                a__f_0(15) -> 17*
                a__f_0(14) -> 17*
                a__f_0(13) -> 17*
                   s_0(22) -> 16*
                   s_0(21) -> 15*
                   s_0(20) -> 16*
                   s_0(19) -> 19 | 18 | 16
                   s_0(18) -> 19 | 18 | 16
                   s_0(17) -> 16*
                   s_0(16) -> 16*
                   s_0(15) -> 16*
                   s_0(14) -> 16*
                   s_0(13) -> 16*
                   f_0(22) -> 17 | 14
                   f_0(21) -> 17 | 14
                   f_0(20) -> 17 | 14
                   f_0(19) -> 19 | 18 | 17 | 14
                   f_0(18) -> 19 | 18 | 17 | 14
                   f_0(17) -> 17 | 14
                   f_0(16) -> 17 | 14
                   f_0(15) -> 17 | 14
                   f_0(14) -> 17 | 14
                   f_0(13) -> 17 | 14
                     0_0() -> 22 | 21 | 19 | 18
            cons_0(22, 22) -> 13*
            cons_0(22, 21) -> 13*
            cons_0(22, 20) -> 13*
            cons_0(22, 19) -> 13*
            cons_0(22, 18) -> 13*
            cons_0(22, 17) -> 13*
            cons_0(22, 16) -> 13*
            cons_0(22, 15) -> 13*
            cons_0(22, 14) -> 13*
            cons_0(22, 13) -> 13*
            cons_0(21, 22) -> 13*
            cons_0(21, 21) -> 13*
            cons_0(21, 20) -> 13*
            cons_0(21, 19) -> 13*
            cons_0(21, 18) -> 13*
            cons_0(21, 17) -> 13*
            cons_0(21, 16) -> 13*
            cons_0(21, 15) -> 13*
            cons_0(21, 14) -> 13*
            cons_0(21, 13) -> 13*
            cons_0(20, 22) -> 13*
            cons_0(20, 21) -> 13*
            cons_0(20, 20) -> 13*
            cons_0(20, 19) -> 13*
            cons_0(20, 18) -> 13*
            cons_0(20, 17) -> 13*
            cons_0(20, 16) -> 13*
            cons_0(20, 15) -> 13*
            cons_0(20, 14) -> 13*
            cons_0(20, 13) -> 13*
            cons_0(19, 22) -> 19 | 18 | 13
            cons_0(19, 21) -> 19 | 18 | 13
            cons_0(19, 20) -> 19 | 18 | 13
            cons_0(19, 19) -> 19 | 18 | 13
            cons_0(19, 18) -> 19 | 18 | 13
            cons_0(19, 17) -> 19 | 18 | 13
            cons_0(19, 16) -> 19 | 18 | 13
            cons_0(19, 15) -> 19 | 18 | 13
            cons_0(19, 14) -> 19 | 18 | 17 | 13
            cons_0(19, 13) -> 19 | 18 | 13
            cons_0(18, 22) -> 19 | 18 | 13
            cons_0(18, 21) -> 19 | 18 | 13
            cons_0(18, 20) -> 19 | 18 | 13
            cons_0(18, 19) -> 19 | 18 | 13
            cons_0(18, 18) -> 19 | 18 | 13
            cons_0(18, 17) -> 19 | 18 | 13
            cons_0(18, 16) -> 19 | 18 | 13
            cons_0(18, 15) -> 19 | 18 | 13
            cons_0(18, 14) -> 19 | 18 | 13
            cons_0(18, 13) -> 19 | 18 | 13
            cons_0(17, 22) -> 13*
            cons_0(17, 21) -> 13*
            cons_0(17, 20) -> 13*
            cons_0(17, 19) -> 13*
            cons_0(17, 18) -> 13*
            cons_0(17, 17) -> 13*
            cons_0(17, 16) -> 13*
            cons_0(17, 15) -> 13*
            cons_0(17, 14) -> 13*
            cons_0(17, 13) -> 13*
            cons_0(16, 22) -> 13*
            cons_0(16, 21) -> 13*
            cons_0(16, 20) -> 13*
            cons_0(16, 19) -> 13*
            cons_0(16, 18) -> 13*
            cons_0(16, 17) -> 13*
            cons_0(16, 16) -> 13*
            cons_0(16, 15) -> 13*
            cons_0(16, 14) -> 13*
            cons_0(16, 13) -> 13*
            cons_0(15, 22) -> 13*
            cons_0(15, 21) -> 13*
            cons_0(15, 20) -> 13*
            cons_0(15, 19) -> 13*
            cons_0(15, 18) -> 13*
            cons_0(15, 17) -> 13*
            cons_0(15, 16) -> 13*
            cons_0(15, 15) -> 13*
            cons_0(15, 14) -> 13*
            cons_0(15, 13) -> 13*
            cons_0(14, 22) -> 13*
            cons_0(14, 21) -> 13*
            cons_0(14, 20) -> 13*
            cons_0(14, 19) -> 13*
            cons_0(14, 18) -> 13*
            cons_0(14, 17) -> 13*
            cons_0(14, 16) -> 13*
            cons_0(14, 15) -> 13*
            cons_0(14, 14) -> 13*
            cons_0(14, 13) -> 13*
            cons_0(13, 22) -> 13*
            cons_0(13, 21) -> 13*
            cons_0(13, 20) -> 13*
            cons_0(13, 19) -> 13*
            cons_0(13, 18) -> 13*
            cons_0(13, 17) -> 13*
            cons_0(13, 16) -> 13*
            cons_0(13, 15) -> 13*
            cons_0(13, 14) -> 13*
            cons_0(13, 13) -> 13*}
          Strict:
           {}
          Qed