Certification Problem

Input (TPDB TRS_Standard/Various_04/26)

The rewrite relation of the following TRS is considered.

f(f(x)) f(g(f(x),x)) (1)
f(f(x)) f(h(f(x),f(x))) (2)
g(x,y) y (3)
h(x,x) g(x,0) (4)

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.
f#(f(x)) h#(f(x),f(x)) (5)
h#(x,x) g#(x,0) (6)
f#(f(x)) f#(g(f(x),x)) (7)
f#(f(x)) f#(h(f(x),f(x))) (8)
f#(f(x)) g#(f(x),x) (9)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.