Certification Problem

Input (TPDB TRS_Standard/Strategy_removed_AG01/#4.22)

The rewrite relation of the following TRS is considered.

quot(0,s(y),s(z)) → 0 (1)
quot(s(x),s(y),z) → quot(x,y,z) (2)
quot(x,0,s(z)) → s(quot(x,s(z),s(z))) (3)

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.
quot#(s(x),s(y),z) → quot#(x,y,z) (4)
quot#(x,0,s(z)) → quot#(x,s(z),s(z)) (5)

1.1 Size-Change Termination

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

quot#(s(x),s(y),z) → quot#(x,y,z) (4)
3 ≥ 3
2 > 2
1 > 1
quot#(x,0,s(z)) → quot#(x,s(z),s(z)) (5)
3 ≥ 3
3 ≥ 2
1 ≥ 1

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