Certification Problem

Input (TPDB TRS_Standard/AG01/#3.8a)

The rewrite relation of the following TRS is considered.

pred(s(x)) x (1)
minus(x,0) x (2)
minus(x,s(y)) pred(minus(x,y)) (3)
quot(0,s(y)) 0 (4)
quot(s(x),s(y)) s(quot(minus(x,y),s(y))) (5)
log(s(0)) 0 (6)
log(s(s(x))) s(log(s(quot(x,s(s(0)))))) (7)

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))) quot#(x,s(s(0))) (8)
minus#(x,s(y)) minus#(x,y) (9)
minus#(x,s(y)) pred#(minus(x,y)) (10)
quot#(s(x),s(y)) quot#(minus(x,y),s(y)) (11)
log#(s(s(x))) log#(s(quot(x,s(s(0))))) (12)
quot#(s(x),s(y)) minus#(x,y) (13)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.