Certification Problem

Input (TPDB TRS_Standard/Secret_06_TRS/7)

The rewrite relation of the following TRS is considered.

c(c(c(a(x,y)))) b(c(c(c(c(y)))),x) (1)
c(c(b(c(y),0))) a(0,c(c(a(y,0)))) (2)
c(c(a(a(y,0),x))) c(y) (3)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
c#(c(b(c(y),0))) c#(a(y,0)) (4)
c#(c(c(a(x,y)))) c#(c(y)) (5)
c#(c(c(a(x,y)))) c#(y) (6)
c#(c(c(a(x,y)))) c#(c(c(y))) (7)
c#(c(a(a(y,0),x))) c#(y) (8)
c#(c(b(c(y),0))) c#(c(a(y,0))) (9)
c#(c(c(a(x,y)))) c#(c(c(c(y)))) (10)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.