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 AProVE @ termCOMP 2023)

1 Switch to Innermost Termination

The TRS is overlay and locally confluent:

10

Hence, it suffices to show innermost termination in the following.

1.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) → f#(y,h(x,y,z)) (8)
h#(g(x),y,z) → h#(x,y,z) (9)

1.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),g(y)) → h#(g(y),x,g(y)) (7)
2 ≥ 1
1 > 2
2 ≥ 3
h#(g(x),y,z) → f#(y,h(x,y,z)) (8)
2 ≥ 1
h#(g(x),y,z) → h#(x,y,z) (9)
1 > 1
2 ≥ 2
3 ≥ 3
f#(g(x),a) → f#(x,g(a)) (6)
1 > 1

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