Certification Problem

Input (TPDB TRS_Standard/AG01/#3.24)

The rewrite relation of the following TRS is considered.

f(0) → s(0) (1)
f(s(0)) → s(0) (2)
f(s(s(x))) → f(f(s(x))) (3)

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
f(0'(x)) → s(0'(x)) (4)
f(s(0'(x))) → s(0'(x)) (5)
f(s(s(x))) → f(f(s(x))) (3)

1.1 String Reversal

Since only unary symbols occur, one can reverse all terms and obtains the TRS
0'(f(x)) → 0'(s(x)) (6)
0'(s(f(x))) → 0'(s(x)) (7)
s(s(f(x))) → s(f(f(x))) (8)

1.1.1 Bounds

The given TRS is match-(raise)-bounded by 3. This is shown by the following automaton.