Certification Problem

Input (TPDB TRS_Standard/AProVE_07/wiehe09)

The rewrite relation of the following TRS is considered.

minus(x,0) x (1)
minus(s(x),s(y)) minus(x,y) (2)
quot(0,s(y)) 0 (3)
quot(s(x),s(y)) s(quot(minus(x,y),s(y))) (4)
minus(minus(x,y),z) minus(x,plus(y,z)) (5)
plus(s(x),s(y)) s(s(plus(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))))) (6)
plus(s(x),x) plus(if(gt(x,x),id(x),id(x)),s(x)) (7)
plus(zero,y) y (8)
plus(id(x),s(y)) s(plus(x,if(gt(s(y),y),y,s(y)))) (9)
id(x) x (10)
if(true,x,y) x (11)
if(false,x,y) y (12)
not(x) if(x,false,true) (13)
gt(s(x),zero) true (14)
gt(zero,y) false (15)
gt(s(x),s(y)) gt(x,y) (16)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
plus#(s(x),s(y)) plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) (17)
plus#(s(x),s(y)) not#(gt(x,y)) (18)
plus#(id(x),s(y)) gt#(s(y),y) (19)
plus#(s(x),s(y)) id#(y) (20)
plus#(id(x),s(y)) plus#(x,if(gt(s(y),y),y,s(y))) (21)
quot#(s(x),s(y)) minus#(x,y) (22)
plus#(id(x),s(y)) if#(gt(s(y),y),y,s(y)) (23)
plus#(s(x),x) plus#(if(gt(x,x),id(x),id(x)),s(x)) (24)
minus#(minus(x,y),z) plus#(y,z) (25)
plus#(s(x),s(y)) gt#(x,y) (26)
not#(x) if#(x,false,true) (27)
plus#(s(x),s(y)) if#(not(gt(x,y)),id(x),id(y)) (28)
quot#(s(x),s(y)) quot#(minus(x,y),s(y)) (29)
plus#(s(x),x) id#(x) (30)
minus#(minus(x,y),z) minus#(x,plus(y,z)) (31)
gt#(s(x),s(y)) gt#(x,y) (32)
plus#(s(x),x) gt#(x,x) (33)
plus#(s(x),s(y)) if#(gt(x,y),x,y) (34)
minus#(s(x),s(y)) minus#(x,y) (35)
plus#(s(x),s(y)) id#(x) (36)
plus#(s(x),x) if#(gt(x,x),id(x),id(x)) (37)
plus#(s(x),s(y)) gt#(x,y) (26)
plus#(s(x),x) id#(x) (30)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.