Certification Problem

Input (TPDB TRS_Innermost/AG01_innermost/#4.32)

The rewrite relation of the following TRS is considered.

f(x,c(y)) f(x,s(f(y,y))) (1)
f(s(x),s(y)) f(x,s(c(s(y)))) (2)
The evaluation strategy is innermost.

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Dependency Pair Transformation

The following set of initial dependency pairs has been identified.
f#(x,c(y)) f#(x,s(f(y,y))) (3)
f#(x,c(y)) f#(y,y) (4)
f#(s(x),s(y)) f#(x,s(c(s(y)))) (5)

1.1 Dependency Graph Processor

The dependency pairs are split into 2 components.