YES
(VAR x y z l l1 l2)
(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))
app(nil,l) -> l
app(cons(x,l1),l2) -> cons(x,app(l1,l2))
sum(nil) -> 0
sum(cons(x,l)) -> +(x,sum(l))
sum(app(l1,l2)) -> +(sum(l1),sum(l2))
prod(nil) -> s(0)
prod(cons(x,l)) -> *(x,prod(l))
prod(app(l1,l2)) -> *(prod(l1),prod(l2))
)

Proving termination of rewriting for list_sum_prod_assoc_append:

-> 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_app(cons(x,l1),l2) -> nF_app(l1,l2)
nF_sum(cons(x,l)) -> nF_+(x,sum(l))
nF_sum(cons(x,l)) -> nF_sum(l)
nF_sum(app(l1,l2)) -> nF_+(sum(l1),sum(l2))
nF_sum(app(l1,l2)) -> nF_sum(l1)
nF_sum(app(l1,l2)) -> nF_sum(l2)
nF_prod(cons(x,l)) -> nF_*(x,prod(l))
nF_prod(cons(x,l)) -> nF_prod(l)
nF_prod(app(l1,l2)) -> nF_*(prod(l1),prod(l2))
nF_prod(app(l1,l2)) -> nF_prod(l1)
nF_prod(app(l1,l2)) -> nF_prod(l2)

-> Proof of termination for list_sum_prod_assoc_append_1_1:
-> -> Dependency pairs in cycle:
nF_prod(cons(x,l)) -> nF_prod(l)
nF_prod(app(l1,l2)) -> nF_prod(l2)
nF_prod(app(l1,l2)) -> nF_prod(l1)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for list_sum_prod_assoc_append_1_2:
-> -> Dependency pairs in cycle:
nF_sum(cons(x,l)) -> nF_sum(l)
nF_sum(app(l1,l2)) -> nF_sum(l2)
nF_sum(app(l1,l2)) -> nF_sum(l1)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for list_sum_prod_assoc_append_1_3:
-> -> Dependency pairs in cycle:
nF_app(cons(x,l1),l2) -> nF_app(l1,l2)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for list_sum_prod_assoc_append_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.

-> Proof of termination for list_sum_prod_assoc_append_1_5:
-> -> 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.