Certification Problem

Input (TPDB SRS_Standard/Wenzel_16/ababaababa-abaabababaabab.srs)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
a(b(a(b(a(a(b(a(b(a(x1)))))))))) → b(a(b(a(a(b(a(b(a(b(a(a(b(a(x1)))))))))))))) (2)

1.1 Closure Under Flat Contexts

Using the flat contexts

{a(☐), b(☐)}

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

1.1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
aa(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))))))) (5)
aa(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))))))) (6)
ba(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → bb(ba(ab(ba(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))))))) (7)
ba(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → bb(ba(ab(ba(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))))))) (8)

1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1)))))))))))))) (9)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1)))))))))))) (10)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) (11)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))) (12)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(ab(ba(aa(x1))))))) (13)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(aa(ab(ba(aa(x1))))) (14)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → aa#(ab(ba(aa(x1)))) (15)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1)))))))))))))) (16)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1)))))))))))) (17)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) (18)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))) (19)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(x1))))))) (20)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(aa(ab(ba(ab(x1))))) (21)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → aa#(ab(ba(ab(x1)))) (22)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1)))))))))))))) (23)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1)))))))))))) (24)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) (25)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))) (26)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(ab(ba(aa(x1))))))) (27)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(aa(ab(ba(aa(x1))))) (28)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → aa#(ab(ba(aa(x1)))) (29)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1)))))))))))))) (30)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1)))))))))))) (31)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) (32)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))) (33)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(x1))))))) (34)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(aa(ab(ba(ab(x1))))) (35)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → aa#(ab(ba(ab(x1)))) (36)

1.1.1.1.1 Split

We split (P,R) into the relative DP-problem (PD,P-PD,RD,R-RD) and (P-PD,R-RD) where the pairs PD

ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1)))))))))))) (24)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(x1))))))) (20)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1)))))))))))) (10)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) (25)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(ab(ba(aa(x1))))))) (13)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(x1))))))) (34)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → aa#(ab(ba(ab(x1)))) (36)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → aa#(ab(ba(aa(x1)))) (15)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) (32)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → aa#(ab(ba(ab(x1)))) (22)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) (18)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1)))))))))))))) (30)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(aa(ab(ba(ab(x1))))) (21)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → aa#(ab(ba(aa(x1)))) (29)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) (11)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(ab(ba(aa(x1))))))) (27)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1)))))))))))))) (9)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(aa(ab(ba(aa(x1))))) (14)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(aa(ab(ba(aa(x1))))) (28)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))) (19)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))) (12)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1)))))))))))))) (16)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1)))))))))))) (31)
aa#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1)))))))))))) (17)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1)))))))))))))) (23)
and the rules RD

There are no rules.

are deleted.

1.1.1.1.1.1 Semantic Labeling Processor

The following interpretations form a model of the rules.

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

[bb(x1)] = 1
[ba(x1)] = 1 + 1x1
[aa#(x1)] = 0
[ba#(x1)] = 0
[ab(x1)] = 1x1
[aa(x1)] = 0

We obtain the set of labeled pairs
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → ba#1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa0(x1)))))))))))))) (37)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → ba#1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa0(x1)))))))))))))) (38)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → ba#1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa1(x1)))))))))))))) (39)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → ba#1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa1(x1)))))))))))))) (40)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → ba#0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa0(x1)))))))))))) (41)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → ba#0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa1(x1)))))))))))) (42)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → aa#1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa0(x1))))))))))) (43)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → aa#1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa1(x1))))))))))) (44)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → ba#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa0(x1))))))))) (45)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → ba#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa1(x1))))))))) (46)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → ba#1(ab1(ba0(aa1(ab1(ba0(aa0(x1))))))) (47)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → ba#1(ab1(ba0(aa1(ab1(ba0(aa1(x1))))))) (48)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → ba#0(aa1(ab1(ba0(aa0(x1))))) (49)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → ba#0(aa1(ab1(ba0(aa1(x1))))) (50)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → aa#1(ab1(ba0(aa0(x1)))) (51)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → aa#1(ab1(ba0(aa1(x1)))) (52)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → ba#1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(x1)))))))))))))) (53)
ba#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → ba#1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(x1)))))))))))))) (54)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → ba#0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(x1)))))))))))) (55)
ba#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → ba#0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(x1)))))))))))) (56)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → aa#1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(x1))))))))))) (57)
ba#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → aa#1(ab1(ba0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(x1))))))))))) (58)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → ba#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(x1))))))))) (59)
ba#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(x1))))))))) (60)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → ba#1(ab1(ba0(aa1(ab1(ba0(ab0(x1))))))) (61)
ba#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → ba#1(ab1(ba0(aa0(ab0(ba1(ab1(x1))))))) (62)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → ba#0(aa1(ab1(ba0(ab0(x1))))) (63)
ba#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → ba#0(aa0(ab0(ba1(ab1(x1))))) (64)
ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → aa#1(ab1(ba0(ab0(x1)))) (65)
ba#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → aa#0(ab0(ba1(ab1(x1)))) (66)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → ba#0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa0(x1)))))))))))) (67)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → ba#0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa1(x1)))))))))))) (68)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → aa#1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa0(x1))))))))))) (69)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → aa#1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa1(x1))))))))))) (70)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → ba#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa0(x1))))))))) (71)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → ba#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa1(x1))))))))) (72)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → ba#1(ab1(ba0(aa1(ab1(ba0(aa0(x1))))))) (73)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → ba#1(ab1(ba0(aa1(ab1(ba0(aa1(x1))))))) (74)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → ba#0(aa1(ab1(ba0(aa0(x1))))) (75)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → ba#0(aa1(ab1(ba0(aa1(x1))))) (76)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → aa#1(ab1(ba0(aa0(x1)))) (77)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → aa#1(ab1(ba0(aa1(x1)))) (78)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → ba#1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(x1)))))))))))))) (79)
aa#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → ba#1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(x1)))))))))))))) (80)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → ba#0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(x1)))))))))))) (81)
aa#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → ba#0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(x1)))))))))))) (82)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → aa#1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(x1))))))))))) (83)
aa#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → aa#1(ab1(ba0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(x1))))))))))) (84)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → ba#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(x1))))))))) (85)
aa#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → ba#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(x1))))))))) (86)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → ba#1(ab1(ba0(aa1(ab1(ba0(ab0(x1))))))) (87)
aa#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → ba#1(ab1(ba0(aa0(ab0(ba1(ab1(x1))))))) (88)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → ba#0(aa1(ab1(ba0(ab0(x1))))) (89)
aa#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → ba#0(aa0(ab0(ba1(ab1(x1))))) (90)
aa#0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → aa#1(ab1(ba0(ab0(x1)))) (91)
aa#0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → aa#0(ab0(ba1(ab1(x1)))) (92)
and the set of labeled rules:
aa0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa0(x1))))))))))))))) (93)
aa0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa1(x1))))))))))))))) (94)
aa0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(x1))))))))))))))) (95)
aa0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(x1))))))))))))))) (96)
ba0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa0(x1))))))))))) → bb0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa0(x1))))))))))))))) (97)
ba0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(aa1(x1))))))))))) → bb0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(aa1(x1))))))))))))))) (98)
ba0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(ba0(ab0(x1))))))))))) → bb0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(x1))))))))))))))) (99)
ba0(ab0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(x1))))))))))) → bb0(ba1(ab1(ba0(aa1(ab1(ba0(ab0(ba1(ab1(ba0(aa0(ab0(ba1(ab1(x1))))))))))))))) (100)

1.1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.

1.1.1.1.1.2 Reduction Pair Processor

Using the linear polynomial interpretation over the naturals
[ba#(x1)] = -2 + 2 · x1
[aa(x1)] = 2 · x1
[ab(x1)] = 1 + x1
[ba(x1)] = x1
[bb(x1)] = 1
the pairs
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(aa(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))) (26)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))) (33)
ba#(ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(x1))))))))))) → ba#(aa(ab(ba(ab(x1))))) (35)
could be deleted.

1.1.1.1.1.2.1 P is empty

There are no pairs anymore.