Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/Ex4_7_37_Bor03)

The rewrite relation of the following TRS is considered.

from(X) → cons(X,from(s(X))) (1)
sel(0,cons(X,XS)) → X (2)
sel(s(N),cons(X,XS)) → sel(N,XS) (3)
minus(X,0) → 0 (4)
minus(s(X),s(Y)) → minus(X,Y) (5)
quot(0,s(Y)) → 0 (6)
quot(s(X),s(Y)) → s(quot(minus(X,Y),s(Y))) (7)
zWquot(XS,nil) → nil (8)
zWquot(nil,XS) → nil (9)
zWquot(cons(X,XS),cons(Y,YS)) → cons(quot(X,Y),zWquot(XS,YS)) (10)
The evaluation strategy is outermost

Property / Task

Prove or disprove termination.

Answer / Result

No.

Proof (by AProVE @ termCOMP 2023)

1 Loop

The following loop proves nontermination.

t0 = from(X)
→ cons(X,from(s(X)))
= t1
where t1 = C[t0σ] and σ = {X/s(X)} and C = cons(X,☐)