Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex26_Luc03b_L)

The rewrite relation of the following TRS is considered.

terms(N) → cons(recip(sqr(N))) (1)
sqr(0) → 0 (2)
sqr(s) → s (3)
dbl(0) → 0 (4)
dbl(s) → s (5)
add(0,X) → X (6)
add(s,Y) → s (7)
first(0,X) → nil (8)
first(s,cons(Y)) → cons(Y) (9)

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.
terms#(N) → sqr#(N) (10)

1.1 Dependency Graph Processor

The dependency pairs are split into 0 components.