Certification Problem

Input (TPDB TRS_Standard/AProVE_07/thiemann15)

The rewrite relation of the following TRS is considered.

half(0) 0 (1)
half(s(0)) 0 (2)
half(s(s(x))) s(half(x)) (3)
inc(0) 0 (4)
inc(s(x)) s(inc(x)) (5)
zero(0) true (6)
zero(s(x)) false (7)
p(0) 0 (8)
p(s(x)) x (9)
bits(x) bitIter(x,0) (10)
bitIter(x,y) if(zero(x),x,inc(y)) (11)
if(true,x,y) p(y) (12)
if(false,x,y) bitIter(half(x),y) (13)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Switch to Innermost Termination

The TRS is overlay and locally confluent:

10

Hence, it suffices to show innermost termination in the following.

1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
half#(s(s(x))) half#(x) (14)
inc#(s(x)) inc#(x) (15)
bits#(x) bitIter#(x,0) (16)
bitIter#(x,y) if#(zero(x),x,inc(y)) (17)
bitIter#(x,y) zero#(x) (18)
bitIter#(x,y) inc#(y) (19)
if#(true,x,y) p#(y) (20)
if#(false,x,y) bitIter#(half(x),y) (21)
if#(false,x,y) half#(x) (22)

1.1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.