Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex1_Luc02b_L)

The rewrite relation of the following TRS is considered.

sel(s(X),cons(Y)) → sel(X,Z) (1)
from(X) → cons(X) (2)
first(0,Z) → nil (3)
first(s(X),cons(Y)) → cons(Y) (4)
sel(0,cons(X)) → X (5)

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.