Certification Problem

Input (TPDB SRS_Standard/Waldmann_07_size12/size-12-alpha-2-num-5)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by matchbox @ termCOMP 2023)

1 Split

We split R in the relative problem D/R-D and R-D, where the rules D

a(a(x1)) → x1 (1)
are deleted.

1.1 Closure Under Flat Contexts

Using the flat contexts

{b(☐), a(☐)}

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

1.1.1 Closure Under Flat Contexts

Using the flat contexts

{b(☐), a(☐)}

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

1.1.1.1 Closure Under Flat Contexts

Using the flat contexts

{b(☐), a(☐)}

We obtain the transformed TRS
b(b(b(a(a(x1))))) → b(b(b(x1))) (15)
b(b(a(a(a(x1))))) → b(b(a(x1))) (16)
b(a(b(a(a(x1))))) → b(a(b(x1))) (17)
b(a(a(a(a(x1))))) → b(a(a(x1))) (18)
a(b(b(a(a(x1))))) → a(b(b(x1))) (19)
a(b(a(a(a(x1))))) → a(b(a(x1))) (20)
a(a(b(a(a(x1))))) → a(a(b(x1))) (21)
a(a(a(a(a(x1))))) → a(a(a(x1))) (22)
b(b(b(a(b(b(a(x1))))))) → b(b(b(a(a(b(a(b(b(x1))))))))) (23)
b(b(a(a(b(b(a(x1))))))) → b(b(a(a(a(b(a(b(b(x1))))))))) (24)
b(a(b(a(b(b(a(x1))))))) → b(a(b(a(a(b(a(b(b(x1))))))))) (25)
b(a(a(a(b(b(a(x1))))))) → b(a(a(a(a(b(a(b(b(x1))))))))) (26)
a(b(b(a(b(b(a(x1))))))) → a(b(b(a(a(b(a(b(b(x1))))))))) (27)
a(b(a(a(b(b(a(x1))))))) → a(b(a(a(a(b(a(b(b(x1))))))))) (28)
a(a(b(a(b(b(a(x1))))))) → a(a(b(a(a(b(a(b(b(x1))))))))) (29)
a(a(a(a(b(b(a(x1))))))) → a(a(a(a(a(b(a(b(b(x1))))))))) (30)

1.1.1.1.1 Semantic Labeling

The following interpretations form a model of the rules.

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

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

We obtain the labeled TRS

There are 128 ruless (increase limit for explicit display).

1.1.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
[b4(x1)] = x1 +
0
[b2(x1)] = x1 +
0
[b6(x1)] = x1 +
0
[b1(x1)] = x1 +
0
[b5(x1)] = x1 +
0
[b3(x1)] = x1 +
1
[b7(x1)] = x1 +
1
[a0(x1)] = x1 +
0
[a4(x1)] = x1 +
1
[a2(x1)] = x1 +
0
[a6(x1)] = x1 +
0
[a1(x1)] = x1 +
0
[a5(x1)] = x1 +
0
[a3(x1)] = x1 +
1
[a7(x1)] = x1 +
1
all of the following rules can be deleted.
a7(a7(a7(a7(a7(x1))))) → a7(a7(a7(x1))) (31)
a7(a7(a7(a7(a3(x1))))) → a7(a7(a3(x1))) (32)
a7(a7(a7(a3(a5(x1))))) → a7(a3(a5(x1))) (33)
a7(a7(a7(a3(a1(x1))))) → a7(a3(a1(x1))) (34)
a7(a7(a3(a5(a6(x1))))) → a3(a5(a6(x1))) (35)
a7(a7(a3(a5(a2(x1))))) → a3(a5(a2(x1))) (36)
a7(a7(a3(a1(a4(x1))))) → a3(a1(a4(x1))) (37)
a7(a7(a3(a1(a0(x1))))) → a3(a1(a0(x1))) (38)
a5(a6(b7(a7(a7(x1))))) → a5(a6(b7(x1))) (39)
a5(a6(b7(a7(a3(x1))))) → a5(a6(b3(x1))) (40)
a5(a6(b7(a3(a5(x1))))) → a5(a2(b5(x1))) (41)
a5(a6(b7(a3(a1(x1))))) → a5(a2(b1(x1))) (42)
a5(a6(b3(a1(a4(x1))))) → a1(a0(b4(x1))) (45)
a5(a6(b3(a1(a0(x1))))) → a1(a0(b0(x1))) (46)
a6(b7(a7(a7(a7(x1))))) → a6(b7(a7(x1))) (47)
a6(b7(a7(a7(a3(x1))))) → a6(b7(a3(x1))) (48)
a6(b7(a7(a3(a5(x1))))) → a6(b3(a5(x1))) (49)
a6(b7(a7(a3(a1(x1))))) → a6(b3(a1(x1))) (50)
a6(b7(a3(a5(a6(x1))))) → a2(b5(a6(x1))) (51)
a6(b7(a3(a5(a2(x1))))) → a2(b5(a2(x1))) (52)
a6(b7(a3(a1(a4(x1))))) → a2(b1(a4(x1))) (53)
a6(b7(a3(a1(a0(x1))))) → a2(b1(a0(x1))) (54)
a4(b6(b7(a7(a7(x1))))) → a4(b6(b7(x1))) (55)
a4(b6(b7(a7(a3(x1))))) → a4(b6(b3(x1))) (56)
a4(b6(b7(a3(a5(x1))))) → a4(b2(b5(x1))) (57)
a4(b6(b7(a3(a1(x1))))) → a4(b2(b1(x1))) (58)
a4(b6(b3(a5(a6(x1))))) → a0(b4(b6(x1))) (59)
a4(b6(b3(a5(a2(x1))))) → a0(b4(b2(x1))) (60)
a4(b6(b3(a1(a4(x1))))) → a0(b0(b4(x1))) (61)
a4(b6(b3(a1(a0(x1))))) → a0(b0(b0(x1))) (62)
b7(a7(a7(a7(a7(x1))))) → b7(a7(a7(x1))) (63)
b7(a7(a7(a7(a3(x1))))) → b7(a7(a3(x1))) (64)
b7(a7(a7(a3(a5(x1))))) → b7(a3(a5(x1))) (65)
b7(a7(a7(a3(a1(x1))))) → b7(a3(a1(x1))) (66)
b7(a7(a3(a5(a6(x1))))) → b3(a5(a6(x1))) (67)
b7(a7(a3(a5(a2(x1))))) → b3(a5(a2(x1))) (68)
b7(a7(a3(a1(a4(x1))))) → b3(a1(a4(x1))) (69)
b7(a7(a3(a1(a0(x1))))) → b3(a1(a0(x1))) (70)
b5(a6(b7(a7(a7(x1))))) → b5(a6(b7(x1))) (71)
b5(a6(b7(a7(a3(x1))))) → b5(a6(b3(x1))) (72)
b5(a6(b7(a3(a5(x1))))) → b5(a2(b5(x1))) (73)
b5(a6(b7(a3(a1(x1))))) → b5(a2(b1(x1))) (74)
b5(a6(b3(a1(a4(x1))))) → b1(a0(b4(x1))) (77)
b5(a6(b3(a1(a0(x1))))) → b1(a0(b0(x1))) (78)
b6(b7(a7(a7(a7(x1))))) → b6(b7(a7(x1))) (79)
b6(b7(a7(a7(a3(x1))))) → b6(b7(a3(x1))) (80)
b6(b7(a7(a3(a5(x1))))) → b6(b3(a5(x1))) (81)
b6(b7(a7(a3(a1(x1))))) → b6(b3(a1(x1))) (82)
b6(b7(a3(a5(a6(x1))))) → b2(b5(a6(x1))) (83)
b6(b7(a3(a5(a2(x1))))) → b2(b5(a2(x1))) (84)
b6(b7(a3(a1(a4(x1))))) → b2(b1(a4(x1))) (85)
b6(b7(a3(a1(a0(x1))))) → b2(b1(a0(x1))) (86)
b4(b6(b7(a7(a7(x1))))) → b4(b6(b7(x1))) (87)
b4(b6(b7(a7(a3(x1))))) → b4(b6(b3(x1))) (88)
b4(b6(b7(a3(a5(x1))))) → b4(b2(b5(x1))) (89)
b4(b6(b7(a3(a1(x1))))) → b4(b2(b1(x1))) (90)
b4(b6(b3(a5(a6(x1))))) → b0(b4(b6(x1))) (91)
b4(b6(b3(a5(a2(x1))))) → b0(b4(b2(x1))) (92)
b4(b6(b3(a1(a4(x1))))) → b0(b0(b4(x1))) (93)
b4(b6(b3(a1(a0(x1))))) → b0(b0(b0(x1))) (94)
a7(a3(a1(a4(b2(b1(a4(x1))))))) → a7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) (101)
a5(a2(b1(a4(b2(b1(a4(x1))))))) → a5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) (109)
a6(b3(a1(a4(b2(b1(a4(x1))))))) → a6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) (117)
a4(b2(b1(a4(b2(b1(a4(x1))))))) → a4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) (125)
b7(a3(a1(a4(b2(b1(a4(x1))))))) → b7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) (133)
b5(a2(b1(a4(b2(b1(a4(x1))))))) → b5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) (141)
b6(b3(a1(a4(b2(b1(a4(x1))))))) → b6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) (149)
b4(b2(b1(a4(b2(b1(a4(x1))))))) → b4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) (157)

1.1.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
a6(a5(b3(a6(a5(x1))))) → b6(a4(a1(x1))) (159)
a2(a5(b3(a6(a5(x1))))) → b2(a4(a1(x1))) (160)
a6(a5(b3(a6(b5(x1))))) → b6(a4(b1(x1))) (161)
a2(a5(b3(a6(b5(x1))))) → b2(a4(b1(x1))) (162)
a7(b7(b6(a4(a1(a3(a7(x1))))))) → b7(b6(a4(b1(a2(a5(a3(a7(a7(x1))))))))) (163)
a3(b7(b6(a4(a1(a3(a7(x1))))))) → b3(b6(a4(b1(a2(a5(a3(a7(a7(x1))))))))) (164)
a5(b3(b6(a4(a1(a3(a7(x1))))))) → b5(b2(a4(b1(a2(a5(a3(a7(a7(x1))))))))) (165)
a1(b3(b6(a4(a1(a3(a7(x1))))))) → b1(b2(a4(b1(a2(a5(a3(a7(a7(x1))))))))) (166)
a6(b5(b2(a4(a1(a3(a7(x1))))))) → b6(b4(a0(b1(a2(a5(a3(a7(a7(x1))))))))) (167)
a2(b5(b2(a4(a1(a3(a7(x1))))))) → b2(b4(a0(b1(a2(a5(a3(a7(a7(x1))))))))) (168)
a0(b1(b2(a4(a1(a3(a7(x1))))))) → b0(b0(a0(b1(a2(a5(a3(a7(a7(x1))))))))) (169)
a7(b7(b6(a4(b1(a2(a5(x1))))))) → b7(b6(a4(b1(a2(a5(b3(a6(a5(x1))))))))) (170)
a3(b7(b6(a4(b1(a2(a5(x1))))))) → b3(b6(a4(b1(a2(a5(b3(a6(a5(x1))))))))) (171)
a5(b3(b6(a4(b1(a2(a5(x1))))))) → b5(b2(a4(b1(a2(a5(b3(a6(a5(x1))))))))) (172)
a1(b3(b6(a4(b1(a2(a5(x1))))))) → b1(b2(a4(b1(a2(a5(b3(a6(a5(x1))))))))) (173)
a6(b5(b2(a4(b1(a2(a5(x1))))))) → b6(b4(a0(b1(a2(a5(b3(a6(a5(x1))))))))) (174)
a2(b5(b2(a4(b1(a2(a5(x1))))))) → b2(b4(a0(b1(a2(a5(b3(a6(a5(x1))))))))) (175)
a0(b1(b2(a4(b1(a2(a5(x1))))))) → b0(b0(a0(b1(a2(a5(b3(a6(a5(x1))))))))) (176)
a7(b7(b6(a4(a1(b3(a6(x1))))))) → b7(b6(a4(b1(a2(a5(a3(b7(a6(x1))))))))) (177)
a3(b7(b6(a4(a1(b3(a6(x1))))))) → b3(b6(a4(b1(a2(a5(a3(b7(a6(x1))))))))) (178)
a5(b3(b6(a4(a1(b3(a6(x1))))))) → b5(b2(a4(b1(a2(a5(a3(b7(a6(x1))))))))) (179)
a1(b3(b6(a4(a1(b3(a6(x1))))))) → b1(b2(a4(b1(a2(a5(a3(b7(a6(x1))))))))) (180)
a6(b5(b2(a4(a1(b3(a6(x1))))))) → b6(b4(a0(b1(a2(a5(a3(b7(a6(x1))))))))) (181)
a2(b5(b2(a4(a1(b3(a6(x1))))))) → b2(b4(a0(b1(a2(a5(a3(b7(a6(x1))))))))) (182)
a0(b1(b2(a4(a1(b3(a6(x1))))))) → b0(b0(a0(b1(a2(a5(a3(b7(a6(x1))))))))) (183)
a7(b7(b6(a4(b1(b2(a4(x1))))))) → b7(b6(a4(b1(a2(a5(b3(b6(a4(x1))))))))) (184)
a3(b7(b6(a4(b1(b2(a4(x1))))))) → b3(b6(a4(b1(a2(a5(b3(b6(a4(x1))))))))) (185)
a5(b3(b6(a4(b1(b2(a4(x1))))))) → b5(b2(a4(b1(a2(a5(b3(b6(a4(x1))))))))) (186)
a1(b3(b6(a4(b1(b2(a4(x1))))))) → b1(b2(a4(b1(a2(a5(b3(b6(a4(x1))))))))) (187)
a6(b5(b2(a4(b1(b2(a4(x1))))))) → b6(b4(a0(b1(a2(a5(b3(b6(a4(x1))))))))) (188)
a2(b5(b2(a4(b1(b2(a4(x1))))))) → b2(b4(a0(b1(a2(a5(b3(b6(a4(x1))))))))) (189)
a0(b1(b2(a4(b1(b2(a4(x1))))))) → b0(b0(a0(b1(a2(a5(b3(b6(a4(x1))))))))) (190)
a7(b7(b6(a4(a1(a3(b7(x1))))))) → b7(b6(a4(b1(a2(a5(a3(a7(b7(x1))))))))) (191)
a3(b7(b6(a4(a1(a3(b7(x1))))))) → b3(b6(a4(b1(a2(a5(a3(a7(b7(x1))))))))) (192)
a5(b3(b6(a4(a1(a3(b7(x1))))))) → b5(b2(a4(b1(a2(a5(a3(a7(b7(x1))))))))) (193)
a1(b3(b6(a4(a1(a3(b7(x1))))))) → b1(b2(a4(b1(a2(a5(a3(a7(b7(x1))))))))) (194)
a6(b5(b2(a4(a1(a3(b7(x1))))))) → b6(b4(a0(b1(a2(a5(a3(a7(b7(x1))))))))) (195)
a2(b5(b2(a4(a1(a3(b7(x1))))))) → b2(b4(a0(b1(a2(a5(a3(a7(b7(x1))))))))) (196)
a0(b1(b2(a4(a1(a3(b7(x1))))))) → b0(b0(a0(b1(a2(a5(a3(a7(b7(x1))))))))) (197)
a7(b7(b6(a4(b1(a2(b5(x1))))))) → b7(b6(a4(b1(a2(a5(b3(a6(b5(x1))))))))) (198)
a3(b7(b6(a4(b1(a2(b5(x1))))))) → b3(b6(a4(b1(a2(a5(b3(a6(b5(x1))))))))) (199)
a5(b3(b6(a4(b1(a2(b5(x1))))))) → b5(b2(a4(b1(a2(a5(b3(a6(b5(x1))))))))) (200)
a1(b3(b6(a4(b1(a2(b5(x1))))))) → b1(b2(a4(b1(a2(a5(b3(a6(b5(x1))))))))) (201)
a6(b5(b2(a4(b1(a2(b5(x1))))))) → b6(b4(a0(b1(a2(a5(b3(a6(b5(x1))))))))) (202)
a2(b5(b2(a4(b1(a2(b5(x1))))))) → b2(b4(a0(b1(a2(a5(b3(a6(b5(x1))))))))) (203)
a0(b1(b2(a4(b1(a2(b5(x1))))))) → b0(b0(a0(b1(a2(a5(b3(a6(b5(x1))))))))) (204)
a7(b7(b6(a4(a1(b3(b6(x1))))))) → b7(b6(a4(b1(a2(a5(a3(b7(b6(x1))))))))) (205)
a3(b7(b6(a4(a1(b3(b6(x1))))))) → b3(b6(a4(b1(a2(a5(a3(b7(b6(x1))))))))) (206)
a5(b3(b6(a4(a1(b3(b6(x1))))))) → b5(b2(a4(b1(a2(a5(a3(b7(b6(x1))))))))) (207)
a1(b3(b6(a4(a1(b3(b6(x1))))))) → b1(b2(a4(b1(a2(a5(a3(b7(b6(x1))))))))) (208)
a6(b5(b2(a4(a1(b3(b6(x1))))))) → b6(b4(a0(b1(a2(a5(a3(b7(b6(x1))))))))) (209)
a2(b5(b2(a4(a1(b3(b6(x1))))))) → b2(b4(a0(b1(a2(a5(a3(b7(b6(x1))))))))) (210)
a0(b1(b2(a4(a1(b3(b6(x1))))))) → b0(b0(a0(b1(a2(a5(a3(b7(b6(x1))))))))) (211)
a7(b7(b6(a4(b1(b2(b4(x1))))))) → b7(b6(a4(b1(a2(a5(b3(b6(b4(x1))))))))) (212)
a3(b7(b6(a4(b1(b2(b4(x1))))))) → b3(b6(a4(b1(a2(a5(b3(b6(b4(x1))))))))) (213)
a5(b3(b6(a4(b1(b2(b4(x1))))))) → b5(b2(a4(b1(a2(a5(b3(b6(b4(x1))))))))) (214)
a1(b3(b6(a4(b1(b2(b4(x1))))))) → b1(b2(a4(b1(a2(a5(b3(b6(b4(x1))))))))) (215)
a6(b5(b2(a4(b1(b2(b4(x1))))))) → b6(b4(a0(b1(a2(a5(b3(b6(b4(x1))))))))) (216)
a2(b5(b2(a4(b1(b2(b4(x1))))))) → b2(b4(a0(b1(a2(a5(b3(b6(b4(x1))))))))) (217)
a0(b1(b2(a4(b1(b2(b4(x1))))))) → b0(b0(a0(b1(a2(a5(b3(b6(b4(x1))))))))) (218)

1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the naturals
[b0(x1)] =
1
· x1 +
0
[b4(x1)] =
1
· x1 +
0
[b2(x1)] =
1
· x1 +
1
[b6(x1)] =
1
· x1 +
1
[b1(x1)] =
1
· x1 +
1
[b5(x1)] =
1
· x1 +
1
[b3(x1)] =
1
· x1 +
1
[b7(x1)] =
2
· x1 +
1
[a0(x1)] =
1
· x1 +
0
[a4(x1)] =
2
· x1 +
0
[a2(x1)] =
1
· x1 +
0
[a6(x1)] =
1
· x1 +
0
[a1(x1)] =
2
· x1 +
0
[a5(x1)] =
2
· x1 +
0
[a3(x1)] =
1
· x1 +
1
[a7(x1)] =
2
· x1 +
1
all of the following rules can be deleted.
a6(a5(b3(a6(a5(x1))))) → b6(a4(a1(x1))) (159)
a2(a5(b3(a6(a5(x1))))) → b2(a4(a1(x1))) (160)
a6(a5(b3(a6(b5(x1))))) → b6(a4(b1(x1))) (161)
a2(a5(b3(a6(b5(x1))))) → b2(a4(b1(x1))) (162)
a0(b1(b2(a4(a1(a3(a7(x1))))))) → b0(b0(a0(b1(a2(a5(a3(a7(a7(x1))))))))) (169)
a0(b1(b2(a4(b1(a2(a5(x1))))))) → b0(b0(a0(b1(a2(a5(b3(a6(a5(x1))))))))) (176)
a0(b1(b2(a4(a1(b3(a6(x1))))))) → b0(b0(a0(b1(a2(a5(a3(b7(a6(x1))))))))) (183)
a0(b1(b2(a4(b1(b2(a4(x1))))))) → b0(b0(a0(b1(a2(a5(b3(b6(a4(x1))))))))) (190)
a0(b1(b2(a4(a1(a3(b7(x1))))))) → b0(b0(a0(b1(a2(a5(a3(a7(b7(x1))))))))) (197)
a0(b1(b2(a4(b1(a2(b5(x1))))))) → b0(b0(a0(b1(a2(a5(b3(a6(b5(x1))))))))) (204)
a0(b1(b2(a4(a1(b3(b6(x1))))))) → b0(b0(a0(b1(a2(a5(a3(b7(b6(x1))))))))) (211)
a0(b1(b2(a4(b1(b2(b4(x1))))))) → b0(b0(a0(b1(a2(a5(b3(b6(b4(x1))))))))) (218)

1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
[b4(x1)] = x1 +
0
[b2(x1)] = x1 +
0
[b6(x1)] = x1 +
1
[b1(x1)] = x1 +
0
[b5(x1)] = x1 +
0
[b3(x1)] = x1 +
0
[b7(x1)] = x1 +
2
[a0(x1)] = x1 +
0
[a4(x1)] = x1 +
6
[a2(x1)] = x1 +
0
[a6(x1)] = x1 +
0
[a1(x1)] = x1 +
6
[a5(x1)] = x1 +
0
[a3(x1)] = x1 +
2
[a7(x1)] = x1 +
2
all of the following rules can be deleted.
a7(b7(b6(a4(a1(a3(a7(x1))))))) → b7(b6(a4(b1(a2(a5(a3(a7(a7(x1))))))))) (163)
a3(b7(b6(a4(a1(a3(a7(x1))))))) → b3(b6(a4(b1(a2(a5(a3(a7(a7(x1))))))))) (164)
a5(b3(b6(a4(a1(a3(a7(x1))))))) → b5(b2(a4(b1(a2(a5(a3(a7(a7(x1))))))))) (165)
a1(b3(b6(a4(a1(a3(a7(x1))))))) → b1(b2(a4(b1(a2(a5(a3(a7(a7(x1))))))))) (166)
a6(b5(b2(a4(a1(a3(a7(x1))))))) → b6(b4(a0(b1(a2(a5(a3(a7(a7(x1))))))))) (167)
a2(b5(b2(a4(a1(a3(a7(x1))))))) → b2(b4(a0(b1(a2(a5(a3(a7(a7(x1))))))))) (168)
a7(b7(b6(a4(b1(a2(a5(x1))))))) → b7(b6(a4(b1(a2(a5(b3(a6(a5(x1))))))))) (170)
a3(b7(b6(a4(b1(a2(a5(x1))))))) → b3(b6(a4(b1(a2(a5(b3(a6(a5(x1))))))))) (171)
a5(b3(b6(a4(b1(a2(a5(x1))))))) → b5(b2(a4(b1(a2(a5(b3(a6(a5(x1))))))))) (172)
a1(b3(b6(a4(b1(a2(a5(x1))))))) → b1(b2(a4(b1(a2(a5(b3(a6(a5(x1))))))))) (173)
a6(b5(b2(a4(b1(a2(a5(x1))))))) → b6(b4(a0(b1(a2(a5(b3(a6(a5(x1))))))))) (174)
a2(b5(b2(a4(b1(a2(a5(x1))))))) → b2(b4(a0(b1(a2(a5(b3(a6(a5(x1))))))))) (175)
a7(b7(b6(a4(a1(b3(a6(x1))))))) → b7(b6(a4(b1(a2(a5(a3(b7(a6(x1))))))))) (177)
a3(b7(b6(a4(a1(b3(a6(x1))))))) → b3(b6(a4(b1(a2(a5(a3(b7(a6(x1))))))))) (178)
a5(b3(b6(a4(a1(b3(a6(x1))))))) → b5(b2(a4(b1(a2(a5(a3(b7(a6(x1))))))))) (179)
a1(b3(b6(a4(a1(b3(a6(x1))))))) → b1(b2(a4(b1(a2(a5(a3(b7(a6(x1))))))))) (180)
a6(b5(b2(a4(a1(b3(a6(x1))))))) → b6(b4(a0(b1(a2(a5(a3(b7(a6(x1))))))))) (181)
a2(b5(b2(a4(a1(b3(a6(x1))))))) → b2(b4(a0(b1(a2(a5(a3(b7(a6(x1))))))))) (182)
a7(b7(b6(a4(b1(b2(a4(x1))))))) → b7(b6(a4(b1(a2(a5(b3(b6(a4(x1))))))))) (184)
a3(b7(b6(a4(b1(b2(a4(x1))))))) → b3(b6(a4(b1(a2(a5(b3(b6(a4(x1))))))))) (185)
a1(b3(b6(a4(b1(b2(a4(x1))))))) → b1(b2(a4(b1(a2(a5(b3(b6(a4(x1))))))))) (187)
a6(b5(b2(a4(b1(b2(a4(x1))))))) → b6(b4(a0(b1(a2(a5(b3(b6(a4(x1))))))))) (188)
a2(b5(b2(a4(b1(b2(a4(x1))))))) → b2(b4(a0(b1(a2(a5(b3(b6(a4(x1))))))))) (189)
a7(b7(b6(a4(a1(a3(b7(x1))))))) → b7(b6(a4(b1(a2(a5(a3(a7(b7(x1))))))))) (191)
a3(b7(b6(a4(a1(a3(b7(x1))))))) → b3(b6(a4(b1(a2(a5(a3(a7(b7(x1))))))))) (192)
a5(b3(b6(a4(a1(a3(b7(x1))))))) → b5(b2(a4(b1(a2(a5(a3(a7(b7(x1))))))))) (193)
a1(b3(b6(a4(a1(a3(b7(x1))))))) → b1(b2(a4(b1(a2(a5(a3(a7(b7(x1))))))))) (194)
a6(b5(b2(a4(a1(a3(b7(x1))))))) → b6(b4(a0(b1(a2(a5(a3(a7(b7(x1))))))))) (195)
a2(b5(b2(a4(a1(a3(b7(x1))))))) → b2(b4(a0(b1(a2(a5(a3(a7(b7(x1))))))))) (196)
a7(b7(b6(a4(b1(a2(b5(x1))))))) → b7(b6(a4(b1(a2(a5(b3(a6(b5(x1))))))))) (198)
a3(b7(b6(a4(b1(a2(b5(x1))))))) → b3(b6(a4(b1(a2(a5(b3(a6(b5(x1))))))))) (199)
a5(b3(b6(a4(b1(a2(b5(x1))))))) → b5(b2(a4(b1(a2(a5(b3(a6(b5(x1))))))))) (200)
a1(b3(b6(a4(b1(a2(b5(x1))))))) → b1(b2(a4(b1(a2(a5(b3(a6(b5(x1))))))))) (201)
a6(b5(b2(a4(b1(a2(b5(x1))))))) → b6(b4(a0(b1(a2(a5(b3(a6(b5(x1))))))))) (202)
a2(b5(b2(a4(b1(a2(b5(x1))))))) → b2(b4(a0(b1(a2(a5(b3(a6(b5(x1))))))))) (203)
a7(b7(b6(a4(a1(b3(b6(x1))))))) → b7(b6(a4(b1(a2(a5(a3(b7(b6(x1))))))))) (205)
a3(b7(b6(a4(a1(b3(b6(x1))))))) → b3(b6(a4(b1(a2(a5(a3(b7(b6(x1))))))))) (206)
a5(b3(b6(a4(a1(b3(b6(x1))))))) → b5(b2(a4(b1(a2(a5(a3(b7(b6(x1))))))))) (207)
a1(b3(b6(a4(a1(b3(b6(x1))))))) → b1(b2(a4(b1(a2(a5(a3(b7(b6(x1))))))))) (208)
a6(b5(b2(a4(a1(b3(b6(x1))))))) → b6(b4(a0(b1(a2(a5(a3(b7(b6(x1))))))))) (209)
a2(b5(b2(a4(a1(b3(b6(x1))))))) → b2(b4(a0(b1(a2(a5(a3(b7(b6(x1))))))))) (210)
a7(b7(b6(a4(b1(b2(b4(x1))))))) → b7(b6(a4(b1(a2(a5(b3(b6(b4(x1))))))))) (212)
a3(b7(b6(a4(b1(b2(b4(x1))))))) → b3(b6(a4(b1(a2(a5(b3(b6(b4(x1))))))))) (213)
a1(b3(b6(a4(b1(b2(b4(x1))))))) → b1(b2(a4(b1(a2(a5(b3(b6(b4(x1))))))))) (215)
a6(b5(b2(a4(b1(b2(b4(x1))))))) → b6(b4(a0(b1(a2(a5(b3(b6(b4(x1))))))))) (216)
a2(b5(b2(a4(b1(b2(b4(x1))))))) → b2(b4(a0(b1(a2(a5(b3(b6(b4(x1))))))))) (217)

1.1.1.1.1.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
a4(b2(b1(a4(b6(b3(a5(x1))))))) → a4(b6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) (121)
b4(b2(b1(a4(b6(b3(a5(x1))))))) → b4(b6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) (153)

1.1.1.1.1.1.1.1.1.1.1 R is empty

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

1.2 Closure Under Flat Contexts

Using the flat contexts

{b(☐), a(☐)}

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

1.2.1 Closure Under Flat Contexts

Using the flat contexts

{b(☐), a(☐)}

We obtain the transformed TRS
b(b(a(b(b(a(x1)))))) → b(b(a(a(b(a(b(b(x1)))))))) (11)
b(a(a(b(b(a(x1)))))) → b(a(a(a(b(a(b(b(x1)))))))) (12)
a(b(a(b(b(a(x1)))))) → a(b(a(a(b(a(b(b(x1)))))))) (13)
a(a(a(b(b(a(x1)))))) → a(a(a(a(b(a(b(b(x1)))))))) (14)

1.2.1.1 Closure Under Flat Contexts

Using the flat contexts

{b(☐), a(☐)}

We obtain the transformed TRS
b(b(b(a(b(b(a(x1))))))) → b(b(b(a(a(b(a(b(b(x1))))))))) (23)
b(b(a(a(b(b(a(x1))))))) → b(b(a(a(a(b(a(b(b(x1))))))))) (24)
b(a(b(a(b(b(a(x1))))))) → b(a(b(a(a(b(a(b(b(x1))))))))) (25)
b(a(a(a(b(b(a(x1))))))) → b(a(a(a(a(b(a(b(b(x1))))))))) (26)
a(b(b(a(b(b(a(x1))))))) → a(b(b(a(a(b(a(b(b(x1))))))))) (27)
a(b(a(a(b(b(a(x1))))))) → a(b(a(a(a(b(a(b(b(x1))))))))) (28)
a(a(b(a(b(b(a(x1))))))) → a(a(b(a(a(b(a(b(b(x1))))))))) (29)
a(a(a(a(b(b(a(x1))))))) → a(a(a(a(a(b(a(b(b(x1))))))))) (30)

1.2.1.1.1 Semantic Labeling

The following interpretations form a model of the rules.

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

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

We obtain the labeled TRS
a7(a3(a1(a4(b6(b7(a7(x1))))))) → a7(a7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) (95)
a7(a3(a1(a4(b6(b7(a3(x1))))))) → a7(a7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) (96)
a7(a3(a1(a4(b6(b3(a5(x1))))))) → a7(a7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) (97)
a7(a3(a1(a4(b6(b3(a1(x1))))))) → a7(a7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) (98)
a7(a3(a1(a4(b2(b5(a6(x1))))))) → a7(a7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) (99)
a7(a3(a1(a4(b2(b5(a2(x1))))))) → a7(a7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) (100)
a7(a3(a1(a4(b2(b1(a4(x1))))))) → a7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) (101)
a7(a3(a1(a4(b2(b1(a0(x1))))))) → a7(a7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) (102)
a5(a2(b1(a4(b6(b7(a7(x1))))))) → a5(a6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) (103)
a5(a2(b1(a4(b6(b7(a3(x1))))))) → a5(a6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) (104)
a5(a2(b1(a4(b6(b3(a5(x1))))))) → a5(a6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) (105)
a5(a2(b1(a4(b6(b3(a1(x1))))))) → a5(a6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) (106)
a5(a2(b1(a4(b2(b5(a6(x1))))))) → a5(a6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) (107)
a5(a2(b1(a4(b2(b5(a2(x1))))))) → a5(a6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) (108)
a5(a2(b1(a4(b2(b1(a4(x1))))))) → a5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) (109)
a5(a2(b1(a4(b2(b1(a0(x1))))))) → a5(a6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) (110)
a6(b3(a1(a4(b6(b7(a7(x1))))))) → a6(b7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) (111)
a6(b3(a1(a4(b6(b7(a3(x1))))))) → a6(b7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) (112)
a6(b3(a1(a4(b6(b3(a5(x1))))))) → a6(b7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) (113)
a6(b3(a1(a4(b6(b3(a1(x1))))))) → a6(b7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) (114)
a6(b3(a1(a4(b2(b5(a6(x1))))))) → a6(b7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) (115)
a6(b3(a1(a4(b2(b5(a2(x1))))))) → a6(b7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) (116)
a6(b3(a1(a4(b2(b1(a4(x1))))))) → a6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) (117)
a6(b3(a1(a4(b2(b1(a0(x1))))))) → a6(b7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) (118)
a4(b2(b1(a4(b6(b7(a7(x1))))))) → a4(b6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) (119)
a4(b2(b1(a4(b6(b7(a3(x1))))))) → a4(b6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) (120)
a4(b2(b1(a4(b6(b3(a5(x1))))))) → a4(b6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) (121)
a4(b2(b1(a4(b6(b3(a1(x1))))))) → a4(b6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) (122)
a4(b2(b1(a4(b2(b5(a6(x1))))))) → a4(b6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) (123)
a4(b2(b1(a4(b2(b5(a2(x1))))))) → a4(b6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) (124)
a4(b2(b1(a4(b2(b1(a4(x1))))))) → a4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) (125)
a4(b2(b1(a4(b2(b1(a0(x1))))))) → a4(b6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) (126)
b7(a3(a1(a4(b6(b7(a7(x1))))))) → b7(a7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) (127)
b7(a3(a1(a4(b6(b7(a3(x1))))))) → b7(a7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) (128)
b7(a3(a1(a4(b6(b3(a5(x1))))))) → b7(a7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) (129)
b7(a3(a1(a4(b6(b3(a1(x1))))))) → b7(a7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) (130)
b7(a3(a1(a4(b2(b5(a6(x1))))))) → b7(a7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) (131)
b7(a3(a1(a4(b2(b5(a2(x1))))))) → b7(a7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) (132)
b7(a3(a1(a4(b2(b1(a4(x1))))))) → b7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) (133)
b7(a3(a1(a4(b2(b1(a0(x1))))))) → b7(a7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) (134)
b5(a2(b1(a4(b6(b7(a7(x1))))))) → b5(a6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) (135)
b5(a2(b1(a4(b6(b7(a3(x1))))))) → b5(a6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) (136)
b5(a2(b1(a4(b6(b3(a5(x1))))))) → b5(a6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) (137)
b5(a2(b1(a4(b6(b3(a1(x1))))))) → b5(a6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) (138)
b5(a2(b1(a4(b2(b5(a6(x1))))))) → b5(a6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) (139)
b5(a2(b1(a4(b2(b5(a2(x1))))))) → b5(a6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) (140)
b5(a2(b1(a4(b2(b1(a4(x1))))))) → b5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) (141)
b5(a2(b1(a4(b2(b1(a0(x1))))))) → b5(a6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) (142)
b6(b3(a1(a4(b6(b7(a7(x1))))))) → b6(b7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) (143)
b6(b3(a1(a4(b6(b7(a3(x1))))))) → b6(b7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) (144)
b6(b3(a1(a4(b6(b3(a5(x1))))))) → b6(b7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) (145)
b6(b3(a1(a4(b6(b3(a1(x1))))))) → b6(b7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) (146)
b6(b3(a1(a4(b2(b5(a6(x1))))))) → b6(b7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) (147)
b6(b3(a1(a4(b2(b5(a2(x1))))))) → b6(b7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) (148)
b6(b3(a1(a4(b2(b1(a4(x1))))))) → b6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) (149)
b6(b3(a1(a4(b2(b1(a0(x1))))))) → b6(b7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) (150)
b4(b2(b1(a4(b6(b7(a7(x1))))))) → b4(b6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) (151)
b4(b2(b1(a4(b6(b7(a3(x1))))))) → b4(b6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) (152)
b4(b2(b1(a4(b6(b3(a5(x1))))))) → b4(b6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) (153)
b4(b2(b1(a4(b6(b3(a1(x1))))))) → b4(b6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) (154)
b4(b2(b1(a4(b2(b5(a6(x1))))))) → b4(b6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) (155)
b4(b2(b1(a4(b2(b5(a2(x1))))))) → b4(b6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) (156)
b4(b2(b1(a4(b2(b1(a4(x1))))))) → b4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) (157)
b4(b2(b1(a4(b2(b1(a0(x1))))))) → b4(b6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) (158)

1.2.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
[b4(x1)] = x1 +
0
[b2(x1)] = x1 +
0
[b6(x1)] = x1 +
1
[b1(x1)] = x1 +
0
[b5(x1)] = x1 +
0
[b3(x1)] = x1 +
0
[b7(x1)] = x1 +
2
[a0(x1)] = x1 +
0
[a4(x1)] = x1 +
6
[a2(x1)] = x1 +
0
[a6(x1)] = x1 +
0
[a1(x1)] = x1 +
6
[a5(x1)] = x1 +
0
[a3(x1)] = x1 +
2
[a7(x1)] = x1 +
2
all of the following rules can be deleted.
a7(a3(a1(a4(b6(b7(a7(x1))))))) → a7(a7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) (95)
a7(a3(a1(a4(b6(b7(a3(x1))))))) → a7(a7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) (96)
a7(a3(a1(a4(b6(b3(a5(x1))))))) → a7(a7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) (97)
a7(a3(a1(a4(b6(b3(a1(x1))))))) → a7(a7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) (98)
a7(a3(a1(a4(b2(b5(a6(x1))))))) → a7(a7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) (99)
a7(a3(a1(a4(b2(b5(a2(x1))))))) → a7(a7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) (100)
a7(a3(a1(a4(b2(b1(a4(x1))))))) → a7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) (101)
a7(a3(a1(a4(b2(b1(a0(x1))))))) → a7(a7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) (102)
a5(a2(b1(a4(b6(b7(a7(x1))))))) → a5(a6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) (103)
a5(a2(b1(a4(b6(b7(a3(x1))))))) → a5(a6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) (104)
a5(a2(b1(a4(b6(b3(a5(x1))))))) → a5(a6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) (105)
a5(a2(b1(a4(b6(b3(a1(x1))))))) → a5(a6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) (106)
a5(a2(b1(a4(b2(b5(a6(x1))))))) → a5(a6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) (107)
a5(a2(b1(a4(b2(b5(a2(x1))))))) → a5(a6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) (108)
a5(a2(b1(a4(b2(b1(a4(x1))))))) → a5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) (109)
a5(a2(b1(a4(b2(b1(a0(x1))))))) → a5(a6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) (110)
a6(b3(a1(a4(b6(b7(a7(x1))))))) → a6(b7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) (111)
a6(b3(a1(a4(b6(b7(a3(x1))))))) → a6(b7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) (112)
a6(b3(a1(a4(b6(b3(a5(x1))))))) → a6(b7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) (113)
a6(b3(a1(a4(b6(b3(a1(x1))))))) → a6(b7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) (114)
a6(b3(a1(a4(b2(b5(a6(x1))))))) → a6(b7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) (115)
a6(b3(a1(a4(b2(b5(a2(x1))))))) → a6(b7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) (116)
a6(b3(a1(a4(b2(b1(a4(x1))))))) → a6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) (117)
a6(b3(a1(a4(b2(b1(a0(x1))))))) → a6(b7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) (118)
a4(b2(b1(a4(b6(b7(a7(x1))))))) → a4(b6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) (119)
a4(b2(b1(a4(b6(b7(a3(x1))))))) → a4(b6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) (120)
a4(b2(b1(a4(b6(b3(a1(x1))))))) → a4(b6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) (122)
a4(b2(b1(a4(b2(b5(a6(x1))))))) → a4(b6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) (123)
a4(b2(b1(a4(b2(b5(a2(x1))))))) → a4(b6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) (124)
a4(b2(b1(a4(b2(b1(a4(x1))))))) → a4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) (125)
a4(b2(b1(a4(b2(b1(a0(x1))))))) → a4(b6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) (126)
b7(a3(a1(a4(b6(b7(a7(x1))))))) → b7(a7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) (127)
b7(a3(a1(a4(b6(b7(a3(x1))))))) → b7(a7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) (128)
b7(a3(a1(a4(b6(b3(a5(x1))))))) → b7(a7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) (129)
b7(a3(a1(a4(b6(b3(a1(x1))))))) → b7(a7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) (130)
b7(a3(a1(a4(b2(b5(a6(x1))))))) → b7(a7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) (131)
b7(a3(a1(a4(b2(b5(a2(x1))))))) → b7(a7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) (132)
b7(a3(a1(a4(b2(b1(a4(x1))))))) → b7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) (133)
b7(a3(a1(a4(b2(b1(a0(x1))))))) → b7(a7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) (134)
b5(a2(b1(a4(b6(b7(a7(x1))))))) → b5(a6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) (135)
b5(a2(b1(a4(b6(b7(a3(x1))))))) → b5(a6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) (136)
b5(a2(b1(a4(b6(b3(a5(x1))))))) → b5(a6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) (137)
b5(a2(b1(a4(b6(b3(a1(x1))))))) → b5(a6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) (138)
b5(a2(b1(a4(b2(b5(a6(x1))))))) → b5(a6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) (139)
b5(a2(b1(a4(b2(b5(a2(x1))))))) → b5(a6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) (140)
b5(a2(b1(a4(b2(b1(a4(x1))))))) → b5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) (141)
b5(a2(b1(a4(b2(b1(a0(x1))))))) → b5(a6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) (142)
b6(b3(a1(a4(b6(b7(a7(x1))))))) → b6(b7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) (143)
b6(b3(a1(a4(b6(b7(a3(x1))))))) → b6(b7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) (144)
b6(b3(a1(a4(b6(b3(a5(x1))))))) → b6(b7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) (145)
b6(b3(a1(a4(b6(b3(a1(x1))))))) → b6(b7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) (146)
b6(b3(a1(a4(b2(b5(a6(x1))))))) → b6(b7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) (147)
b6(b3(a1(a4(b2(b5(a2(x1))))))) → b6(b7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) (148)
b6(b3(a1(a4(b2(b1(a4(x1))))))) → b6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) (149)
b6(b3(a1(a4(b2(b1(a0(x1))))))) → b6(b7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) (150)
b4(b2(b1(a4(b6(b7(a7(x1))))))) → b4(b6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) (151)
b4(b2(b1(a4(b6(b7(a3(x1))))))) → b4(b6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) (152)
b4(b2(b1(a4(b6(b3(a1(x1))))))) → b4(b6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) (154)
b4(b2(b1(a4(b2(b5(a6(x1))))))) → b4(b6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) (155)
b4(b2(b1(a4(b2(b5(a2(x1))))))) → b4(b6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) (156)
b4(b2(b1(a4(b2(b1(a4(x1))))))) → b4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) (157)
b4(b2(b1(a4(b2(b1(a0(x1))))))) → b4(b6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) (158)

1.2.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
a5(b3(b6(a4(b1(b2(a4(x1))))))) → b5(b2(a4(b1(a2(a5(b3(b6(a4(x1))))))))) (186)
a5(b3(b6(a4(b1(b2(b4(x1))))))) → b5(b2(a4(b1(a2(a5(b3(b6(b4(x1))))))))) (214)

1.2.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 1 with strict dimension 1 over the naturals
[b4(x1)] =
2
· x1 +
1
[b2(x1)] =
2
· x1 +
1
[b6(x1)] =
2
· x1 +
1
[b1(x1)] =
1
· x1 +
1
[b5(x1)] =
1
· x1 +
0
[b3(x1)] =
2
· x1 +
1
[a4(x1)] =
2
· x1 +
1
[a2(x1)] =
1
· x1 +
1
[a5(x1)] =
2
· x1 +
1
all of the following rules can be deleted.
a5(b3(b6(a4(b1(b2(a4(x1))))))) → b5(b2(a4(b1(a2(a5(b3(b6(a4(x1))))))))) (186)
a5(b3(b6(a4(b1(b2(b4(x1))))))) → b5(b2(a4(b1(a2(a5(b3(b6(b4(x1))))))))) (214)

1.2.1.1.1.1.1.1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS

There are no rules.

1.2.1.1.1.1.1.1.1.1 R is empty

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