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.