YES
(VAR x y z l)
(RULES 
+(x,0) -> x
+(0,x) -> x
+(s(x),s(y)) -> s(s(+(x,y)))
+(+(x,y),z) -> +(x,+(y,z))
*(x,0) -> 0
*(0,x) -> 0
*(s(x),s(y)) -> s(+(*(x,y),+(x,y)))
*(*(x,y),z) -> *(x,*(y,z))
sum(nil) -> 0
sum(cons(x,l)) -> +(x,sum(l))
prod(nil) -> s(0)
prod(cons(x,l)) -> *(x,prod(l))
)

Proving termination of rewriting for list_sum_prod_assoc:

-> Dependency pairs:
nF_+(s(x),s(y)) -> nF_+(x,y)
nF_+(+(x,y),z) -> nF_+(x,+(y,z))
nF_+(+(x,y),z) -> nF_+(y,z)
nF_*(s(x),s(y)) -> nF_+(*(x,y),+(x,y))
nF_*(s(x),s(y)) -> nF_*(x,y)
nF_*(s(x),s(y)) -> nF_+(x,y)
nF_*(*(x,y),z) -> nF_*(x,*(y,z))
nF_*(*(x,y),z) -> nF_*(y,z)
nF_sum(cons(x,l)) -> nF_+(x,sum(l))
nF_sum(cons(x,l)) -> nF_sum(l)
nF_prod(cons(x,l)) -> nF_*(x,prod(l))
nF_prod(cons(x,l)) -> nF_prod(l)

-> Proof of termination for list_sum_prod_assoc_1_1:
-> -> Dependency pairs in cycle:
nF_prod(cons(x,l)) -> nF_prod(l)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for list_sum_prod_assoc_1_2:
-> -> Dependency pairs in cycle:
nF_sum(cons(x,l)) -> nF_sum(l)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for list_sum_prod_assoc_1_3:
-> -> Dependency pairs in cycle:
nF_*(s(x),s(y)) -> nF_*(x,y)
nF_*(*(x,y),z) -> nF_*(y,z)
nF_*(*(x,y),z) -> nF_*(x,*(y,z))

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for list_sum_prod_assoc_1_4:
-> -> Dependency pairs in cycle:
nF_+(s(x),s(y)) -> nF_+(x,y)
nF_+(+(x,y),z) -> nF_+(y,z)
nF_+(+(x,y),z) -> nF_+(x,+(y,z))

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.