Certification Problem

Input (TPDB SRS_Relative/Mixed_relative_SRS/zr06)

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

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

and S is the following TRS.

b(x1) → 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(a(b(a(x1)))) → b(a(b(b(a(x1))))) (3)
a(a(b(a(x1)))) → a(a(b(b(a(x1))))) (4)
b(b(x1)) → b(b(b(b(x1)))) (5)
a(b(x1)) → a(b(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(a(a(b(a(x1))))) → b(a(a(b(b(a(x1)))))) (8)
a(b(a(b(a(x1))))) → a(b(a(b(b(a(x1)))))) (9)
a(a(a(b(a(x1))))) → a(a(a(b(b(a(x1)))))) (10)
b(b(b(x1))) → b(b(b(b(b(x1))))) (11)
b(a(b(x1))) → b(a(b(b(b(x1))))) (12)
a(b(b(x1))) → a(b(b(b(b(x1))))) (13)
a(a(b(x1))) → a(a(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
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(a2(b3(x1))) → a1(a0(b0(b2(b3(x1))))) (31)
a1(a2(b1(x1))) → a1(a0(b0(b2(b1(x1))))) (32)
a1(a0(b2(x1))) → a1(a0(b0(b0(b2(x1))))) (33)
a1(a0(b0(x1))) → a1(a0(b0(b0(b0(x1))))) (34)
a0(b2(b3(x1))) → a0(b0(b0(b2(b3(x1))))) (35)
a0(b2(b1(x1))) → a0(b0(b0(b2(b1(x1))))) (36)
a0(b0(b2(x1))) → a0(b0(b0(b0(b2(x1))))) (37)
a0(b0(b0(x1))) → a0(b0(b0(b0(b0(x1))))) (38)
b1(a2(b3(x1))) → b1(a0(b0(b2(b3(x1))))) (39)
b1(a2(b1(x1))) → b1(a0(b0(b2(b1(x1))))) (40)
b1(a0(b2(x1))) → b1(a0(b0(b0(b2(x1))))) (41)
b1(a0(b0(x1))) → b1(a0(b0(b0(b0(x1))))) (42)
b0(b2(b3(x1))) → b0(b0(b0(b2(b3(x1))))) (43)
b0(b2(b1(x1))) → b0(b0(b0(b2(b1(x1))))) (44)
b0(b0(b2(x1))) → b0(b0(b0(b0(b2(x1))))) (45)
b0(b0(b0(x1))) → b0(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 +
0
[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(a2(b3(x1))) → a1(a0(b0(b2(b3(x1))))) (31)
a1(a2(b1(x1))) → a1(a0(b0(b2(b1(x1))))) (32)
b1(a2(b3(x1))) → b1(a0(b0(b2(b3(x1))))) (39)
b1(a2(b1(x1))) → b1(a0(b0(b2(b1(x1))))) (40)

1.1.1.1.1 R is empty

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