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 NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

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

1.1 Dependency Graph Processor

The dependency pairs are split into 9 components.