Certification Problem

Input (TPDB SRS_Standard/Zantema_04/z045)

The rewrite relation of the following TRS is considered.

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

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Closure Under Flat Contexts

Using the flat contexts

{c(☐), a(☐), b(☐)}

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

1.1 Semantic Labeling

Root-labeling is applied.

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

1.1.1 Rule Removal

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

1.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
ac#(ca(ab(ba(ab(bc(x1)))))) → bc#(ca(ab(bc(ca(ac(x1)))))) (14)
ac#(ca(ab(ba(ab(bc(x1)))))) → bc#(ca(ac(x1))) (15)
ac#(ca(ab(ba(ab(bc(x1)))))) → ac#(x1) (16)
ac#(ca(ab(ba(ab(ba(x1)))))) → bc#(ca(ab(bc(ca(aa(x1)))))) (17)
ac#(ca(ab(ba(ab(ba(x1)))))) → bc#(ca(aa(x1))) (18)
ac#(ca(ab(ba(ab(bb(x1)))))) → bc#(ca(ab(bc(ca(ab(x1)))))) (19)
ac#(ca(ab(ba(ab(bb(x1)))))) → bc#(ca(ab(x1))) (20)
bc#(ca(ab(ba(ab(bc(x1)))))) → bc#(ca(ab(bc(ca(ac(x1)))))) (21)
bc#(ca(ab(ba(ab(bc(x1)))))) → bc#(ca(ac(x1))) (22)
bc#(ca(ab(ba(ab(bc(x1)))))) → ac#(x1) (23)
bc#(ca(ab(ba(ab(ba(x1)))))) → bc#(ca(ab(bc(ca(aa(x1)))))) (24)
bc#(ca(ab(ba(ab(ba(x1)))))) → bc#(ca(aa(x1))) (25)
bc#(ca(ab(ba(ab(bb(x1)))))) → bc#(ca(ab(bc(ca(ab(x1)))))) (26)
bc#(ca(ab(ba(ab(bb(x1)))))) → bc#(ca(ab(x1))) (27)

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.