Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/Ex1_Luc04b_L)

The rewrite relation of the following TRS is considered.

tail(cons(X)) → XS (1)
nats → cons(0) (2)
pairs → cons(0) (3)
odds → incr(pairs) (4)
incr(cons(X)) → cons(s(X)) (5)
head(cons(X)) → X (6)

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.