Certification Problem

Input (TPDB TRS_Standard/AProVE_07/kabasci02)

The rewrite relation of the following TRS is considered.

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

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) (32)
plus#(s(x),y) plus#(p(s(x)),y) (33)
plus#(s(x),y) p#(s(x)) (34)
plus#(x,s(y)) plus#(x,p(s(y))) (35)
plus#(x,s(y)) p#(s(y)) (36)
times#(s(x),y) plus#(y,times(x,y)) (37)
times#(s(x),y) times#(x,y) (38)
div#(x,y) quot#(x,y,y) (39)
quot#(s(x),s(y),z) quot#(x,y,z) (40)
quot#(x,0,s(z)) div#(x,s(z)) (41)
div#(div(x,y),z) div#(x,times(zero(y),z)) (42)
div#(div(x,y),z) times#(zero(y),z) (43)
div#(div(x,y),z) zero#(y) (44)
eq#(s(x),s(y)) eq#(x,y) (45)
divides#(y,x) eq#(x,times(div(x,y),y)) (46)
divides#(y,x) times#(div(x,y),y) (47)
divides#(y,x) div#(x,y) (48)
prime#(s(s(x))) pr#(s(s(x)),s(x)) (49)
pr#(x,s(s(y))) if#(divides(s(s(y)),x),x,s(y)) (50)
pr#(x,s(s(y))) divides#(s(s(y)),x) (51)
if#(false,x,y) pr#(x,y) (52)
zero#(s(x)) if#(eq(x,s(0)),plus(zero(0),0),s(plus(0,zero(0)))) (53)
zero#(s(x)) eq#(x,s(0)) (54)
zero#(s(x)) plus#(zero(0),0) (55)
zero#(s(x)) zero#(0) (56)
zero#(s(x)) plus#(0,zero(0)) (57)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.