Certification Problem

Input (TPDB TRS_Innermost/AG01_innermost/#4.28)

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)
bits(0) → 0 (4)
bits(s(x)) → s(bits(half(s(x)))) (5)
The evaluation strategy is innermost.

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Constant to Unary

Every constant is turned into a unary function symbol to obtain the TRS
half(0'(x)) → 0'(x) (6)
half(s(0'(x))) → 0'(x) (7)
half(s(s(x))) → s(half(x)) (3)
bits(0'(x)) → 0'(x) (8)
bits(s(x)) → s(bits(half(s(x)))) (5)

1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
0'(half(x)) → 0'(x) (9)
0'(s(half(x))) → 0'(x) (10)
s(s(half(x))) → half(s(x)) (11)
0'(bits(x)) → 0'(x) (12)
s(bits(x)) → s(half(bits(s(x)))) (13)

1.1.1 Rule Removal

Using the linear polynomial interpretation over the naturals
[0'(x1)] = 1 · x1
[half(x1)] = 1 · x1
[s(x1)] = 1 · x1
[bits(x1)] = 1 · x1 + 1
all of the following rules can be deleted.
0'(bits(x)) → 0'(x) (12)

1.1.1.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.1.1.1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
0'#(half(x)) → 0'#(x) (14)
0'#(s(half(x))) → 0'#(x) (15)
s#(s(half(x))) → s#(x) (16)
s#(bits(x)) → s#(half(bits(s(x)))) (17)
s#(bits(x)) → s#(x) (18)

1.1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.