Certification Problem

Input (TPDB TRS_Standard/AProVE_07/wiehe01)

The rewrite relation of the following TRS is considered.

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

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

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.