Certification Problem

Input (TPDB SRS_Relative/Zantema_06_relative/rel07)

The relative rewrite relation R/S is considered where R is the following TRS

a(d(x1)) → d(b(x1)) (1)
a(x1) → b(b(b(x1))) (2)
d(x1) → x1 (3)
a(x1) → x1 (4)
b(c(x1)) → c(d(d(x1))) (5)
a(c(x1)) → b(b(c(d(x1)))) (6)

and S is the following TRS.

b(d(b(x1))) → a(d(x1)) (7)
a(d(x1)) → b(d(b(x1))) (8)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Rule Removal

Using the matrix interpretations of dimension 3 with strict dimension 1 over the arctic semiring over the naturals
[d(x1)] =
0 -∞ 0
6 4 -∞
0 -∞ 0
· x1
[c(x1)] =
0 -∞ -∞
-6 -∞ -∞
5 -∞ 5
· x1
[b(x1)] =
0 -2 -5
0 0 -6
-∞ 0 0
· x1
[a(x1)] =
0 -2 0
1 0 -4
0 0 1
· x1
all of the following rules can be deleted.
a(c(x1)) → b(b(c(d(x1)))) (6)

1.1 Split

We split R in the relative problem D/R-D and R-D, where the rules D

a(d(x1)) → d(b(x1)) (1)
d(x1) → x1 (3)
a(x1) → x1 (4)
b(c(x1)) → c(d(d(x1))) (5)
are deleted.

1.1.1 Closure Under Flat Contexts

Using the flat contexts

{d(☐), c(☐), b(☐), a(☐)}

We obtain the transformed TRS
d(a(d(x1))) → d(d(b(x1))) (9)
d(d(x1)) → d(x1) (10)
d(a(x1)) → d(x1) (11)
d(b(c(x1))) → d(c(d(d(x1)))) (12)
c(a(d(x1))) → c(d(b(x1))) (13)
c(d(x1)) → c(x1) (14)
c(a(x1)) → c(x1) (15)
c(b(c(x1))) → c(c(d(d(x1)))) (16)
b(a(d(x1))) → b(d(b(x1))) (17)
b(d(x1)) → b(x1) (18)
b(a(x1)) → b(x1) (19)
b(b(c(x1))) → b(c(d(d(x1)))) (20)
a(a(d(x1))) → a(d(b(x1))) (21)
a(d(x1)) → a(x1) (22)
a(a(x1)) → a(x1) (23)
a(b(c(x1))) → a(c(d(d(x1)))) (24)
d(a(x1)) → d(b(b(b(x1)))) (25)
d(b(d(b(x1)))) → d(a(d(x1))) (26)
d(a(d(x1))) → d(b(d(b(x1)))) (27)
c(a(x1)) → c(b(b(b(x1)))) (28)
c(b(d(b(x1)))) → c(a(d(x1))) (29)
c(a(d(x1))) → c(b(d(b(x1)))) (30)
b(a(x1)) → b(b(b(b(x1)))) (31)
b(b(d(b(x1)))) → b(a(d(x1))) (32)
b(a(d(x1))) → b(b(d(b(x1)))) (33)
a(a(x1)) → a(b(b(b(x1)))) (34)
a(b(d(b(x1)))) → a(a(d(x1))) (35)
a(a(d(x1))) → a(b(d(b(x1)))) (36)

1.1.1.1 Closure Under Flat Contexts

Using the flat contexts

{d(☐), c(☐), b(☐), a(☐)}

We obtain the transformed TRS

There are 112 ruless (increase limit for explicit display).

1.1.1.1.1 Semantic Labeling

The following interpretations form a model of the rules.

As carrier we take the set {0,...,15}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 16):

[d(x1)] = 4x1 + 0
[c(x1)] = 4x1 + 1
[b(x1)] = 4x1 + 2
[a(x1)] = 4x1 + 3

We obtain the labeled TRS

There are 1792 ruless (increase limit for explicit display).

1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[d0(x1)] = x1 +
0
[d4(x1)] = x1 +
0
[d8(x1)] = x1 +
4
[d12(x1)] = x1 +
4
[d1(x1)] = x1 +
1
[d5(x1)] = x1 +
1
[d9(x1)] = x1 +
5
[d13(x1)] = x1 +
5
[d2(x1)] = x1 +
2
[d6(x1)] = x1 +
3
[d10(x1)] = x1 +
2
[d14(x1)] = x1 +
4
[d3(x1)] = x1 +
5
[d7(x1)] = x1 +
4
[d11(x1)] = x1 +
4
[d15(x1)] = x1 +
5
[c0(x1)] = x1 +
0
[c4(x1)] = x1 +
0
[c8(x1)] = x1 +
4
[c12(x1)] = x1 +
4
[c1(x1)] = x1 +
1
[c5(x1)] = x1 +
1
[c9(x1)] = x1 +
5
[c13(x1)] = x1 +
5
[c2(x1)] = x1 +
2
[c6(x1)] = x1 +
3
[c10(x1)] = x1 +
2
[c14(x1)] = x1 +
4
[c3(x1)] = x1 +
5
[c7(x1)] = x1 +
4
[c11(x1)] = x1 +
4
[c15(x1)] = x1 +
5
[b0(x1)] = x1 +
1
[b4(x1)] = x1 +
1
[b8(x1)] = x1 +
5
[b12(x1)] = x1 +
5
[b1(x1)] = x1 +
0
[b5(x1)] = x1 +
0
[b9(x1)] = x1 +
4
[b13(x1)] = x1 +
4
[b2(x1)] = x1 +
0
[b6(x1)] = x1 +
1
[b10(x1)] = x1 +
0
[b14(x1)] = x1 +
2
[b3(x1)] = x1 +
1
[b7(x1)] = x1 +
0
[b11(x1)] = x1 +
0
[b15(x1)] = x1 +
1
[a0(x1)] = x1 +
5
[a4(x1)] = x1 +
4
[a8(x1)] = x1 +
2
[a12(x1)] = x1 +
2
[a1(x1)] = x1 +
1
[a5(x1)] = x1 +
0
[a9(x1)] = x1 +
4
[a13(x1)] = x1 +
4
[a2(x1)] = x1 +
3
[a6(x1)] = x1 +
2
[a10(x1)] = x1 +
3
[a14(x1)] = x1 +
5
[a3(x1)] = x1 +
5
[a7(x1)] = x1 +
4
[a11(x1)] = x1 +
4
[a15(x1)] = x1 +
5
all of the following rules can be deleted.

There are 970 ruless (increase limit for explicit display).

1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the naturals
[d0(x1)] =
1
· x1 +
0
[d4(x1)] =
1
· x1 +
0
[d8(x1)] =
1
· x1 +
1
[d12(x1)] =
2
· x1 +
1
[d1(x1)] =
1
· x1 +
0
[d5(x1)] =
1
· x1 +
0
[d9(x1)] =
1
· x1 +
1
[d13(x1)] =
2
· x1 +
1
[d2(x1)] =
2
· x1 +
0
[d6(x1)] =
1
· x1 +
0
[d10(x1)] =
1
· x1 +
1
[d14(x1)] =
2
· x1 +
1
[d3(x1)] =
1
· x1 +
1
[d7(x1)] =
1
· x1 +
0
[d11(x1)] =
1
· x1 +
0
[d15(x1)] =
2
· x1 +
0
[c0(x1)] =
1
· x1 +
1
[c4(x1)] =
1
· x1 +
1
[c8(x1)] =
1
· x1 +
1
[c12(x1)] =
2
· x1 +
1
[c1(x1)] =
1
· x1 +
1
[c5(x1)] =
1
· x1 +
0
[c9(x1)] =
1
· x1 +
1
[c13(x1)] =
2
· x1 +
1
[c2(x1)] =
2
· x1 +
0
[c6(x1)] =
1
· x1 +
0
[c10(x1)] =
1
· x1 +
1
[c14(x1)] =
2
· x1 +
1
[c3(x1)] =
1
· x1 +
1
[c7(x1)] =
1
· x1 +
0
[c11(x1)] =
1
· x1 +
0
[c15(x1)] =
2
· x1 +
0
[b0(x1)] =
1
· x1 +
0
[b4(x1)] =
1
· x1 +
0
[b8(x1)] =
1
· x1 +
1
[b12(x1)] =
2
· x1 +
1
[b1(x1)] =
1
· x1 +
0
[b5(x1)] =
1
· x1 +
0
[b9(x1)] =
1
· x1 +
1
[b13(x1)] =
2
· x1 +
1
[b2(x1)] =
2
· x1 +
0
[b6(x1)] =
1
· x1 +
0
[b10(x1)] =
1
· x1 +
1
[b14(x1)] =
2
· x1 +
1
[b3(x1)] =
1
· x1 +
1
[b7(x1)] =
1
· x1 +
0
[b11(x1)] =
1
· x1 +
0
[b15(x1)] =
2
· x1 +
0
[a0(x1)] =
2
· x1 +
0
[a4(x1)] =
1
· x1 +
0
[a8(x1)] =
1
· x1 +
1
[a12(x1)] =
2
· x1 +
1
[a1(x1)] =
1
· x1 +
0
[a9(x1)] =
1
· x1 +
0
[a13(x1)] =
2
· x1 +
0
[a2(x1)] =
2
· x1 +
0
[a10(x1)] =
1
· x1 +
0
[a14(x1)] =
2
· x1 +
0
[a3(x1)] =
1
· x1 +
1
[a11(x1)] =
1
· x1 +
1
[a15(x1)] =
2
· x1 +
1
all of the following rules can be deleted.

There are 128 ruless (increase limit for explicit display).

1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[d0(x1)] = x1 +
2
[d4(x1)] = x1 +
0
[d8(x1)] = x1 +
0
[d12(x1)] = x1 +
0
[d1(x1)] = x1 +
2
[d5(x1)] = x1 +
2
[d9(x1)] = x1 +
12
[d13(x1)] = x1 +
12
[d2(x1)] = x1 +
14
[d6(x1)] = x1 +
14
[d10(x1)] = x1 +
2
[d14(x1)] = x1 +
2
[d3(x1)] = x1 +
14
[d7(x1)] = x1 +
2
[d11(x1)] = x1 +
2
[d15(x1)] = x1 +
2
[c0(x1)] = x1 +
1
[c4(x1)] = x1 +
0
[c8(x1)] = x1 +
14
[c12(x1)] = x1 +
14
[c1(x1)] = x1 +
0
[c5(x1)] = x1 +
4
[c9(x1)] = x1 +
14
[c13(x1)] = x1 +
14
[c2(x1)] = x1 +
14
[c6(x1)] = x1 +
6
[c10(x1)] = x1 +
0
[c14(x1)] = x1 +
0
[c3(x1)] = x1 +
14
[c7(x1)] = x1 +
0
[c11(x1)] = x1 +
0
[c15(x1)] = x1 +
0
[b0(x1)] = x1 +
2
[b4(x1)] = x1 +
0
[b8(x1)] = x1 +
0
[b12(x1)] = x1 +
0
[b1(x1)] = x1 +
2
[b5(x1)] = x1 +
2
[b9(x1)] = x1 +
12
[b13(x1)] = x1 +
12
[b2(x1)] = x1 +
12
[b6(x1)] = x1 +
12
[b10(x1)] = x1 +
0
[b14(x1)] = x1 +
0
[b3(x1)] = x1 +
12
[b7(x1)] = x1 +
0
[b11(x1)] = x1 +
0
[b15(x1)] = x1 +
0
[a0(x1)] = x1 +
14
[a4(x1)] = x1 +
14
[a8(x1)] = x1 +
0
[a12(x1)] = x1 +
0
[a1(x1)] = x1 +
0
[a9(x1)] = x1 +
0
[a13(x1)] = x1 +
0
[a2(x1)] = x1 +
0
[a10(x1)] = x1 +
12
[a14(x1)] = x1 +
12
[a3(x1)] = x1 +
0
[a11(x1)] = x1 +
0
[a15(x1)] = x1 +
0
all of the following rules can be deleted.

There are 166 ruless (increase limit for explicit display).

1.1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.

1.1.2 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the naturals
[d(x1)] =
1 1
0 2
· x1 +
1
0
[b(x1)] =
1 0
0 1
· x1 +
0
1
[a(x1)] =
1 0
0 1
· x1 +
1
3
all of the following rules can be deleted.
a(x1) → b(b(b(x1))) (2)

1.1.2.1 R is empty

There are no rules in the TRS. Hence, it is terminating.