Certification Problem

Input (TPDB TRS_Standard/Various_04/14)

The rewrite relation of the following TRS is considered.

O(0) → 0 (1)
+(0,x) → x (2)
+(x,0) → x (3)
+(O(x),O(y)) → O(+(x,y)) (4)
+(O(x),I(y)) → I(+(x,y)) (5)
+(I(x),O(y)) → I(+(x,y)) (6)
+(I(x),I(y)) → O(+(+(x,y),I(0))) (7)
+(x,+(y,z)) → +(+(x,y),z) (8)
-(x,0) → x (9)
-(0,x) → 0 (10)
-(O(x),O(y)) → O(-(x,y)) (11)
-(O(x),I(y)) → I(-(-(x,y),I(1))) (12)
-(I(x),O(y)) → I(-(x,y)) (13)
-(I(x),I(y)) → O(-(x,y)) (14)
not(true) → false (15)
not(false) → true (16)
and(x,true) → x (17)
and(x,false) → false (18)
if(true,x,y) → x (19)
if(false,x,y) → y (20)
ge(O(x),O(y)) → ge(x,y) (21)
ge(O(x),I(y)) → not(ge(y,x)) (22)
ge(I(x),O(y)) → ge(x,y) (23)
ge(I(x),I(y)) → ge(x,y) (24)
ge(x,0) → true (25)
ge(0,O(x)) → ge(0,x) (26)
ge(0,I(x)) → false (27)
Log'(0) → 0 (28)
Log'(I(x)) → +(Log'(x),I(0)) (29)
Log'(O(x)) → if(ge(x,I(0)),+(Log'(x),I(0)),0) (30)
Log(x) → -(Log'(x),I(0)) (31)
Val(L(x)) → x (32)
Val(N(x,l,r)) → x (33)
Min(L(x)) → x (34)
Min(N(x,l,r)) → Min(l) (35)
Max(L(x)) → x (36)
Max(N(x,l,r)) → Max(r) (37)
BS(L(x)) → true (38)
BS(N(x,l,r)) → and(and(ge(x,Max(l)),ge(Min(r),x)),and(BS(l),BS(r))) (39)
Size(L(x)) → I(0) (40)
Size(N(x,l,r)) → +(+(Size(l),Size(r)),I(1)) (41)
WB(L(x)) → true (42)
WB(N(x,l,r)) → and(if(ge(Size(l),Size(r)),ge(I(0),-(Size(l),Size(r))),ge(I(0),-(Size(r),Size(l)))),and(WB(l),WB(r))) (43)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the linear polynomial interpretation over the naturals
[O(x1)] = 2 · x1
[0] = 0
[+(x1, x2)] = 1 · x1 + 2 · x2
[I(x1)] = 2 · x1
[-(x1, x2)] = 1 · x1 + 2 · x2
[1] = 0
[not(x1)] = 1 · x1
[true] = 0
[false] = 0
[and(x1, x2)] = 1 · x1 + 2 · x2
[if(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ge(x1, x2)] = 1 · x1 + 1 · x2
[Log'(x1)] = 1 · x1
[Log(x1)] = 2 + 1 · x1
[Val(x1)] = 2 · x1
[L(x1)] = 1 · x1
[N(x1, x2, x3)] = 2 · x1 + 1 · x2 + 1 · x3
[l] = 0
[r] = 0
[Min(x1)] = 2 · x1
[Max(x1)] = 1 · x1
[BS(x1)] = 2 · x1
[Size(x1)] = 1 · x1
[WB(x1)] = 1 · x1
all of the following rules can be deleted.
Log(x) → -(Log'(x),I(0)) (31)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[O(x1)] = 2 · x1
[0] = 0
[+(x1, x2)] = 1 · x1 + 1 · x2
[I(x1)] = 2 · x1
[-(x1, x2)] = 1 · x1 + 1 · x2
[1] = 0
[not(x1)] = 1 · x1
[true] = 0
[false] = 0
[and(x1, x2)] = 1 · x1 + 1 · x2
[if(x1, x2, x3)] = 1 · x1 + 1 · x2 + 1 · x3
[ge(x1, x2)] = 1 · x1 + 1 · x2
[Log'(x1)] = 2 · x1
[Val(x1)] = 1 + 2 · x1
[L(x1)] = 1 · x1
[N(x1, x2, x3)] = 2 · x1 + 1 · x2 + 1 · x3
[l] = 0
[r] = 0
[Min(x1)] = 1 · x1
[Max(x1)] = 1 · x1
[BS(x1)] = 2 · x1
[Size(x1)] = 1 · x1
[WB(x1)] = 1 · x1
all of the following rules can be deleted.
Val(L(x)) → x (32)
Val(N(x,l,r)) → x (33)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[O(x1)] = 2 · x1
[0] = 0
[+(x1, x2)] = 1 · x1 + 2 · x2
[I(x1)] = 2 · x1
[-(x1, x2)] = 1 · x1 + 2 · x2
[1] = 0
[not(x1)] = 2 · x1
[true] = 0
[false] = 0
[and(x1, x2)] = 1 · x1 + 2 · x2
[if(x1, x2, x3)] = 2 · x1 + 1 · x2 + 1 · x3
[ge(x1, x2)] = 1 · x1 + 1 · x2
[Log'(x1)] = 2 · x1
[Min(x1)] = 1 · x1
[L(x1)] = 1 · x1
[N(x1, x2, x3)] = 2 + 2 · x1 + 2 · x2 + 1 · x3
[l] = 0
[r] = 0
[Max(x1)] = 2 + 2 · x1
[BS(x1)] = 2 · x1
[Size(x1)] = 2 · x1
[WB(x1)] = 1 · x1
all of the following rules can be deleted.
Min(N(x,l,r)) → Min(l) (35)
Max(L(x)) → x (36)
Max(N(x,l,r)) → Max(r) (37)
BS(N(x,l,r)) → and(and(ge(x,Max(l)),ge(Min(r),x)),and(BS(l),BS(r))) (39)
Size(N(x,l,r)) → +(+(Size(l),Size(r)),I(1)) (41)
WB(N(x,l,r)) → and(if(ge(Size(l),Size(r)),ge(I(0),-(Size(l),Size(r))),ge(I(0),-(Size(r),Size(l)))),and(WB(l),WB(r))) (43)

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[O(x1)] = 2 · x1
[0] = 0
[+(x1, x2)] = 1 · x1 + 1 · x2
[I(x1)] = 2 · x1
[-(x1, x2)] = 1 · x1 + 2 · x2
[1] = 0
[not(x1)] = 1 · x1
[true] = 0
[false] = 0
[and(x1, x2)] = 2 + 1 · x1 + 2 · x2
[if(x1, x2, x3)] = 2 · x1 + 1 · x2 + 1 · x3
[ge(x1, x2)] = 1 · x1 + 2 · x2
[Log'(x1)] = 2 · x1
[Min(x1)] = 1 · x1
[L(x1)] = 1 · x1
[BS(x1)] = 2 + 2 · x1
[Size(x1)] = 1 · x1
[WB(x1)] = 2 + 2 · x1
all of the following rules can be deleted.
and(x,true) → x (17)
and(x,false) → false (18)
BS(L(x)) → true (38)
WB(L(x)) → true (42)

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[O(x1)] = 2 · x1
[0] = 0
[+(x1, x2)] = 1 · x1 + 2 · x2
[I(x1)] = 2 · x1
[-(x1, x2)] = 1 · x1 + 1 · x2
[1] = 0
[not(x1)] = 2 · x1
[true] = 0
[false] = 0
[if(x1, x2, x3)] = 1 · x1 + 1 · x2 + 2 · x3
[ge(x1, x2)] = 1 · x1 + 1 · x2
[Log'(x1)] = 2 · x1
[Min(x1)] = 1 + 1 · x1
[L(x1)] = 1 · x1
[Size(x1)] = 1 · x1
all of the following rules can be deleted.
Min(L(x)) → x (34)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[O(x1)] = 2 · x1
[0] = 0
[+(x1, x2)] = 1 · x1 + 2 · x2
[I(x1)] = 2 · x1
[-(x1, x2)] = 1 · x1 + 1 · x2
[1] = 0
[not(x1)] = 1 · x1
[true] = 0
[false] = 0
[if(x1, x2, x3)] = 1 · x1 + 1 · x2 + 2 · x3
[ge(x1, x2)] = 1 · x1 + 1 · x2
[Log'(x1)] = 1 · x1
[Size(x1)] = 1 + 2 · x1
[L(x1)] = 2 + 1 · x1
all of the following rules can be deleted.
Size(L(x)) → I(0) (40)

1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[O(x1)] = 2 · x1
[0] = 0
[+(x1, x2)] = 1 · x1 + 2 · x2
[I(x1)] = 2 · x1
[-(x1, x2)] = 1 · x1 + 2 · x2
[1] = 0
[not(x1)] = 1 · x1
[true] = 0
[false] = 0
[if(x1, x2, x3)] = 2 · x1 + 1 · x2 + 2 · x3
[ge(x1, x2)] = 1 · x1 + 2 · x2
[Log'(x1)] = 2 + 2 · x1
all of the following rules can be deleted.
Log'(0) → 0 (28)

1.1.1.1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
+#(O(x),O(y)) → O#(+(x,y)) (44)
+#(O(x),O(y)) → +#(x,y) (45)
+#(O(x),I(y)) → +#(x,y) (46)
+#(I(x),O(y)) → +#(x,y) (47)
+#(I(x),I(y)) → O#(+(+(x,y),I(0))) (48)
+#(I(x),I(y)) → +#(+(x,y),I(0)) (49)
+#(I(x),I(y)) → +#(x,y) (50)
+#(x,+(y,z)) → +#(+(x,y),z) (51)
+#(x,+(y,z)) → +#(x,y) (52)
-#(O(x),O(y)) → O#(-(x,y)) (53)
-#(O(x),O(y)) → -#(x,y) (54)
-#(O(x),I(y)) → -#(-(x,y),I(1)) (55)
-#(O(x),I(y)) → -#(x,y) (56)
-#(I(x),O(y)) → -#(x,y) (57)
-#(I(x),I(y)) → O#(-(x,y)) (58)
-#(I(x),I(y)) → -#(x,y) (59)
ge#(O(x),O(y)) → ge#(x,y) (60)
ge#(O(x),I(y)) → not#(ge(y,x)) (61)
ge#(O(x),I(y)) → ge#(y,x) (62)
ge#(I(x),O(y)) → ge#(x,y) (63)
ge#(I(x),I(y)) → ge#(x,y) (64)
ge#(0,O(x)) → ge#(0,x) (65)
Log'#(I(x)) → +#(Log'(x),I(0)) (66)
Log'#(I(x)) → Log'#(x) (67)
Log'#(O(x)) → if#(ge(x,I(0)),+(Log'(x),I(0)),0) (68)
Log'#(O(x)) → ge#(x,I(0)) (69)
Log'#(O(x)) → +#(Log'(x),I(0)) (70)
Log'#(O(x)) → Log'#(x) (71)

1.1.1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.