Certification Problem

Input (TPDB TRS_Standard/AProVE_04/IJCAR_26)

The rewrite relation of the following TRS is considered.

p(s(x)) x (1)
plus(x,0) x (2)
plus(0,y) y (3)
plus(s(x),y) s(plus(x,y)) (4)
plus(s(x),y) s(plus(p(s(x)),y)) (5)
plus(x,s(y)) s(plus(x,p(s(y)))) (6)
times(0,y) 0 (7)
times(s(0),y) y (8)
times(s(x),y) plus(y,times(x,y)) (9)
div(0,y) 0 (10)
div(x,y) quot(x,y,y) (11)
quot(0,s(y),z) 0 (12)
quot(s(x),s(y),z) quot(x,y,z) (13)
quot(x,0,s(z)) s(div(x,s(z))) (14)
div(div(x,y),z) div(x,times(y,z)) (15)
eq(0,0) true (16)
eq(s(x),0) false (17)
eq(0,s(y)) false (18)
eq(s(x),s(y)) eq(x,y) (19)
divides(y,x) eq(x,times(div(x,y),y)) (20)
prime(s(s(x))) pr(s(s(x)),s(x)) (21)
pr(x,s(0)) true (22)
pr(x,s(s(y))) if(divides(s(s(y)),x),x,s(y)) (23)
if(true,x,y) false (24)
if(false,x,y) pr(x,y) (25)

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) (26)
plus#(s(x),y) p#(s(x)) (27)
plus#(s(x),y) plus#(p(s(x)),y) (28)
plus#(x,s(y)) p#(s(y)) (29)
plus#(x,s(y)) plus#(x,p(s(y))) (30)
times#(s(x),y) times#(x,y) (31)
times#(s(x),y) plus#(y,times(x,y)) (32)
div#(x,y) quot#(x,y,y) (33)
quot#(s(x),s(y),z) quot#(x,y,z) (34)
quot#(x,0,s(z)) div#(x,s(z)) (35)
div#(div(x,y),z) times#(y,z) (36)
div#(div(x,y),z) div#(x,times(y,z)) (37)
eq#(s(x),s(y)) eq#(x,y) (38)
divides#(y,x) div#(x,y) (39)
divides#(y,x) times#(div(x,y),y) (40)
divides#(y,x) eq#(x,times(div(x,y),y)) (41)
prime#(s(s(x))) pr#(s(s(x)),s(x)) (42)
pr#(x,s(s(y))) divides#(s(s(y)),x) (43)
pr#(x,s(s(y))) if#(divides(s(s(y)),x),x,s(y)) (44)
if#(false,x,y) pr#(x,y) (45)

1.1 Dependency Graph Processor

The dependency pairs are split into 5 components.