YES

Problem:
 intlist(nil()) -> nil()
 int(s(x),0()) -> nil()
 int(x,x) -> cons(x,nil())
 intlist(cons(x,y)) -> cons(s(x),intlist(y))
 int(s(x),s(y)) -> intlist(int(x,y))
 int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
 intlist(cons(x,nil())) -> cons(s(x),nil())

Proof:
 DP Processor:
  DPs:
   intlist#(cons(x,y)) -> intlist#(y)
   int#(s(x),s(y)) -> int#(x,y)
   int#(s(x),s(y)) -> intlist#(int(x,y))
   int#(0(),s(y)) -> int#(s(0()),s(y))
  TRS:
   intlist(nil()) -> nil()
   int(s(x),0()) -> nil()
   int(x,x) -> cons(x,nil())
   intlist(cons(x,y)) -> cons(s(x),intlist(y))
   int(s(x),s(y)) -> intlist(int(x,y))
   int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
   intlist(cons(x,nil())) -> cons(s(x),nil())
  TDG Processor:
   DPs:
    intlist#(cons(x,y)) -> intlist#(y)
    int#(s(x),s(y)) -> int#(x,y)
    int#(s(x),s(y)) -> intlist#(int(x,y))
    int#(0(),s(y)) -> int#(s(0()),s(y))
   TRS:
    intlist(nil()) -> nil()
    int(s(x),0()) -> nil()
    int(x,x) -> cons(x,nil())
    intlist(cons(x,y)) -> cons(s(x),intlist(y))
    int(s(x),s(y)) -> intlist(int(x,y))
    int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
    intlist(cons(x,nil())) -> cons(s(x),nil())
   graph:
    int#(0(),s(y)) -> int#(s(0()),s(y)) ->
    int#(0(),s(y)) -> int#(s(0()),s(y))
    int#(0(),s(y)) -> int#(s(0()),s(y)) ->
    int#(s(x),s(y)) -> intlist#(int(x,y))
    int#(0(),s(y)) -> int#(s(0()),s(y)) -> int#(s(x),s(y)) -> int#(x,y)
    int#(s(x),s(y)) -> int#(x,y) -> int#(0(),s(y)) -> int#(s(0()),s(y))
    int#(s(x),s(y)) -> int#(x,y) ->
    int#(s(x),s(y)) -> intlist#(int(x,y))
    int#(s(x),s(y)) -> int#(x,y) ->
    int#(s(x),s(y)) -> int#(x,y)
    int#(s(x),s(y)) -> intlist#(int(x,y)) ->
    intlist#(cons(x,y)) -> intlist#(y)
    intlist#(cons(x,y)) -> intlist#(y) -> intlist#(cons(x,y)) -> intlist#(y)
   SCC Processor:
    #sccs: 2
    #rules: 3
    #arcs: 8/16
    DPs:
     int#(0(),s(y)) -> int#(s(0()),s(y))
     int#(s(x),s(y)) -> int#(x,y)
    TRS:
     intlist(nil()) -> nil()
     int(s(x),0()) -> nil()
     int(x,x) -> cons(x,nil())
     intlist(cons(x,y)) -> cons(s(x),intlist(y))
     int(s(x),s(y)) -> intlist(int(x,y))
     int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
     intlist(cons(x,nil())) -> cons(s(x),nil())
    Subterm Criterion Processor:
     simple projection:
      pi(int#) = 1
     problem:
      DPs:
       int#(0(),s(y)) -> int#(s(0()),s(y))
      TRS:
       intlist(nil()) -> nil()
       int(s(x),0()) -> nil()
       int(x,x) -> cons(x,nil())
       intlist(cons(x,y)) -> cons(s(x),intlist(y))
       int(s(x),s(y)) -> intlist(int(x,y))
       int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
       intlist(cons(x,nil())) -> cons(s(x),nil())
     EDG Processor:
      DPs:
       int#(0(),s(y)) -> int#(s(0()),s(y))
      TRS:
       intlist(nil()) -> nil()
       int(s(x),0()) -> nil()
       int(x,x) -> cons(x,nil())
       intlist(cons(x,y)) -> cons(s(x),intlist(y))
       int(s(x),s(y)) -> intlist(int(x,y))
       int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
       intlist(cons(x,nil())) -> cons(s(x),nil())
      graph:
       
      Qed
    
    DPs:
     intlist#(cons(x,y)) -> intlist#(y)
    TRS:
     intlist(nil()) -> nil()
     int(s(x),0()) -> nil()
     int(x,x) -> cons(x,nil())
     intlist(cons(x,y)) -> cons(s(x),intlist(y))
     int(s(x),s(y)) -> intlist(int(x,y))
     int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
     intlist(cons(x,nil())) -> cons(s(x),nil())
    Subterm Criterion Processor:
     simple projection:
      pi(intlist#) = 0
     problem:
      DPs:
       
      TRS:
       intlist(nil()) -> nil()
       int(s(x),0()) -> nil()
       int(x,x) -> cons(x,nil())
       intlist(cons(x,y)) -> cons(s(x),intlist(y))
       int(s(x),s(y)) -> intlist(int(x,y))
       int(0(),s(y)) -> cons(0(),int(s(0()),s(y)))
       intlist(cons(x,nil())) -> cons(s(x),nil())
     Qed