Certification Problem

Input (TPDB SRS_Standard/Wenzel_16/abaabababa-aababababaabab.srs)

The rewrite relation of the following TRS is considered.

a(b(a(a(b(a(b(a(b(a(x1)))))))))) → a(a(b(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(b(a(a(b(a(x1)))))))))) → b(a(b(a(a(b(a(b(a(b(a(b(a(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(b(a(a(b(a(x1))))))))))) → a(b(a(b(a(a(b(a(b(a(b(a(b(a(a(x1))))))))))))))) (3)
b(a(b(a(b(a(b(a(a(b(a(x1))))))))))) → b(b(a(b(a(a(b(a(b(a(b(a(b(a(a(x1))))))))))))))) (4)

1.1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(aa(x1))))))))))))))) (5)
aa(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ab(ba(ab(ba(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(ab(x1))))))))))))))) (6)
ba(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → bb(ba(ab(ba(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(aa(x1))))))))))))))) (7)
ba(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → bb(ba(ab(ba(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(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(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(aa(x1)))))))))))))) (9)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(aa(x1)))))))))))) (10)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(ab(ba(aa(aa(x1))))))))))) (11)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(ab(ba(ab(ba(aa(aa(x1))))))))) (12)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(ab(ba(aa(aa(x1))))))) (13)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(aa(x1))))) (14)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(aa(aa(x1))) (15)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → aa#(aa(x1)) (16)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(ab(x1)))))))))))))) (17)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(ab(x1)))))))))))) (18)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(ab(ba(aa(ab(x1))))))))))) (19)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(ab(ba(ab(ba(aa(ab(x1))))))))) (20)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(x1))))))) (21)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(x1))))) (22)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(aa(ab(x1))) (23)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → aa#(ab(x1)) (24)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(aa(x1)))))))))))))) (25)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(aa(x1)))))))))))) (26)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(ab(ba(aa(aa(x1))))))))))) (27)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(ab(ba(ab(ba(aa(aa(x1))))))))) (28)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(ab(ba(aa(aa(x1))))))) (29)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(aa(x1))))) (30)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(aa(aa(x1))) (31)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → aa#(aa(x1)) (32)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(ab(x1)))))))))))))) (33)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(ab(x1)))))))))))) (34)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(ab(ba(aa(ab(x1))))))))))) (35)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(ab(ba(ab(ba(aa(ab(x1))))))))) (36)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(x1))))))) (37)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(x1))))) (38)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(aa(ab(x1))) (39)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → aa#(ab(x1)) (40)

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

aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(aa(x1))))) (14)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(aa(x1))))) (30)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(ab(ba(aa(aa(x1))))))) (29)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → aa#(aa(x1)) (16)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(x1))))))) (21)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(ab(x1)))))))))))) (34)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(ab(ba(ab(ba(aa(aa(x1))))))))) (12)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → aa#(aa(x1)) (32)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(ab(x1)))))))))))) (18)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(ab(ba(aa(ab(x1))))))) (37)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(aa(aa(x1))) (31)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(aa(x1)))))))))))) (10)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(ab(x1)))))))))))))) (17)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(ab(ba(aa(ab(x1))))))))))) (35)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(aa(x1)))))))))))))) (9)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(ab(ba(aa(aa(x1))))))))))) (11)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(aa(ab(x1))) (23)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(ab(ba(aa(aa(x1))))))))))) (27)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(ab(x1)))))))))))))) (33)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(aa(aa(x1))) (15)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → aa#(ab(ba(ab(ba(ab(ba(ab(ba(aa(ab(x1))))))))))) (19)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(aa(ab(x1))) (39)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(aa(x1)))))))))))) (26)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → aa#(ab(x1)) (24)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(ab(ba(ab(ba(aa(ab(x1))))))))) (20)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → aa#(ab(x1)) (40)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(x1))))) (22)
aa#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(ab(ba(aa(aa(x1))))))) (13)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(aa(ab(ba(ab(ba(ab(ba(ab(ba(aa(aa(x1)))))))))))))) (25)
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)] = 0
[ba(x1)] = 1 + 1x1
[aa#(x1)] = 0
[ba#(x1)] = 0
[ab(x1)] = 1x1
[aa(x1)] = 0

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

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
[ab(x1)] = 2 + x1
[ba(x1)] = 2 + x1
[aa(x1)] = 2 · x1
[bb(x1)] = -2
the pairs
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(aa(x1))))))))))) → ba#(ab(ba(ab(ba(ab(ba(aa(aa(x1))))))))) (28)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(ab(ba(ab(ba(aa(ab(x1))))))))) (36)
ba#(ab(ba(ab(ba(ab(ba(aa(ab(ba(ab(x1))))))))))) → ba#(ab(ba(aa(ab(x1))))) (38)
could be deleted.

1.1.1.1.1.2.1 P is empty

There are no pairs anymore.