Certification Problem

Input (TPDB SRS_Standard/Waldmann_19/random-403)

The rewrite relation of the following TRS is considered.

a(b(b(a(x1)))) → b(a(a(b(x1)))) (1)
a(b(b(b(x1)))) → a(a(a(b(x1)))) (2)
b(b(a(a(x1)))) → b(b(b(a(x1)))) (3)

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

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
ab(bb(bb(ba(x1)))) → aa(aa(ab(ba(x1)))) (6)
ab(bb(bb(bb(x1)))) → aa(aa(ab(bb(x1)))) (7)
bb(ba(aa(aa(x1)))) → bb(bb(ba(aa(x1)))) (8)
bb(ba(aa(ab(x1)))) → bb(bb(ba(ab(x1)))) (9)
aa(ab(bb(ba(aa(x1))))) → ab(ba(aa(ab(ba(x1))))) (10)
aa(ab(bb(ba(ab(x1))))) → ab(ba(aa(ab(bb(x1))))) (11)
ba(ab(bb(ba(aa(x1))))) → bb(ba(aa(ab(ba(x1))))) (12)
ba(ab(bb(ba(ab(x1))))) → bb(ba(aa(ab(bb(x1))))) (13)

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
ab#(bb(bb(ba(x1)))) → aa#(aa(ab(ba(x1)))) (14)
ab#(bb(bb(ba(x1)))) → aa#(ab(ba(x1))) (15)
ab#(bb(bb(ba(x1)))) → ab#(ba(x1)) (16)
ab#(bb(bb(bb(x1)))) → aa#(aa(ab(bb(x1)))) (17)
ab#(bb(bb(bb(x1)))) → aa#(ab(bb(x1))) (18)
ab#(bb(bb(bb(x1)))) → ab#(bb(x1)) (19)
bb#(ba(aa(aa(x1)))) → bb#(bb(ba(aa(x1)))) (20)
bb#(ba(aa(aa(x1)))) → bb#(ba(aa(x1))) (21)
bb#(ba(aa(aa(x1)))) → ba#(aa(x1)) (22)
bb#(ba(aa(ab(x1)))) → bb#(bb(ba(ab(x1)))) (23)
bb#(ba(aa(ab(x1)))) → bb#(ba(ab(x1))) (24)
bb#(ba(aa(ab(x1)))) → ba#(ab(x1)) (25)
aa#(ab(bb(ba(aa(x1))))) → ab#(ba(aa(ab(ba(x1))))) (26)
aa#(ab(bb(ba(aa(x1))))) → ba#(aa(ab(ba(x1)))) (27)
aa#(ab(bb(ba(aa(x1))))) → aa#(ab(ba(x1))) (28)
aa#(ab(bb(ba(aa(x1))))) → ab#(ba(x1)) (29)
aa#(ab(bb(ba(aa(x1))))) → ba#(x1) (30)
aa#(ab(bb(ba(ab(x1))))) → ab#(ba(aa(ab(bb(x1))))) (31)
aa#(ab(bb(ba(ab(x1))))) → ba#(aa(ab(bb(x1)))) (32)
aa#(ab(bb(ba(ab(x1))))) → aa#(ab(bb(x1))) (33)
aa#(ab(bb(ba(ab(x1))))) → ab#(bb(x1)) (34)
aa#(ab(bb(ba(ab(x1))))) → bb#(x1) (35)
ba#(ab(bb(ba(aa(x1))))) → bb#(ba(aa(ab(ba(x1))))) (36)
ba#(ab(bb(ba(aa(x1))))) → ba#(aa(ab(ba(x1)))) (37)
ba#(ab(bb(ba(aa(x1))))) → aa#(ab(ba(x1))) (38)
ba#(ab(bb(ba(aa(x1))))) → ab#(ba(x1)) (39)
ba#(ab(bb(ba(aa(x1))))) → ba#(x1) (40)
ba#(ab(bb(ba(ab(x1))))) → bb#(ba(aa(ab(bb(x1))))) (41)
ba#(ab(bb(ba(ab(x1))))) → ba#(aa(ab(bb(x1)))) (42)
ba#(ab(bb(ba(ab(x1))))) → aa#(ab(bb(x1))) (43)
ba#(ab(bb(ba(ab(x1))))) → ab#(bb(x1)) (44)
ba#(ab(bb(ba(ab(x1))))) → bb#(x1) (45)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.