Certification Problem

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

The rewrite relation of the following TRS is considered.

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

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.
sum#(nil) 0#(#) (17)
*#(*(x,y),z) *#(x,*(y,z)) (18)
*#(0(x),y) 0#(*(x,y)) (19)
sum#(cons(x,l)) sum#(l) (20)
+#(1(x),1(y)) +#(+(x,y),1(#)) (21)
+#(1(x),1(y)) +#(x,y) (22)
*#(0(x),y) *#(x,y) (23)
+#(0(x),0(y)) 0#(+(x,y)) (24)
*#(*(x,y),z) *#(y,z) (25)
+#(1(x),1(y)) 0#(+(+(x,y),1(#))) (26)
*#(1(x),y) *#(x,y) (27)
prod#(cons(x,l)) prod#(l) (28)
+#(+(x,y),z) +#(y,z) (29)
+#(0(x),0(y)) +#(x,y) (30)
prod#(cons(x,l)) *#(x,prod(l)) (31)
*#(1(x),y) +#(0(*(x,y)),y) (32)
+#(1(x),0(y)) +#(x,y) (33)
sum#(cons(x,l)) +#(x,sum(l)) (34)
+#(0(x),1(y)) +#(x,y) (35)
*#(1(x),y) 0#(*(x,y)) (36)
+#(+(x,y),z) +#(x,+(y,z)) (37)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.