Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex6_9_Luc02c_L)

The rewrite relation of the following TRS is considered.

2nd(cons(X)) → 2nd(cons1(X,X1)) (1)
2nd(cons1(X,cons(Y))) → Y (2)
from(X) → cons(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.