Certification Problem

Input (TPDB TRS_Standard/CiME_04/list-sum-prod-assoc)

The rewrite relation of the following TRS is considered.

+(x,0) x (1)
+(0,x) x (2)
+(s(x),s(y)) s(s(+(x,y))) (3)
+(+(x,y),z) +(x,+(y,z)) (4)
*(x,0) 0 (5)
*(0,x) 0 (6)
*(s(x),s(y)) s(+(*(x,y),+(x,y))) (7)
*(*(x,y),z) *(x,*(y,z)) (8)
sum(nil) 0 (9)
sum(cons(x,l)) +(x,sum(l)) (10)
prod(nil) s(0) (11)
prod(cons(x,l)) *(x,prod(l)) (12)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
prod#(cons(x,l)) prod#(l) (13)
sum#(cons(x,l)) +#(x,sum(l)) (14)
*#(*(x,y),z) *#(x,*(y,z)) (15)
+#(+(x,y),z) +#(x,+(y,z)) (16)
+#(+(x,y),z) +#(y,z) (17)
sum#(cons(x,l)) sum#(l) (18)
*#(*(x,y),z) *#(y,z) (19)
*#(s(x),s(y)) +#(x,y) (20)
*#(s(x),s(y)) +#(*(x,y),+(x,y)) (21)
prod#(cons(x,l)) *#(x,prod(l)) (22)
+#(s(x),s(y)) +#(x,y) (23)
*#(s(x),s(y)) *#(x,y) (24)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.