Certification Problem

Input (TPDB SRS_Standard/Wenzel_16/baabbaabaab-aabbaabaabbaab.srs)

The rewrite relation of the following TRS is considered.

b(a(a(b(b(a(a(b(a(a(b(x1))))))))))) → a(a(b(b(a(a(b(a(a(b(b(a(a(b(x1)))))))))))))) (1)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

{b(☐), a(☐)}

We obtain the transformed TRS
b(b(a(a(b(b(a(a(b(a(a(b(x1)))))))))))) → b(a(a(b(b(a(a(b(a(a(b(b(a(a(b(x1))))))))))))))) (2)
a(b(a(a(b(b(a(a(b(a(a(b(x1)))))))))))) → a(a(a(b(b(a(a(b(a(a(b(b(a(a(b(x1))))))))))))))) (3)

1.1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
bb(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(x1)))))))))))) → ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(ba(aa(ab(bb(x1))))))))))))))) (4)
bb(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(ba(x1)))))))))))) → ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(ba(aa(ab(ba(x1))))))))))))))) (5)
ab(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(x1)))))))))))) → aa(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(ba(aa(ab(bb(x1))))))))))))))) (6)
ab(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(ba(x1)))))))))))) → aa(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(ba(aa(ab(ba(x1))))))))))))))) (7)

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
bb#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(x1)))))))))))) → bb#(ba(aa(ab(bb(x1))))) (8)
bb#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(x1)))))))))))) → ab#(bb(ba(aa(ab(bb(x1)))))) (9)
bb#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(x1)))))))))))) → ab#(ba(aa(ab(bb(ba(aa(ab(bb(x1))))))))) (10)
bb#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(x1)))))))))))) → bb#(ba(aa(ab(ba(aa(ab(bb(ba(aa(ab(bb(x1)))))))))))) (11)
bb#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(x1)))))))))))) → ab#(bb(ba(aa(ab(ba(aa(ab(bb(ba(aa(ab(bb(x1))))))))))))) (12)
bb#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(ba(x1)))))))))))) → bb#(ba(aa(ab(ba(x1))))) (13)
bb#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(ba(x1)))))))))))) → ab#(bb(ba(aa(ab(ba(x1)))))) (14)
bb#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(ba(x1)))))))))))) → ab#(ba(aa(ab(bb(ba(aa(ab(ba(x1))))))))) (15)
bb#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(ba(x1)))))))))))) → bb#(ba(aa(ab(ba(aa(ab(bb(ba(aa(ab(ba(x1)))))))))))) (16)
bb#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(ba(x1)))))))))))) → ab#(bb(ba(aa(ab(ba(aa(ab(bb(ba(aa(ab(ba(x1))))))))))))) (17)
ab#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(x1)))))))))))) → bb#(ba(aa(ab(bb(x1))))) (18)
ab#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(x1)))))))))))) → ab#(bb(ba(aa(ab(bb(x1)))))) (19)
ab#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(x1)))))))))))) → ab#(ba(aa(ab(bb(ba(aa(ab(bb(x1))))))))) (20)
ab#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(x1)))))))))))) → bb#(ba(aa(ab(ba(aa(ab(bb(ba(aa(ab(bb(x1)))))))))))) (21)
ab#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(bb(x1)))))))))))) → ab#(bb(ba(aa(ab(ba(aa(ab(bb(ba(aa(ab(bb(x1))))))))))))) (22)
ab#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(ba(x1)))))))))))) → bb#(ba(aa(ab(ba(x1))))) (23)
ab#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(ba(x1)))))))))))) → ab#(bb(ba(aa(ab(ba(x1)))))) (24)
ab#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(ba(x1)))))))))))) → ab#(ba(aa(ab(bb(ba(aa(ab(ba(x1))))))))) (25)
ab#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(ba(x1)))))))))))) → bb#(ba(aa(ab(ba(aa(ab(bb(ba(aa(ab(ba(x1)))))))))))) (26)
ab#(ba(aa(ab(bb(ba(aa(ab(ba(aa(ab(ba(x1)))))))))))) → ab#(bb(ba(aa(ab(ba(aa(ab(bb(ba(aa(ab(ba(x1))))))))))))) (27)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.