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

The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting.

Proving termination of innermost rewriting for list_sum_prod:

-> Dependency pairs:
nF_+(s(x),s(y)) -> nF_+(x,y)
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_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_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_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_1_3:
-> -> Dependency pairs in cycle:
nF_*(s(x),s(y)) -> nF_*(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for list_sum_prod_1_4:
-> -> Dependency pairs in cycle:
nF_+(s(x),s(y)) -> nF_+(x,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.