Certification Problem

Input (TPDB TRS_Standard/Rubio_04/logarquot)

The rewrite relation of the following TRS is considered.

min(X,0) X (1)
min(s(X),s(Y)) min(X,Y) (2)
quot(0,s(Y)) 0 (3)
quot(s(X),s(Y)) s(quot(min(X,Y),s(Y))) (4)
log(s(0)) 0 (5)
log(s(s(X))) s(log(s(quot(X,s(s(0)))))) (6)

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.
log#(s(s(X))) log#(s(quot(X,s(s(0))))) (7)
quot#(s(X),s(Y)) min#(X,Y) (8)
log#(s(s(X))) quot#(X,s(s(0))) (9)
min#(s(X),s(Y)) min#(X,Y) (10)
quot#(s(X),s(Y)) quot#(min(X,Y),s(Y)) (11)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.