YES
(VAR x y)
(RULES 
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)
)

Proving termination of rewriting for LPAR_intlist:

-> Dependency pairs:
nF_intlist(cons(x,y)) -> nF_intlist(y)
nF_int(s(x),s(y)) -> nF_intlist(int(x,y))
nF_int(s(x),s(y)) -> nF_int(x,y)
nF_int(0,s(y)) -> nF_int(s(0),s(y))

-> Proof of termination for LPAR_intlist_1_1:
-> -> Dependency pairs in cycle:
nF_int(s(x),s(y)) -> nF_int(x,y)
nF_int(0,s(y)) -> nF_int(s(0),s(y))

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for LPAR_intlist_1_2:
-> -> Dependency pairs in cycle:
nF_intlist(cons(x,y)) -> nF_intlist(y)

Termination proved: Cycles verify subterm criterion.

SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.