YES

Problem:
 from(X) -> cons(X,n__from(n__s(X)))
 head(cons(X,XS)) -> X
 2nd(cons(X,XS)) -> head(activate(XS))
 take(0(),XS) -> nil()
 take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
 sel(0(),cons(X,XS)) -> X
 sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
 from(X) -> n__from(X)
 s(X) -> n__s(X)
 take(X1,X2) -> n__take(X1,X2)
 activate(n__from(X)) -> from(activate(X))
 activate(n__s(X)) -> s(activate(X))
 activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
 activate(X) -> X

Proof:
 DP Processor:
  DPs:
   2nd#(cons(X,XS)) -> activate#(XS)
   2nd#(cons(X,XS)) -> head#(activate(XS))
   take#(s(N),cons(X,XS)) -> activate#(XS)
   sel#(s(N),cons(X,XS)) -> activate#(XS)
   sel#(s(N),cons(X,XS)) -> sel#(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))
   activate#(n__take(X1,X2)) -> activate#(X2)
   activate#(n__take(X1,X2)) -> activate#(X1)
   activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
  TRS:
   from(X) -> cons(X,n__from(n__s(X)))
   head(cons(X,XS)) -> X
   2nd(cons(X,XS)) -> head(activate(XS))
   take(0(),XS) -> nil()
   take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
   sel(0(),cons(X,XS)) -> X
   sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
   from(X) -> n__from(X)
   s(X) -> n__s(X)
   take(X1,X2) -> n__take(X1,X2)
   activate(n__from(X)) -> from(activate(X))
   activate(n__s(X)) -> s(activate(X))
   activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
   activate(X) -> X
  TDG Processor:
   DPs:
    2nd#(cons(X,XS)) -> activate#(XS)
    2nd#(cons(X,XS)) -> head#(activate(XS))
    take#(s(N),cons(X,XS)) -> activate#(XS)
    sel#(s(N),cons(X,XS)) -> activate#(XS)
    sel#(s(N),cons(X,XS)) -> sel#(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))
    activate#(n__take(X1,X2)) -> activate#(X2)
    activate#(n__take(X1,X2)) -> activate#(X1)
    activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
   TRS:
    from(X) -> cons(X,n__from(n__s(X)))
    head(cons(X,XS)) -> X
    2nd(cons(X,XS)) -> head(activate(XS))
    take(0(),XS) -> nil()
    take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
    sel(0(),cons(X,XS)) -> X
    sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
    from(X) -> n__from(X)
    s(X) -> n__s(X)
    take(X1,X2) -> n__take(X1,X2)
    activate(n__from(X)) -> from(activate(X))
    activate(n__s(X)) -> s(activate(X))
    activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
    activate(X) -> X
   graph:
    sel#(s(N),cons(X,XS)) -> sel#(N,activate(XS)) ->
    sel#(s(N),cons(X,XS)) -> sel#(N,activate(XS))
    sel#(s(N),cons(X,XS)) -> sel#(N,activate(XS)) ->
    sel#(s(N),cons(X,XS)) -> activate#(XS)
    sel#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
    sel#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__take(X1,X2)) -> activate#(X1)
    sel#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__take(X1,X2)) -> activate#(X2)
    sel#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__s(X)) -> s#(activate(X))
    sel#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__s(X)) -> activate#(X)
    sel#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__from(X)) -> from#(activate(X))
    sel#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__from(X)) -> activate#(X)
    take#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
    take#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__take(X1,X2)) -> activate#(X1)
    take#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__take(X1,X2)) -> activate#(X2)
    take#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__s(X)) -> s#(activate(X))
    take#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__s(X)) -> activate#(X)
    take#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__from(X)) -> from#(activate(X))
    take#(s(N),cons(X,XS)) -> activate#(XS) ->
    activate#(n__from(X)) -> activate#(X)
    activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2)) ->
    take#(s(N),cons(X,XS)) -> activate#(XS)
    activate#(n__take(X1,X2)) -> activate#(X2) ->
    activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
    activate#(n__take(X1,X2)) -> activate#(X2) ->
    activate#(n__take(X1,X2)) -> activate#(X1)
    activate#(n__take(X1,X2)) -> activate#(X2) ->
    activate#(n__take(X1,X2)) -> activate#(X2)
    activate#(n__take(X1,X2)) -> activate#(X2) ->
    activate#(n__s(X)) -> s#(activate(X))
    activate#(n__take(X1,X2)) -> activate#(X2) ->
    activate#(n__s(X)) -> activate#(X)
    activate#(n__take(X1,X2)) -> activate#(X2) ->
    activate#(n__from(X)) -> from#(activate(X))
    activate#(n__take(X1,X2)) -> activate#(X2) ->
    activate#(n__from(X)) -> activate#(X)
    activate#(n__take(X1,X2)) -> activate#(X1) ->
    activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
    activate#(n__take(X1,X2)) -> activate#(X1) ->
    activate#(n__take(X1,X2)) -> activate#(X1)
    activate#(n__take(X1,X2)) -> activate#(X1) ->
    activate#(n__take(X1,X2)) -> activate#(X2)
    activate#(n__take(X1,X2)) -> activate#(X1) ->
    activate#(n__s(X)) -> s#(activate(X))
    activate#(n__take(X1,X2)) -> activate#(X1) ->
    activate#(n__s(X)) -> activate#(X)
    activate#(n__take(X1,X2)) -> activate#(X1) ->
    activate#(n__from(X)) -> from#(activate(X))
    activate#(n__take(X1,X2)) -> activate#(X1) ->
    activate#(n__from(X)) -> activate#(X)
    activate#(n__from(X)) -> activate#(X) ->
    activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
    activate#(n__from(X)) -> activate#(X) ->
    activate#(n__take(X1,X2)) -> activate#(X1)
    activate#(n__from(X)) -> activate#(X) ->
    activate#(n__take(X1,X2)) -> activate#(X2)
    activate#(n__from(X)) -> activate#(X) ->
    activate#(n__s(X)) -> s#(activate(X))
    activate#(n__from(X)) -> activate#(X) ->
    activate#(n__s(X)) -> activate#(X)
    activate#(n__from(X)) -> activate#(X) ->
    activate#(n__from(X)) -> from#(activate(X))
    activate#(n__from(X)) -> activate#(X) ->
    activate#(n__from(X)) -> activate#(X)
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__take(X1,X2)) -> activate#(X1)
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__take(X1,X2)) -> activate#(X2)
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__s(X)) -> s#(activate(X))
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__s(X)) -> activate#(X)
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__from(X)) -> from#(activate(X))
    activate#(n__s(X)) -> activate#(X) ->
    activate#(n__from(X)) -> activate#(X)
    2nd#(cons(X,XS)) -> activate#(XS) ->
    activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
    2nd#(cons(X,XS)) -> activate#(XS) ->
    activate#(n__take(X1,X2)) -> activate#(X1)
    2nd#(cons(X,XS)) -> activate#(XS) ->
    activate#(n__take(X1,X2)) -> activate#(X2)
    2nd#(cons(X,XS)) -> activate#(XS) ->
    activate#(n__s(X)) -> s#(activate(X))
    2nd#(cons(X,XS)) -> activate#(XS) ->
    activate#(n__s(X)) -> activate#(X)
    2nd#(cons(X,XS)) -> activate#(XS) ->
    activate#(n__from(X)) -> from#(activate(X))
    2nd#(cons(X,XS)) -> activate#(XS) -> activate#(n__from(X)) -> activate#(X)
   SCC Processor:
    #sccs: 2
    #rules: 7
    #arcs: 52/144
    DPs:
     sel#(s(N),cons(X,XS)) -> sel#(N,activate(XS))
    TRS:
     from(X) -> cons(X,n__from(n__s(X)))
     head(cons(X,XS)) -> X
     2nd(cons(X,XS)) -> head(activate(XS))
     take(0(),XS) -> nil()
     take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
     sel(0(),cons(X,XS)) -> X
     sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
     from(X) -> n__from(X)
     s(X) -> n__s(X)
     take(X1,X2) -> n__take(X1,X2)
     activate(n__from(X)) -> from(activate(X))
     activate(n__s(X)) -> s(activate(X))
     activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
     activate(X) -> X
    Subterm Criterion Processor:
     simple projection:
      pi(sel#) = 0
     problem:
      DPs:
       
      TRS:
       from(X) -> cons(X,n__from(n__s(X)))
       head(cons(X,XS)) -> X
       2nd(cons(X,XS)) -> head(activate(XS))
       take(0(),XS) -> nil()
       take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
       sel(0(),cons(X,XS)) -> X
       sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
       from(X) -> n__from(X)
       s(X) -> n__s(X)
       take(X1,X2) -> n__take(X1,X2)
       activate(n__from(X)) -> from(activate(X))
       activate(n__s(X)) -> s(activate(X))
       activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
       activate(X) -> X
     Qed
    
    DPs:
     activate#(n__from(X)) -> activate#(X)
     activate#(n__s(X)) -> activate#(X)
     activate#(n__take(X1,X2)) -> activate#(X2)
     activate#(n__take(X1,X2)) -> activate#(X1)
     activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
     take#(s(N),cons(X,XS)) -> activate#(XS)
    TRS:
     from(X) -> cons(X,n__from(n__s(X)))
     head(cons(X,XS)) -> X
     2nd(cons(X,XS)) -> head(activate(XS))
     take(0(),XS) -> nil()
     take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
     sel(0(),cons(X,XS)) -> X
     sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
     from(X) -> n__from(X)
     s(X) -> n__s(X)
     take(X1,X2) -> n__take(X1,X2)
     activate(n__from(X)) -> from(activate(X))
     activate(n__s(X)) -> s(activate(X))
     activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
     activate(X) -> X
    Arctic Interpretation Processor:
     dimension: 1
     interpretation:
      [take#](x0, x1) = x1 + 0,
      
      [activate#](x0) = x0,
      
      [sel](x0, x1) = x0 + x1 + 7,
      
      [n__take](x0, x1) = 7x0 + x1 + 0,
      
      [s](x0) = x0 + 0,
      
      [nil] = 0,
      
      [take](x0, x1) = 7x0 + x1 + 0,
      
      [0] = 0,
      
      [activate](x0) = x0,
      
      [2nd](x0) = x0 + 0,
      
      [head](x0) = x0 + 7,
      
      [cons](x0, x1) = x0 + x1 + 7,
      
      [n__from](x0) = x0 + 7,
      
      [n__s](x0) = x0 + 0,
      
      [from](x0) = x0 + 7
     orientation:
      activate#(n__from(X)) = X + 7 >= X = activate#(X)
      
      activate#(n__s(X)) = X + 0 >= X = activate#(X)
      
      activate#(n__take(X1,X2)) = 7X1 + X2 + 0 >= X2 = activate#(X2)
      
      activate#(n__take(X1,X2)) = 7X1 + X2 + 0 >= X1 = activate#(X1)
      
      activate#(n__take(X1,X2)) = 7X1 + X2 + 0 >= X2 + 0 = take#(activate(X1),activate(X2))
      
      take#(s(N),cons(X,XS)) = X + XS + 7 >= XS = activate#(XS)
      
      from(X) = X + 7 >= X + 7 = cons(X,n__from(n__s(X)))
      
      head(cons(X,XS)) = X + XS + 7 >= X = X
      
      2nd(cons(X,XS)) = X + XS + 7 >= XS + 7 = head(activate(XS))
      
      take(0(),XS) = XS + 7 >= 0 = nil()
      
      take(s(N),cons(X,XS)) = 7N + X + XS + 7 >= 7N + X + XS + 7 = cons(X,n__take(N,activate(XS)))
      
      sel(0(),cons(X,XS)) = X + XS + 7 >= X = X
      
      sel(s(N),cons(X,XS)) = N + X + XS + 7 >= N + XS + 7 = sel(N,activate(XS))
      
      from(X) = X + 7 >= X + 7 = n__from(X)
      
      s(X) = X + 0 >= X + 0 = n__s(X)
      
      take(X1,X2) = 7X1 + X2 + 0 >= 7X1 + X2 + 0 = n__take(X1,X2)
      
      activate(n__from(X)) = X + 7 >= X + 7 = from(activate(X))
      
      activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X))
      
      activate(n__take(X1,X2)) = 7X1 + X2 + 0 >= 7X1 + X2 + 0 = take(activate(X1),activate(X2))
      
      activate(X) = X >= X = X
     problem:
      DPs:
       activate#(n__from(X)) -> activate#(X)
       activate#(n__s(X)) -> activate#(X)
       activate#(n__take(X1,X2)) -> activate#(X2)
       activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
       take#(s(N),cons(X,XS)) -> activate#(XS)
      TRS:
       from(X) -> cons(X,n__from(n__s(X)))
       head(cons(X,XS)) -> X
       2nd(cons(X,XS)) -> head(activate(XS))
       take(0(),XS) -> nil()
       take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
       sel(0(),cons(X,XS)) -> X
       sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
       from(X) -> n__from(X)
       s(X) -> n__s(X)
       take(X1,X2) -> n__take(X1,X2)
       activate(n__from(X)) -> from(activate(X))
       activate(n__s(X)) -> s(activate(X))
       activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
       activate(X) -> X
     Arctic Interpretation Processor:
      dimension: 1
      interpretation:
       [take#](x0, x1) = x0 + x1 + 0,
       
       [activate#](x0) = x0 + 0,
       
       [sel](x0, x1) = x0 + 5x1,
       
       [n__take](x0, x1) = x0 + x1 + 0,
       
       [s](x0) = x0,
       
       [nil] = 3,
       
       [take](x0, x1) = x0 + x1 + 0,
       
       [0] = 3,
       
       [activate](x0) = x0 + 0,
       
       [2nd](x0) = 7x0 + 0,
       
       [head](x0) = 2x0 + 4,
       
       [cons](x0, x1) = x0 + x1 + 0,
       
       [n__from](x0) = 1x0 + 2,
       
       [n__s](x0) = x0,
       
       [from](x0) = 1x0 + 2
      orientation:
       activate#(n__from(X)) = 1X + 2 >= X + 0 = activate#(X)
       
       activate#(n__s(X)) = X + 0 >= X + 0 = activate#(X)
       
       activate#(n__take(X1,X2)) = X1 + X2 + 0 >= X2 + 0 = activate#(X2)
       
       activate#(n__take(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = take#(activate(X1),activate(X2))
       
       take#(s(N),cons(X,XS)) = N + X + XS + 0 >= XS + 0 = activate#(XS)
       
       from(X) = 1X + 2 >= 1X + 2 = cons(X,n__from(n__s(X)))
       
       head(cons(X,XS)) = 2X + 2XS + 4 >= X = X
       
       2nd(cons(X,XS)) = 7X + 7XS + 7 >= 2XS + 4 = head(activate(XS))
       
       take(0(),XS) = XS + 3 >= 3 = nil()
       
       take(s(N),cons(X,XS)) = N + X + XS + 0 >= N + X + XS + 0 = cons(X,n__take(N,activate(XS)))
       
       sel(0(),cons(X,XS)) = 5X + 5XS + 5 >= X = X
       
       sel(s(N),cons(X,XS)) = N + 5X + 5XS + 5 >= N + 5XS + 5 = sel(N,activate(XS))
       
       from(X) = 1X + 2 >= 1X + 2 = n__from(X)
       
       s(X) = X >= X = n__s(X)
       
       take(X1,X2) = X1 + X2 + 0 >= X1 + X2 + 0 = n__take(X1,X2)
       
       activate(n__from(X)) = 1X + 2 >= 1X + 2 = from(activate(X))
       
       activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X))
       
       activate(n__take(X1,X2)) = X1 + X2 + 0 >= X1 + X2 + 0 = take(activate(X1),activate(X2))
       
       activate(X) = X + 0 >= X = X
      problem:
       DPs:
        activate#(n__s(X)) -> activate#(X)
        activate#(n__take(X1,X2)) -> activate#(X2)
        activate#(n__take(X1,X2)) -> take#(activate(X1),activate(X2))
        take#(s(N),cons(X,XS)) -> activate#(XS)
       TRS:
        from(X) -> cons(X,n__from(n__s(X)))
        head(cons(X,XS)) -> X
        2nd(cons(X,XS)) -> head(activate(XS))
        take(0(),XS) -> nil()
        take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
        sel(0(),cons(X,XS)) -> X
        sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
        from(X) -> n__from(X)
        s(X) -> n__s(X)
        take(X1,X2) -> n__take(X1,X2)
        activate(n__from(X)) -> from(activate(X))
        activate(n__s(X)) -> s(activate(X))
        activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
        activate(X) -> X
      Arctic Interpretation Processor:
       dimension: 1
       interpretation:
        [take#](x0, x1) = x0 + x1 + 0,
        
        [activate#](x0) = x0 + 2,
        
        [sel](x0, x1) = 6x0 + x1,
        
        [n__take](x0, x1) = 2x0 + 2x1,
        
        [s](x0) = x0 + 0,
        
        [nil] = 1,
        
        [take](x0, x1) = 2x0 + 2x1,
        
        [0] = 0,
        
        [activate](x0) = x0,
        
        [2nd](x0) = 4x0 + 1,
        
        [head](x0) = 4x0,
        
        [cons](x0, x1) = x0 + x1 + 2,
        
        [n__from](x0) = x0 + 2,
        
        [n__s](x0) = x0 + 0,
        
        [from](x0) = x0 + 2
       orientation:
        activate#(n__s(X)) = X + 2 >= X + 2 = activate#(X)
        
        activate#(n__take(X1,X2)) = 2X1 + 2X2 + 2 >= X2 + 2 = activate#(X2)
        
        activate#(n__take(X1,X2)) = 2X1 + 2X2 + 2 >= X1 + X2 + 0 = take#(activate(X1),activate(X2))
        
        take#(s(N),cons(X,XS)) = N + X + XS + 2 >= XS + 2 = activate#(XS)
        
        from(X) = X + 2 >= X + 2 = cons(X,n__from(n__s(X)))
        
        head(cons(X,XS)) = 4X + 4XS + 6 >= X = X
        
        2nd(cons(X,XS)) = 4X + 4XS + 6 >= 4XS = head(activate(XS))
        
        take(0(),XS) = 2XS + 2 >= 1 = nil()
        
        take(s(N),cons(X,XS)) = 2N + 2X + 2XS + 4 >= 2N + X + 2XS + 2 = cons(X,n__take(N,activate(XS)))
        
        sel(0(),cons(X,XS)) = X + XS + 6 >= X = X
        
        sel(s(N),cons(X,XS)) = 6N + X + XS + 6 >= 6N + XS = sel(N,activate(XS))
        
        from(X) = X + 2 >= X + 2 = n__from(X)
        
        s(X) = X + 0 >= X + 0 = n__s(X)
        
        take(X1,X2) = 2X1 + 2X2 >= 2X1 + 2X2 = n__take(X1,X2)
        
        activate(n__from(X)) = X + 2 >= X + 2 = from(activate(X))
        
        activate(n__s(X)) = X + 0 >= X + 0 = s(activate(X))
        
        activate(n__take(X1,X2)) = 2X1 + 2X2 >= 2X1 + 2X2 = take(activate(X1),activate(X2))
        
        activate(X) = X >= X = X
       problem:
        DPs:
         activate#(n__s(X)) -> activate#(X)
         activate#(n__take(X1,X2)) -> activate#(X2)
         take#(s(N),cons(X,XS)) -> activate#(XS)
        TRS:
         from(X) -> cons(X,n__from(n__s(X)))
         head(cons(X,XS)) -> X
         2nd(cons(X,XS)) -> head(activate(XS))
         take(0(),XS) -> nil()
         take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
         sel(0(),cons(X,XS)) -> X
         sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
         from(X) -> n__from(X)
         s(X) -> n__s(X)
         take(X1,X2) -> n__take(X1,X2)
         activate(n__from(X)) -> from(activate(X))
         activate(n__s(X)) -> s(activate(X))
         activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
         activate(X) -> X
       SCC Processor:
        #sccs: 1
        #rules: 2
        #arcs: 26/9
        DPs:
         activate#(n__s(X)) -> activate#(X)
         activate#(n__take(X1,X2)) -> activate#(X2)
        TRS:
         from(X) -> cons(X,n__from(n__s(X)))
         head(cons(X,XS)) -> X
         2nd(cons(X,XS)) -> head(activate(XS))
         take(0(),XS) -> nil()
         take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
         sel(0(),cons(X,XS)) -> X
         sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
         from(X) -> n__from(X)
         s(X) -> n__s(X)
         take(X1,X2) -> n__take(X1,X2)
         activate(n__from(X)) -> from(activate(X))
         activate(n__s(X)) -> s(activate(X))
         activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
         activate(X) -> X
        Subterm Criterion Processor:
         simple projection:
          pi(activate#) = 0
         problem:
          DPs:
           
          TRS:
           from(X) -> cons(X,n__from(n__s(X)))
           head(cons(X,XS)) -> X
           2nd(cons(X,XS)) -> head(activate(XS))
           take(0(),XS) -> nil()
           take(s(N),cons(X,XS)) -> cons(X,n__take(N,activate(XS)))
           sel(0(),cons(X,XS)) -> X
           sel(s(N),cons(X,XS)) -> sel(N,activate(XS))
           from(X) -> n__from(X)
           s(X) -> n__s(X)
           take(X1,X2) -> n__take(X1,X2)
           activate(n__from(X)) -> from(activate(X))
           activate(n__s(X)) -> s(activate(X))
           activate(n__take(X1,X2)) -> take(activate(X1),activate(X2))
           activate(X) -> X
         Qed