Certification Problem

Input (TPDB TRS_Standard/AProVE_07/thiemann10)

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)
lastbit(0) 0 (4)
lastbit(s(0)) s(0) (5)
lastbit(s(s(x))) lastbit(x) (6)
zero(0) true (7)
zero(s(x)) false (8)
conv(x) conviter(x,cons(0,nil)) (9)
conviter(x,l) if(zero(x),x,l) (10)
if(true,x,l) l (11)
if(false,x,l) conviter(half(x),cons(lastbit(x),l)) (12)

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.
half#(s(s(x))) half#(x) (13)
lastbit#(s(s(x))) lastbit#(x) (14)
conv#(x) conviter#(x,cons(0,nil)) (15)
conviter#(x,l) zero#(x) (16)
conviter#(x,l) if#(zero(x),x,l) (17)
if#(false,x,l) lastbit#(x) (18)
if#(false,x,l) half#(x) (19)
if#(false,x,l) conviter#(half(x),cons(lastbit(x),l)) (20)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.