Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z024)

The rewrite relation of the following TRS is considered.

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

1.1.1.1.1 R is empty

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