Certification Problem

Input (TPDB TRS_Innermost/AG01_innermost/#4.23)

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)
plus(0,y) y (3)
plus(s(x),y) s(plus(x,y)) (4)
quot(x,0,s(z)) s(quot(x,plus(z,s(0)),s(z))) (5)
The evaluation strategy is innermost.

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ 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) (6)
plus#(s(x),y) plus#(x,y) (7)
quot#(x,0,s(z)) quot#(x,plus(z,s(0)),s(z)) (8)
quot#(x,0,s(z)) plus#(z,s(0)) (9)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.