Certification Problem

Input (TPDB TRS_Standard/CiME_04/ternary-hard)

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)
+(0(x),j(y)) j(+(x,y)) (7)
+(j(x),0(y)) j(+(x,y)) (8)
+(1(x),1(y)) j(+(+(x,y),1(#))) (9)
+(j(x),j(y)) 1(+(+(x,y),j(#))) (10)
+(1(x),j(y)) 0(+(x,y)) (11)
+(j(x),1(y)) 0(+(x,y)) (12)
+(+(x,y),z) +(x,+(y,z)) (13)
opp(#) # (14)
opp(0(x)) 0(opp(x)) (15)
opp(1(x)) j(opp(x)) (16)
opp(j(x)) 1(opp(x)) (17)
-(x,y) +(x,opp(y)) (18)
*(#,x) # (19)
*(0(x),y) 0(*(x,y)) (20)
*(1(x),y) +(0(*(x,y)),y) (21)
*(j(x),y) -(0(*(x,y)),y) (22)
*(*(x,y),z) *(x,*(y,z)) (23)
*(+(x,y),z) +(*(x,z),*(y,z)) (24)
*(x,+(y,z)) +(*(x,y),*(x,z)) (25)

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.
+#(+(x,y),z) +#(x,+(y,z)) (26)
*#(1(x),y) 0#(*(x,y)) (27)
+#(0(x),0(y)) 0#(+(x,y)) (28)
-#(x,y) +#(x,opp(y)) (29)
-#(x,y) opp#(y) (30)
+#(1(x),j(y)) 0#(+(x,y)) (31)
+#(j(x),1(y)) 0#(+(x,y)) (32)
*#(+(x,y),z) *#(x,z) (33)
*#(*(x,y),z) *#(x,*(y,z)) (34)
*#(j(x),y) -#(0(*(x,y)),y) (35)
+#(0(x),1(y)) +#(x,y) (36)
*#(*(x,y),z) *#(y,z) (37)
opp#(1(x)) opp#(x) (38)
+#(j(x),1(y)) +#(x,y) (39)
*#(1(x),y) *#(x,y) (40)
*#(j(x),y) 0#(*(x,y)) (41)
+#(0(x),j(y)) +#(x,y) (42)
+#(1(x),j(y)) +#(x,y) (43)
*#(+(x,y),z) *#(y,z) (44)
opp#(0(x)) 0#(opp(x)) (45)
+#(1(x),1(y)) +#(x,y) (46)
*#(1(x),y) +#(0(*(x,y)),y) (47)
+#(j(x),j(y)) +#(x,y) (48)
opp#(0(x)) opp#(x) (49)
opp#(j(x)) opp#(x) (50)
*#(x,+(y,z)) *#(x,z) (51)
+#(j(x),0(y)) +#(x,y) (52)
*#(0(x),y) *#(x,y) (53)
*#(j(x),y) *#(x,y) (54)
+#(0(x),0(y)) +#(x,y) (55)
+#(j(x),j(y)) +#(+(x,y),j(#)) (56)
*#(x,+(y,z)) *#(x,y) (57)
+#(+(x,y),z) +#(y,z) (58)
+#(1(x),0(y)) +#(x,y) (59)
*#(+(x,y),z) +#(*(x,z),*(y,z)) (60)
*#(x,+(y,z)) +#(*(x,y),*(x,z)) (61)
+#(1(x),1(y)) +#(+(x,y),1(#)) (62)
*#(0(x),y) 0#(*(x,y)) (63)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.