Certification Problem

Input (TPDB SRS_Standard/Wenzel_16/bababaaba-ababaababababa.srs)

The rewrite relation of the following TRS is considered.

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

1.1 Semantic Labeling

Root-labeling is applied.

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

1.1.1 Dependency Pair Transformation

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

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.