Certification Problem

Input (TPDB TRS_Standard/AG01/#3.42)

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)
conv(0) cons(nil,0) (7)
conv(s(x)) cons(conv(half(s(x))),lastbit(s(x))) (8)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by NaTT @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
half#(s(s(x))) half#(x) (9)
conv#(s(x)) lastbit#(s(x)) (10)
conv#(s(x)) conv#(half(s(x))) (11)
lastbit#(s(s(x))) lastbit#(x) (12)
conv#(s(x)) half#(s(x)) (13)

1.1 Dependency Graph Processor

The dependency pairs are split into 3 components.