Certification Problem

Input (TPDB TRS_Standard/CiME_04/tree)

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,#) x (9)
-(#,x) # (10)
-(0(x),0(y)) 0(-(x,y)) (11)
-(0(x),1(y)) 1(-(-(x,y),1(#))) (12)
-(1(x),0(y)) 1(-(x,y)) (13)
-(1(x),1(y)) 0(-(x,y)) (14)
not(false) true (15)
not(true) false (16)
and(x,true) x (17)
and(x,false) false (18)
if(true,x,y) x (19)
if(false,x,y) y (20)
ge(0(x),0(y)) ge(x,y) (21)
ge(0(x),1(y)) not(ge(y,x)) (22)
ge(1(x),0(y)) ge(x,y) (23)
ge(1(x),1(y)) ge(x,y) (24)
ge(x,#) true (25)
ge(#,1(x)) false (26)
ge(#,0(x)) ge(#,x) (27)
val(l(x)) x (28)
val(n(x,y,z)) x (29)
min(l(x)) x (30)
min(n(x,y,z)) min(y) (31)
max(l(x)) x (32)
max(n(x,y,z)) max(z) (33)
bs(l(x)) true (34)
bs(n(x,y,z)) and(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z))) (35)
size(l(x)) 1(#) (36)
size(n(x,y,z)) +(+(size(x),size(y)),1(#)) (37)
wb(l(x)) true (38)
wb(n(x,y,z)) and(if(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))),ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z))) (39)

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) (40)
+#(0(x),0(y)) 0#(+(x,y)) (41)
+#(0(x),1(y)) +#(x,y) (42)
+#(1(x),0(y)) +#(x,y) (43)
+#(1(x),1(y)) +#(x,y) (44)
+#(1(x),1(y)) +#(+(x,y),1(#)) (45)
+#(1(x),1(y)) 0#(+(+(x,y),1(#))) (46)
+#(x,+(y,z)) +#(x,y) (47)
+#(x,+(y,z)) +#(+(x,y),z) (48)
-#(0(x),0(y)) -#(x,y) (49)
-#(0(x),0(y)) 0#(-(x,y)) (50)
-#(0(x),1(y)) -#(x,y) (51)
-#(0(x),1(y)) -#(-(x,y),1(#)) (52)
-#(1(x),0(y)) -#(x,y) (53)
-#(1(x),1(y)) -#(x,y) (54)
-#(1(x),1(y)) 0#(-(x,y)) (55)
ge#(0(x),0(y)) ge#(x,y) (56)
ge#(0(x),1(y)) ge#(y,x) (57)
ge#(0(x),1(y)) not#(ge(y,x)) (58)
ge#(1(x),0(y)) ge#(x,y) (59)
ge#(1(x),1(y)) ge#(x,y) (60)
ge#(#,0(x)) ge#(#,x) (61)
min#(n(x,y,z)) min#(y) (62)
max#(n(x,y,z)) max#(z) (63)
bs#(n(x,y,z)) bs#(z) (64)
bs#(n(x,y,z)) bs#(y) (65)
bs#(n(x,y,z)) and#(bs(y),bs(z)) (66)
bs#(n(x,y,z)) min#(z) (67)
bs#(n(x,y,z)) ge#(min(z),x) (68)
bs#(n(x,y,z)) max#(y) (69)
bs#(n(x,y,z)) ge#(x,max(y)) (70)
bs#(n(x,y,z)) and#(ge(x,max(y)),ge(min(z),x)) (71)
bs#(n(x,y,z)) and#(and(ge(x,max(y)),ge(min(z),x)),and(bs(y),bs(z))) (72)
size#(n(x,y,z)) size#(y) (73)
size#(n(x,y,z)) size#(x) (74)
size#(n(x,y,z)) +#(size(x),size(y)) (75)
size#(n(x,y,z)) +#(+(size(x),size(y)),1(#)) (76)
wb#(n(x,y,z)) wb#(z) (77)
wb#(n(x,y,z)) wb#(y) (78)
wb#(n(x,y,z)) and#(wb(y),wb(z)) (79)
wb#(n(x,y,z)) -#(size(z),size(y)) (80)
wb#(n(x,y,z)) ge#(1(#),-(size(z),size(y))) (81)
wb#(n(x,y,z)) -#(size(y),size(z)) (82)
wb#(n(x,y,z)) ge#(1(#),-(size(y),size(z))) (83)
wb#(n(x,y,z)) size#(z) (84)
wb#(n(x,y,z)) size#(y) (85)
wb#(n(x,y,z)) ge#(size(y),size(z)) (86)
wb#(n(x,y,z)) if#(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))),ge(1(#),-(size(z),size(y)))) (87)
wb#(n(x,y,z)) and#(if(ge(size(y),size(z)),ge(1(#),-(size(y),size(z))),ge(1(#),-(size(z),size(y)))),and(wb(y),wb(z))) (88)

1.1 Dependency Graph Processor

The dependency pairs are split into 9 components.