Certification Problem

Input (TPDB TRS_Standard/Rubio_04/gm)

The rewrite relation of the following TRS is considered.

minus(X,0) X (1)
minus(s(X),s(Y)) p(minus(X,Y)) (2)
p(s(X)) X (3)
div(0,s(Y)) 0 (4)
div(s(X),s(Y)) s(div(minus(X,Y),s(Y))) (5)

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.
minus#(s(X),s(Y)) minus#(X,Y) (6)
div#(s(X),s(Y)) div#(minus(X,Y),s(Y)) (7)
minus#(s(X),s(Y)) p#(minus(X,Y)) (8)
div#(s(X),s(Y)) minus#(X,Y) (9)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.