Certification Problem

Input (TPDB SRS_Relative/Waldmann_06_relative/r4)

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

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

and S is the following TRS.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

{a(☐), b(☐)}

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

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
aa(ab(ba(ab(ba(aa(x1)))))) → aa(x1) (7)
aa(ab(ba(ab(ba(ab(x1)))))) → ab(x1) (8)
ba(ab(ba(ab(ba(aa(x1)))))) → ba(x1) (9)
ba(ab(ba(ab(ba(ab(x1)))))) → bb(x1) (10)
aa(ab(ba(x1))) → ab(bb(ba(aa(aa(x1))))) (11)
aa(ab(bb(x1))) → ab(bb(ba(aa(ab(x1))))) (12)
ba(ab(ba(x1))) → bb(bb(ba(aa(aa(x1))))) (13)
ba(ab(bb(x1))) → bb(bb(ba(aa(ab(x1))))) (14)

1.1.1 Closure Under Flat Contexts

Using the flat contexts

{aa(☐), ab(☐), ba(☐), bb(☐)}

We obtain the transformed TRS
aa(ab(ba(ab(ba(aa(x1)))))) → aa(x1) (7)
ba(ab(ba(ab(ba(aa(x1)))))) → ba(x1) (9)
aa(aa(ab(ba(ab(ba(ab(x1))))))) → aa(ab(x1)) (15)
ab(aa(ab(ba(ab(ba(ab(x1))))))) → ab(ab(x1)) (16)
ba(aa(ab(ba(ab(ba(ab(x1))))))) → ba(ab(x1)) (17)
bb(aa(ab(ba(ab(ba(ab(x1))))))) → bb(ab(x1)) (18)
aa(ba(ab(ba(ab(ba(ab(x1))))))) → aa(bb(x1)) (19)
ab(ba(ab(ba(ab(ba(ab(x1))))))) → ab(bb(x1)) (20)
ba(ba(ab(ba(ab(ba(ab(x1))))))) → ba(bb(x1)) (21)
bb(ba(ab(ba(ab(ba(ab(x1))))))) → bb(bb(x1)) (22)
aa(aa(ab(ba(x1)))) → aa(ab(bb(ba(aa(aa(x1)))))) (23)
ab(aa(ab(ba(x1)))) → ab(ab(bb(ba(aa(aa(x1)))))) (24)
ba(aa(ab(ba(x1)))) → ba(ab(bb(ba(aa(aa(x1)))))) (25)
bb(aa(ab(ba(x1)))) → bb(ab(bb(ba(aa(aa(x1)))))) (26)
aa(aa(ab(bb(x1)))) → aa(ab(bb(ba(aa(ab(x1)))))) (27)
ab(aa(ab(bb(x1)))) → ab(ab(bb(ba(aa(ab(x1)))))) (28)
ba(aa(ab(bb(x1)))) → ba(ab(bb(ba(aa(ab(x1)))))) (29)
bb(aa(ab(bb(x1)))) → bb(ab(bb(ba(aa(ab(x1)))))) (30)
aa(ba(ab(ba(x1)))) → aa(bb(bb(ba(aa(aa(x1)))))) (31)
ab(ba(ab(ba(x1)))) → ab(bb(bb(ba(aa(aa(x1)))))) (32)
ba(ba(ab(ba(x1)))) → ba(bb(bb(ba(aa(aa(x1)))))) (33)
bb(ba(ab(ba(x1)))) → bb(bb(bb(ba(aa(aa(x1)))))) (34)
aa(ba(ab(bb(x1)))) → aa(bb(bb(ba(aa(ab(x1)))))) (35)
ab(ba(ab(bb(x1)))) → ab(bb(bb(ba(aa(ab(x1)))))) (36)
ba(ba(ab(bb(x1)))) → ba(bb(bb(ba(aa(ab(x1)))))) (37)
bb(ba(ab(bb(x1)))) → bb(bb(bb(ba(aa(ab(x1)))))) (38)

1.1.1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS

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

1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aaab(x1)] = 1 · x1
[abba(x1)] = 1 · x1
[baab(x1)] = 1 · x1
[baaa(x1)] = 1 · x1
[aaaa(x1)] = 1 · x1
[aaba(x1)] = 1 + 1 · x1
[aabb(x1)] = 1 · x1
[baba(x1)] = 1 + 1 · x1
[babb(x1)] = 1 · x1
[abaa(x1)] = 1 + 1 · x1
[abab(x1)] = 1 + 1 · x1
[abbb(x1)] = 1 · x1
[bbaa(x1)] = 1 + 1 · x1
[bbab(x1)] = 1 + 1 · x1
[bbba(x1)] = 1 · x1
[bbbb(x1)] = 1 · x1
all of the following rules can be deleted.
aaba(baab(abba(baab(abba(baab(abaa(x1))))))) → aabb(bbaa(x1)) (63)
aaba(baab(abba(baab(abba(baab(abab(x1))))))) → aabb(bbab(x1)) (64)
aaba(baab(abba(baab(abba(baab(abba(x1))))))) → aabb(bbba(x1)) (65)
aaba(baab(abba(baab(abba(baab(abbb(x1))))))) → aabb(bbbb(x1)) (66)
baba(baab(abba(baab(abba(baab(abaa(x1))))))) → babb(bbaa(x1)) (71)
baba(baab(abba(baab(abba(baab(abab(x1))))))) → babb(bbab(x1)) (72)
baba(baab(abba(baab(abba(baab(abba(x1))))))) → babb(bbba(x1)) (73)
baba(baab(abba(baab(abba(baab(abbb(x1))))))) → babb(bbbb(x1)) (74)
aaba(baab(abba(baaa(x1)))) → aabb(bbbb(bbba(baaa(aaaa(aaaa(x1)))))) (111)
aaba(baab(abba(baab(x1)))) → aabb(bbbb(bbba(baaa(aaaa(aaab(x1)))))) (112)
aaba(baab(abba(baba(x1)))) → aabb(bbbb(bbba(baaa(aaaa(aaba(x1)))))) (113)
aaba(baab(abba(babb(x1)))) → aabb(bbbb(bbba(baaa(aaaa(aabb(x1)))))) (114)
baba(baab(abba(baaa(x1)))) → babb(bbbb(bbba(baaa(aaaa(aaaa(x1)))))) (119)
baba(baab(abba(baab(x1)))) → babb(bbbb(bbba(baaa(aaaa(aaab(x1)))))) (120)
baba(baab(abba(baba(x1)))) → babb(bbbb(bbba(baaa(aaaa(aaba(x1)))))) (121)
baba(baab(abba(babb(x1)))) → babb(bbbb(bbba(baaa(aaaa(aabb(x1)))))) (122)
aaba(baab(abbb(bbaa(x1)))) → aabb(bbbb(bbba(baaa(aaab(abaa(x1)))))) (127)
aaba(baab(abbb(bbab(x1)))) → aabb(bbbb(bbba(baaa(aaab(abab(x1)))))) (128)
aaba(baab(abbb(bbba(x1)))) → aabb(bbbb(bbba(baaa(aaab(abba(x1)))))) (129)
aaba(baab(abbb(bbbb(x1)))) → aabb(bbbb(bbba(baaa(aaab(abbb(x1)))))) (130)
baba(baab(abbb(bbaa(x1)))) → babb(bbbb(bbba(baaa(aaab(abaa(x1)))))) (135)
baba(baab(abbb(bbab(x1)))) → babb(bbbb(bbba(baaa(aaab(abab(x1)))))) (136)
baba(baab(abbb(bbba(x1)))) → babb(bbbb(bbba(baaa(aaab(abba(x1)))))) (137)
baba(baab(abbb(bbbb(x1)))) → babb(bbbb(bbba(baaa(aaab(abbb(x1)))))) (138)

1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aaab(x1)] = 1 · x1
[abba(x1)] = 1 · x1
[baab(x1)] = 1 · x1
[baaa(x1)] = 1 · x1
[aaaa(x1)] = 1 · x1
[aaba(x1)] = 1 · x1
[aabb(x1)] = 1 · x1
[baba(x1)] = 1 · x1
[babb(x1)] = 1 · x1
[abaa(x1)] = 1 + 1 · x1
[abab(x1)] = 1 · x1
[abbb(x1)] = 1 · x1
[bbaa(x1)] = 1 + 1 · x1
[bbab(x1)] = 1 · x1
[bbba(x1)] = 1 · x1
[bbbb(x1)] = 1 · x1
all of the following rules can be deleted.
abaa(aaab(abba(baab(abba(baab(abaa(x1))))))) → abab(abaa(x1)) (51)
abaa(aaab(abba(baab(abba(baab(abab(x1))))))) → abab(abab(x1)) (52)
abaa(aaab(abba(baab(abba(baab(abba(x1))))))) → abab(abba(x1)) (53)
abaa(aaab(abba(baab(abba(baab(abbb(x1))))))) → abab(abbb(x1)) (54)
bbaa(aaab(abba(baab(abba(baab(abaa(x1))))))) → bbab(abaa(x1)) (59)
bbaa(aaab(abba(baab(abba(baab(abab(x1))))))) → bbab(abab(x1)) (60)
bbaa(aaab(abba(baab(abba(baab(abba(x1))))))) → bbab(abba(x1)) (61)
bbaa(aaab(abba(baab(abba(baab(abbb(x1))))))) → bbab(abbb(x1)) (62)
abaa(aaab(abba(baaa(x1)))) → abab(abbb(bbba(baaa(aaaa(aaaa(x1)))))) (83)
abaa(aaab(abba(baab(x1)))) → abab(abbb(bbba(baaa(aaaa(aaab(x1)))))) (84)
abaa(aaab(abba(baba(x1)))) → abab(abbb(bbba(baaa(aaaa(aaba(x1)))))) (85)
abaa(aaab(abba(babb(x1)))) → abab(abbb(bbba(baaa(aaaa(aabb(x1)))))) (86)
bbaa(aaab(abba(baaa(x1)))) → bbab(abbb(bbba(baaa(aaaa(aaaa(x1)))))) (91)
bbaa(aaab(abba(baab(x1)))) → bbab(abbb(bbba(baaa(aaaa(aaab(x1)))))) (92)
bbaa(aaab(abba(baba(x1)))) → bbab(abbb(bbba(baaa(aaaa(aaba(x1)))))) (93)
bbaa(aaab(abba(babb(x1)))) → bbab(abbb(bbba(baaa(aaaa(aabb(x1)))))) (94)
abaa(aaab(abbb(bbaa(x1)))) → abab(abbb(bbba(baaa(aaab(abaa(x1)))))) (99)
abaa(aaab(abbb(bbab(x1)))) → abab(abbb(bbba(baaa(aaab(abab(x1)))))) (100)
abaa(aaab(abbb(bbba(x1)))) → abab(abbb(bbba(baaa(aaab(abba(x1)))))) (101)
abaa(aaab(abbb(bbbb(x1)))) → abab(abbb(bbba(baaa(aaab(abbb(x1)))))) (102)
bbaa(aaab(abbb(bbaa(x1)))) → bbab(abbb(bbba(baaa(aaab(abaa(x1)))))) (107)
bbaa(aaab(abbb(bbab(x1)))) → bbab(abbb(bbba(baaa(aaab(abab(x1)))))) (108)
bbaa(aaab(abbb(bbba(x1)))) → bbab(abbb(bbba(baaa(aaab(abba(x1)))))) (109)
bbaa(aaab(abbb(bbbb(x1)))) → bbab(abbb(bbba(baaa(aaab(abbb(x1)))))) (110)

1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 3 with strict dimension 1 over the integers
[aaab(x1)] =
0
0
0
+
1 0 0
0 1 0
0 0 0
· x1
[abba(x1)] =
0
0
0
+
1 0 0
0 1 0
0 0 0
· x1
[baab(x1)] =
0
0
0
+
1 1 0
0 1 0
0 0 0
· x1
[baaa(x1)] =
0
1
0
+
1 0 0
0 1 0
0 0 0
· x1
[aaaa(x1)] =
0
0
0
+
1 0 0
0 1 0
0 0 0
· x1
[aaba(x1)] =
0
0
0
+
1 0 0
1 0 0
0 0 0
· x1
[aabb(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[baba(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[babb(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[abaa(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[abab(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[abbb(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[bbaa(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[bbab(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[bbba(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[bbbb(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
all of the following rules can be deleted.
aaab(abba(baab(abba(baaa(aaaa(x1)))))) → aaaa(x1) (39)
aaab(abba(baab(abba(baaa(aaab(x1)))))) → aaab(x1) (40)
aaab(abba(baab(abba(baaa(aaba(x1)))))) → aaba(x1) (41)
aaab(abba(baab(abba(baaa(aabb(x1)))))) → aabb(x1) (42)
baab(abba(baab(abba(baaa(aaaa(x1)))))) → baaa(x1) (43)
baab(abba(baab(abba(baaa(aaab(x1)))))) → baab(x1) (44)
baab(abba(baab(abba(baaa(aaba(x1)))))) → baba(x1) (45)
baab(abba(baab(abba(baaa(aabb(x1)))))) → babb(x1) (46)
abba(baab(abba(baaa(x1)))) → abbb(bbbb(bbba(baaa(aaaa(aaaa(x1)))))) (115)
bbba(baab(abba(baaa(x1)))) → bbbb(bbbb(bbba(baaa(aaaa(aaaa(x1)))))) (123)

1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aaaa(x1)] = 1 · x1
[aaab(x1)] = 1 · x1
[abba(x1)] = 1 · x1
[baab(x1)] = 1 · x1
[abaa(x1)] = 1 · x1
[abab(x1)] = 1 · x1
[abbb(x1)] = 1 · x1
[baaa(x1)] = 1 · x1
[bbaa(x1)] = 1 · x1
[bbab(x1)] = 1 · x1
[bbba(x1)] = 1 · x1
[bbbb(x1)] = 1 · x1
[baba(x1)] = 1 + 1 · x1
[aaba(x1)] = 1 + 1 · x1
[babb(x1)] = 1 + 1 · x1
[aabb(x1)] = 1 · x1
all of the following rules can be deleted.
aaaa(aaab(abba(babb(x1)))) → aaab(abbb(bbba(baaa(aaaa(aabb(x1)))))) (82)
baaa(aaab(abba(babb(x1)))) → baab(abbb(bbba(baaa(aaaa(aabb(x1)))))) (90)
abba(baab(abba(babb(x1)))) → abbb(bbbb(bbba(baaa(aaaa(aabb(x1)))))) (118)
bbba(baab(abba(babb(x1)))) → bbbb(bbbb(bbba(baaa(aaaa(aabb(x1)))))) (126)

1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aaaa(x1)] = 1 · x1
[aaab(x1)] = 1 · x1
[abba(x1)] = 1 · x1
[baab(x1)] = 1 · x1
[abaa(x1)] = 1 · x1
[abab(x1)] = 1 · x1
[abbb(x1)] = 1 · x1
[baaa(x1)] = 1 · x1
[bbaa(x1)] = 1 · x1
[bbab(x1)] = 1 · x1
[bbba(x1)] = 1 · x1
[bbbb(x1)] = 1 · x1
[baba(x1)] = 1 + 1 · x1
[aaba(x1)] = 1 · x1
all of the following rules can be deleted.
aaaa(aaab(abba(baba(x1)))) → aaab(abbb(bbba(baaa(aaaa(aaba(x1)))))) (81)
baaa(aaab(abba(baba(x1)))) → baab(abbb(bbba(baaa(aaaa(aaba(x1)))))) (89)
abba(baab(abba(baba(x1)))) → abbb(bbbb(bbba(baaa(aaaa(aaba(x1)))))) (117)
bbba(baab(abba(baba(x1)))) → bbbb(bbbb(bbba(baaa(aaaa(aaba(x1)))))) (125)

1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 3 with strict dimension 1 over the integers
[aaaa(x1)] =
0
0
1
+
1 0 0
0 0 0
0 0 0
· x1
[aaab(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[abba(x1)] =
0
0
0
+
1 0 0
0 1 0
0 0 1
· x1
[baab(x1)] =
0
0
1
+
1 1 0
0 0 1
1 0 0
· x1
[abaa(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[abab(x1)] =
1
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[abbb(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[baaa(x1)] =
0
1
1
+
1 0 0
1 0 1
1 0 0
· x1
[bbaa(x1)] =
1
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[bbab(x1)] =
1
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[bbba(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[bbbb(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
all of the following rules can be deleted.
abba(baab(abba(baab(abba(baab(abab(x1))))))) → abbb(bbab(x1)) (68)
abba(baab(abba(baab(abba(baab(abba(x1))))))) → abbb(bbba(x1)) (69)
abba(baab(abba(baab(abba(baab(abbb(x1))))))) → abbb(bbbb(x1)) (70)
bbba(baab(abba(baab(abba(baab(abab(x1))))))) → bbbb(bbab(x1)) (76)
bbba(baab(abba(baab(abba(baab(abba(x1))))))) → bbbb(bbba(x1)) (77)
bbba(baab(abba(baab(abba(baab(abbb(x1))))))) → bbbb(bbbb(x1)) (78)
aaaa(aaab(abbb(bbaa(x1)))) → aaab(abbb(bbba(baaa(aaab(abaa(x1)))))) (95)
baaa(aaab(abbb(bbaa(x1)))) → baab(abbb(bbba(baaa(aaab(abaa(x1)))))) (103)
abba(baab(abbb(bbaa(x1)))) → abbb(bbbb(bbba(baaa(aaab(abaa(x1)))))) (131)
bbba(baab(abbb(bbaa(x1)))) → bbbb(bbbb(bbba(baaa(aaab(abaa(x1)))))) (139)

1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aaaa(x1)] = 1 · x1
[aaab(x1)] = 1 · x1
[abba(x1)] = 1 · x1
[baab(x1)] = 1 · x1
[abaa(x1)] = 1 + 1 · x1
[abab(x1)] = 1 · x1
[abbb(x1)] = 1 · x1
[baaa(x1)] = 1 · x1
[bbaa(x1)] = 1 + 1 · x1
[bbba(x1)] = 1 · x1
[bbbb(x1)] = 1 · x1
[bbab(x1)] = 1 + 1 · x1
all of the following rules can be deleted.
aaaa(aaab(abbb(bbab(x1)))) → aaab(abbb(bbba(baaa(aaab(abab(x1)))))) (96)
baaa(aaab(abbb(bbab(x1)))) → baab(abbb(bbba(baaa(aaab(abab(x1)))))) (104)
abba(baab(abbb(bbab(x1)))) → abbb(bbbb(bbba(baaa(aaab(abab(x1)))))) (132)
bbba(baab(abbb(bbab(x1)))) → bbbb(bbbb(bbba(baaa(aaab(abab(x1)))))) (140)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aaaa(x1)] = 1 · x1
[aaab(x1)] = 1 · x1
[abba(x1)] = 1 · x1
[baab(x1)] = 1 · x1
[abaa(x1)] = 1 + 1 · x1
[abab(x1)] = 1 · x1
[abbb(x1)] = 1 · x1
[baaa(x1)] = 1 · x1
[bbaa(x1)] = 1 · x1
[bbba(x1)] = 1 · x1
[bbbb(x1)] = 1 · x1
all of the following rules can be deleted.
abba(baab(abba(baab(abba(baab(abaa(x1))))))) → abbb(bbaa(x1)) (67)
bbba(baab(abba(baab(abba(baab(abaa(x1))))))) → bbbb(bbaa(x1)) (75)

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[aaaa(x1)] =
0
2
+
1 0
0 0
· x1
[aaab(x1)] =
0
0
+
1 0
0 0
· x1
[abba(x1)] =
0
0
+
1 0
0 0
· x1
[baab(x1)] =
0
0
+
1 1
0 0
· x1
[abaa(x1)] =
2
2
+
1 0
1 0
· x1
[abab(x1)] =
0
0
+
1 0
1 0
· x1
[abbb(x1)] =
0
0
+
1 0
0 0
· x1
[baaa(x1)] =
0
0
+
1 0
0 0
· x1
[bbba(x1)] =
0
0
+
1 0
0 0
· x1
[bbbb(x1)] =
0
0
+
1 0
0 0
· x1
all of the following rules can be deleted.
aaaa(aaab(abba(baab(abba(baab(abaa(x1))))))) → aaab(abaa(x1)) (47)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[aaaa(x1)] =
0
0
+
1 0
0 0
· x1
[aaab(x1)] =
0
0
+
1 0
0 0
· x1
[abba(x1)] =
0
0
+
1 0
1 0
· x1
[baab(x1)] =
0
0
+
1 1
0 0
· x1
[abab(x1)] =
0
0
+
1 0
0 0
· x1
[abbb(x1)] =
0
0
+
1 0
0 0
· x1
[baaa(x1)] =
0
0
+
1 0
0 0
· x1
[abaa(x1)] =
2
2
+
1 0
0 0
· x1
[bbba(x1)] =
0
2
+
1 0
0 0
· x1
[bbbb(x1)] =
0
0
+
1 0
0 0
· x1
all of the following rules can be deleted.
baaa(aaab(abba(baab(abba(baab(abaa(x1))))))) → baab(abaa(x1)) (55)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[aaaa(x1)] =
0
0
+
1 0
0 0
· x1
[aaab(x1)] =
0
0
+
1 0
0 0
· x1
[abba(x1)] =
0
0
+
1 0
0 0
· x1
[baab(x1)] =
0
0
+
1 2
0 0
· x1
[abab(x1)] =
0
2
+
2 0
1 0
· x1
[abbb(x1)] =
0
0
+
1 0
0 0
· x1
[baaa(x1)] =
0
0
+
1 0
0 0
· x1
[bbba(x1)] =
0
0
+
1 0
0 0
· x1
[bbbb(x1)] =
0
0
+
1 0
0 0
· x1
all of the following rules can be deleted.
aaaa(aaab(abba(baab(abba(baab(abab(x1))))))) → aaab(abab(x1)) (48)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 3 with strict dimension 1 over the integers
[aaaa(x1)] =
0
1
1
+
1 0 0
0 0 0
0 0 0
· x1
[aaab(x1)] =
0
1
0
+
1 0 0
0 0 0
0 0 0
· x1
[abba(x1)] =
0
1
0
+
1 0 0
0 0 0
0 1 0
· x1
[baab(x1)] =
0
0
0
+
1 0 1
0 1 0
0 0 0
· x1
[abbb(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[baaa(x1)] =
0
0
0
+
1 0 0
0 1 0
0 0 0
· x1
[abab(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[bbba(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
[bbbb(x1)] =
0
0
0
+
1 0 0
0 0 0
0 0 0
· x1
all of the following rules can be deleted.
aaaa(aaab(abba(baab(abba(baab(abba(x1))))))) → aaab(abba(x1)) (49)
baaa(aaab(abba(baab(abba(baab(abba(x1))))))) → baab(abba(x1)) (57)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[aaaa(x1)] =
0
0
+
1 0
0 0
· x1
[aaab(x1)] =
0
0
+
1 0
0 0
· x1
[abba(x1)] =
0
0
+
1 0
2 2
· x1
[baab(x1)] =
0
0
+
1 1
0 1
· x1
[abbb(x1)] =
0
0
+
1 0
0 0
· x1
[baaa(x1)] =
0
2
+
1 0
0 0
· x1
[abab(x1)] =
0
2
+
1 0
0 0
· x1
[bbba(x1)] =
0
0
+
1 0
0 0
· x1
[bbbb(x1)] =
0
0
+
1 0
0 0
· x1
all of the following rules can be deleted.
baaa(aaab(abba(baab(abba(baab(abab(x1))))))) → baab(abab(x1)) (56)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[aaaa(x1)] =
0
0
+
1 0
0 0
· x1
[aaab(x1)] =
0
0
+
1 0
0 0
· x1
[abba(x1)] =
0
2
+
1 0
0 0
· x1
[baab(x1)] =
0
0
+
1 0
0 2
· x1
[abbb(x1)] =
0
0
+
1 0
0 0
· x1
[baaa(x1)] =
0
0
+
1 0
0 0
· x1
[bbba(x1)] =
0
0
+
1 2
0 0
· x1
[bbbb(x1)] =
0
0
+
1 0
0 0
· x1
all of the following rules can be deleted.
bbba(baab(abba(baab(x1)))) → bbbb(bbbb(bbba(baaa(aaaa(aaab(x1)))))) (124)

1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Removal

Using the matrix interpretations of dimension 2 with strict dimension 1 over the integers
[aaaa(x1)] =
0
0
+
1 0
0 0
· x1
[aaab(x1)] =
0
0
+
1 0
0 0
· x1
[abba(x1)] =
0
2
+
1 0
0 0
· x1
[baab(x1)] =
0
0
+
1 2
0 0
· x1
[abbb(x1)] =
0
0
+
1 0
0 0
· x1
[baaa(x1)] =
0
0
+
1 0
0 0
· x1
[bbba(x1)] =
0
0
+
1 0
0 0
· x1
[bbbb(x1)] =
0
0
+
1 0
0 0
· x1
all of the following rules can be deleted.
aaaa(aaab(abba(baab(abba(baab(abbb(x1))))))) → aaab(abbb(x1)) (50)
baaa(aaab(abba(baab(abba(baab(abbb(x1))))))) → baab(abbb(x1)) (58)
abba(baab(abba(baab(x1)))) → abbb(bbbb(bbba(baaa(aaaa(aaab(x1)))))) (116)

1.1.1.1.1.1.1.1.1.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.