YES
TRS:
 {          a__first(X1, X2) -> first(X1, X2),
            a__first(0(), X) -> nil(),
  a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                 mark(nil()) -> nil(),
                   mark(0()) -> 0(),
          mark(cons(X1, X2)) -> cons(mark(X1), X2),
         mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                  mark(s(X)) -> s(mark(X)),
               mark(from(X)) -> a__from(mark(X)),
                  a__from(X) -> cons(mark(X), from(s(X))),
                  a__from(X) -> from(X)}
 DP:
  Strict:
   {a__first#(s(X), cons(Y, Z)) -> mark#(Y),
            mark#(cons(X1, X2)) -> mark#(X1),
           mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
           mark#(first(X1, X2)) -> mark#(X1),
           mark#(first(X1, X2)) -> mark#(X2),
                    mark#(s(X)) -> mark#(X),
                 mark#(from(X)) -> mark#(X),
                 mark#(from(X)) -> a__from#(mark(X)),
                    a__from#(X) -> mark#(X)}
  Weak:
  {          a__first(X1, X2) -> first(X1, X2),
             a__first(0(), X) -> nil(),
   a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                  mark(nil()) -> nil(),
                    mark(0()) -> 0(),
           mark(cons(X1, X2)) -> cons(mark(X1), X2),
          mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                   mark(s(X)) -> s(mark(X)),
                mark(from(X)) -> a__from(mark(X)),
                   a__from(X) -> cons(mark(X), from(s(X))),
                   a__from(X) -> from(X)}
  EDG:
   {(a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(from(X)) -> a__from#(mark(X)))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(from(X)) -> mark#(X))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(s(X)) -> mark#(X))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(from(X)) -> a__from#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(from(X)) -> mark#(X), mark#(from(X)) -> a__from#(mark(X)))
    (mark#(from(X)) -> mark#(X), mark#(from(X)) -> mark#(X))
    (mark#(from(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(from(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(from(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(from(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(from(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(from(X)) -> a__from#(mark(X)), a__from#(X) -> mark#(X))
    (mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y))
    (a__from#(X) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (a__from#(X) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (a__from#(X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (a__from#(X) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (a__from#(X) -> mark#(X), mark#(s(X)) -> mark#(X))
    (a__from#(X) -> mark#(X), mark#(from(X)) -> mark#(X))
    (a__from#(X) -> mark#(X), mark#(from(X)) -> a__from#(mark(X)))
    (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(from(X)) -> mark#(X))
    (mark#(s(X)) -> mark#(X), mark#(from(X)) -> a__from#(mark(X)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> mark#(X))
    (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> a__from#(mark(X)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(from(X)) -> mark#(X))
    (mark#(first(X1, X2)) -> mark#(X2), mark#(from(X)) -> a__from#(mark(X)))}
   SCCS:
    Scc:
     {a__first#(s(X), cons(Y, Z)) -> mark#(Y),
              mark#(cons(X1, X2)) -> mark#(X1),
             mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
             mark#(first(X1, X2)) -> mark#(X1),
             mark#(first(X1, X2)) -> mark#(X2),
                      mark#(s(X)) -> mark#(X),
                   mark#(from(X)) -> mark#(X),
                   mark#(from(X)) -> a__from#(mark(X)),
                      a__from#(X) -> mark#(X)}
    SCC:
     Strict:
      {a__first#(s(X), cons(Y, Z)) -> mark#(Y),
               mark#(cons(X1, X2)) -> mark#(X1),
              mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
              mark#(first(X1, X2)) -> mark#(X1),
              mark#(first(X1, X2)) -> mark#(X2),
                       mark#(s(X)) -> mark#(X),
                    mark#(from(X)) -> mark#(X),
                    mark#(from(X)) -> a__from#(mark(X)),
                       a__from#(X) -> mark#(X)}
     Weak:
     {          a__first(X1, X2) -> first(X1, X2),
                a__first(0(), X) -> nil(),
      a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                     mark(nil()) -> nil(),
                       mark(0()) -> 0(),
              mark(cons(X1, X2)) -> cons(mark(X1), X2),
             mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                      mark(s(X)) -> s(mark(X)),
                   mark(from(X)) -> a__from(mark(X)),
                      a__from(X) -> cons(mark(X), from(s(X))),
                      a__from(X) -> from(X)}
     POLY:
      Argument Filtering:
       pi(a__from#) = [0], pi(a__from) = [0], pi(from) = [0], pi(s) = 0, pi(first) = [0,1], pi(mark#) = 0, pi(mark) = 0, pi(cons) = 0, pi(0) = [], pi(a__first#) = 1, pi(a__first) = [0,1], pi(nil) = []
      Usable Rules:
       {}
      Interpretation:
       [a__from#](x0) = x0 + 1,
       [first](x0, x1) = x0 + x1,
       [from](x0) = x0 + 1
      Strict:
       {a__first#(s(X), cons(Y, Z)) -> mark#(Y),
                mark#(cons(X1, X2)) -> mark#(X1),
               mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
               mark#(first(X1, X2)) -> mark#(X1),
               mark#(first(X1, X2)) -> mark#(X2),
                        mark#(s(X)) -> mark#(X),
                     mark#(from(X)) -> a__from#(mark(X))}
      Weak:
       {          a__first(X1, X2) -> first(X1, X2),
                  a__first(0(), X) -> nil(),
        a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                       mark(nil()) -> nil(),
                         mark(0()) -> 0(),
                mark(cons(X1, X2)) -> cons(mark(X1), X2),
               mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                        mark(s(X)) -> s(mark(X)),
                     mark(from(X)) -> a__from(mark(X)),
                        a__from(X) -> cons(mark(X), from(s(X))),
                        a__from(X) -> from(X)}
      EDG:
       {(mark#(first(X1, X2)) -> mark#(X2), mark#(from(X)) -> a__from#(mark(X)))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(s(X)) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
        (mark#(first(X1, X2)) -> mark#(X2), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(from(X)) -> a__from#(mark(X)))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
        (mark#(first(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(from(X)) -> a__from#(mark(X)))
        (mark#(s(X)) -> mark#(X), mark#(s(X)) -> mark#(X))
        (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(s(X)) -> mark#(X), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
        (mark#(s(X)) -> mark#(X), mark#(cons(X1, X2)) -> mark#(X1))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X1))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(first(X1, X2)) -> mark#(X2))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(s(X)) -> mark#(X))
        (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(from(X)) -> a__from#(mark(X)))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X1))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(first(X1, X2)) -> mark#(X2))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(s(X)) -> mark#(X))
        (mark#(cons(X1, X2)) -> mark#(X1), mark#(from(X)) -> a__from#(mark(X)))
        (mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)), a__first#(s(X), cons(Y, Z)) -> mark#(Y))}
       SCCS:
        Scc:
         {a__first#(s(X), cons(Y, Z)) -> mark#(Y),
                  mark#(cons(X1, X2)) -> mark#(X1),
                 mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                 mark#(first(X1, X2)) -> mark#(X1),
                 mark#(first(X1, X2)) -> mark#(X2),
                          mark#(s(X)) -> mark#(X)}
        SCC:
         Strict:
          {a__first#(s(X), cons(Y, Z)) -> mark#(Y),
                   mark#(cons(X1, X2)) -> mark#(X1),
                  mark#(first(X1, X2)) -> a__first#(mark(X1), mark(X2)),
                  mark#(first(X1, X2)) -> mark#(X1),
                  mark#(first(X1, X2)) -> mark#(X2),
                           mark#(s(X)) -> mark#(X)}
         Weak:
         {          a__first(X1, X2) -> first(X1, X2),
                    a__first(0(), X) -> nil(),
          a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                         mark(nil()) -> nil(),
                           mark(0()) -> 0(),
                  mark(cons(X1, X2)) -> cons(mark(X1), X2),
                 mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                          mark(s(X)) -> s(mark(X)),
                       mark(from(X)) -> a__from(mark(X)),
                          a__from(X) -> cons(mark(X), from(s(X))),
                          a__from(X) -> from(X)}
         POLY:
          Argument Filtering:
           pi(a__from) = 0, pi(from) = 0, pi(s) = [0], pi(first) = [0,1], pi(mark#) = [0], pi(mark) = 0, pi(cons) = 0, pi(0) = [], pi(a__first#) = [0,1], pi(a__first) = [0,1], pi(nil) = []
          Usable Rules:
           {}
          Interpretation:
           [a__first#](x0, x1) = x0 + x1,
           [mark#](x0) = x0 + 1,
           [first](x0, x1) = x0 + x1 + 1,
           [s](x0) = x0 + 1
          Strict:
           {a__first#(s(X), cons(Y, Z)) -> mark#(Y),
                    mark#(cons(X1, X2)) -> mark#(X1)}
          Weak:
           {          a__first(X1, X2) -> first(X1, X2),
                      a__first(0(), X) -> nil(),
            a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                           mark(nil()) -> nil(),
                             mark(0()) -> 0(),
                    mark(cons(X1, X2)) -> cons(mark(X1), X2),
                   mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                            mark(s(X)) -> s(mark(X)),
                         mark(from(X)) -> a__from(mark(X)),
                            a__from(X) -> cons(mark(X), from(s(X))),
                            a__from(X) -> from(X)}
          EDG:
           {(mark#(cons(X1, X2)) -> mark#(X1), mark#(cons(X1, X2)) -> mark#(X1))
            (a__first#(s(X), cons(Y, Z)) -> mark#(Y), mark#(cons(X1, X2)) -> mark#(X1))}
           SCCS:
            Scc:
             {mark#(cons(X1, X2)) -> mark#(X1)}
            SCC:
             Strict:
              {mark#(cons(X1, X2)) -> mark#(X1)}
             Weak:
             {          a__first(X1, X2) -> first(X1, X2),
                        a__first(0(), X) -> nil(),
              a__first(s(X), cons(Y, Z)) -> cons(mark(Y), first(X, Z)),
                             mark(nil()) -> nil(),
                               mark(0()) -> 0(),
                      mark(cons(X1, X2)) -> cons(mark(X1), X2),
                     mark(first(X1, X2)) -> a__first(mark(X1), mark(X2)),
                              mark(s(X)) -> s(mark(X)),
                           mark(from(X)) -> a__from(mark(X)),
                              a__from(X) -> cons(mark(X), from(s(X))),
                              a__from(X) -> from(X)}
             SPSC:
              Simple Projection:
               pi(mark#) = 0
              Strict:
               {}
              Qed