Certification Problem

Input (TPDB TRS_Standard/AProVE_07/wiehe05)

The rewrite relation of the following TRS is considered.

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

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.
minus#(s(x),s(y)) minus#(x,y) (16)
double#(s(x)) double#(x) (17)
plus#(s(x),s(y)) id#(y) (18)
plus#(s(x),s(y)) id#(x) (19)
plus#(s(x),s(y)) not#(gt(x,y)) (20)
plus#(s(x),s(y)) if#(not(gt(x,y)),id(x),id(y)) (21)
plus#(s(x),s(y)) gt#(x,y) (22)
plus#(s(x),s(y)) if#(gt(x,y),x,y) (23)
plus#(s(x),s(y)) plus#(if(gt(x,y),x,y),if(not(gt(x,y)),id(x),id(y))) (24)
plus#(s(x),x) id#(x) (25)
plus#(s(x),x) gt#(x,x) (26)
plus#(s(x),x) if#(gt(x,x),id(x),id(x)) (27)
plus#(s(x),x) plus#(if(gt(x,x),id(x),id(x)),s(x)) (28)
plus#(id(x),s(y)) gt#(s(y),y) (29)
plus#(id(x),s(y)) if#(gt(s(y),y),y,s(y)) (30)
plus#(id(x),s(y)) plus#(x,if(gt(s(y),y),y,s(y))) (31)
not#(x) if#(x,false,true) (32)
gt#(s(x),s(y)) gt#(x,y) (33)

1.1 Dependency Graph Processor

The dependency pairs are split into 4 components.