Certification Problem

Input (TPDB TRS_Standard/Transformed_CSR_04/ExIntrod_GM04_Z)

The rewrite relation of the following TRS is considered.

nats → adx(zeros) (1)
zeros → cons(n__0,n__zeros) (2)
incr(cons(X,Y)) → cons(n__s(activate(X)),n__incr(activate(Y))) (3)
adx(cons(X,Y)) → incr(cons(activate(X),n__adx(activate(Y)))) (4)
hd(cons(X,Y)) → activate(X) (5)
tl(cons(X,Y)) → activate(Y) (6)
0 → n__0 (7)
zeros → n__zeros (8)
s(X) → n__s(X) (9)
incr(X) → n__incr(X) (10)
adx(X) → n__adx(X) (11)
activate(n__0) → 0 (12)
activate(n__zeros) → zeros (13)
activate(n__s(X)) → s(X) (14)
activate(n__incr(X)) → incr(X) (15)
activate(n__adx(X)) → adx(X) (16)
activate(X) → X (17)

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by ttt2 @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = incr(cons(X,n__adx(cons(x39262,n__zeros))))
→ cons(n__s(activate(X)),n__incr(activate(n__adx(cons(x39262,n__zeros)))))
→ cons(n__s(activate(X)),n__incr(adx(cons(x39262,n__zeros))))
→ cons(n__s(activate(X)),n__incr(incr(cons(activate(x39262),n__adx(activate(n__zeros))))))
→ cons(n__s(activate(X)),n__incr(incr(cons(activate(x39262),n__adx(zeros)))))
→ cons(n__s(activate(X)),n__incr(incr(cons(activate(x39262),n__adx(cons(n__0,n__zeros))))))
= t5
where t5 = C[t0σ] and σ = {x39262/n__0, X/activate(x39262)} and C = cons(n__s(activate(X)),n__incr(☐))