Certification Problem

Input (TPDB TRS_Standard/HirokawaMiddeldorp_04/t004)

The rewrite relation of the following TRS is considered.

f(s(x)) s(f(f(p(s(x))))) (1)
f(0) 0 (2)
p(s(x)) 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(s(x)) s(f(f(p(s(x))))) (1)
f(0'(x)) 0'(x) (4)
p(s(x)) x (3)

1.1 String Reversal

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

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

The following set of initial dependency pairs has been identified.
s#(f(x)) s#(p(f(f(s(x))))) (8)
s#(f(x)) s#(x) (9)
0'#(f(x)) 0'#(x) (10)

1.1.1.1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.