Certification Problem

Input (TPDB TRS_Standard/AProVE_04/IJCAR_18)

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)
eq(0,0) true (13)
eq(s(x),0) false (14)
eq(0,s(y)) false (15)
eq(s(x),s(y)) eq(x,y) (16)
divides(y,x) eq(x,times(div(x,y),y)) (17)
prime(s(s(x))) pr(s(s(x)),s(x)) (18)
pr(x,s(0)) true (19)
pr(x,s(s(y))) if(divides(s(s(y)),x),x,s(y)) (20)
if(true,x,y) false (21)
if(false,x,y) pr(x,y) (22)

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.
plus#(s(x),y) plus#(x,y) (23)
times#(s(x),y) times#(x,y) (24)
times#(s(x),y) plus#(y,times(x,y)) (25)
div#(x,y) quot#(x,y,y) (26)
quot#(s(x),s(y),z) quot#(x,y,z) (27)
quot#(x,0,s(z)) div#(x,s(z)) (28)
div#(div(x,y),z) times#(y,z) (29)
div#(div(x,y),z) div#(x,times(y,z)) (30)
eq#(s(x),s(y)) eq#(x,y) (31)
divides#(y,x) div#(x,y) (32)
divides#(y,x) times#(div(x,y),y) (33)
divides#(y,x) eq#(x,times(div(x,y),y)) (34)
prime#(s(s(x))) pr#(s(s(x)),s(x)) (35)
pr#(x,s(s(y))) divides#(s(s(y)),x) (36)
pr#(x,s(s(y))) if#(divides(s(s(y)),x),x,s(y)) (37)
if#(false,x,y) pr#(x,y) (38)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.