Certification Problem

Input (TPDB SRS_Standard/Trafo_06/hom03)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Semantic Labeling

Root-labeling is applied.

We obtain the labeled TRS
ab(bc(ca(ab(bc(ca(aa(aa(aa(x1))))))))) → aa(aa(aa(ab(bc(ca(ab(bc(ca(ab(bc(ca(x1)))))))))))) (2)
ab(bc(ca(ab(bc(ca(aa(aa(ab(x1))))))))) → aa(aa(aa(ab(bc(ca(ab(bc(ca(ab(bc(cb(x1)))))))))))) (3)
ab(bc(ca(ab(bc(ca(aa(aa(ac(x1))))))))) → aa(aa(aa(ab(bc(ca(ab(bc(ca(ab(bc(cc(x1)))))))))))) (4)

1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[ab(x1)] = 1 · x1
[bc(x1)] = 1 · x1
[ca(x1)] = 1 · x1
[aa(x1)] = 1 · x1
[cb(x1)] = 1 · x1
[ac(x1)] = 1 · x1 + 1
[cc(x1)] = 1 · x1
all of the following rules can be deleted.
ab(bc(ca(ab(bc(ca(aa(aa(ac(x1))))))))) → aa(aa(aa(ab(bc(ca(ab(bc(ca(ab(bc(cc(x1)))))))))))) (4)

1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
ab#(bc(ca(ab(bc(ca(aa(aa(aa(x1))))))))) → ab#(bc(ca(ab(bc(ca(ab(bc(ca(x1))))))))) (5)
ab#(bc(ca(ab(bc(ca(aa(aa(aa(x1))))))))) → ab#(bc(ca(ab(bc(ca(x1)))))) (6)
ab#(bc(ca(ab(bc(ca(aa(aa(aa(x1))))))))) → ab#(bc(ca(x1))) (7)
ab#(bc(ca(ab(bc(ca(aa(aa(ab(x1))))))))) → ab#(bc(ca(ab(bc(ca(ab(bc(cb(x1))))))))) (8)
ab#(bc(ca(ab(bc(ca(aa(aa(ab(x1))))))))) → ab#(bc(ca(ab(bc(cb(x1)))))) (9)
ab#(bc(ca(ab(bc(ca(aa(aa(ab(x1))))))))) → ab#(bc(cb(x1))) (10)

1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.