YES

Problem:
 from(X) -> cons(X,n__from(n__s(X)))
 after(0(),XS) -> XS
 after(s(N),cons(X,XS)) -> after(N,activate(XS))
 from(X) -> n__from(X)
 s(X) -> n__s(X)
 activate(n__from(X)) -> from(activate(X))
 activate(n__s(X)) -> s(activate(X))
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   after#(s(N),cons(X,XS)) -> activate#(XS)
   after#(s(N),cons(X,XS)) -> after#(N,activate(XS))
   activate#(n__from(X)) -> activate#(X)
   activate#(n__from(X)) -> from#(activate(X))
   activate#(n__s(X)) -> activate#(X)
   activate#(n__s(X)) -> s#(activate(X))
  TRS:
   from(X) -> cons(X,n__from(n__s(X)))
   after(0(),XS) -> XS
   after(s(N),cons(X,XS)) -> after(N,activate(XS))
   from(X) -> n__from(X)
   s(X) -> n__s(X)
   activate(n__from(X)) -> from(activate(X))
   activate(n__s(X)) -> s(activate(X))
   activate(X) -> X
  Matrix Interpretation Processor: dim=2
   
   interpretation:
    [s#](x0) = [0],
    
    [activate#](x0) = [0 1]x0 + [1],
    
    [after#](x0, x1) = [0 3]x0 + [1 1]x1,
    
    [from#](x0) = [1],
    
                          [2]
    [activate](x0) = x0 + [0],
    
              [0 0]     [2]
    [s](x0) = [0 1]x0 + [1],
    
                      [0 2]     [1 1]     [3]
    [after](x0, x1) = [0 3]x0 + [1 1]x1 + [1],
    
          [0]
    [0] = [0],
    
                     [0 1]  
    [cons](x0, x1) = [1 0]x1,
    
                    [0 1]     [0]
    [n__from](x0) = [0 1]x0 + [1],
    
                 [0 0]     [0]
    [n__s](x0) = [0 1]x0 + [1],
    
                 [0 1]     [2]
    [from](x0) = [0 1]x0 + [1]
   orientation:
    after#(s(N),cons(X,XS)) = [0 3]N + [1 1]XS + [3] >= [0 1]XS + [1] = activate#(XS)
    
    after#(s(N),cons(X,XS)) = [0 3]N + [1 1]XS + [3] >= [0 3]N + [1 1]XS + [2] = after#(N,activate(XS))
    
    activate#(n__from(X)) = [0 1]X + [2] >= [0 1]X + [1] = activate#(X)
    
    activate#(n__from(X)) = [0 1]X + [2] >= [1] = from#(activate(X))
    
    activate#(n__s(X)) = [0 1]X + [2] >= [0 1]X + [1] = activate#(X)
    
    activate#(n__s(X)) = [0 1]X + [2] >= [0] = s#(activate(X))
    
              [0 1]    [2]    [0 1]    [2]                           
    from(X) = [0 1]X + [1] >= [0 1]X + [1] = cons(X,n__from(n__s(X)))
    
                    [1 1]     [3]           
    after(0(),XS) = [1 1]XS + [1] >= XS = XS
    
                             [0 2]    [1 1]     [5]    [0 2]    [1 1]     [5]                        
    after(s(N),cons(X,XS)) = [0 3]N + [1 1]XS + [4] >= [0 3]N + [1 1]XS + [3] = after(N,activate(XS))
    
              [0 1]    [2]    [0 1]    [0]             
    from(X) = [0 1]X + [1] >= [0 1]X + [1] = n__from(X)
    
           [0 0]    [2]    [0 0]    [0]          
    s(X) = [0 1]X + [1] >= [0 1]X + [1] = n__s(X)
    
                           [0 1]    [2]    [0 1]    [2]                    
    activate(n__from(X)) = [0 1]X + [1] >= [0 1]X + [1] = from(activate(X))
    
                        [0 0]    [2]    [0 0]    [2]                 
    activate(n__s(X)) = [0 1]X + [1] >= [0 1]X + [1] = s(activate(X))
    
                      [2]         
    activate(X) = X + [0] >= X = X
   problem:
    DPs:
     
    TRS:
     from(X) -> cons(X,n__from(n__s(X)))
     after(0(),XS) -> XS
     after(s(N),cons(X,XS)) -> after(N,activate(XS))
     from(X) -> n__from(X)
     s(X) -> n__s(X)
     activate(n__from(X)) -> from(activate(X))
     activate(n__s(X)) -> s(activate(X))
     activate(X) -> X
   Qed