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