Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/LengthOfFiniteLists_nosorts-noand_L)

The rewrite relation of the following TRS is considered.

U12(tt) → s(length(L)) (1)
zeros → cons(0) (2)
U11(tt) → U12(tt) (3)
length(nil) → 0 (4)
length(cons(N)) → U11(tt) (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.