Certification Problem

Input (TPDB SRS_Standard/Zantema_06/17)

The rewrite relation of the following TRS is considered.

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

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(a(x1)) → b(x1) (1)
a(a(a(x1))) → a(b(a(x1))) (2)
a(b(a(x1))) → b(b(b(x1))) (3)
a(a(a(a(x1)))) → a(a(b(a(a(x1))))) (4)
a(b(a(a(x1)))) → b(a(b(b(a(x1))))) (6)
a(a(b(a(x1)))) → a(b(b(a(b(x1))))) (5)
a(b(b(a(x1)))) → b(b(b(b(b(x1))))) (7)
a(a(a(a(a(x1))))) → a(a(a(b(a(a(a(x1))))))) (8)
a(b(a(a(a(x1))))) → b(a(a(b(b(a(a(x1))))))) (12)
a(a(b(a(a(x1))))) → a(b(a(b(a(b(a(x1))))))) (10)
a(b(b(a(a(x1))))) → b(b(a(b(b(b(a(x1))))))) (14)
a(a(a(b(a(x1))))) → a(a(b(b(a(a(b(x1))))))) (9)
a(b(a(b(a(x1))))) → b(a(b(b(b(a(b(x1))))))) (13)
a(a(b(b(a(x1))))) → a(b(b(b(a(b(b(x1))))))) (11)
a(b(b(b(a(x1))))) → b(b(b(b(b(b(b(x1))))))) (15)

1.1 Closure Under Flat Contexts

Using the flat contexts

{a(☐), b(☐)}

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

1.1.1 Semantic Labeling

Root-labeling is applied.

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

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[aa(x1)] = 1 · x1 + 1
[ab(x1)] = 1 · x1
[ba(x1)] = 1 · x1
[bb(x1)] = 1 · x1
all of the following rules can be deleted.
aa(aa(aa(x1))) → ab(ba(aa(x1))) (32)
aa(aa(ab(x1))) → ab(ba(ab(x1))) (33)
aa(aa(aa(aa(x1)))) → aa(ab(ba(aa(aa(x1))))) (34)
aa(aa(aa(ab(x1)))) → aa(ab(ba(aa(ab(x1))))) (35)
aa(ab(ba(aa(x1)))) → ab(bb(ba(ab(ba(x1))))) (36)
aa(ab(ba(ab(x1)))) → ab(bb(ba(ab(bb(x1))))) (37)
aa(ab(ba(aa(aa(x1))))) → ab(ba(ab(ba(ab(ba(aa(x1))))))) (40)
aa(ab(ba(aa(ab(x1))))) → ab(ba(ab(ba(ab(ba(ab(x1))))))) (41)
aa(aa(ab(ba(aa(x1))))) → aa(ab(bb(ba(aa(ab(ba(x1))))))) (42)
aa(ab(bb(ba(aa(x1))))) → ab(bb(bb(ba(ab(bb(ba(x1))))))) (44)
aa(ab(bb(ba(ab(x1))))) → ab(bb(bb(ba(ab(bb(bb(x1))))))) (45)
aa(aa(aa(x1))) → ab(ba(x1)) (46)
aa(aa(ab(x1))) → ab(bb(x1)) (47)
ba(aa(aa(x1))) → bb(ba(x1)) (48)
ba(aa(ab(x1))) → bb(bb(x1)) (49)
aa(ab(ba(aa(x1)))) → ab(bb(bb(ba(x1)))) (50)
aa(ab(ba(ab(x1)))) → ab(bb(bb(bb(x1)))) (51)
ba(ab(ba(aa(x1)))) → bb(bb(bb(ba(x1)))) (52)
aa(ab(ba(aa(aa(x1))))) → ab(ba(ab(bb(ba(aa(x1)))))) (54)
aa(ab(ba(aa(ab(x1))))) → ab(ba(ab(bb(ba(ab(x1)))))) (55)
ba(ab(ba(aa(aa(x1))))) → bb(ba(ab(bb(ba(aa(x1)))))) (56)
ba(ab(ba(aa(ab(x1))))) → bb(ba(ab(bb(ba(ab(x1)))))) (57)
aa(ab(bb(ba(aa(x1))))) → ab(bb(bb(bb(bb(ba(x1)))))) (58)
aa(ab(bb(ba(ab(x1))))) → ab(bb(bb(bb(bb(bb(x1)))))) (59)
ba(ab(bb(ba(aa(x1))))) → bb(bb(bb(bb(bb(ba(x1)))))) (60)
aa(ab(ba(aa(aa(aa(x1)))))) → ab(ba(aa(ab(bb(ba(aa(aa(x1)))))))) (62)
aa(ab(ba(aa(aa(ab(x1)))))) → ab(ba(aa(ab(bb(ba(aa(ab(x1)))))))) (63)
aa(ab(bb(ba(aa(aa(x1)))))) → ab(bb(ba(ab(bb(bb(ba(aa(x1)))))))) (66)
aa(ab(bb(ba(aa(ab(x1)))))) → ab(bb(ba(ab(bb(bb(ba(ab(x1)))))))) (67)
ba(ab(bb(ba(aa(aa(x1)))))) → bb(bb(ba(ab(bb(bb(ba(aa(x1)))))))) (68)
ba(ab(bb(ba(aa(ab(x1)))))) → bb(bb(ba(ab(bb(bb(ba(ab(x1)))))))) (69)
aa(ab(ba(ab(ba(aa(x1)))))) → ab(ba(ab(bb(bb(ba(ab(ba(x1)))))))) (70)
aa(ab(ba(ab(ba(ab(x1)))))) → ab(ba(ab(bb(bb(ba(ab(bb(x1)))))))) (71)
ba(ab(ba(ab(ba(aa(x1)))))) → bb(ba(ab(bb(bb(ba(ab(ba(x1)))))))) (72)
aa(ab(bb(bb(ba(aa(x1)))))) → ab(bb(bb(bb(bb(bb(bb(ba(x1)))))))) (74)
aa(ab(bb(bb(ba(ab(x1)))))) → ab(bb(bb(bb(bb(bb(bb(bb(x1)))))))) (75)
ba(ab(bb(bb(ba(aa(x1)))))) → bb(bb(bb(bb(bb(bb(bb(ba(x1)))))))) (76)

1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
aa#(aa(aa(aa(aa(x1))))) → aa#(aa(ab(ba(aa(aa(aa(x1))))))) (78)
aa#(aa(aa(aa(aa(x1))))) → aa#(ab(ba(aa(aa(aa(x1)))))) (79)
aa#(aa(aa(aa(aa(x1))))) → ba#(aa(aa(aa(x1)))) (80)
aa#(aa(aa(aa(ab(x1))))) → aa#(aa(ab(ba(aa(aa(ab(x1))))))) (81)
aa#(aa(aa(aa(ab(x1))))) → aa#(ab(ba(aa(aa(ab(x1)))))) (82)
aa#(aa(aa(aa(ab(x1))))) → ba#(aa(aa(ab(x1)))) (83)
aa#(aa(ab(ba(ab(x1))))) → aa#(ab(bb(ba(aa(ab(bb(x1))))))) (84)
aa#(aa(ab(ba(ab(x1))))) → ba#(aa(ab(bb(x1)))) (85)
aa#(aa(ab(ba(ab(x1))))) → aa#(ab(bb(x1))) (86)
ba#(ab(ba(aa(aa(aa(x1)))))) → ba#(aa(ab(bb(ba(aa(aa(x1))))))) (87)
ba#(ab(ba(aa(aa(aa(x1)))))) → aa#(ab(bb(ba(aa(aa(x1)))))) (88)
ba#(ab(ba(aa(aa(aa(x1)))))) → ba#(aa(aa(x1))) (89)
ba#(ab(ba(aa(aa(ab(x1)))))) → ba#(aa(ab(bb(ba(aa(ab(x1))))))) (90)
ba#(ab(ba(aa(aa(ab(x1)))))) → aa#(ab(bb(ba(aa(ab(x1)))))) (91)
ba#(ab(ba(aa(aa(ab(x1)))))) → ba#(aa(ab(x1))) (92)
ba#(ab(ba(ab(ba(ab(x1)))))) → ba#(ab(bb(bb(ba(ab(bb(x1))))))) (93)
ba#(ab(ba(ab(ba(ab(x1)))))) → ba#(ab(bb(x1))) (94)

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.