Certification Problem

Input (TPDB TRS_Standard/CiME_04/dpqs)

The rewrite relation of the following TRS is considered.

f(f(x)) f(c(f(x))) (1)
f(f(x)) f(d(f(x))) (2)
g(c(x)) x (3)
g(d(x)) x (4)
g(c(0)) g(d(1)) (5)
g(c(1)) g(d(0)) (6)

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.
g#(c(1)) g#(d(0)) (7)
g#(c(0)) g#(d(1)) (8)
f#(f(x)) f#(d(f(x))) (9)
f#(f(x)) f#(c(f(x))) (10)

1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.