Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex3_12_Luc96a_L)

The rewrite relation of the following TRS is considered.

sel(s(X),cons(Y)) → sel(X,Z) (1)
from(X) → cons(X) (2)
sel(0,cons(X)) → X (3)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Variable Condition Violated

The TRS violates one of the two variable conditions. Thus, it is not terminating.