Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExIntrod_GM04_L)

The rewrite relation of the following TRS is considered.

hd(cons) → X (1)
tl(cons) → Y (2)
nats → adx(zeros) (3)
zeros → cons (4)
incr(cons) → cons (5)
adx(cons) → incr(cons) (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.