Certification Problem

Input (TPDB TRS_Outermost/Strategy_outermost_added_08/Ex4_DLMMU04_Z)

The rewrite relation of the following TRS is considered.

and(tt,T) → T (1)
isNatIList(IL) → isNatList(activate(IL)) (2)
isNat(n__0) → tt (3)
isNat(n__s(N)) → isNat(activate(N)) (4)
isNat(n__length(L)) → isNatList(activate(L)) (5)
isNatIList(n__zeros) → tt (6)
isNatIList(n__cons(N,IL)) → and(isNat(activate(N)),isNatIList(activate(IL))) (7)
isNatList(n__nil) → tt (8)
isNatList(n__cons(N,L)) → and(isNat(activate(N)),isNatList(activate(L))) (9)
isNatList(n__take(N,IL)) → and(isNat(activate(N)),isNatIList(activate(IL))) (10)
zeros → cons(0,n__zeros) (11)
take(0,IL) → uTake1(isNatIList(IL)) (12)
uTake1(tt) → nil (13)
take(s(M),cons(N,IL)) → uTake2(and(isNat(M),and(isNat(N),isNatIList(activate(IL)))),M,N,activate(IL)) (14)
uTake2(tt,M,N,IL) → cons(activate(N),n__take(activate(M),activate(IL))) (15)
length(cons(N,L)) → uLength(and(isNat(N),isNatList(activate(L))),activate(L)) (16)
uLength(tt,L) → s(length(activate(L))) (17)
0 → n__0 (18)
s(X) → n__s(X) (19)
length(X) → n__length(X) (20)
zeros → n__zeros (21)
cons(X1,X2) → n__cons(X1,X2) (22)
nil → n__nil (23)
take(X1,X2) → n__take(X1,X2) (24)
activate(n__0) → 0 (25)
activate(n__s(X)) → s(X) (26)
activate(n__length(X)) → length(X) (27)
activate(n__zeros) → zeros (28)
activate(n__cons(X1,X2)) → cons(X1,X2) (29)
activate(n__nil) → nil (30)
activate(n__take(X1,X2)) → take(X1,X2) (31)
activate(X) → X (32)
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 = isNatList(activate(n__zeros))
→ isNatList(zeros)
→ isNatList(cons(0,n__zeros))
→ isNatList(n__cons(0,n__zeros))
→ and(isNat(activate(0)),isNatList(activate(n__zeros)))
= t4
where t4 = C[t0] and C = and(isNat(activate(0)),☐)