Certification Problem

Input (TPDB TRS_Standard/AProVE_08/thiemann40_modified)

The rewrite relation of the following TRS is considered.

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

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.