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 AProVE @ 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(a(x1))))) (2)
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(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(a(x1))) → a(b(a(b(x1)))) (16)
b(a(a(x1))) → b(b(a(b(x1)))) (17)
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(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(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(aa(x1))))) (32)
aa(aa(ab(x1))) → ab(ba(ab(ba(ab(x1))))) (33)
aa(aa(aa(aa(x1)))) → aa(ab(ba(ab(ba(aa(aa(x1))))))) (34)
aa(aa(aa(ab(x1)))) → aa(ab(ba(ab(ba(aa(ab(x1))))))) (35)
aa(ab(ba(aa(x1)))) → ab(bb(ba(ab(ba(ab(ba(x1))))))) (36)
aa(ab(ba(ab(x1)))) → ab(bb(ba(ab(ba(ab(bb(x1))))))) (37)
aa(aa(aa(aa(aa(x1))))) → aa(aa(ab(ba(ab(ba(aa(aa(aa(x1))))))))) (38)
aa(aa(aa(aa(ab(x1))))) → aa(aa(ab(ba(ab(ba(aa(aa(ab(x1))))))))) (39)
aa(aa(ab(ba(aa(x1))))) → aa(ab(bb(ba(ab(ba(aa(ab(ba(x1))))))))) (40)
aa(aa(ab(ba(ab(x1))))) → aa(ab(bb(ba(ab(ba(aa(ab(bb(x1))))))))) (41)
aa(ab(ba(aa(aa(x1))))) → ab(ba(ab(ba(ab(ba(ab(ba(aa(x1))))))))) (42)
aa(ab(ba(aa(ab(x1))))) → ab(ba(ab(ba(ab(ba(ab(ba(ab(x1))))))))) (43)
aa(ab(bb(ba(aa(x1))))) → ab(bb(bb(ba(ab(ba(ab(bb(ba(x1))))))))) (44)
aa(ab(bb(ba(ab(x1))))) → ab(bb(bb(ba(ab(ba(ab(bb(bb(x1))))))))) (45)
aa(aa(aa(x1))) → ab(ba(ab(ba(x1)))) (46)
aa(aa(ab(x1))) → ab(ba(ab(bb(x1)))) (47)
ba(aa(aa(x1))) → bb(ba(ab(ba(x1)))) (48)
ba(aa(ab(x1))) → bb(ba(ab(bb(x1)))) (49)
aa(ab(ba(aa(x1)))) → ab(bb(ba(ab(bb(ba(x1)))))) (50)
aa(ab(ba(ab(x1)))) → ab(bb(ba(ab(bb(bb(x1)))))) (51)
ba(ab(ba(aa(x1)))) → bb(bb(ba(ab(bb(ba(x1)))))) (52)
ba(ab(ba(ab(x1)))) → bb(bb(ba(ab(bb(bb(x1)))))) (53)
aa(ab(ba(aa(aa(x1))))) → ab(ba(ab(ba(ab(bb(ba(aa(x1)))))))) (54)
aa(ab(ba(aa(ab(x1))))) → ab(ba(ab(ba(ab(bb(ba(ab(x1)))))))) (55)
ba(ab(ba(aa(aa(x1))))) → bb(ba(ab(ba(ab(bb(ba(aa(x1)))))))) (56)
ba(ab(ba(aa(ab(x1))))) → bb(ba(ab(ba(ab(bb(ba(ab(x1)))))))) (57)
aa(ab(bb(ba(aa(x1))))) → ab(bb(bb(ba(ab(bb(bb(ba(x1)))))))) (58)
aa(ab(bb(ba(ab(x1))))) → ab(bb(bb(ba(ab(bb(bb(bb(x1)))))))) (59)
ba(ab(bb(ba(aa(x1))))) → bb(bb(bb(ba(ab(bb(bb(ba(x1)))))))) (60)
ba(ab(bb(ba(ab(x1))))) → bb(bb(bb(ba(ab(bb(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 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(ab(ba(aa(x1))))) (32)
aa(aa(ab(x1))) → ab(ba(ab(ba(ab(x1))))) (33)
aa(aa(aa(aa(x1)))) → aa(ab(ba(ab(ba(aa(aa(x1))))))) (34)
aa(aa(aa(ab(x1)))) → aa(ab(ba(ab(ba(aa(ab(x1))))))) (35)
aa(ab(ba(aa(x1)))) → ab(bb(ba(ab(ba(ab(ba(x1))))))) (36)
aa(ab(ba(ab(x1)))) → ab(bb(ba(ab(ba(ab(bb(x1))))))) (37)
aa(aa(ab(ba(aa(x1))))) → aa(ab(bb(ba(ab(ba(aa(ab(ba(x1))))))))) (40)
aa(ab(ba(aa(aa(x1))))) → ab(ba(ab(ba(ab(ba(ab(ba(aa(x1))))))))) (42)
aa(ab(ba(aa(ab(x1))))) → ab(ba(ab(ba(ab(ba(ab(ba(ab(x1))))))))) (43)
aa(ab(bb(ba(aa(x1))))) → ab(bb(bb(ba(ab(ba(ab(bb(ba(x1))))))))) (44)
aa(ab(bb(ba(ab(x1))))) → ab(bb(bb(ba(ab(ba(ab(bb(bb(x1))))))))) (45)
aa(aa(aa(x1))) → ab(ba(ab(ba(x1)))) (46)
aa(aa(ab(x1))) → ab(ba(ab(bb(x1)))) (47)
ba(aa(aa(x1))) → bb(ba(ab(ba(x1)))) (48)
ba(aa(ab(x1))) → bb(ba(ab(bb(x1)))) (49)
aa(ab(ba(aa(x1)))) → ab(bb(ba(ab(bb(ba(x1)))))) (50)
aa(ab(ba(ab(x1)))) → ab(bb(ba(ab(bb(bb(x1)))))) (51)
ba(ab(ba(aa(x1)))) → bb(bb(ba(ab(bb(ba(x1)))))) (52)
aa(ab(ba(aa(aa(x1))))) → ab(ba(ab(ba(ab(bb(ba(aa(x1)))))))) (54)
aa(ab(ba(aa(ab(x1))))) → ab(ba(ab(ba(ab(bb(ba(ab(x1)))))))) (55)
ba(ab(ba(aa(aa(x1))))) → bb(ba(ab(ba(ab(bb(ba(aa(x1)))))))) (56)
ba(ab(ba(aa(ab(x1))))) → bb(ba(ab(ba(ab(bb(ba(ab(x1)))))))) (57)
aa(ab(bb(ba(aa(x1))))) → ab(bb(bb(ba(ab(bb(bb(ba(x1)))))))) (58)
aa(ab(bb(ba(ab(x1))))) → ab(bb(bb(ba(ab(bb(bb(bb(x1)))))))) (59)
ba(ab(bb(ba(aa(x1))))) → bb(bb(bb(ba(ab(bb(bb(ba(x1)))))))) (60)
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)
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)
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)

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(ab(ba(aa(aa(aa(x1))))))))) (78)
aa#(aa(aa(aa(aa(x1))))) → aa#(ab(ba(ab(ba(aa(aa(aa(x1)))))))) (79)
aa#(aa(aa(aa(aa(x1))))) → ba#(ab(ba(aa(aa(aa(x1)))))) (80)
aa#(aa(aa(aa(aa(x1))))) → ba#(aa(aa(aa(x1)))) (81)
aa#(aa(aa(aa(ab(x1))))) → aa#(aa(ab(ba(ab(ba(aa(aa(ab(x1))))))))) (82)
aa#(aa(aa(aa(ab(x1))))) → aa#(ab(ba(ab(ba(aa(aa(ab(x1)))))))) (83)
aa#(aa(aa(aa(ab(x1))))) → ba#(ab(ba(aa(aa(ab(x1)))))) (84)
aa#(aa(aa(aa(ab(x1))))) → ba#(aa(aa(ab(x1)))) (85)
aa#(aa(ab(ba(ab(x1))))) → aa#(ab(bb(ba(ab(ba(aa(ab(bb(x1))))))))) (86)
aa#(aa(ab(ba(ab(x1))))) → ba#(ab(ba(aa(ab(bb(x1)))))) (87)
aa#(aa(ab(ba(ab(x1))))) → ba#(aa(ab(bb(x1)))) (88)
aa#(aa(ab(ba(ab(x1))))) → aa#(ab(bb(x1))) (89)
ba#(ab(ba(ab(x1)))) → ba#(ab(bb(bb(x1)))) (90)
ba#(ab(bb(ba(ab(x1))))) → ba#(ab(bb(bb(bb(x1))))) (91)
ba#(ab(ba(aa(aa(aa(x1)))))) → ba#(aa(ab(ba(ab(bb(ba(aa(aa(x1))))))))) (92)
ba#(ab(ba(aa(aa(aa(x1)))))) → aa#(ab(ba(ab(bb(ba(aa(aa(x1)))))))) (93)
ba#(ab(ba(aa(aa(aa(x1)))))) → ba#(ab(bb(ba(aa(aa(x1)))))) (94)
ba#(ab(ba(aa(aa(aa(x1)))))) → ba#(aa(aa(x1))) (95)
ba#(ab(ba(aa(aa(ab(x1)))))) → ba#(aa(ab(ba(ab(bb(ba(aa(ab(x1))))))))) (96)
ba#(ab(ba(aa(aa(ab(x1)))))) → aa#(ab(ba(ab(bb(ba(aa(ab(x1)))))))) (97)
ba#(ab(ba(aa(aa(ab(x1)))))) → ba#(ab(bb(ba(aa(ab(x1)))))) (98)
ba#(ab(ba(aa(aa(ab(x1)))))) → ba#(aa(ab(x1))) (99)
ba#(ab(ba(ab(ba(ab(x1)))))) → ba#(ab(bb(ba(ab(bb(ba(ab(bb(x1))))))))) (100)
ba#(ab(ba(ab(ba(ab(x1)))))) → ba#(ab(bb(ba(ab(bb(x1)))))) (101)
ba#(ab(ba(ab(ba(ab(x1)))))) → ba#(ab(bb(x1))) (102)
ba#(ab(bb(bb(ba(ab(x1)))))) → ba#(ab(bb(bb(bb(bb(x1)))))) (103)

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.