Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex4_7_56_Bor03_L)

The rewrite relation of the following TRS is considered.

after(s(N),cons(X)) → after(N,XS) (1)
from(X) → cons(X) (2)
after(0,XS) → XS (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.