Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z126)

The rewrite relation of the following TRS is considered.

a(b(a(x1))) → a(b(b(a(x1)))) (1)
b(b(b(x1))) → 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(a(b(a(x1)))) → b(a(b(b(a(x1))))) (3)
b(b(b(b(x1)))) → b(b(b(x1))) (4)
a(a(b(a(x1)))) → a(a(b(b(a(x1))))) (5)
a(b(b(b(x1)))) → a(b(b(x1))) (6)

1.1 Closure Under Flat Contexts

Using the flat contexts

{b(☐), a(☐)}

We obtain the transformed TRS
b(b(a(b(a(x1))))) → b(b(a(b(b(a(x1)))))) (7)
b(b(b(b(b(x1))))) → b(b(b(b(x1)))) (8)
b(a(a(b(a(x1))))) → b(a(a(b(b(a(x1)))))) (9)
b(a(b(b(b(x1))))) → b(a(b(b(x1)))) (10)
a(b(a(b(a(x1))))) → a(b(a(b(b(a(x1)))))) (11)
a(b(b(b(b(x1))))) → a(b(b(b(x1)))) (12)
a(a(a(b(a(x1))))) → a(a(a(b(b(a(x1)))))) (13)
a(a(b(b(b(x1))))) → a(a(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
a3(a1(a2(b3(a3(x1))))) → a3(a1(a0(b2(b3(a3(x1)))))) (15)
a3(a1(a2(b3(a1(x1))))) → a3(a1(a0(b2(b3(a1(x1)))))) (16)
a3(a1(a2(b1(a2(x1))))) → a3(a1(a0(b2(b1(a2(x1)))))) (17)
a3(a1(a2(b1(a0(x1))))) → a3(a1(a0(b2(b1(a0(x1)))))) (18)
a2(b1(a2(b3(a3(x1))))) → a2(b1(a0(b2(b3(a3(x1)))))) (19)
a2(b1(a2(b3(a1(x1))))) → a2(b1(a0(b2(b3(a1(x1)))))) (20)
a2(b1(a2(b1(a2(x1))))) → a2(b1(a0(b2(b1(a2(x1)))))) (21)
a2(b1(a2(b1(a0(x1))))) → a2(b1(a0(b2(b1(a0(x1)))))) (22)
b3(a1(a2(b3(a3(x1))))) → b3(a1(a0(b2(b3(a3(x1)))))) (23)
b3(a1(a2(b3(a1(x1))))) → b3(a1(a0(b2(b3(a1(x1)))))) (24)
b3(a1(a2(b1(a2(x1))))) → b3(a1(a0(b2(b1(a2(x1)))))) (25)
b3(a1(a2(b1(a0(x1))))) → b3(a1(a0(b2(b1(a0(x1)))))) (26)
b2(b1(a2(b3(a3(x1))))) → b2(b1(a0(b2(b3(a3(x1)))))) (27)
b2(b1(a2(b3(a1(x1))))) → b2(b1(a0(b2(b3(a1(x1)))))) (28)
b2(b1(a2(b1(a2(x1))))) → b2(b1(a0(b2(b1(a2(x1)))))) (29)
b2(b1(a2(b1(a0(x1))))) → b2(b1(a0(b2(b1(a0(x1)))))) (30)
a1(a0(b0(b2(b3(x1))))) → a1(a0(b2(b3(x1)))) (31)
a1(a0(b0(b2(b1(x1))))) → a1(a0(b2(b1(x1)))) (32)
a1(a0(b0(b0(b2(x1))))) → a1(a0(b0(b2(x1)))) (33)
a1(a0(b0(b0(b0(x1))))) → a1(a0(b0(b0(x1)))) (34)
a0(b0(b0(b2(b3(x1))))) → a0(b0(b2(b3(x1)))) (35)
a0(b0(b0(b2(b1(x1))))) → a0(b0(b2(b1(x1)))) (36)
a0(b0(b0(b0(b2(x1))))) → a0(b0(b0(b2(x1)))) (37)
a0(b0(b0(b0(b0(x1))))) → a0(b0(b0(b0(x1)))) (38)
b1(a0(b0(b2(b3(x1))))) → b1(a0(b2(b3(x1)))) (39)
b1(a0(b0(b2(b1(x1))))) → b1(a0(b2(b1(x1)))) (40)
b1(a0(b0(b0(b2(x1))))) → b1(a0(b0(b2(x1)))) (41)
b1(a0(b0(b0(b0(x1))))) → b1(a0(b0(b0(x1)))) (42)
b0(b0(b0(b2(b3(x1))))) → b0(b0(b2(b3(x1)))) (43)
b0(b0(b0(b2(b1(x1))))) → b0(b0(b2(b1(x1)))) (44)
b0(b0(b0(b0(b2(x1))))) → b0(b0(b0(b2(x1)))) (45)
b0(b0(b0(b0(b0(x1))))) → b0(b0(b0(b0(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 +
1
[b2(x1)] = x1 +
0
[b1(x1)] = x1 +
0
[b3(x1)] = x1 +
0
[a0(x1)] = x1 +
0
[a2(x1)] = x1 +
1
[a1(x1)] = x1 +
0
[a3(x1)] = x1 +
0
all of the following rules can be deleted.
a3(a1(a2(b3(a3(x1))))) → a3(a1(a0(b2(b3(a3(x1)))))) (15)
a3(a1(a2(b3(a1(x1))))) → a3(a1(a0(b2(b3(a1(x1)))))) (16)
a3(a1(a2(b1(a2(x1))))) → a3(a1(a0(b2(b1(a2(x1)))))) (17)
a3(a1(a2(b1(a0(x1))))) → a3(a1(a0(b2(b1(a0(x1)))))) (18)
a2(b1(a2(b3(a3(x1))))) → a2(b1(a0(b2(b3(a3(x1)))))) (19)
a2(b1(a2(b3(a1(x1))))) → a2(b1(a0(b2(b3(a1(x1)))))) (20)
a2(b1(a2(b1(a2(x1))))) → a2(b1(a0(b2(b1(a2(x1)))))) (21)
a2(b1(a2(b1(a0(x1))))) → a2(b1(a0(b2(b1(a0(x1)))))) (22)
b3(a1(a2(b3(a3(x1))))) → b3(a1(a0(b2(b3(a3(x1)))))) (23)
b3(a1(a2(b3(a1(x1))))) → b3(a1(a0(b2(b3(a1(x1)))))) (24)
b3(a1(a2(b1(a2(x1))))) → b3(a1(a0(b2(b1(a2(x1)))))) (25)
b3(a1(a2(b1(a0(x1))))) → b3(a1(a0(b2(b1(a0(x1)))))) (26)
b2(b1(a2(b3(a3(x1))))) → b2(b1(a0(b2(b3(a3(x1)))))) (27)
b2(b1(a2(b3(a1(x1))))) → b2(b1(a0(b2(b3(a1(x1)))))) (28)
b2(b1(a2(b1(a2(x1))))) → b2(b1(a0(b2(b1(a2(x1)))))) (29)
b2(b1(a2(b1(a0(x1))))) → b2(b1(a0(b2(b1(a0(x1)))))) (30)
a1(a0(b0(b2(b3(x1))))) → a1(a0(b2(b3(x1)))) (31)
a1(a0(b0(b2(b1(x1))))) → a1(a0(b2(b1(x1)))) (32)
a1(a0(b0(b0(b2(x1))))) → a1(a0(b0(b2(x1)))) (33)
a1(a0(b0(b0(b0(x1))))) → a1(a0(b0(b0(x1)))) (34)
a0(b0(b0(b2(b3(x1))))) → a0(b0(b2(b3(x1)))) (35)
a0(b0(b0(b2(b1(x1))))) → a0(b0(b2(b1(x1)))) (36)
a0(b0(b0(b0(b2(x1))))) → a0(b0(b0(b2(x1)))) (37)
a0(b0(b0(b0(b0(x1))))) → a0(b0(b0(b0(x1)))) (38)
b1(a0(b0(b2(b3(x1))))) → b1(a0(b2(b3(x1)))) (39)
b1(a0(b0(b2(b1(x1))))) → b1(a0(b2(b1(x1)))) (40)
b1(a0(b0(b0(b2(x1))))) → b1(a0(b0(b2(x1)))) (41)
b1(a0(b0(b0(b0(x1))))) → b1(a0(b0(b0(x1)))) (42)
b0(b0(b0(b2(b3(x1))))) → b0(b0(b2(b3(x1)))) (43)
b0(b0(b0(b2(b1(x1))))) → b0(b0(b2(b1(x1)))) (44)
b0(b0(b0(b0(b2(x1))))) → b0(b0(b0(b2(x1)))) (45)
b0(b0(b0(b0(b0(x1))))) → b0(b0(b0(b0(x1)))) (46)

1.1.1.1.1 R is empty

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