Certification Problem

Input (TPDB SRS_Standard/Zantema_06/15)

The rewrite relation of the following TRS is considered.

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

Using the flat contexts

{a(☐), b(☐)}

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

1.1 Semantic Labeling

Root-labeling is applied.

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

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
aa#(aa(x1)) → ba#(aa(x1)) (78)
aa#(ab(x1)) → ba#(ab(x1)) (79)
aa#(aa(aa(x1))) → aa#(ab(ba(aa(aa(x1))))) (80)
aa#(aa(aa(x1))) → ba#(aa(aa(x1))) (81)
aa#(aa(ab(x1))) → aa#(ab(ba(aa(ab(x1))))) (82)
aa#(aa(ab(x1))) → ba#(aa(ab(x1))) (83)
aa#(ab(ba(x1))) → ba#(ab(ba(x1))) (84)
aa#(ab(bb(x1))) → ba#(ab(bb(x1))) (85)
aa#(aa(aa(aa(x1)))) → aa#(aa(ab(ba(aa(aa(aa(x1))))))) (86)
aa#(aa(aa(aa(x1)))) → aa#(ab(ba(aa(aa(aa(x1)))))) (87)
aa#(aa(aa(aa(x1)))) → ba#(aa(aa(aa(x1)))) (88)
aa#(aa(aa(ab(x1)))) → aa#(aa(ab(ba(aa(aa(ab(x1))))))) (89)
aa#(aa(aa(ab(x1)))) → aa#(ab(ba(aa(aa(ab(x1)))))) (90)
aa#(aa(aa(ab(x1)))) → ba#(aa(aa(ab(x1)))) (91)
aa#(aa(ab(ba(x1)))) → aa#(ab(bb(ba(aa(ab(ba(x1))))))) (92)
aa#(aa(ab(ba(x1)))) → ba#(aa(ab(ba(x1)))) (93)
aa#(aa(ab(bb(x1)))) → aa#(ab(bb(ba(aa(ab(bb(x1))))))) (94)
aa#(aa(ab(bb(x1)))) → ba#(aa(ab(bb(x1)))) (95)
aa#(ab(ba(aa(x1)))) → ba#(ab(ba(ab(ba(aa(x1)))))) (96)
aa#(ab(ba(aa(x1)))) → ba#(ab(ba(aa(x1)))) (97)
aa#(ab(ba(ab(x1)))) → ba#(ab(ba(ab(ba(ab(x1)))))) (98)
aa#(ab(ba(ab(x1)))) → ba#(ab(ba(ab(x1)))) (99)
aa#(ab(bb(ba(x1)))) → ba#(ab(bb(ba(x1)))) (100)
aa#(ab(bb(bb(x1)))) → ba#(ab(bb(bb(x1)))) (101)
aa#(aa(x1)) → ba#(x1) (102)
ba#(aa(x1)) → ba#(x1) (103)
aa#(ab(ba(aa(x1)))) → ba#(ab(bb(ba(aa(x1))))) (104)
aa#(ab(ba(ab(x1)))) → ba#(ab(bb(ba(ab(x1))))) (105)
ba#(ab(ba(aa(x1)))) → ba#(ab(bb(ba(aa(x1))))) (106)
ba#(ab(ba(ab(x1)))) → ba#(ab(bb(ba(ab(x1))))) (107)
aa#(ab(ba(aa(aa(x1))))) → ba#(aa(ab(bb(ba(aa(aa(x1))))))) (108)
aa#(ab(ba(aa(aa(x1))))) → aa#(ab(bb(ba(aa(aa(x1)))))) (109)
aa#(ab(ba(aa(ab(x1))))) → ba#(aa(ab(bb(ba(aa(ab(x1))))))) (110)
aa#(ab(ba(aa(ab(x1))))) → aa#(ab(bb(ba(aa(ab(x1)))))) (111)
ba#(ab(ba(aa(aa(x1))))) → ba#(aa(ab(bb(ba(aa(aa(x1))))))) (112)
ba#(ab(ba(aa(aa(x1))))) → aa#(ab(bb(ba(aa(aa(x1)))))) (113)
ba#(ab(ba(aa(ab(x1))))) → ba#(aa(ab(bb(ba(aa(ab(x1))))))) (114)
ba#(ab(ba(aa(ab(x1))))) → aa#(ab(bb(ba(aa(ab(x1)))))) (115)
aa#(ab(ba(ab(ba(x1))))) → ba#(ab(bb(bb(ba(ab(ba(x1))))))) (116)
aa#(ab(ba(ab(bb(x1))))) → ba#(ab(bb(bb(ba(ab(bb(x1))))))) (117)
ba#(ab(ba(ab(ba(x1))))) → ba#(ab(bb(bb(ba(ab(ba(x1))))))) (118)
ba#(ab(ba(ab(bb(x1))))) → ba#(ab(bb(bb(ba(ab(bb(x1))))))) (119)
aa#(ab(bb(ba(aa(x1))))) → ba#(ab(bb(bb(ba(aa(x1)))))) (120)
aa#(ab(bb(ba(ab(x1))))) → ba#(ab(bb(bb(ba(ab(x1)))))) (121)
ba#(ab(bb(ba(aa(x1))))) → ba#(ab(bb(bb(ba(aa(x1)))))) (122)
ba#(ab(bb(ba(ab(x1))))) → ba#(ab(bb(bb(ba(ab(x1)))))) (123)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.