Certification Problem

Input (TPDB TRS_Standard/Rubio_04/division)

The rewrite relation of the following TRS is considered.

le(0,Y) true (1)
le(s(X),0) false (2)
le(s(X),s(Y)) le(X,Y) (3)
minus(0,Y) 0 (4)
minus(s(X),Y) ifMinus(le(s(X),Y),s(X),Y) (5)
ifMinus(true,s(X),Y) 0 (6)
ifMinus(false,s(X),Y) s(minus(X,Y)) (7)
quot(0,s(Y)) 0 (8)
quot(s(X),s(Y)) s(quot(minus(X,Y),s(Y))) (9)

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.
le#(s(X),s(Y)) le#(X,Y) (10)
minus#(s(X),Y) le#(s(X),Y) (11)
minus#(s(X),Y) ifMinus#(le(s(X),Y),s(X),Y) (12)
ifMinus#(false,s(X),Y) minus#(X,Y) (13)
quot#(s(X),s(Y)) minus#(X,Y) (14)
quot#(s(X),s(Y)) quot#(minus(X,Y),s(Y)) (15)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.