Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex4_Zan97_L)

The rewrite relation of the following TRS is considered.

sel(s(X),cons(Y)) → sel(X,Z) (1)
f(X) → cons(X) (2)
g(0) → s(0) (3)
g(s(X)) → s(s(g(X))) (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.