Certification Problem

Input (TPDB TRS_Standard/AProVE_07/thiemann40)

The rewrite relation of the following TRS is considered.

nonZero(0) false (1)
nonZero(s(x)) true (2)
p(0) 0 (3)
p(s(x)) x (4)
id_inc(x) x (5)
id_inc(x) s(x) (6)
random(x) rand(x,0) (7)
rand(x,y) if(nonZero(x),x,y) (8)
if(false,x,y) y (9)
if(true,x,y) rand(p(x),id_inc(y)) (10)

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.
random#(x) rand#(x,0) (11)
rand#(x,y) if#(nonZero(x),x,y) (12)
rand#(x,y) nonZero#(x) (13)
if#(true,x,y) rand#(p(x),id_inc(y)) (14)
if#(true,x,y) p#(x) (15)
if#(true,x,y) id_inc#(y) (16)

1.1 Dependency Graph Processor

The dependency pairs are split into 1 component.