Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z054)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
b(a(b(a(a(b(x1)))))) → a(b(a(b(a(b(a(x1))))))) (2)

1.1 Closure Under Flat Contexts

Using the flat contexts

{b(☐), a(☐)}

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

1.1.1 Semantic Labeling

Root-labeling is applied.

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

1.1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[bb(x1)] = 1 · x1 + 1
[ba(x1)] = 1 · x1
[ab(x1)] = 1 · x1
[aa(x1)] = 1 · x1
all of the following rules can be deleted.
bb(ba(ab(ba(aa(ab(bb(x1))))))) → ba(ab(ba(ab(ba(ab(ba(ab(x1)))))))) (5)
bb(ba(ab(ba(aa(ab(ba(x1))))))) → ba(ab(ba(ab(ba(ab(ba(aa(x1)))))))) (6)
ab(ba(ab(ba(aa(ab(bb(x1))))))) → aa(ab(ba(ab(ba(ab(ba(ab(x1)))))))) (7)

1.1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
ab#(ba(ab(ba(aa(ab(ba(x1))))))) → ab#(ba(ab(ba(ab(ba(aa(x1))))))) (9)
ab#(ba(ab(ba(aa(ab(ba(x1))))))) → ab#(ba(ab(ba(aa(x1))))) (10)
ab#(ba(ab(ba(aa(ab(ba(x1))))))) → ab#(ba(aa(x1))) (11)

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.