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

Proving termination of rewriting for list_sum_prod_bin:

-> Dependency pairs:
nF_+(0(x),0(y)) -> nF_0(+(x,y))
nF_+(0(x),0(y)) -> nF_+(x,y)
nF_+(0(x),1(y)) -> nF_+(x,y)
nF_+(1(x),0(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_0(+(+(x,y),1(#)))
nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#))
nF_+(1(x),1(y)) -> nF_+(x,y)
nF_*(0(x),y) -> nF_0(*(x,y))
nF_*(0(x),y) -> nF_*(x,y)
nF_*(1(x),y) -> nF_+(0(*(x,y)),y)
nF_*(1(x),y) -> nF_0(*(x,y))
nF_*(1(x),y) -> nF_*(x,y)
nF_sum(nil) -> nF_0(#)
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_bin_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_bin_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_bin_1_3:
-> -> Dependency pairs in cycle:
nF_*(0(x),y) -> nF_*(x,y)
nF_*(1(x),y) -> nF_*(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for list_sum_prod_bin_1_4:
-> -> Dependency pairs in cycle:
nF_+(0(x),0(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#))
nF_+(1(x),0(y)) -> nF_+(x,y)
nF_+(0(x),1(y)) -> nF_+(x,y)

UsableRules:
0(#) -> #
+(x,#) -> x
+(#,x) -> x
+(0(x),0(y)) -> 0(+(x,y))
+(0(x),1(y)) -> 1(+(x,y))
+(1(x),0(y)) -> 1(+(x,y))
+(1(x),1(y)) -> 0(+(+(x,y),1(#)))

Polynomial Interpretation:

[0](X) = X
[#] = 0
[+](X1,X2) = X1 + X2
[1](X) = X + 1
[*](X1,X2) = 0
[sum](X) = 0
[nil] = 0
[cons](X1,X2) = 0
[prod](X) = 0
[nF_+](X1,X2) = X2

TIME: 4.8689e-2

-> -> Dependency pairs in cycle:
nF_+(0(x),0(y)) -> nF_+(x,y)
nF_+(1(x),0(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_+(+(x,y),1(#))

UsableRules:
0(#) -> #
+(x,#) -> x
+(#,x) -> x
+(0(x),0(y)) -> 0(+(x,y))
+(0(x),1(y)) -> 1(+(x,y))
+(1(x),0(y)) -> 1(+(x,y))
+(1(x),1(y)) -> 0(+(+(x,y),1(#)))

Polynomial Interpretation:

[0](X) = X
[#] = 0
[+](X1,X2) = X1 + X2
[1](X) = X + 1
[*](X1,X2) = 0
[sum](X) = 0
[nil] = 0
[cons](X1,X2) = 0
[prod](X) = 0
[nF_+](X1,X2) = X1 + X2

TIME: 4.8436e-2

-> -> Dependency pairs in cycle:
nF_+(0(x),0(y)) -> nF_+(x,y)
nF_+(1(x),1(y)) -> nF_+(x,y)
nF_+(1(x),0(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.