Certification Problem

Input (TPDB SRS_Relative/Waldmann_06_relative/r9)

The rewrite relation of the following TRS is considered.

b(a(b(x1))) → b(a(a(a(b(x1))))) (1)
a(a(a(x1))) → b(b(b(b(x1)))) (2)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

{b(☐), a(☐)}

We obtain the transformed TRS
b(b(a(b(x1)))) → b(b(a(a(a(b(x1)))))) (3)
b(a(a(a(x1)))) → b(b(b(b(b(x1))))) (4)
a(b(a(b(x1)))) → a(b(a(a(a(b(x1)))))) (5)
a(a(a(a(x1)))) → a(b(b(b(b(x1))))) (6)

1.1 Closure Under Flat Contexts

Using the flat contexts

{b(☐), a(☐)}

We obtain the transformed TRS
b(b(b(a(b(x1))))) → b(b(b(a(a(a(b(x1))))))) (7)
b(b(a(a(a(x1))))) → b(b(b(b(b(b(x1)))))) (8)
b(a(b(a(b(x1))))) → b(a(b(a(a(a(b(x1))))))) (9)
b(a(a(a(a(x1))))) → b(a(b(b(b(b(x1)))))) (10)
a(b(b(a(b(x1))))) → a(b(b(a(a(a(b(x1))))))) (11)
a(b(a(a(a(x1))))) → a(b(b(b(b(b(x1)))))) (12)
a(a(b(a(b(x1))))) → a(a(b(a(a(a(b(x1))))))) (13)
a(a(a(a(a(x1))))) → a(a(b(b(b(b(x1)))))) (14)

1.1.1 Semantic Labeling

The following interpretations form a model of the rules.

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

[b(x1)] = 2x1 + 0
[a(x1)] = 2x1 + 1

We obtain the labeled TRS
b0(b2(b1(a0(b0(x1))))) → b0(b2(b3(a3(a1(a0(b0(x1))))))) (15)
b0(b2(b1(a0(b2(x1))))) → b0(b2(b3(a3(a1(a0(b2(x1))))))) (16)
b0(b2(b1(a2(b1(x1))))) → b0(b2(b3(a3(a1(a2(b1(x1))))))) (17)
b0(b2(b1(a2(b3(x1))))) → b0(b2(b3(a3(a1(a2(b3(x1))))))) (18)
b1(a2(b1(a0(b0(x1))))) → b1(a2(b3(a3(a1(a0(b0(x1))))))) (19)
b1(a2(b1(a0(b2(x1))))) → b1(a2(b3(a3(a1(a0(b2(x1))))))) (20)
b1(a2(b1(a2(b1(x1))))) → b1(a2(b3(a3(a1(a2(b1(x1))))))) (21)
b1(a2(b1(a2(b3(x1))))) → b1(a2(b3(a3(a1(a2(b3(x1))))))) (22)
a0(b2(b1(a0(b0(x1))))) → a0(b2(b3(a3(a1(a0(b0(x1))))))) (23)
a0(b2(b1(a0(b2(x1))))) → a0(b2(b3(a3(a1(a0(b2(x1))))))) (24)
a0(b2(b1(a2(b1(x1))))) → a0(b2(b3(a3(a1(a2(b1(x1))))))) (25)
a0(b2(b1(a2(b3(x1))))) → a0(b2(b3(a3(a1(a2(b3(x1))))))) (26)
a1(a2(b1(a0(b0(x1))))) → a1(a2(b3(a3(a1(a0(b0(x1))))))) (27)
a1(a2(b1(a0(b2(x1))))) → a1(a2(b3(a3(a1(a0(b2(x1))))))) (28)
a1(a2(b1(a2(b1(x1))))) → a1(a2(b3(a3(a1(a2(b1(x1))))))) (29)
a1(a2(b1(a2(b3(x1))))) → a1(a2(b3(a3(a1(a2(b3(x1))))))) (30)
b2(b3(a3(a1(a0(x1))))) → b0(b0(b0(b0(b0(b0(x1)))))) (31)
b2(b3(a3(a1(a2(x1))))) → b0(b0(b0(b0(b0(b2(x1)))))) (32)
b2(b3(a3(a3(a1(x1))))) → b0(b0(b0(b0(b2(b1(x1)))))) (33)
b2(b3(a3(a3(a3(x1))))) → b0(b0(b0(b0(b2(b3(x1)))))) (34)
b3(a3(a3(a1(a0(x1))))) → b1(a0(b0(b0(b0(b0(x1)))))) (35)
b3(a3(a3(a1(a2(x1))))) → b1(a0(b0(b0(b0(b2(x1)))))) (36)
b3(a3(a3(a3(a1(x1))))) → b1(a0(b0(b0(b2(b1(x1)))))) (37)
b3(a3(a3(a3(a3(x1))))) → b1(a0(b0(b0(b2(b3(x1)))))) (38)
a2(b3(a3(a1(a0(x1))))) → a0(b0(b0(b0(b0(b0(x1)))))) (39)
a2(b3(a3(a1(a2(x1))))) → a0(b0(b0(b0(b0(b2(x1)))))) (40)
a2(b3(a3(a3(a1(x1))))) → a0(b0(b0(b0(b2(b1(x1)))))) (41)
a2(b3(a3(a3(a3(x1))))) → a0(b0(b0(b0(b2(b3(x1)))))) (42)
a3(a3(a3(a1(a0(x1))))) → a1(a0(b0(b0(b0(b0(x1)))))) (43)
a3(a3(a3(a1(a2(x1))))) → a1(a0(b0(b0(b0(b2(x1)))))) (44)
a3(a3(a3(a3(a1(x1))))) → a1(a0(b0(b0(b2(b1(x1)))))) (45)
a3(a3(a3(a3(a3(x1))))) → a1(a0(b0(b0(b2(b3(x1)))))) (46)

1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[b0(x1)] = x1 +
0
[b2(x1)] = x1 +
0
[b1(x1)] = x1 +
4
[b3(x1)] = x1 +
0
[a0(x1)] = x1 +
0
[a2(x1)] = x1 +
1
[a1(x1)] = x1 +
0
[a3(x1)] = x1 +
3
all of the following rules can be deleted.
b0(b2(b1(a0(b0(x1))))) → b0(b2(b3(a3(a1(a0(b0(x1))))))) (15)
b0(b2(b1(a0(b2(x1))))) → b0(b2(b3(a3(a1(a0(b2(x1))))))) (16)
b0(b2(b1(a2(b1(x1))))) → b0(b2(b3(a3(a1(a2(b1(x1))))))) (17)
b0(b2(b1(a2(b3(x1))))) → b0(b2(b3(a3(a1(a2(b3(x1))))))) (18)
b1(a2(b1(a0(b0(x1))))) → b1(a2(b3(a3(a1(a0(b0(x1))))))) (19)
b1(a2(b1(a0(b2(x1))))) → b1(a2(b3(a3(a1(a0(b2(x1))))))) (20)
b1(a2(b1(a2(b1(x1))))) → b1(a2(b3(a3(a1(a2(b1(x1))))))) (21)
b1(a2(b1(a2(b3(x1))))) → b1(a2(b3(a3(a1(a2(b3(x1))))))) (22)
a0(b2(b1(a0(b0(x1))))) → a0(b2(b3(a3(a1(a0(b0(x1))))))) (23)
a0(b2(b1(a0(b2(x1))))) → a0(b2(b3(a3(a1(a0(b2(x1))))))) (24)
a0(b2(b1(a2(b1(x1))))) → a0(b2(b3(a3(a1(a2(b1(x1))))))) (25)
a0(b2(b1(a2(b3(x1))))) → a0(b2(b3(a3(a1(a2(b3(x1))))))) (26)
a1(a2(b1(a0(b0(x1))))) → a1(a2(b3(a3(a1(a0(b0(x1))))))) (27)
a1(a2(b1(a0(b2(x1))))) → a1(a2(b3(a3(a1(a0(b2(x1))))))) (28)
a1(a2(b1(a2(b1(x1))))) → a1(a2(b3(a3(a1(a2(b1(x1))))))) (29)
a1(a2(b1(a2(b3(x1))))) → a1(a2(b3(a3(a1(a2(b3(x1))))))) (30)
b2(b3(a3(a1(a0(x1))))) → b0(b0(b0(b0(b0(b0(x1)))))) (31)
b2(b3(a3(a1(a2(x1))))) → b0(b0(b0(b0(b0(b2(x1)))))) (32)
b2(b3(a3(a3(a1(x1))))) → b0(b0(b0(b0(b2(b1(x1)))))) (33)
b2(b3(a3(a3(a3(x1))))) → b0(b0(b0(b0(b2(b3(x1)))))) (34)
b3(a3(a3(a1(a0(x1))))) → b1(a0(b0(b0(b0(b0(x1)))))) (35)
b3(a3(a3(a1(a2(x1))))) → b1(a0(b0(b0(b0(b2(x1)))))) (36)
b3(a3(a3(a3(a1(x1))))) → b1(a0(b0(b0(b2(b1(x1)))))) (37)
b3(a3(a3(a3(a3(x1))))) → b1(a0(b0(b0(b2(b3(x1)))))) (38)
a2(b3(a3(a1(a0(x1))))) → a0(b0(b0(b0(b0(b0(x1)))))) (39)
a2(b3(a3(a1(a2(x1))))) → a0(b0(b0(b0(b0(b2(x1)))))) (40)
a2(b3(a3(a3(a1(x1))))) → a0(b0(b0(b0(b2(b1(x1)))))) (41)
a2(b3(a3(a3(a3(x1))))) → a0(b0(b0(b0(b2(b3(x1)))))) (42)
a3(a3(a3(a1(a0(x1))))) → a1(a0(b0(b0(b0(b0(x1)))))) (43)
a3(a3(a3(a1(a2(x1))))) → a1(a0(b0(b0(b0(b2(x1)))))) (44)
a3(a3(a3(a3(a1(x1))))) → a1(a0(b0(b0(b2(b1(x1)))))) (45)
a3(a3(a3(a3(a3(x1))))) → a1(a0(b0(b0(b2(b3(x1)))))) (46)

1.1.1.1.1 R is empty

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