YES
Time: 0.009027
TRS:
 {            first(X1, X2) -> n__first(X1, X2),
              first(0(), X) -> nil(),
     first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
                 activate X -> X,
  activate n__first(X1, X2) -> first(X1, X2),
         activate n__from X -> from X,
                     from X -> cons(X, n__from s X),
                     from X -> n__from X}
 DP:
  DP:
   {   first#(s X, cons(Y, Z)) -> activate# Z,
    activate# n__first(X1, X2) -> first#(X1, X2),
           activate# n__from X -> from# X}
  TRS:
  {            first(X1, X2) -> n__first(X1, X2),
               first(0(), X) -> nil(),
      first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
                  activate X -> X,
   activate n__first(X1, X2) -> first(X1, X2),
          activate n__from X -> from X,
                      from X -> cons(X, n__from s X),
                      from X -> n__from X}
  UR:
   {}
   EDG:
    {(first#(s X, cons(Y, Z)) -> activate# Z, activate# n__from X -> from# X)
     (first#(s X, cons(Y, Z)) -> activate# Z, activate# n__first(X1, X2) -> first#(X1, X2))
     (activate# n__first(X1, X2) -> first#(X1, X2), first#(s X, cons(Y, Z)) -> activate# Z)}
    STATUS:
     arrows: 0.666667
     SCCS (1):
      Scc:
       {   first#(s X, cons(Y, Z)) -> activate# Z,
        activate# n__first(X1, X2) -> first#(X1, X2)}
      
      SCC (2):
       Strict:
        {   first#(s X, cons(Y, Z)) -> activate# Z,
         activate# n__first(X1, X2) -> first#(X1, X2)}
       Weak:
       {            first(X1, X2) -> n__first(X1, X2),
                    first(0(), X) -> nil(),
           first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z)),
                       activate X -> X,
        activate n__first(X1, X2) -> first(X1, X2),
               activate n__from X -> from X,
                           from X -> cons(X, n__from s X),
                           from X -> n__from X}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [first](x0, x1) = x0 + x1,
         
         [cons](x0, x1) = x0 + 1,
         
         [n__first](x0, x1) = x0 + x1 + 1,
         
         [activate](x0) = 1,
         
         [s](x0) = 1,
         
         [n__from](x0) = 0,
         
         [from](x0) = 0,
         
         [nil] = 0,
         
         [0] = 0,
         
         [first#](x0, x1) = x0,
         
         [activate#](x0) = x0
        Strict:
         activate# n__first(X1, X2) -> first#(X1, X2)
         1 + 1X1 + 1X2 >= 0 + 0X1 + 1X2
         first#(s X, cons(Y, Z)) -> activate# Z
         1 + 0X + 0Y + 1Z >= 0 + 1Z
        Weak:
         from X -> n__from X
         0 + 0X >= 0 + 0X
         from X -> cons(X, n__from s X)
         0 + 0X >= 1 + 0X
         activate n__from X -> from X
         1 + 0X >= 0 + 0X
         activate n__first(X1, X2) -> first(X1, X2)
         1 + 0X1 + 0X2 >= 0 + 1X1 + 1X2
         activate X -> X
         1 + 0X >= 1X
         first(s X, cons(Y, Z)) -> cons(Y, n__first(X, activate Z))
         2 + 0X + 0Y + 1Z >= 3 + 1X + 0Y + 0Z
         first(0(), X) -> nil()
         0 + 1X >= 0
         first(X1, X2) -> n__first(X1, X2)
         0 + 1X1 + 1X2 >= 1 + 1X1 + 1X2
       Qed