Certification Problem

Input (TPDB SRS_Standard/Zantema_06/18)

The rewrite relation of the following TRS is considered.

a(a(x1)) → b(a(b(x1))) (1)
a(a(a(x1))) → a(b(a(b(a(x1))))) (2)
a(b(a(x1))) → b(b(a(b(b(x1))))) (3)
a(a(a(a(x1)))) → a(a(b(a(b(a(a(x1))))))) (4)
a(a(b(a(x1)))) → a(b(b(a(b(a(b(x1))))))) (5)
a(b(a(a(x1)))) → b(a(b(a(b(b(a(x1))))))) (6)
a(b(b(a(x1)))) → b(b(b(a(b(b(b(x1))))))) (7)
a(a(a(a(a(x1))))) → a(a(a(b(a(b(a(a(a(x1))))))))) (8)
a(a(a(b(a(x1))))) → a(a(b(b(a(b(a(a(b(x1))))))))) (9)
a(a(b(a(a(x1))))) → a(b(a(b(a(b(a(b(a(x1))))))))) (10)
a(a(b(b(a(x1))))) → a(b(b(b(a(b(a(b(b(x1))))))))) (11)
a(b(a(a(a(x1))))) → b(a(a(b(a(b(b(a(a(x1))))))))) (12)
a(b(a(b(a(x1))))) → b(a(b(b(a(b(b(a(b(x1))))))))) (13)
a(b(b(a(a(x1))))) → b(b(a(b(a(b(b(b(a(x1))))))))) (14)
a(b(b(b(a(x1))))) → b(b(b(b(a(b(b(b(b(x1))))))))) (15)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

{a(☐), b(☐)}

We obtain the transformed TRS
a(a(a(x1))) → a(b(a(b(x1)))) (16)
b(a(a(x1))) → b(b(a(b(x1)))) (17)
a(a(a(x1))) → a(b(a(b(a(x1))))) (2)
a(a(b(a(x1)))) → a(b(b(a(b(b(x1)))))) (18)
b(a(b(a(x1)))) → b(b(b(a(b(b(x1)))))) (19)
a(a(a(a(x1)))) → a(a(b(a(b(a(a(x1))))))) (4)
a(a(b(a(x1)))) → a(b(b(a(b(a(b(x1))))))) (5)
a(a(b(a(a(x1))))) → a(b(a(b(a(b(b(a(x1)))))))) (20)
b(a(b(a(a(x1))))) → b(b(a(b(a(b(b(a(x1)))))))) (21)
a(a(b(b(a(x1))))) → a(b(b(b(a(b(b(b(x1)))))))) (22)
b(a(b(b(a(x1))))) → b(b(b(b(a(b(b(b(x1)))))))) (23)
a(a(a(a(a(x1))))) → a(a(a(b(a(b(a(a(a(x1))))))))) (8)
a(a(a(b(a(x1))))) → a(a(b(b(a(b(a(a(b(x1))))))))) (9)
a(a(b(a(a(x1))))) → a(b(a(b(a(b(a(b(a(x1))))))))) (10)
a(a(b(b(a(x1))))) → a(b(b(b(a(b(a(b(b(x1))))))))) (11)
a(a(b(a(a(a(x1)))))) → a(b(a(a(b(a(b(b(a(a(x1)))))))))) (24)
b(a(b(a(a(a(x1)))))) → b(b(a(a(b(a(b(b(a(a(x1)))))))))) (25)
a(a(b(a(b(a(x1)))))) → a(b(a(b(b(a(b(b(a(b(x1)))))))))) (26)
b(a(b(a(b(a(x1)))))) → b(b(a(b(b(a(b(b(a(b(x1)))))))))) (27)
a(a(b(b(a(a(x1)))))) → a(b(b(a(b(a(b(b(b(a(x1)))))))))) (28)
b(a(b(b(a(a(x1)))))) → b(b(b(a(b(a(b(b(b(a(x1)))))))))) (29)
a(a(b(b(b(a(x1)))))) → a(b(b(b(b(a(b(b(b(b(x1)))))))))) (30)
b(a(b(b(b(a(x1)))))) → b(b(b(b(b(a(b(b(b(b(x1)))))))))) (31)

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
aa(aa(aa(x1))) → ab(ba(ab(ba(x1)))) (32)
aa(aa(ab(x1))) → ab(ba(ab(bb(x1)))) (33)
ba(aa(aa(x1))) → bb(ba(ab(ba(x1)))) (34)
ba(aa(ab(x1))) → bb(ba(ab(bb(x1)))) (35)
aa(aa(aa(x1))) → ab(ba(ab(ba(aa(x1))))) (36)
aa(aa(ab(x1))) → ab(ba(ab(ba(ab(x1))))) (37)
aa(ab(ba(aa(x1)))) → ab(bb(ba(ab(bb(ba(x1)))))) (38)
aa(ab(ba(ab(x1)))) → ab(bb(ba(ab(bb(bb(x1)))))) (39)
ba(ab(ba(aa(x1)))) → bb(bb(ba(ab(bb(ba(x1)))))) (40)
ba(ab(ba(ab(x1)))) → bb(bb(ba(ab(bb(bb(x1)))))) (41)
aa(aa(aa(aa(x1)))) → aa(ab(ba(ab(ba(aa(aa(x1))))))) (42)
aa(aa(aa(ab(x1)))) → aa(ab(ba(ab(ba(aa(ab(x1))))))) (43)
aa(ab(ba(aa(x1)))) → ab(bb(ba(ab(ba(ab(ba(x1))))))) (44)
aa(ab(ba(ab(x1)))) → ab(bb(ba(ab(ba(ab(bb(x1))))))) (45)
aa(ab(ba(aa(aa(x1))))) → ab(ba(ab(ba(ab(bb(ba(aa(x1)))))))) (46)
aa(ab(ba(aa(ab(x1))))) → ab(ba(ab(ba(ab(bb(ba(ab(x1)))))))) (47)
ba(ab(ba(aa(aa(x1))))) → bb(ba(ab(ba(ab(bb(ba(aa(x1)))))))) (48)
ba(ab(ba(aa(ab(x1))))) → bb(ba(ab(ba(ab(bb(ba(ab(x1)))))))) (49)
aa(ab(bb(ba(aa(x1))))) → ab(bb(bb(ba(ab(bb(bb(ba(x1)))))))) (50)
aa(ab(bb(ba(ab(x1))))) → ab(bb(bb(ba(ab(bb(bb(bb(x1)))))))) (51)
ba(ab(bb(ba(aa(x1))))) → bb(bb(bb(ba(ab(bb(bb(ba(x1)))))))) (52)
ba(ab(bb(ba(ab(x1))))) → bb(bb(bb(ba(ab(bb(bb(bb(x1)))))))) (53)
aa(aa(aa(aa(aa(x1))))) → aa(aa(ab(ba(ab(ba(aa(aa(aa(x1))))))))) (54)
aa(aa(aa(aa(ab(x1))))) → aa(aa(ab(ba(ab(ba(aa(aa(ab(x1))))))))) (55)
aa(aa(ab(ba(aa(x1))))) → aa(ab(bb(ba(ab(ba(aa(ab(ba(x1))))))))) (56)
aa(aa(ab(ba(ab(x1))))) → aa(ab(bb(ba(ab(ba(aa(ab(bb(x1))))))))) (57)
aa(ab(ba(aa(aa(x1))))) → ab(ba(ab(ba(ab(ba(ab(ba(aa(x1))))))))) (58)
aa(ab(ba(aa(ab(x1))))) → ab(ba(ab(ba(ab(ba(ab(ba(ab(x1))))))))) (59)
aa(ab(bb(ba(aa(x1))))) → ab(bb(bb(ba(ab(ba(ab(bb(ba(x1))))))))) (60)
aa(ab(bb(ba(ab(x1))))) → ab(bb(bb(ba(ab(ba(ab(bb(bb(x1))))))))) (61)
aa(ab(ba(aa(aa(aa(x1)))))) → ab(ba(aa(ab(ba(ab(bb(ba(aa(aa(x1)))))))))) (62)
aa(ab(ba(aa(aa(ab(x1)))))) → ab(ba(aa(ab(ba(ab(bb(ba(aa(ab(x1)))))))))) (63)
ba(ab(ba(aa(aa(aa(x1)))))) → bb(ba(aa(ab(ba(ab(bb(ba(aa(aa(x1)))))))))) (64)
ba(ab(ba(aa(aa(ab(x1)))))) → bb(ba(aa(ab(ba(ab(bb(ba(aa(ab(x1)))))))))) (65)
aa(ab(ba(ab(ba(aa(x1)))))) → ab(ba(ab(bb(ba(ab(bb(ba(ab(ba(x1)))))))))) (66)
aa(ab(ba(ab(ba(ab(x1)))))) → ab(ba(ab(bb(ba(ab(bb(ba(ab(bb(x1)))))))))) (67)
ba(ab(ba(ab(ba(aa(x1)))))) → bb(ba(ab(bb(ba(ab(bb(ba(ab(ba(x1)))))))))) (68)
ba(ab(ba(ab(ba(ab(x1)))))) → bb(ba(ab(bb(ba(ab(bb(ba(ab(bb(x1)))))))))) (69)
aa(ab(bb(ba(aa(aa(x1)))))) → ab(bb(ba(ab(ba(ab(bb(bb(ba(aa(x1)))))))))) (70)
aa(ab(bb(ba(aa(ab(x1)))))) → ab(bb(ba(ab(ba(ab(bb(bb(ba(ab(x1)))))))))) (71)
ba(ab(bb(ba(aa(aa(x1)))))) → bb(bb(ba(ab(ba(ab(bb(bb(ba(aa(x1)))))))))) (72)
ba(ab(bb(ba(aa(ab(x1)))))) → bb(bb(ba(ab(ba(ab(bb(bb(ba(ab(x1)))))))))) (73)
aa(ab(bb(bb(ba(aa(x1)))))) → ab(bb(bb(bb(ba(ab(bb(bb(bb(ba(x1)))))))))) (74)
aa(ab(bb(bb(ba(ab(x1)))))) → ab(bb(bb(bb(ba(ab(bb(bb(bb(bb(x1)))))))))) (75)
ba(ab(bb(bb(ba(aa(x1)))))) → bb(bb(bb(bb(ba(ab(bb(bb(bb(ba(x1)))))))))) (76)
ba(ab(bb(bb(ba(ab(x1)))))) → bb(bb(bb(bb(ba(ab(bb(bb(bb(bb(x1)))))))))) (77)

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.

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

1.1.1.1 Reduction Pair Processor with Usable Rules

Using the
prec(ba#) = 0 stat(ba#) = lex
prec(aa#) = 0 stat(aa#) = lex
prec(bb) = 0 stat(bb) = lex
prec(ba) = 0 stat(ba) = lex
prec(ab) = 0 stat(ab) = lex
prec(aa) = 0 stat(aa) = lex

π(ba#) = 1
π(aa#) = 1
π(bb) = 1
π(ba) = 1
π(ab) = 1
π(aa) = [1]

together with the usable rules
aa(aa(aa(x1))) → ab(ba(ab(ba(x1)))) (32)
aa(aa(ab(x1))) → ab(ba(ab(bb(x1)))) (33)
ba(aa(aa(x1))) → bb(ba(ab(ba(x1)))) (34)
ba(aa(ab(x1))) → bb(ba(ab(bb(x1)))) (35)
aa(aa(aa(x1))) → ab(ba(ab(ba(aa(x1))))) (36)
aa(aa(ab(x1))) → ab(ba(ab(ba(ab(x1))))) (37)
aa(ab(ba(aa(x1)))) → ab(bb(ba(ab(bb(ba(x1)))))) (38)
aa(ab(ba(ab(x1)))) → ab(bb(ba(ab(bb(bb(x1)))))) (39)
ba(ab(ba(aa(x1)))) → bb(bb(ba(ab(bb(ba(x1)))))) (40)
ba(ab(ba(ab(x1)))) → bb(bb(ba(ab(bb(bb(x1)))))) (41)
aa(aa(aa(aa(x1)))) → aa(ab(ba(ab(ba(aa(aa(x1))))))) (42)
aa(aa(aa(ab(x1)))) → aa(ab(ba(ab(ba(aa(ab(x1))))))) (43)
aa(ab(ba(aa(x1)))) → ab(bb(ba(ab(ba(ab(ba(x1))))))) (44)
aa(ab(ba(ab(x1)))) → ab(bb(ba(ab(ba(ab(bb(x1))))))) (45)
aa(ab(ba(aa(aa(x1))))) → ab(ba(ab(ba(ab(bb(ba(aa(x1)))))))) (46)
aa(ab(ba(aa(ab(x1))))) → ab(ba(ab(ba(ab(bb(ba(ab(x1)))))))) (47)
ba(ab(ba(aa(aa(x1))))) → bb(ba(ab(ba(ab(bb(ba(aa(x1)))))))) (48)
ba(ab(ba(aa(ab(x1))))) → bb(ba(ab(ba(ab(bb(ba(ab(x1)))))))) (49)
aa(ab(bb(ba(aa(x1))))) → ab(bb(bb(ba(ab(bb(bb(ba(x1)))))))) (50)
aa(ab(bb(ba(ab(x1))))) → ab(bb(bb(ba(ab(bb(bb(bb(x1)))))))) (51)
ba(ab(bb(ba(aa(x1))))) → bb(bb(bb(ba(ab(bb(bb(ba(x1)))))))) (52)
ba(ab(bb(ba(ab(x1))))) → bb(bb(bb(ba(ab(bb(bb(bb(x1)))))))) (53)
aa(aa(aa(aa(aa(x1))))) → aa(aa(ab(ba(ab(ba(aa(aa(aa(x1))))))))) (54)
aa(aa(aa(aa(ab(x1))))) → aa(aa(ab(ba(ab(ba(aa(aa(ab(x1))))))))) (55)
aa(aa(ab(ba(aa(x1))))) → aa(ab(bb(ba(ab(ba(aa(ab(ba(x1))))))))) (56)
aa(aa(ab(ba(ab(x1))))) → aa(ab(bb(ba(ab(ba(aa(ab(bb(x1))))))))) (57)
aa(ab(ba(aa(aa(x1))))) → ab(ba(ab(ba(ab(ba(ab(ba(aa(x1))))))))) (58)
aa(ab(ba(aa(ab(x1))))) → ab(ba(ab(ba(ab(ba(ab(ba(ab(x1))))))))) (59)
aa(ab(bb(ba(aa(x1))))) → ab(bb(bb(ba(ab(ba(ab(bb(ba(x1))))))))) (60)
aa(ab(bb(ba(ab(x1))))) → ab(bb(bb(ba(ab(ba(ab(bb(bb(x1))))))))) (61)
aa(ab(ba(aa(aa(aa(x1)))))) → ab(ba(aa(ab(ba(ab(bb(ba(aa(aa(x1)))))))))) (62)
aa(ab(ba(aa(aa(ab(x1)))))) → ab(ba(aa(ab(ba(ab(bb(ba(aa(ab(x1)))))))))) (63)
ba(ab(ba(aa(aa(aa(x1)))))) → bb(ba(aa(ab(ba(ab(bb(ba(aa(aa(x1)))))))))) (64)
ba(ab(ba(aa(aa(ab(x1)))))) → bb(ba(aa(ab(ba(ab(bb(ba(aa(ab(x1)))))))))) (65)
aa(ab(ba(ab(ba(aa(x1)))))) → ab(ba(ab(bb(ba(ab(bb(ba(ab(ba(x1)))))))))) (66)
aa(ab(ba(ab(ba(ab(x1)))))) → ab(ba(ab(bb(ba(ab(bb(ba(ab(bb(x1)))))))))) (67)
ba(ab(ba(ab(ba(aa(x1)))))) → bb(ba(ab(bb(ba(ab(bb(ba(ab(ba(x1)))))))))) (68)
ba(ab(ba(ab(ba(ab(x1)))))) → bb(ba(ab(bb(ba(ab(bb(ba(ab(bb(x1)))))))))) (69)
aa(ab(bb(ba(aa(aa(x1)))))) → ab(bb(ba(ab(ba(ab(bb(bb(ba(aa(x1)))))))))) (70)
aa(ab(bb(ba(aa(ab(x1)))))) → ab(bb(ba(ab(ba(ab(bb(bb(ba(ab(x1)))))))))) (71)
ba(ab(bb(ba(aa(aa(x1)))))) → bb(bb(ba(ab(ba(ab(bb(bb(ba(aa(x1)))))))))) (72)
ba(ab(bb(ba(aa(ab(x1)))))) → bb(bb(ba(ab(ba(ab(bb(bb(ba(ab(x1)))))))))) (73)
aa(ab(bb(bb(ba(aa(x1)))))) → ab(bb(bb(bb(ba(ab(bb(bb(bb(ba(x1)))))))))) (74)
aa(ab(bb(bb(ba(ab(x1)))))) → ab(bb(bb(bb(ba(ab(bb(bb(bb(bb(x1)))))))))) (75)
ba(ab(bb(bb(ba(aa(x1)))))) → bb(bb(bb(bb(ba(ab(bb(bb(bb(ba(x1)))))))))) (76)
ba(ab(bb(bb(ba(ab(x1)))))) → bb(bb(bb(bb(ba(ab(bb(bb(bb(bb(x1)))))))))) (77)
(w.r.t. the implicit argument filter of the reduction pair), the pairs
aa#(aa(aa(x1))) → ba#(x1) (78)
aa#(aa(aa(x1))) → ba#(ab(ba(x1))) (79)
aa#(aa(ab(x1))) → ba#(ab(bb(x1))) (80)
ba#(aa(aa(x1))) → ba#(x1) (81)
ba#(aa(aa(x1))) → ba#(ab(ba(x1))) (82)
ba#(aa(ab(x1))) → ba#(ab(bb(x1))) (83)
aa#(aa(aa(x1))) → ba#(aa(x1)) (84)
aa#(aa(aa(x1))) → ba#(ab(ba(aa(x1)))) (85)
aa#(aa(ab(x1))) → ba#(ab(x1)) (86)
aa#(aa(ab(x1))) → ba#(ab(ba(ab(x1)))) (87)
aa#(ab(ba(aa(x1)))) → ba#(x1) (88)
aa#(ab(ba(aa(x1)))) → ba#(ab(bb(ba(x1)))) (89)
ba#(ab(ba(aa(x1)))) → ba#(x1) (91)
ba#(ab(ba(aa(x1)))) → ba#(ab(bb(ba(x1)))) (92)
aa#(aa(aa(aa(x1)))) → ba#(aa(aa(x1))) (94)
aa#(aa(aa(aa(x1)))) → ba#(ab(ba(aa(aa(x1))))) (95)
aa#(aa(aa(aa(x1)))) → aa#(ab(ba(ab(ba(aa(aa(x1))))))) (96)
aa#(aa(aa(ab(x1)))) → ba#(aa(ab(x1))) (97)
aa#(aa(aa(ab(x1)))) → ba#(ab(ba(aa(ab(x1))))) (98)
aa#(aa(aa(ab(x1)))) → aa#(ab(ba(ab(ba(aa(ab(x1))))))) (99)
aa#(ab(ba(aa(x1)))) → ba#(ab(ba(x1))) (100)
aa#(ab(ba(aa(x1)))) → ba#(ab(ba(ab(ba(x1))))) (101)
aa#(ab(ba(aa(aa(x1))))) → ba#(aa(x1)) (104)
aa#(ab(ba(aa(aa(x1))))) → ba#(ab(bb(ba(aa(x1))))) (105)
aa#(ab(ba(aa(aa(x1))))) → ba#(ab(ba(ab(bb(ba(aa(x1))))))) (106)
aa#(ab(ba(aa(ab(x1))))) → ba#(ab(x1)) (107)
aa#(ab(ba(aa(ab(x1))))) → ba#(ab(bb(ba(ab(x1))))) (108)
aa#(ab(ba(aa(ab(x1))))) → ba#(ab(ba(ab(bb(ba(ab(x1))))))) (109)
ba#(ab(ba(aa(aa(x1))))) → ba#(aa(x1)) (110)
ba#(ab(ba(aa(aa(x1))))) → ba#(ab(bb(ba(aa(x1))))) (111)
ba#(ab(ba(aa(aa(x1))))) → ba#(ab(ba(ab(bb(ba(aa(x1))))))) (112)
ba#(ab(ba(aa(ab(x1))))) → ba#(ab(x1)) (113)
ba#(ab(ba(aa(ab(x1))))) → ba#(ab(bb(ba(ab(x1))))) (114)
ba#(ab(ba(aa(ab(x1))))) → ba#(ab(ba(ab(bb(ba(ab(x1))))))) (115)
aa#(ab(bb(ba(aa(x1))))) → ba#(x1) (116)
aa#(ab(bb(ba(aa(x1))))) → ba#(ab(bb(bb(ba(x1))))) (117)
ba#(ab(bb(ba(aa(x1))))) → ba#(x1) (119)
ba#(ab(bb(ba(aa(x1))))) → ba#(ab(bb(bb(ba(x1))))) (120)
aa#(aa(aa(aa(aa(x1))))) → ba#(aa(aa(aa(x1)))) (122)
aa#(aa(aa(aa(aa(x1))))) → ba#(ab(ba(aa(aa(aa(x1)))))) (123)
aa#(aa(aa(aa(aa(x1))))) → aa#(ab(ba(ab(ba(aa(aa(aa(x1)))))))) (124)
aa#(aa(aa(aa(ab(x1))))) → ba#(aa(aa(ab(x1)))) (126)
aa#(aa(aa(aa(ab(x1))))) → ba#(ab(ba(aa(aa(ab(x1)))))) (127)
aa#(aa(aa(aa(ab(x1))))) → aa#(ab(ba(ab(ba(aa(aa(ab(x1)))))))) (128)
aa#(aa(ab(ba(aa(x1))))) → ba#(x1) (130)
aa#(aa(ab(ba(aa(x1))))) → aa#(ab(ba(x1))) (131)
aa#(aa(ab(ba(aa(x1))))) → ba#(aa(ab(ba(x1)))) (132)
aa#(aa(ab(ba(aa(x1))))) → ba#(ab(ba(aa(ab(ba(x1)))))) (133)
aa#(aa(ab(ba(aa(x1))))) → aa#(ab(bb(ba(ab(ba(aa(ab(ba(x1))))))))) (134)
aa#(aa(ab(ba(ab(x1))))) → aa#(ab(bb(x1))) (135)
aa#(ab(ba(aa(aa(x1))))) → ba#(ab(ba(aa(x1)))) (139)
aa#(ab(ba(aa(aa(x1))))) → ba#(ab(ba(ab(ba(aa(x1)))))) (140)
aa#(ab(ba(aa(aa(x1))))) → ba#(ab(ba(ab(ba(ab(ba(aa(x1)))))))) (141)
aa#(ab(ba(aa(ab(x1))))) → ba#(ab(ba(ab(x1)))) (142)
aa#(ab(ba(aa(ab(x1))))) → ba#(ab(ba(ab(ba(ab(x1)))))) (143)
aa#(ab(ba(aa(ab(x1))))) → ba#(ab(ba(ab(ba(ab(ba(ab(x1)))))))) (144)
aa#(ab(bb(ba(aa(x1))))) → ba#(ab(bb(ba(x1)))) (145)
aa#(ab(bb(ba(aa(x1))))) → ba#(ab(ba(ab(bb(ba(x1)))))) (146)
aa#(ab(ba(aa(aa(aa(x1)))))) → ba#(aa(aa(x1))) (149)
aa#(ab(ba(aa(aa(aa(x1)))))) → ba#(ab(bb(ba(aa(aa(x1)))))) (150)
aa#(ab(ba(aa(aa(aa(x1)))))) → aa#(ab(ba(ab(bb(ba(aa(aa(x1)))))))) (151)
aa#(ab(ba(aa(aa(ab(x1)))))) → ba#(aa(ab(x1))) (153)
aa#(ab(ba(aa(aa(ab(x1)))))) → ba#(ab(bb(ba(aa(ab(x1)))))) (154)
aa#(ab(ba(aa(aa(ab(x1)))))) → aa#(ab(ba(ab(bb(ba(aa(ab(x1)))))))) (155)
ba#(ab(ba(aa(aa(aa(x1)))))) → ba#(aa(aa(x1))) (157)
ba#(ab(ba(aa(aa(aa(x1)))))) → ba#(ab(bb(ba(aa(aa(x1)))))) (158)
ba#(ab(ba(aa(aa(aa(x1)))))) → aa#(ab(ba(ab(bb(ba(aa(aa(x1)))))))) (159)
ba#(ab(ba(aa(aa(ab(x1)))))) → ba#(aa(ab(x1))) (161)
ba#(ab(ba(aa(aa(ab(x1)))))) → ba#(ab(bb(ba(aa(ab(x1)))))) (162)
ba#(ab(ba(aa(aa(ab(x1)))))) → aa#(ab(ba(ab(bb(ba(aa(ab(x1)))))))) (163)
aa#(ab(ba(ab(ba(aa(x1)))))) → ba#(x1) (165)
aa#(ab(ba(ab(ba(aa(x1)))))) → ba#(ab(ba(x1))) (166)
aa#(ab(ba(ab(ba(aa(x1)))))) → ba#(ab(bb(ba(ab(ba(x1)))))) (167)
aa#(ab(ba(ab(ba(aa(x1)))))) → ba#(ab(bb(ba(ab(bb(ba(ab(ba(x1))))))))) (168)
ba#(ab(ba(ab(ba(aa(x1)))))) → ba#(x1) (172)
ba#(ab(ba(ab(ba(aa(x1)))))) → ba#(ab(ba(x1))) (173)
ba#(ab(ba(ab(ba(aa(x1)))))) → ba#(ab(bb(ba(ab(ba(x1)))))) (174)
ba#(ab(ba(ab(ba(aa(x1)))))) → ba#(ab(bb(ba(ab(bb(ba(ab(ba(x1))))))))) (175)
aa#(ab(bb(ba(aa(aa(x1)))))) → ba#(aa(x1)) (179)
aa#(ab(bb(ba(aa(aa(x1)))))) → ba#(ab(bb(bb(ba(aa(x1)))))) (180)
aa#(ab(bb(ba(aa(aa(x1)))))) → ba#(ab(ba(ab(bb(bb(ba(aa(x1)))))))) (181)
aa#(ab(bb(ba(aa(ab(x1)))))) → ba#(ab(x1)) (182)
aa#(ab(bb(ba(aa(ab(x1)))))) → ba#(ab(bb(bb(ba(ab(x1)))))) (183)
aa#(ab(bb(ba(aa(ab(x1)))))) → ba#(ab(ba(ab(bb(bb(ba(ab(x1)))))))) (184)
ba#(ab(bb(ba(aa(aa(x1)))))) → ba#(aa(x1)) (185)
ba#(ab(bb(ba(aa(aa(x1)))))) → ba#(ab(bb(bb(ba(aa(x1)))))) (186)
ba#(ab(bb(ba(aa(aa(x1)))))) → ba#(ab(ba(ab(bb(bb(ba(aa(x1)))))))) (187)
ba#(ab(bb(ba(aa(ab(x1)))))) → ba#(ab(x1)) (188)
ba#(ab(bb(ba(aa(ab(x1)))))) → ba#(ab(bb(bb(ba(ab(x1)))))) (189)
ba#(ab(bb(ba(aa(ab(x1)))))) → ba#(ab(ba(ab(bb(bb(ba(ab(x1)))))))) (190)
aa#(ab(bb(bb(ba(aa(x1)))))) → ba#(x1) (191)
aa#(ab(bb(bb(ba(aa(x1)))))) → ba#(ab(bb(bb(bb(ba(x1)))))) (192)
ba#(ab(bb(bb(ba(aa(x1)))))) → ba#(x1) (194)
ba#(ab(bb(bb(ba(aa(x1)))))) → ba#(ab(bb(bb(bb(ba(x1)))))) (195)
could be deleted.

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.