Certification Problem

Input (TPDB TRS_Standard/SK90/4.42)

The rewrite relation of the following TRS is considered.

f(a,g(y)) g(g(y)) (1)
f(g(x),a) f(x,g(a)) (2)
f(g(x),g(y)) h(g(y),x,g(y)) (3)
h(g(x),y,z) f(y,h(x,y,z)) (4)
h(a,y,z) z (5)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by ttt2 @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
f#(g(x),a) f#(x,g(a)) (6)
f#(g(x),g(y)) h#(g(y),x,g(y)) (7)
h#(g(x),y,z) h#(x,y,z) (8)
h#(g(x),y,z) f#(y,h(x,y,z)) (9)

1.1 Size-Change Termination

Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.

f#(g(x),a) f#(x,g(a)) (6)
1 > 1
f#(g(x),g(y)) h#(g(y),x,g(y)) (7)
2 3
2 1
1 > 2
h#(g(x),y,z) h#(x,y,z) (8)
3 3
2 2
1 > 1
h#(g(x),y,z) f#(y,h(x,y,z)) (9)
2 1

As there is no critical graph in the transitive closure, there are no infinite chains.