Certification Problem

Input (TPDB SRS_Relative/Mixed_relative_SRS/zr10)

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

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

and S is the following TRS.

a(x1) → a(a(a(x1))) (3)
b(x1) → b(b(b(x1))) (4)

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))))) (5)
b(b(a(b(x1)))) → b(b(a(a(b(x1))))) (6)
a(a(b(a(x1)))) → a(a(b(b(a(x1))))) (7)
a(b(a(b(x1)))) → a(b(a(a(b(x1))))) (8)
b(a(x1)) → b(a(a(a(x1)))) (9)
b(b(x1)) → b(b(b(b(x1)))) (10)
a(a(x1)) → a(a(a(a(x1)))) (11)
a(b(x1)) → a(b(b(b(x1)))) (12)

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)))))) (13)
b(b(b(a(b(x1))))) → b(b(b(a(a(b(x1)))))) (14)
b(a(a(b(a(x1))))) → b(a(a(b(b(a(x1)))))) (15)
b(a(b(a(b(x1))))) → b(a(b(a(a(b(x1)))))) (16)
a(b(a(b(a(x1))))) → a(b(a(b(b(a(x1)))))) (17)
a(b(b(a(b(x1))))) → a(b(b(a(a(b(x1)))))) (18)
a(a(a(b(a(x1))))) → a(a(a(b(b(a(x1)))))) (19)
a(a(b(a(b(x1))))) → a(a(b(a(a(b(x1)))))) (20)
b(b(a(x1))) → b(b(a(a(a(x1))))) (21)
b(b(b(x1))) → b(b(b(b(b(x1))))) (22)
b(a(a(x1))) → b(a(a(a(a(x1))))) (23)
b(a(b(x1))) → b(a(b(b(b(x1))))) (24)
a(b(a(x1))) → a(b(a(a(a(x1))))) (25)
a(b(b(x1))) → a(b(b(b(b(x1))))) (26)
a(a(a(x1))) → a(a(a(a(a(x1))))) (27)
a(a(b(x1))) → a(a(b(b(b(x1))))) (28)

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)))))) (29)
a3(a1(a2(b3(a1(x1))))) → a3(a1(a0(b2(b3(a1(x1)))))) (30)
a3(a1(a2(b1(a2(x1))))) → a3(a1(a0(b2(b1(a2(x1)))))) (31)
a3(a1(a2(b1(a0(x1))))) → a3(a1(a0(b2(b1(a0(x1)))))) (32)
a2(b1(a2(b3(a3(x1))))) → a2(b1(a0(b2(b3(a3(x1)))))) (33)
a2(b1(a2(b3(a1(x1))))) → a2(b1(a0(b2(b3(a1(x1)))))) (34)
a2(b1(a2(b1(a2(x1))))) → a2(b1(a0(b2(b1(a2(x1)))))) (35)
a2(b1(a2(b1(a0(x1))))) → a2(b1(a0(b2(b1(a0(x1)))))) (36)
b3(a1(a2(b3(a3(x1))))) → b3(a1(a0(b2(b3(a3(x1)))))) (37)
b3(a1(a2(b3(a1(x1))))) → b3(a1(a0(b2(b3(a1(x1)))))) (38)
b3(a1(a2(b1(a2(x1))))) → b3(a1(a0(b2(b1(a2(x1)))))) (39)
b3(a1(a2(b1(a0(x1))))) → b3(a1(a0(b2(b1(a0(x1)))))) (40)
b2(b1(a2(b3(a3(x1))))) → b2(b1(a0(b2(b3(a3(x1)))))) (41)
b2(b1(a2(b3(a1(x1))))) → b2(b1(a0(b2(b3(a1(x1)))))) (42)
b2(b1(a2(b1(a2(x1))))) → b2(b1(a0(b2(b1(a2(x1)))))) (43)
b2(b1(a2(b1(a0(x1))))) → b2(b1(a0(b2(b1(a0(x1)))))) (44)
a1(a2(b1(a2(b3(x1))))) → a1(a2(b3(a1(a2(b3(x1)))))) (45)
a1(a2(b1(a2(b1(x1))))) → a1(a2(b3(a1(a2(b1(x1)))))) (46)
a1(a2(b1(a0(b2(x1))))) → a1(a2(b3(a1(a0(b2(x1)))))) (47)
a1(a2(b1(a0(b0(x1))))) → a1(a2(b3(a1(a0(b0(x1)))))) (48)
a0(b2(b1(a2(b3(x1))))) → a0(b2(b3(a1(a2(b3(x1)))))) (49)
a0(b2(b1(a2(b1(x1))))) → a0(b2(b3(a1(a2(b1(x1)))))) (50)
a0(b2(b1(a0(b2(x1))))) → a0(b2(b3(a1(a0(b2(x1)))))) (51)
a0(b2(b1(a0(b0(x1))))) → a0(b2(b3(a1(a0(b0(x1)))))) (52)
b1(a2(b1(a2(b3(x1))))) → b1(a2(b3(a1(a2(b3(x1)))))) (53)
b1(a2(b1(a2(b1(x1))))) → b1(a2(b3(a1(a2(b1(x1)))))) (54)
b1(a2(b1(a0(b2(x1))))) → b1(a2(b3(a1(a0(b2(x1)))))) (55)
b1(a2(b1(a0(b0(x1))))) → b1(a2(b3(a1(a0(b0(x1)))))) (56)
b0(b2(b1(a2(b3(x1))))) → b0(b2(b3(a1(a2(b3(x1)))))) (57)
b0(b2(b1(a2(b1(x1))))) → b0(b2(b3(a1(a2(b1(x1)))))) (58)
b0(b2(b1(a0(b2(x1))))) → b0(b2(b3(a1(a0(b2(x1)))))) (59)
b0(b2(b1(a0(b0(x1))))) → b0(b2(b3(a1(a0(b0(x1)))))) (60)
a3(a3(a3(x1))) → a3(a3(a3(a3(a3(x1))))) (61)
a3(a3(a1(x1))) → a3(a3(a3(a3(a1(x1))))) (62)
a3(a1(a2(x1))) → a3(a3(a3(a1(a2(x1))))) (63)
a3(a1(a0(x1))) → a3(a3(a3(a1(a0(x1))))) (64)
a2(b3(a3(x1))) → a2(b3(a3(a3(a3(x1))))) (65)
a2(b3(a1(x1))) → a2(b3(a3(a3(a1(x1))))) (66)
a2(b1(a2(x1))) → a2(b3(a3(a1(a2(x1))))) (67)
a2(b1(a0(x1))) → a2(b3(a3(a1(a0(x1))))) (68)
b3(a3(a3(x1))) → b3(a3(a3(a3(a3(x1))))) (69)
b3(a3(a1(x1))) → b3(a3(a3(a3(a1(x1))))) (70)
b3(a1(a2(x1))) → b3(a3(a3(a1(a2(x1))))) (71)
b3(a1(a0(x1))) → b3(a3(a3(a1(a0(x1))))) (72)
b2(b3(a3(x1))) → b2(b3(a3(a3(a3(x1))))) (73)
b2(b3(a1(x1))) → b2(b3(a3(a3(a1(x1))))) (74)
b2(b1(a2(x1))) → b2(b3(a3(a1(a2(x1))))) (75)
b2(b1(a0(x1))) → b2(b3(a3(a1(a0(x1))))) (76)
a1(a2(b3(x1))) → a1(a0(b0(b2(b3(x1))))) (77)
a1(a2(b1(x1))) → a1(a0(b0(b2(b1(x1))))) (78)
a1(a0(b2(x1))) → a1(a0(b0(b0(b2(x1))))) (79)
a1(a0(b0(x1))) → a1(a0(b0(b0(b0(x1))))) (80)
a0(b2(b3(x1))) → a0(b0(b0(b2(b3(x1))))) (81)
a0(b2(b1(x1))) → a0(b0(b0(b2(b1(x1))))) (82)
a0(b0(b2(x1))) → a0(b0(b0(b0(b2(x1))))) (83)
a0(b0(b0(x1))) → a0(b0(b0(b0(b0(x1))))) (84)
b1(a2(b3(x1))) → b1(a0(b0(b2(b3(x1))))) (85)
b1(a2(b1(x1))) → b1(a0(b0(b2(b1(x1))))) (86)
b1(a0(b2(x1))) → b1(a0(b0(b0(b2(x1))))) (87)
b1(a0(b0(x1))) → b1(a0(b0(b0(b0(x1))))) (88)
b0(b2(b3(x1))) → b0(b0(b0(b2(b3(x1))))) (89)
b0(b2(b1(x1))) → b0(b0(b0(b2(b1(x1))))) (90)
b0(b0(b2(x1))) → b0(b0(b0(b0(b2(x1))))) (91)
b0(b0(b0(x1))) → b0(b0(b0(b0(b0(x1))))) (92)

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 +
1
[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)))))) (29)
a3(a1(a2(b3(a1(x1))))) → a3(a1(a0(b2(b3(a1(x1)))))) (30)
a3(a1(a2(b1(a2(x1))))) → a3(a1(a0(b2(b1(a2(x1)))))) (31)
a3(a1(a2(b1(a0(x1))))) → a3(a1(a0(b2(b1(a0(x1)))))) (32)
a2(b1(a2(b3(a3(x1))))) → a2(b1(a0(b2(b3(a3(x1)))))) (33)
a2(b1(a2(b3(a1(x1))))) → a2(b1(a0(b2(b3(a1(x1)))))) (34)
a2(b1(a2(b1(a2(x1))))) → a2(b1(a0(b2(b1(a2(x1)))))) (35)
a2(b1(a2(b1(a0(x1))))) → a2(b1(a0(b2(b1(a0(x1)))))) (36)
b3(a1(a2(b3(a3(x1))))) → b3(a1(a0(b2(b3(a3(x1)))))) (37)
b3(a1(a2(b3(a1(x1))))) → b3(a1(a0(b2(b3(a1(x1)))))) (38)
b3(a1(a2(b1(a2(x1))))) → b3(a1(a0(b2(b1(a2(x1)))))) (39)
b3(a1(a2(b1(a0(x1))))) → b3(a1(a0(b2(b1(a0(x1)))))) (40)
b2(b1(a2(b3(a3(x1))))) → b2(b1(a0(b2(b3(a3(x1)))))) (41)
b2(b1(a2(b3(a1(x1))))) → b2(b1(a0(b2(b3(a1(x1)))))) (42)
b2(b1(a2(b1(a2(x1))))) → b2(b1(a0(b2(b1(a2(x1)))))) (43)
b2(b1(a2(b1(a0(x1))))) → b2(b1(a0(b2(b1(a0(x1)))))) (44)
a1(a2(b1(a2(b3(x1))))) → a1(a2(b3(a1(a2(b3(x1)))))) (45)
a1(a2(b1(a2(b1(x1))))) → a1(a2(b3(a1(a2(b1(x1)))))) (46)
a1(a2(b1(a0(b2(x1))))) → a1(a2(b3(a1(a0(b2(x1)))))) (47)
a1(a2(b1(a0(b0(x1))))) → a1(a2(b3(a1(a0(b0(x1)))))) (48)
a0(b2(b1(a2(b3(x1))))) → a0(b2(b3(a1(a2(b3(x1)))))) (49)
a0(b2(b1(a2(b1(x1))))) → a0(b2(b3(a1(a2(b1(x1)))))) (50)
a0(b2(b1(a0(b2(x1))))) → a0(b2(b3(a1(a0(b2(x1)))))) (51)
a0(b2(b1(a0(b0(x1))))) → a0(b2(b3(a1(a0(b0(x1)))))) (52)
b1(a2(b1(a2(b3(x1))))) → b1(a2(b3(a1(a2(b3(x1)))))) (53)
b1(a2(b1(a2(b1(x1))))) → b1(a2(b3(a1(a2(b1(x1)))))) (54)
b1(a2(b1(a0(b2(x1))))) → b1(a2(b3(a1(a0(b2(x1)))))) (55)
b1(a2(b1(a0(b0(x1))))) → b1(a2(b3(a1(a0(b0(x1)))))) (56)
b0(b2(b1(a2(b3(x1))))) → b0(b2(b3(a1(a2(b3(x1)))))) (57)
b0(b2(b1(a2(b1(x1))))) → b0(b2(b3(a1(a2(b1(x1)))))) (58)
b0(b2(b1(a0(b2(x1))))) → b0(b2(b3(a1(a0(b2(x1)))))) (59)
b0(b2(b1(a0(b0(x1))))) → b0(b2(b3(a1(a0(b0(x1)))))) (60)
a2(b1(a2(x1))) → a2(b3(a3(a1(a2(x1))))) (67)
a2(b1(a0(x1))) → a2(b3(a3(a1(a0(x1))))) (68)
b2(b1(a2(x1))) → b2(b3(a3(a1(a2(x1))))) (75)
b2(b1(a0(x1))) → b2(b3(a3(a1(a0(x1))))) (76)
a1(a2(b3(x1))) → a1(a0(b0(b2(b3(x1))))) (77)
a1(a2(b1(x1))) → a1(a0(b0(b2(b1(x1))))) (78)
b1(a2(b3(x1))) → b1(a0(b0(b2(b3(x1))))) (85)
b1(a2(b1(x1))) → b1(a0(b0(b2(b1(x1))))) (86)

1.1.1.1.1 R is empty

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