Certification Problem

Input (TPDB TRS_Standard/AProVE_04/IJCAR_12)

The rewrite relation of the following TRS is considered.

plus(x,0) x (1)
plus(0,y) y (2)
plus(s(x),y) s(plus(x,y)) (3)
times(0,y) 0 (4)
times(s(0),y) y (5)
times(s(x),y) plus(y,times(x,y)) (6)
div(0,y) 0 (7)
div(x,y) quot(x,y,y) (8)
quot(0,s(y),z) 0 (9)
quot(s(x),s(y),z) quot(x,y,z) (10)
quot(x,0,s(z)) s(div(x,s(z))) (11)
div(div(x,y),z) div(x,times(y,z)) (12)

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.
plus#(s(x),y) plus#(x,y) (13)
times#(s(x),y) plus#(y,times(x,y)) (14)
times#(s(x),y) times#(x,y) (15)
div#(x,y) quot#(x,y,y) (16)
quot#(s(x),s(y),z) quot#(x,y,z) (17)
quot#(x,0,s(z)) div#(x,s(z)) (18)
div#(div(x,y),z) div#(x,times(y,z)) (19)
div#(div(x,y),z) times#(y,z) (20)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.