Certification Problem

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

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)
*(x,+(y,z)) +(*(x,y),*(x,z)) (13)
app(nil,l) l (14)
app(cons(x,l1),l2) cons(x,app(l1,l2)) (15)
sum(nil) 0(#) (16)
sum(cons(x,l)) +(x,sum(l)) (17)
sum(app(l1,l2)) +(sum(l1),sum(l2)) (18)
prod(nil) 1(#) (19)
prod(cons(x,l)) *(x,prod(l)) (20)
prod(app(l1,l2)) *(prod(l1),prod(l2)) (21)

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) (22)
+#(0(x),0(y)) 0#(+(x,y)) (23)
+#(0(x),1(y)) +#(x,y) (24)
+#(1(x),0(y)) +#(x,y) (25)
+#(1(x),1(y)) +#(x,y) (26)
+#(1(x),1(y)) +#(+(x,y),1(#)) (27)
+#(1(x),1(y)) 0#(+(+(x,y),1(#))) (28)
+#(+(x,y),z) +#(y,z) (29)
+#(+(x,y),z) +#(x,+(y,z)) (30)
*#(0(x),y) *#(x,y) (31)
*#(0(x),y) 0#(*(x,y)) (32)
*#(1(x),y) *#(x,y) (33)
*#(1(x),y) 0#(*(x,y)) (34)
*#(1(x),y) +#(0(*(x,y)),y) (35)
*#(*(x,y),z) *#(y,z) (36)
*#(*(x,y),z) *#(x,*(y,z)) (37)
*#(x,+(y,z)) *#(x,z) (38)
*#(x,+(y,z)) *#(x,y) (39)
*#(x,+(y,z)) +#(*(x,y),*(x,z)) (40)
app#(cons(x,l1),l2) app#(l1,l2) (41)
sum#(nil) 0#(#) (42)
sum#(cons(x,l)) sum#(l) (43)
sum#(cons(x,l)) +#(x,sum(l)) (44)
sum#(app(l1,l2)) sum#(l2) (45)
sum#(app(l1,l2)) sum#(l1) (46)
sum#(app(l1,l2)) +#(sum(l1),sum(l2)) (47)
prod#(cons(x,l)) prod#(l) (48)
prod#(cons(x,l)) *#(x,prod(l)) (49)
prod#(app(l1,l2)) prod#(l2) (50)
prod#(app(l1,l2)) prod#(l1) (51)
prod#(app(l1,l2)) *#(prod(l1),prod(l2)) (52)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.