Certification Problem

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

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) # (8)
*(0(x),y) 0(*(x,y)) (9)
*(1(x),y) +(0(*(x,y)),y) (10)
sum(nil) 0(#) (11)
sum(cons(x,l)) +(x,sum(l)) (12)
prod(nil) 1(#) (13)
prod(cons(x,l)) *(x,prod(l)) (14)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
+#(0(x),0(y)) +#(x,y) (15)
+#(0(x),0(y)) 0#(+(x,y)) (16)
+#(0(x),1(y)) +#(x,y) (17)
+#(1(x),0(y)) +#(x,y) (18)
+#(1(x),1(y)) +#(x,y) (19)
+#(1(x),1(y)) +#(+(x,y),1(#)) (20)
+#(1(x),1(y)) 0#(+(+(x,y),1(#))) (21)
*#(0(x),y) *#(x,y) (22)
*#(0(x),y) 0#(*(x,y)) (23)
*#(1(x),y) *#(x,y) (24)
*#(1(x),y) 0#(*(x,y)) (25)
*#(1(x),y) +#(0(*(x,y)),y) (26)
sum#(nil) 0#(#) (27)
sum#(cons(x,l)) sum#(l) (28)
sum#(cons(x,l)) +#(x,sum(l)) (29)
prod#(cons(x,l)) prod#(l) (30)
prod#(cons(x,l)) *#(x,prod(l)) (31)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.