Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/Ex4_DLMMU04_L)

The rewrite relation of the following TRS is considered.

uTake2(tt) → cons(N) (1)
uLength(tt) → s(length(L)) (2)
and(tt,T) → T (3)
isNatIList → isNatList (4)
isNat → tt (5)
isNat → isNat (6)
isNat → isNatList (7)
isNatIList → tt (8)
isNatIList → and(isNat,isNatIList) (9)
isNatList → tt (10)
isNatList → and(isNat,isNatList) (11)
isNatList → and(isNat,isNatIList) (12)
zeros → cons(0) (13)
take(0,IL) → uTake1(isNatIList) (14)
uTake1(tt) → nil (15)
take(s(M),cons(N)) → uTake2(and(isNat,and(isNat,isNatIList))) (16)
length(cons(N)) → uLength(and(isNat,isNatList)) (17)
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 = uTake2(tt)
→ cons(uTake2(tt))
= t1
where t1 = C[t0] and C = cons(☐)