Termination w.r.t. Q of the given QTRS could be disproven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ZEROS → CONS(0, n__zeros)
ZEROS → 0¹
U11¹(tt, L) → S(length(activate(L)))
U11¹(tt, L) → LENGTH(activate(L))
U11¹(tt, L) → ACTIVATE(L)
U21¹(tt) → NIL
U31¹(tt, IL, M, N) → CONS(activate(N), n__take(activate(M), activate(IL)))
U31¹(tt, IL, M, N) → ACTIVATE(N)
U31¹(tt, IL, M, N) → ACTIVATE(M)
U31¹(tt, IL, M, N) → ACTIVATE(IL)
AND(tt, X) → ACTIVATE(X)
ISNAT(n__length(V1)) → ISNATLIST(activate(V1))
ISNAT(n__length(V1)) → ACTIVATE(V1)
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ISNATILIST(V) → ISNATLIST(activate(V))
ISNATILIST(V) → ACTIVATE(V)
ISNATILIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))
ISNATILIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V2)
ISNATLIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatList(activate(V2)))
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
ISNATLIST(n__take(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))
ISNATLIST(n__take(V1, V2)) → ISNAT(activate(V1))
ISNATLIST(n__take(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__take(V1, V2)) → ACTIVATE(V2)
LENGTH(nil) → 0¹
LENGTH(cons(N, L)) → U11¹(and(isNatList(activate(L)), n__isNat(N)), activate(L))
LENGTH(cons(N, L)) → AND(isNatList(activate(L)), n__isNat(N))
LENGTH(cons(N, L)) → ISNATLIST(activate(L))
LENGTH(cons(N, L)) → ACTIVATE(L)
TAKE(0, IL) → U21¹(isNatIList(IL))
TAKE(0, IL) → ISNATILIST(IL)
TAKE(s(M), cons(N, IL)) → U31¹(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
TAKE(s(M), cons(N, IL)) → AND(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(activate(IL))
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
TAKE(s(M), cons(N, IL)) → ISNAT(M)
ACTIVATE(n__zeros) → ZEROS
ACTIVATE(n__take(X1, X2)) → TAKE(X1, X2)
ACTIVATE(n__0) → 0¹
ACTIVATE(n__length(X)) → LENGTH(X)
ACTIVATE(n__s(X)) → S(X)
ACTIVATE(n__cons(X1, X2)) → CONS(X1, X2)
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ACTIVATE(n__nil) → NIL
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ACTIVATE(n__isNat(X)) → ISNAT(X)
ACTIVATE(n__and(X1, X2)) → AND(X1, X2)

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 12 less nodes.

(4) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__take(X1, X2)) → TAKE(X1, X2)
TAKE(0, IL) → ISNATILIST(IL)
ISNATILIST(V) → ISNATLIST(activate(V))
ISNATLIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatList(activate(V2)))
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__length(X)) → LENGTH(X)
LENGTH(cons(N, L)) → U11¹(and(isNatList(activate(L)), n__isNat(N)), activate(L))
U11¹(tt, L) → LENGTH(activate(L))
LENGTH(cons(N, L)) → AND(isNatList(activate(L)), n__isNat(N))
LENGTH(cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__length(V1)) → ISNATLIST(activate(V1))
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNATILIST(V) → ACTIVATE(V)
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
ACTIVATE(n__isNat(X)) → ISNAT(X)
ISNAT(n__length(V1)) → ACTIVATE(V1)
ACTIVATE(n__and(X1, X2)) → AND(X1, X2)
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ISNATLIST(n__take(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))
ISNATLIST(n__take(V1, V2)) → ISNAT(activate(V1))
ISNATLIST(n__take(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__take(V1, V2)) → ACTIVATE(V2)
ISNATILIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))
ISNATILIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V2)
LENGTH(cons(N, L)) → ACTIVATE(L)
U11¹(tt, L) → ACTIVATE(L)
TAKE(s(M), cons(N, IL)) → U31¹(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
U31¹(tt, IL, M, N) → ACTIVATE(N)
U31¹(tt, IL, M, N) → ACTIVATE(M)
U31¹(tt, IL, M, N) → ACTIVATE(IL)
TAKE(s(M), cons(N, IL)) → AND(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(activate(IL))
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
TAKE(s(M), cons(N, IL)) → ISNAT(M)

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(5) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ACTIVATE(n__length(X)) → LENGTH(X)
ISNAT(n__length(V1)) → ISNATLIST(activate(V1))
ISNAT(n__length(V1)) → ACTIVATE(V1)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x₁)) = x₁   
POL(AND(x₁, x₂)) = x₂   
POL(ISNAT(x₁)) = x₁   
POL(ISNATILIST(x₁)) = x₁   
POL(ISNATLIST(x₁)) = x₁   
POL(LENGTH(x₁)) = x₁   
POL(TAKE(x₁, x₂)) = x₁ + x₂   
POL(U11(x₁, x₂)) = 1 + x₁ + x₂   
POL(U11¹(x₁, x₂)) = x₂   
POL(U21(x₁)) = 0   
POL(U31(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄   
POL(U31¹(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄   
POL(activate(x₁)) = x₁   
POL(and(x₁, x₂)) = x₂   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(isNat(x₁)) = x₁   
POL(isNatIList(x₁)) = x₁   
POL(isNatList(x₁)) = x₁   
POL(length(x₁)) = 1 + x₁   
POL(n__0) = 0   
POL(n__and(x₁, x₂)) = x₂   
POL(n__cons(x₁, x₂)) = x₁ + x₂   
POL(n__isNat(x₁)) = x₁   
POL(n__isNatIList(x₁)) = x₁   
POL(n__isNatList(x₁)) = x₁   
POL(n__length(x₁)) = 1 + x₁   
POL(n__nil) = 0   
POL(n__s(x₁)) = x₁   
POL(n__take(x₁, x₂)) = x₁ + x₂   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x₁)) = x₁   
POL(take(x₁, x₂)) = x₁ + x₂   
POL(tt) = 0   
POL(zeros) = 0   

The following usable rules [FROCOS05] were oriented:

U11(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
U21(tt) → nil
isNat(n__0) → tt
activate(X) → X
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatIList(V) → isNatList(activate(V))
activate(n__isNat(X)) → isNat(X)
isNat(n__s(V1)) → isNat(activate(V1))
and(tt, X) → activate(X)
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__and(X1, X2)) → and(X1, X2)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
0 → n__0
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt

(6) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__take(X1, X2)) → TAKE(X1, X2)
TAKE(0, IL) → ISNATILIST(IL)
ISNATILIST(V) → ISNATLIST(activate(V))
ISNATLIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatList(activate(V2)))
AND(tt, X) → ACTIVATE(X)
LENGTH(cons(N, L)) → U11¹(and(isNatList(activate(L)), n__isNat(N)), activate(L))
U11¹(tt, L) → LENGTH(activate(L))
LENGTH(cons(N, L)) → AND(isNatList(activate(L)), n__isNat(N))
LENGTH(cons(N, L)) → ISNATLIST(activate(L))
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNATILIST(V) → ACTIVATE(V)
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
ACTIVATE(n__isNat(X)) → ISNAT(X)
ACTIVATE(n__and(X1, X2)) → AND(X1, X2)
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ISNATLIST(n__take(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))
ISNATLIST(n__take(V1, V2)) → ISNAT(activate(V1))
ISNATLIST(n__take(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__take(V1, V2)) → ACTIVATE(V2)
ISNATILIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))
ISNATILIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V2)
LENGTH(cons(N, L)) → ACTIVATE(L)
U11¹(tt, L) → ACTIVATE(L)
TAKE(s(M), cons(N, IL)) → U31¹(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
U31¹(tt, IL, M, N) → ACTIVATE(N)
U31¹(tt, IL, M, N) → ACTIVATE(M)
U31¹(tt, IL, M, N) → ACTIVATE(IL)
TAKE(s(M), cons(N, IL)) → AND(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(activate(IL))
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
TAKE(s(M), cons(N, IL)) → ISNAT(M)

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 4 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TAKE(0, IL) → ISNATILIST(IL)
ISNATILIST(V) → ISNATLIST(activate(V))
ISNATLIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatList(activate(V2)))
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__take(X1, X2)) → TAKE(X1, X2)
TAKE(s(M), cons(N, IL)) → U31¹(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
U31¹(tt, IL, M, N) → ACTIVATE(N)
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNATILIST(V) → ACTIVATE(V)
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__isNat(X)) → ISNAT(X)
ACTIVATE(n__and(X1, X2)) → AND(X1, X2)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
ISNATLIST(n__take(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))
ISNATLIST(n__take(V1, V2)) → ISNAT(activate(V1))
ISNATLIST(n__take(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__take(V1, V2)) → ACTIVATE(V2)
ISNATILIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))
ISNATILIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V2)
U31¹(tt, IL, M, N) → ACTIVATE(M)
U31¹(tt, IL, M, N) → ACTIVATE(IL)
TAKE(s(M), cons(N, IL)) → AND(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(activate(IL))
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
TAKE(s(M), cons(N, IL)) → ISNAT(M)

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(10) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ACTIVATE(n__take(X1, X2)) → TAKE(X1, X2)
ISNATLIST(n__take(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))
ISNATLIST(n__take(V1, V2)) → ISNAT(activate(V1))
ISNATLIST(n__take(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__take(V1, V2)) → ACTIVATE(V2)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x₁)) = x₁   
POL(AND(x₁, x₂)) = x₂   
POL(ISNAT(x₁)) = x₁   
POL(ISNATILIST(x₁)) = x₁   
POL(ISNATLIST(x₁)) = x₁   
POL(TAKE(x₁, x₂)) = x₁ + x₂   
POL(U11(x₁, x₂)) = x₁ + x₂   
POL(U21(x₁)) = 1   
POL(U31(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃ + x₄   
POL(U31¹(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄   
POL(activate(x₁)) = x₁   
POL(and(x₁, x₂)) = x₂   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(isNat(x₁)) = x₁   
POL(isNatIList(x₁)) = x₁   
POL(isNatList(x₁)) = x₁   
POL(length(x₁)) = x₁   
POL(n__0) = 0   
POL(n__and(x₁, x₂)) = x₂   
POL(n__cons(x₁, x₂)) = x₁ + x₂   
POL(n__isNat(x₁)) = x₁   
POL(n__isNatIList(x₁)) = x₁   
POL(n__isNatList(x₁)) = x₁   
POL(n__length(x₁)) = x₁   
POL(n__nil) = 1   
POL(n__s(x₁)) = x₁   
POL(n__take(x₁, x₂)) = 1 + x₁ + x₂   
POL(n__zeros) = 0   
POL(nil) = 1   
POL(s(x₁)) = x₁   
POL(take(x₁, x₂)) = 1 + x₁ + x₂   
POL(tt) = 0   
POL(zeros) = 0   

The following usable rules [FROCOS05] were oriented:

U11(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
U21(tt) → nil
isNat(n__0) → tt
activate(X) → X
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatIList(V) → isNatList(activate(V))
activate(n__isNat(X)) → isNat(X)
isNat(n__s(V1)) → isNat(activate(V1))
and(tt, X) → activate(X)
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__and(X1, X2)) → and(X1, X2)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
0 → n__0
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

TAKE(0, IL) → ISNATILIST(IL)
ISNATILIST(V) → ISNATLIST(activate(V))
ISNATLIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatList(activate(V2)))
AND(tt, X) → ACTIVATE(X)
TAKE(s(M), cons(N, IL)) → U31¹(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
U31¹(tt, IL, M, N) → ACTIVATE(N)
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNATILIST(V) → ACTIVATE(V)
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__isNat(X)) → ISNAT(X)
ACTIVATE(n__and(X1, X2)) → AND(X1, X2)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
ISNATILIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))
ISNATILIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V2)
U31¹(tt, IL, M, N) → ACTIVATE(M)
U31¹(tt, IL, M, N) → ACTIVATE(IL)
TAKE(s(M), cons(N, IL)) → AND(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(activate(IL))
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
TAKE(s(M), cons(N, IL)) → ISNAT(M)

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(12) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 9 less nodes.

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatList(activate(V2)))
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNATILIST(V) → ISNATLIST(activate(V))
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ACTIVATE(n__isNat(X)) → ISNAT(X)
ACTIVATE(n__and(X1, X2)) → AND(X1, X2)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
ISNATILIST(V) → ACTIVATE(V)
ISNATILIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))
ISNATILIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V2)

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(14) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ACTIVATE(n__isNat(X)) → ISNAT(X)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x₁)) = x₁   
POL(AND(x₁, x₂)) = x₂   
POL(ISNAT(x₁)) = x₁   
POL(ISNATILIST(x₁)) = x₁   
POL(ISNATLIST(x₁)) = x₁   
POL(U11(x₁, x₂)) = x₂   
POL(U21(x₁)) = 0   
POL(U31(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄   
POL(activate(x₁)) = x₁   
POL(and(x₁, x₂)) = x₂   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(isNat(x₁)) = 1 + x₁   
POL(isNatIList(x₁)) = x₁   
POL(isNatList(x₁)) = x₁   
POL(length(x₁)) = x₁   
POL(n__0) = 0   
POL(n__and(x₁, x₂)) = x₂   
POL(n__cons(x₁, x₂)) = x₁ + x₂   
POL(n__isNat(x₁)) = 1 + x₁   
POL(n__isNatIList(x₁)) = x₁   
POL(n__isNatList(x₁)) = x₁   
POL(n__length(x₁)) = x₁   
POL(n__nil) = 0   
POL(n__s(x₁)) = x₁   
POL(n__take(x₁, x₂)) = x₁ + x₂   
POL(n__zeros) = 1   
POL(nil) = 0   
POL(s(x₁)) = x₁   
POL(take(x₁, x₂)) = x₁ + x₂   
POL(tt) = 0   
POL(zeros) = 1   

The following usable rules [FROCOS05] were oriented:

U11(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
U21(tt) → nil
isNat(n__0) → tt
activate(X) → X
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatIList(V) → isNatList(activate(V))
activate(n__isNat(X)) → isNat(X)
isNat(n__s(V1)) → isNat(activate(V1))
and(tt, X) → activate(X)
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__and(X1, X2)) → and(X1, X2)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
0 → n__0
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt

(15) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatList(activate(V2)))
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNATILIST(V) → ISNATLIST(activate(V))
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ACTIVATE(n__and(X1, X2)) → AND(X1, X2)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
ISNATILIST(V) → ACTIVATE(V)
ISNATILIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))
ISNATILIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V2)

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(16) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ISNATILIST(V) → ISNATLIST(activate(V))
ISNATILIST(V) → ACTIVATE(V)
ISNATILIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATILIST(n__cons(V1, V2)) → ACTIVATE(V2)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x₁)) = x₁   
POL(AND(x₁, x₂)) = x₂   
POL(ISNAT(x₁)) = x₁   
POL(ISNATILIST(x₁)) = 1 + x₁   
POL(ISNATLIST(x₁)) = x₁   
POL(U11(x₁, x₂)) = x₂   
POL(U21(x₁)) = 0   
POL(U31(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃ + x₄   
POL(activate(x₁)) = x₁   
POL(and(x₁, x₂)) = x₁ + x₂   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(isNat(x₁)) = x₁   
POL(isNatIList(x₁)) = 1 + x₁   
POL(isNatList(x₁)) = x₁   
POL(length(x₁)) = x₁   
POL(n__0) = 0   
POL(n__and(x₁, x₂)) = x₁ + x₂   
POL(n__cons(x₁, x₂)) = x₁ + x₂   
POL(n__isNat(x₁)) = x₁   
POL(n__isNatIList(x₁)) = 1 + x₁   
POL(n__isNatList(x₁)) = x₁   
POL(n__length(x₁)) = x₁   
POL(n__nil) = 0   
POL(n__s(x₁)) = x₁   
POL(n__take(x₁, x₂)) = 1 + x₁ + x₂   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x₁)) = x₁   
POL(take(x₁, x₂)) = 1 + x₁ + x₂   
POL(tt) = 0   
POL(zeros) = 0   

The following usable rules [FROCOS05] were oriented:

U11(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
U21(tt) → nil
isNat(n__0) → tt
activate(X) → X
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatIList(V) → isNatList(activate(V))
activate(n__isNat(X)) → isNat(X)
isNat(n__s(V1)) → isNat(activate(V1))
and(tt, X) → activate(X)
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__and(X1, X2)) → and(X1, X2)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
0 → n__0
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt

(17) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatList(activate(V2)))
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ACTIVATE(n__and(X1, X2)) → AND(X1, X2)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)
ISNATILIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(18) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ISNATLIST(n__cons(V1, V2)) → ISNAT(activate(V1))
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V1)
ISNATLIST(n__cons(V1, V2)) → ACTIVATE(V2)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x₁)) = x₁   
POL(AND(x₁, x₂)) = x₂   
POL(ISNAT(x₁)) = x₁   
POL(ISNATILIST(x₁)) = 1 + x₁   
POL(ISNATLIST(x₁)) = 1 + x₁   
POL(U11(x₁, x₂)) = x₂   
POL(U21(x₁)) = 0   
POL(U31(x₁, x₂, x₃, x₄)) = x₂ + x₄   
POL(activate(x₁)) = x₁   
POL(and(x₁, x₂)) = x₂   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(isNat(x₁)) = 1 + x₁   
POL(isNatIList(x₁)) = 1 + x₁   
POL(isNatList(x₁)) = 1 + x₁   
POL(length(x₁)) = x₁   
POL(n__0) = 0   
POL(n__and(x₁, x₂)) = x₂   
POL(n__cons(x₁, x₂)) = x₁ + x₂   
POL(n__isNat(x₁)) = 1 + x₁   
POL(n__isNatIList(x₁)) = 1 + x₁   
POL(n__isNatList(x₁)) = 1 + x₁   
POL(n__length(x₁)) = x₁   
POL(n__nil) = 0   
POL(n__s(x₁)) = x₁   
POL(n__take(x₁, x₂)) = x₂   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x₁)) = x₁   
POL(take(x₁, x₂)) = x₂   
POL(tt) = 0   
POL(zeros) = 0   

The following usable rules [FROCOS05] were oriented:

U11(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
U21(tt) → nil
isNat(n__0) → tt
activate(X) → X
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatIList(V) → isNatList(activate(V))
activate(n__isNat(X)) → isNat(X)
isNat(n__s(V1)) → isNat(activate(V1))
and(tt, X) → activate(X)
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__and(X1, X2)) → and(X1, X2)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
0 → n__0
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt

(19) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatList(activate(V2)))
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNAT(n__s(V1)) → ISNAT(activate(V1))
ISNAT(n__s(V1)) → ACTIVATE(V1)
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ACTIVATE(n__and(X1, X2)) → AND(X1, X2)
ISNATILIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(20) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 1 less node.

(21) Complex Obligation (AND)

(22) Obligation:

Q DP problem:
The TRS P consists of the following rules:

AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNATILIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatList(activate(V2)))
ACTIVATE(n__and(X1, X2)) → AND(X1, X2)

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(23) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ACTIVATE(n__and(X1, X2)) → AND(X1, X2)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x₁)) = x₁   
POL(AND(x₁, x₂)) = x₂   
POL(ISNATILIST(x₁)) = 0   
POL(ISNATLIST(x₁)) = 0   
POL(U11(x₁, x₂)) = 0   
POL(U21(x₁)) = 0   
POL(U31(x₁, x₂, x₃, x₄)) = 0   
POL(activate(x₁)) = 0   
POL(and(x₁, x₂)) = 0   
POL(cons(x₁, x₂)) = 0   
POL(isNat(x₁)) = 0   
POL(isNatIList(x₁)) = 0   
POL(isNatList(x₁)) = 0   
POL(length(x₁)) = 0   
POL(n__0) = 0   
POL(n__and(x₁, x₂)) = 1 + x₂   
POL(n__cons(x₁, x₂)) = 0   
POL(n__isNat(x₁)) = 0   
POL(n__isNatIList(x₁)) = 0   
POL(n__isNatList(x₁)) = 0   
POL(n__length(x₁)) = 0   
POL(n__nil) = 0   
POL(n__s(x₁)) = 0   
POL(n__take(x₁, x₂)) = 0   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x₁)) = 0   
POL(take(x₁, x₂)) = 0   
POL(tt) = 0   
POL(zeros) = 0   

The following usable rules [FROCOS05] were oriented: none

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNATILIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2)))
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatList(activate(V2)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(25) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATILIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatIList(activate(V2))) at position [0] we obtained the following new rules [LPAR04]:

ISNATILIST(n__cons(y0, y1)) → AND(n__isNat(activate(y0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__zeros, y1)) → AND(isNat(zeros), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__take(x0, x1), y1)) → AND(isNat(take(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatIList(activate(y1)))

(26) Obligation:

Q DP problem:
The TRS P consists of the following rules:

AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatList(activate(V2)))
ISNATILIST(n__cons(y0, y1)) → AND(n__isNat(activate(y0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__zeros, y1)) → AND(isNat(zeros), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__take(x0, x1), y1)) → AND(isNat(take(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatIList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(27) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(28) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNATILIST(n__cons(n__zeros, y1)) → AND(isNat(zeros), n__isNatIList(activate(y1)))
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatList(activate(V2)))
ISNATILIST(n__cons(n__take(x0, x1), y1)) → AND(isNat(take(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatIList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(29) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule ISNATLIST(n__cons(V1, V2)) → AND(isNat(activate(V1)), n__isNatList(activate(V2))) at position [0] we obtained the following new rules [LPAR04]:

ISNATLIST(n__cons(y0, y1)) → AND(n__isNat(activate(y0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__zeros, y1)) → AND(isNat(zeros), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__take(x0, x1), y1)) → AND(isNat(take(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))

(30) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNATILIST(n__cons(n__zeros, y1)) → AND(isNat(zeros), n__isNatIList(activate(y1)))
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATILIST(n__cons(n__take(x0, x1), y1)) → AND(isNat(take(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatIList(activate(y1)))
ISNATLIST(n__cons(y0, y1)) → AND(n__isNat(activate(y0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__zeros, y1)) → AND(isNat(zeros), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__take(x0, x1), y1)) → AND(isNat(take(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(31) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(32) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(n__cons(n__zeros, y1)) → AND(isNat(zeros), n__isNatIList(activate(y1)))
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNATILIST(n__cons(n__take(x0, x1), y1)) → AND(isNat(take(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatIList(activate(y1)))
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(n__zeros, y1)) → AND(isNat(zeros), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__take(x0, x1), y1)) → AND(isNat(take(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(33) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule AND(tt, X) → ACTIVATE(X) we obtained the following new rules [LPAR04]:

AND(tt, n__isNatIList(y_3)) → ACTIVATE(n__isNatIList(y_3))
AND(tt, n__isNatList(y_3)) → ACTIVATE(n__isNatList(y_3))

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATILIST(n__cons(n__zeros, y1)) → AND(isNat(zeros), n__isNatIList(activate(y1)))
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNATILIST(n__cons(n__take(x0, x1), y1)) → AND(isNat(take(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatIList(activate(y1)))
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(n__zeros, y1)) → AND(isNat(zeros), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__take(x0, x1), y1)) → AND(isNat(take(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))
AND(tt, n__isNatIList(y_3)) → ACTIVATE(n__isNatIList(y_3))
AND(tt, n__isNatList(y_3)) → ACTIVATE(n__isNatList(y_3))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(35) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.

(36) Complex Obligation (AND)

(37) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(n__cons(n__zeros, y1)) → AND(isNat(zeros), n__isNatList(activate(y1)))
AND(tt, n__isNatList(y_3)) → ACTIVATE(n__isNatList(y_3))
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(n__take(x0, x1), y1)) → AND(isNat(take(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(38) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ISNATLIST(n__cons(n__take(x0, x1), y1)) → AND(isNat(take(x0, x1)), n__isNatList(activate(y1)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x₁)) = x₁   
POL(AND(x₁, x₂)) = x₂   
POL(ISNATLIST(x₁)) = x₁   
POL(U11(x₁, x₂)) = x₂   
POL(U21(x₁)) = 1   
POL(U31(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃ + x₄   
POL(activate(x₁)) = x₁   
POL(and(x₁, x₂)) = x₁ + x₂   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(isNat(x₁)) = x₁   
POL(isNatIList(x₁)) = x₁   
POL(isNatList(x₁)) = x₁   
POL(length(x₁)) = x₁   
POL(n__0) = 0   
POL(n__and(x₁, x₂)) = x₁ + x₂   
POL(n__cons(x₁, x₂)) = x₁ + x₂   
POL(n__isNat(x₁)) = x₁   
POL(n__isNatIList(x₁)) = x₁   
POL(n__isNatList(x₁)) = x₁   
POL(n__length(x₁)) = x₁   
POL(n__nil) = 0   
POL(n__s(x₁)) = x₁   
POL(n__take(x₁, x₂)) = 1 + x₁ + x₂   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x₁)) = x₁   
POL(take(x₁, x₂)) = 1 + x₁ + x₂   
POL(tt) = 0   
POL(zeros) = 0   

The following usable rules [FROCOS05] were oriented:

U11(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
U21(tt) → nil
isNat(n__0) → tt
activate(X) → X
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatIList(V) → isNatList(activate(V))
activate(n__isNat(X)) → isNat(X)
isNat(n__s(V1)) → isNat(activate(V1))
and(tt, X) → activate(X)
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__and(X1, X2)) → and(X1, X2)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
0 → n__0
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNATLIST(n__cons(n__zeros, y1)) → AND(isNat(zeros), n__isNatList(activate(y1)))
AND(tt, n__isNatList(y_3)) → ACTIVATE(n__isNatList(y_3))
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(40) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ISNATLIST(n__cons(n__zeros, y1)) → AND(isNat(zeros), n__isNatList(activate(y1)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x₁)) = x₁   
POL(AND(x₁, x₂)) = x₂   
POL(ISNATLIST(x₁)) = x₁   
POL(U11(x₁, x₂)) = x₂   
POL(U21(x₁)) = 0   
POL(U31(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄   
POL(activate(x₁)) = x₁   
POL(and(x₁, x₂)) = x₂   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(isNat(x₁)) = x₁   
POL(isNatIList(x₁)) = x₁   
POL(isNatList(x₁)) = x₁   
POL(length(x₁)) = x₁   
POL(n__0) = 0   
POL(n__and(x₁, x₂)) = x₂   
POL(n__cons(x₁, x₂)) = x₁ + x₂   
POL(n__isNat(x₁)) = x₁   
POL(n__isNatIList(x₁)) = x₁   
POL(n__isNatList(x₁)) = x₁   
POL(n__length(x₁)) = x₁   
POL(n__nil) = 0   
POL(n__s(x₁)) = x₁   
POL(n__take(x₁, x₂)) = x₁ + x₂   
POL(n__zeros) = 1   
POL(nil) = 0   
POL(s(x₁)) = x₁   
POL(take(x₁, x₂)) = x₁ + x₂   
POL(tt) = 0   
POL(zeros) = 1   

The following usable rules [FROCOS05] were oriented:

U11(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
U21(tt) → nil
isNat(n__0) → tt
activate(X) → X
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatIList(V) → isNatList(activate(V))
activate(n__isNat(X)) → isNat(X)
isNat(n__s(V1)) → isNat(activate(V1))
and(tt, X) → activate(X)
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__and(X1, X2)) → and(X1, X2)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
0 → n__0
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt

(41) Obligation:

Q DP problem:
The TRS P consists of the following rules:

AND(tt, n__isNatList(y_3)) → ACTIVATE(n__isNatList(y_3))
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(42) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ISNATLIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatList(activate(y1)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x₁)) = x₁   
POL(AND(x₁, x₂)) = x₂   
POL(ISNATLIST(x₁)) = x₁   
POL(U11(x₁, x₂)) = x₂   
POL(U21(x₁)) = 0   
POL(U31(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₄   
POL(activate(x₁)) = x₁   
POL(and(x₁, x₂)) = x₂   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(isNat(x₁)) = x₁   
POL(isNatIList(x₁)) = 1 + x₁   
POL(isNatList(x₁)) = x₁   
POL(length(x₁)) = x₁   
POL(n__0) = 0   
POL(n__and(x₁, x₂)) = x₂   
POL(n__cons(x₁, x₂)) = x₁ + x₂   
POL(n__isNat(x₁)) = x₁   
POL(n__isNatIList(x₁)) = 1 + x₁   
POL(n__isNatList(x₁)) = x₁   
POL(n__length(x₁)) = x₁   
POL(n__nil) = 0   
POL(n__s(x₁)) = x₁   
POL(n__take(x₁, x₂)) = 1 + x₂   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x₁)) = x₁   
POL(take(x₁, x₂)) = 1 + x₂   
POL(tt) = 0   
POL(zeros) = 0   

The following usable rules [FROCOS05] were oriented:

U11(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
U21(tt) → nil
isNat(n__0) → tt
activate(X) → X
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatIList(V) → isNatList(activate(V))
activate(n__isNat(X)) → isNat(X)
isNat(n__s(V1)) → isNat(activate(V1))
and(tt, X) → activate(X)
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__and(X1, X2)) → and(X1, X2)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
0 → n__0
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt

(43) Obligation:

Q DP problem:
The TRS P consists of the following rules:

AND(tt, n__isNatList(y_3)) → ACTIVATE(n__isNatList(y_3))
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(44) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ISNATLIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatList(activate(y1)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x₁)) = x₁   
POL(AND(x₁, x₂)) = x₂   
POL(ISNATLIST(x₁)) = x₁   
POL(U11(x₁, x₂)) = x₂   
POL(U21(x₁)) = 1   
POL(U31(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₄   
POL(activate(x₁)) = x₁   
POL(and(x₁, x₂)) = x₂   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(isNat(x₁)) = x₁   
POL(isNatIList(x₁)) = x₁   
POL(isNatList(x₁)) = x₁   
POL(length(x₁)) = x₁   
POL(n__0) = 0   
POL(n__and(x₁, x₂)) = x₂   
POL(n__cons(x₁, x₂)) = x₁ + x₂   
POL(n__isNat(x₁)) = x₁   
POL(n__isNatIList(x₁)) = x₁   
POL(n__isNatList(x₁)) = x₁   
POL(n__length(x₁)) = x₁   
POL(n__nil) = 1   
POL(n__s(x₁)) = x₁   
POL(n__take(x₁, x₂)) = 1 + x₂   
POL(n__zeros) = 0   
POL(nil) = 1   
POL(s(x₁)) = x₁   
POL(take(x₁, x₂)) = 1 + x₂   
POL(tt) = 0   
POL(zeros) = 0   

The following usable rules [FROCOS05] were oriented:

U11(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
U21(tt) → nil
isNat(n__0) → tt
activate(X) → X
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatIList(V) → isNatList(activate(V))
activate(n__isNat(X)) → isNat(X)
isNat(n__s(V1)) → isNat(activate(V1))
and(tt, X) → activate(X)
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__and(X1, X2)) → and(X1, X2)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
0 → n__0
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt

(45) Obligation:

Q DP problem:
The TRS P consists of the following rules:

AND(tt, n__isNatList(y_3)) → ACTIVATE(n__isNatList(y_3))
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(46) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ISNATLIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatList(activate(y1)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x₁)) = x₁   
POL(AND(x₁, x₂)) = x₂   
POL(ISNATLIST(x₁)) = x₁   
POL(U11(x₁, x₂)) = 1 + x₂   
POL(U21(x₁)) = 0   
POL(U31(x₁, x₂, x₃, x₄)) = x₂ + x₃ + x₄   
POL(activate(x₁)) = x₁   
POL(and(x₁, x₂)) = x₁ + x₂   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(isNat(x₁)) = x₁   
POL(isNatIList(x₁)) = x₁   
POL(isNatList(x₁)) = x₁   
POL(length(x₁)) = 1 + x₁   
POL(n__0) = 0   
POL(n__and(x₁, x₂)) = x₁ + x₂   
POL(n__cons(x₁, x₂)) = x₁ + x₂   
POL(n__isNat(x₁)) = x₁   
POL(n__isNatIList(x₁)) = x₁   
POL(n__isNatList(x₁)) = x₁   
POL(n__length(x₁)) = 1 + x₁   
POL(n__nil) = 0   
POL(n__s(x₁)) = x₁   
POL(n__take(x₁, x₂)) = x₁ + x₂   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x₁)) = x₁   
POL(take(x₁, x₂)) = x₁ + x₂   
POL(tt) = 0   
POL(zeros) = 0   

The following usable rules [FROCOS05] were oriented:

U11(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
U21(tt) → nil
isNat(n__0) → tt
activate(X) → X
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatIList(V) → isNatList(activate(V))
activate(n__isNat(X)) → isNat(X)
isNat(n__s(V1)) → isNat(activate(V1))
and(tt, X) → activate(X)
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__and(X1, X2)) → and(X1, X2)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
0 → n__0
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt

(47) Obligation:

Q DP problem:
The TRS P consists of the following rules:

AND(tt, n__isNatList(y_3)) → ACTIVATE(n__isNatList(y_3))
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(48) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ISNATLIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatList(activate(y1)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x₁)) = x₁   
POL(AND(x₁, x₂)) = x₂   
POL(ISNATLIST(x₁)) = x₁   
POL(U11(x₁, x₂)) = x₂   
POL(U21(x₁)) = 1   
POL(U31(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃ + x₄   
POL(activate(x₁)) = x₁   
POL(and(x₁, x₂)) = x₂   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(isNat(x₁)) = 1 + x₁   
POL(isNatIList(x₁)) = 1 + x₁   
POL(isNatList(x₁)) = x₁   
POL(length(x₁)) = x₁   
POL(n__0) = 0   
POL(n__and(x₁, x₂)) = x₂   
POL(n__cons(x₁, x₂)) = x₁ + x₂   
POL(n__isNat(x₁)) = 1 + x₁   
POL(n__isNatIList(x₁)) = 1 + x₁   
POL(n__isNatList(x₁)) = x₁   
POL(n__length(x₁)) = x₁   
POL(n__nil) = 1   
POL(n__s(x₁)) = x₁   
POL(n__take(x₁, x₂)) = 1 + x₁ + x₂   
POL(n__zeros) = 0   
POL(nil) = 1   
POL(s(x₁)) = x₁   
POL(take(x₁, x₂)) = 1 + x₁ + x₂   
POL(tt) = 0   
POL(zeros) = 0   

The following usable rules [FROCOS05] were oriented:

U11(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
U21(tt) → nil
isNat(n__0) → tt
activate(X) → X
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatIList(V) → isNatList(activate(V))
activate(n__isNat(X)) → isNat(X)
isNat(n__s(V1)) → isNat(activate(V1))
and(tt, X) → activate(X)
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__and(X1, X2)) → and(X1, X2)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
0 → n__0
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt

(49) Obligation:

Q DP problem:
The TRS P consists of the following rules:

AND(tt, n__isNatList(y_3)) → ACTIVATE(n__isNatList(y_3))
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(50) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ISNATLIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatList(activate(y1)))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(ACTIVATE(x₁)) = x₁   
POL(AND(x₁, x₂)) = x₂   
POL(ISNATLIST(x₁)) = 1 + x₁   
POL(U11(x₁, x₂)) = 1 + x₂   
POL(U21(x₁)) = 0   
POL(U31(x₁, x₂, x₃, x₄)) = 1 + x₂ + x₃ + x₄   
POL(activate(x₁)) = x₁   
POL(and(x₁, x₂)) = x₂   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(isNat(x₁)) = x₁   
POL(isNatIList(x₁)) = 1 + x₁   
POL(isNatList(x₁)) = 1 + x₁   
POL(length(x₁)) = 1 + x₁   
POL(n__0) = 0   
POL(n__and(x₁, x₂)) = x₂   
POL(n__cons(x₁, x₂)) = x₁ + x₂   
POL(n__isNat(x₁)) = x₁   
POL(n__isNatIList(x₁)) = 1 + x₁   
POL(n__isNatList(x₁)) = 1 + x₁   
POL(n__length(x₁)) = 1 + x₁   
POL(n__nil) = 0   
POL(n__s(x₁)) = x₁   
POL(n__take(x₁, x₂)) = 1 + x₁ + x₂   
POL(n__zeros) = 0   
POL(nil) = 0   
POL(s(x₁)) = x₁   
POL(take(x₁, x₂)) = 1 + x₁ + x₂   
POL(tt) = 0   
POL(zeros) = 0   

The following usable rules [FROCOS05] were oriented:

U11(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
U21(tt) → nil
isNat(n__0) → tt
activate(X) → X
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatIList(V) → isNatList(activate(V))
activate(n__isNat(X)) → isNat(X)
isNat(n__s(V1)) → isNat(activate(V1))
and(tt, X) → activate(X)
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__and(X1, X2)) → and(X1, X2)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
0 → n__0
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt

(51) Obligation:

Q DP problem:
The TRS P consists of the following rules:

AND(tt, n__isNatList(y_3)) → ACTIVATE(n__isNatList(y_3))
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(52) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatList(activate(y1)))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(AND(x1, x2)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

+

/ 0 1 \ \ 0 0 /

·

x2

POL(tt) =

/ 0 \ \ 0 /

POL(n__isNatList(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 1 /

·

x1

POL(ACTIVATE(x1)) =

/ 0 \ \ 0 /

+

/ 0 1 \ \ 0 0 /

·

x1

POL(ISNATLIST(x1)) =

/ 0 \ \ 0 /

+

/ 0 1 \ \ 0 0 /

·

x1

POL(n__cons(x1, x2)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 1 0 /

·

x1

+

/ 0 0 \ \ 0 1 /

·

x2

POL(n__0) =

/ 0 \ \ 0 /

POL(isNat(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 1 /

·

x1

POL(0) =

/ 0 \ \ 0 /

POL(activate(x1)) =

/ 0 \ \ 0 /

+

/ 1 0 \ \ 0 1 /

·

x1

POL(n__s(x1)) =

/ 1 \ \ 0 /

+

/ 0 0 \ \ 0 1 /

·

x1

POL(s(x1)) =

/ 1 \ \ 0 /

+

/ 0 0 \ \ 0 1 /

·

x1

POL(cons(x1, x2)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 1 0 /

·

x1

+

/ 0 0 \ \ 0 1 /

·

x2

POL(n__and(x1, x2)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

+

/ 1 0 \ \ 0 1 /

·

x2

POL(and(x1, x2)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

+

/ 1 0 \ \ 0 1 /

·

x2

POL(U11(x1, x2)) =

/ 1 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

+

/ 0 0 \ \ 0 1 /

·

x2

POL(length(x1)) =

/ 1 \ \ 0 /

+

/ 0 0 \ \ 0 1 /

·

x1

POL(zeros) =

/ 0 \ \ 0 /

POL(n__zeros) =

/ 0 \ \ 0 /

POL(U31(x1, x2, x3, x4)) =

/ 1 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

+

/ 0 0 \ \ 0 1 /

·

x2

+

/ 0 0 \ \ 0 0 /

·

x3

+

/ 0 0 \ \ 1 0 /

·

x4

POL(n__take(x1, x2)) =

/ 0 \ \ 0 /

+

/ 1 0 \ \ 0 0 /

·

x1

+

/ 0 0 \ \ 0 1 /

·

x2

POL(U21(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

POL(nil) =

/ 0 \ \ 0 /

POL(n__nil) =

/ 0 \ \ 0 /

POL(isNatList(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 1 /

·

x1

POL(isNatIList(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 1 /

·

x1

POL(n__isNat(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 1 /

·

x1

POL(n__isNatIList(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 1 /

·

x1

POL(n__length(x1)) =

/ 1 \ \ 0 /

+

/ 0 0 \ \ 0 1 /

·

x1

POL(take(x1, x2)) =

/ 0 \ \ 0 /

+

/ 1 0 \ \ 0 0 /

·

x1

+

/ 0 0 \ \ 0 1 /

·

x2

The following usable rules [FROCOS05] were oriented:

U11(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
U21(tt) → nil
isNat(n__0) → tt
activate(X) → X
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatIList(V) → isNatList(activate(V))
activate(n__isNat(X)) → isNat(X)
isNat(n__s(V1)) → isNat(activate(V1))
and(tt, X) → activate(X)
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__and(X1, X2)) → and(X1, X2)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
0 → n__0
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt

(53) Obligation:

Q DP problem:
The TRS P consists of the following rules:

AND(tt, n__isNatList(y_3)) → ACTIVATE(n__isNatList(y_3))
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(54) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatList(activate(y1)))

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(AND(x1, x2)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

+

/ 0 1 \ \ 0 0 /

·

x2

POL(tt) =

/ 0 \ \ 0 /

POL(n__isNatList(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 1 0 /

·

x1

POL(ACTIVATE(x1)) =

/ 0 \ \ 0 /

+

/ 0 1 \ \ 0 0 /

·

x1

POL(ISNATLIST(x1)) =

/ 0 \ \ 0 /

+

/ 1 0 \ \ 0 0 /

·

x1

POL(n__cons(x1, x2)) =

/ 0 \ \ 1 /

+

/ 0 1 \ \ 0 0 /

·

x1

+

/ 1 0 \ \ 0 0 /

·

x2

POL(n__0) =

/ 0 \ \ 0 /

POL(isNat(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 1 /

·

x1

POL(0) =

/ 0 \ \ 0 /

POL(activate(x1)) =

/ 0 \ \ 0 /

+

/ 1 0 \ \ 0 1 /

·

x1

POL(cons(x1, x2)) =

/ 0 \ \ 1 /

+

/ 0 1 \ \ 0 0 /

·

x1

+

/ 1 0 \ \ 0 0 /

·

x2

POL(n__and(x1, x2)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

+

/ 1 0 \ \ 0 1 /

·

x2

POL(and(x1, x2)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

+

/ 1 0 \ \ 0 1 /

·

x2

POL(U11(x1, x2)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

+

/ 0 0 \ \ 1 0 /

·

x2

POL(s(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 1 /

·

x1

POL(length(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 1 0 /

·

x1

POL(zeros) =

/ 0 \ \ 1 /

POL(n__zeros) =

/ 0 \ \ 1 /

POL(U31(x1, x2, x3, x4)) =

/ 1 \ \ 1 /

+

/ 0 0 \ \ 0 0 /

·

x1

+

/ 1 0 \ \ 0 0 /

·

x2

+

/ 0 1 \ \ 0 0 /

·

x3

+

/ 0 1 \ \ 0 0 /

·

x4

POL(n__take(x1, x2)) =

/ 1 \ \ 0 /

+

/ 0 1 \ \ 0 0 /

·

x1

+

/ 1 0 \ \ 0 1 /

·

x2

POL(U21(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

POL(nil) =

/ 0 \ \ 0 /

POL(n__nil) =

/ 0 \ \ 0 /

POL(isNatList(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 1 0 /

·

x1

POL(isNatIList(x1)) =

/ 0 \ \ 1 /

+

/ 0 0 \ \ 1 0 /

·

x1

POL(n__isNat(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 1 /

·

x1

POL(n__s(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 1 /

·

x1

POL(n__isNatIList(x1)) =

/ 0 \ \ 1 /

+

/ 0 0 \ \ 1 0 /

·

x1

POL(n__length(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 1 0 /

·

x1

POL(take(x1, x2)) =

/ 1 \ \ 0 /

+

/ 0 1 \ \ 0 0 /

·

x1

+

/ 1 0 \ \ 0 1 /

·

x2

The following usable rules [FROCOS05] were oriented:

U11(tt, L) → s(length(activate(L)))
zeros → cons(0, n__zeros)
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
U21(tt) → nil
isNat(n__0) → tt
activate(X) → X
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatIList(V) → isNatList(activate(V))
activate(n__isNat(X)) → isNat(X)
isNat(n__s(V1)) → isNat(activate(V1))
and(tt, X) → activate(X)
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__and(X1, X2)) → and(X1, X2)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
length(X) → n__length(X)
0 → n__0
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt

(55) Obligation:

Q DP problem:
The TRS P consists of the following rules:

AND(tt, n__isNatList(y_3)) → ACTIVATE(n__isNatList(y_3))
ACTIVATE(n__isNatList(X)) → ISNATLIST(X)
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(56) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = ACTIVATE(n__isNatList(activate(n__zeros))) evaluates to t =ACTIVATE(n__isNatList(activate(n__zeros)))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [ ]

---

Rewriting sequence

ACTIVATE(n__isNatList(activate(n__zeros))) → ACTIVATE(n__isNatList(zeros))
with rule activate(n__zeros) → zeros at position [0,0] and matcher [ ]

ACTIVATE(n__isNatList(zeros)) → ACTIVATE(n__isNatList(cons(0, n__zeros)))
with rule zeros → cons(0, n__zeros) at position [0,0] and matcher [ ]

ACTIVATE(n__isNatList(cons(0, n__zeros))) → ACTIVATE(n__isNatList(cons(n__0, n__zeros)))
with rule 0 → n__0 at position [0,0,0] and matcher [ ]

ACTIVATE(n__isNatList(cons(n__0, n__zeros))) → ACTIVATE(n__isNatList(n__cons(n__0, n__zeros)))
with rule cons(X1, X2) → n__cons(X1, X2) at position [0,0] and matcher [X1 / n__0, X2 / n__zeros]

ACTIVATE(n__isNatList(n__cons(n__0, n__zeros))) → ISNATLIST(n__cons(n__0, n__zeros))
with rule ACTIVATE(n__isNatList(X)) → ISNATLIST(X) at position [] and matcher [X / n__cons(n__0, n__zeros)]

ISNATLIST(n__cons(n__0, n__zeros)) → AND(isNat(n__0), n__isNatList(activate(n__zeros)))
with rule ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1))) at position [] and matcher [x0 / n__0, y1 / n__zeros]

AND(isNat(n__0), n__isNatList(activate(n__zeros))) → AND(tt, n__isNatList(activate(n__zeros)))
with rule isNat(n__0) → tt at position [0] and matcher [ ]

AND(tt, n__isNatList(activate(n__zeros))) → ACTIVATE(n__isNatList(activate(n__zeros)))
with rule AND(tt, n__isNatList(y_3)) → ACTIVATE(n__isNatList(y_3))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.

(57) FALSE

(58) Obligation:

Q DP problem:
The TRS P consists of the following rules:

AND(tt, n__isNatIList(y_3)) → ACTIVATE(n__isNatIList(y_3))
ACTIVATE(n__isNatIList(X)) → ISNATILIST(X)
ISNATILIST(n__cons(n__zeros, y1)) → AND(isNat(zeros), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__take(x0, x1), y1)) → AND(isNat(take(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__length(x0), y1)) → AND(isNat(length(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__s(x0), y1)) → AND(isNat(s(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNatIList(x0), y1)) → AND(isNat(isNatIList(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__nil, y1)) → AND(isNat(nil), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNatList(x0), y1)) → AND(isNat(isNatList(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__isNat(x0), y1)) → AND(isNat(isNat(x0)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(x0, x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatIList(activate(y1)))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(59) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ISNAT(n__s(V1)) → ISNAT(activate(V1))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(60) Obligation:

Q DP problem:
The TRS P consists of the following rules:

LENGTH(cons(N, L)) → U11¹(and(isNatList(activate(L)), n__isNat(N)), activate(L))
U11¹(tt, L) → LENGTH(activate(L))

The TRS R consists of the following rules:

zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
and(tt, X) → activate(X)
isNat(n__0) → tt
isNat(n__length(V1)) → isNatList(activate(V1))
isNat(n__s(V1)) → isNat(activate(V1))
isNatIList(V) → isNatList(activate(V))
isNatIList(n__zeros) → tt
isNatIList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
isNatList(n__nil) → tt
isNatList(n__cons(V1, V2)) → and(isNat(activate(V1)), n__isNatList(activate(V2)))
isNatList(n__take(V1, V2)) → and(isNat(activate(V1)), n__isNatIList(activate(V2)))
length(nil) → 0
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
take(0, IL) → U21(isNatIList(IL))
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(isNat(M), n__isNat(N))), activate(IL), M, N)
zeros → n__zeros
take(X1, X2) → n__take(X1, X2)
0 → n__0
length(X) → n__length(X)
s(X) → n__s(X)
cons(X1, X2) → n__cons(X1, X2)
isNatIList(X) → n__isNatIList(X)
nil → n__nil
isNatList(X) → n__isNatList(X)
isNat(X) → n__isNat(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(X1, X2)
activate(n__0) → 0
activate(n__length(X)) → length(X)
activate(n__s(X)) → s(X)
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(n__isNatIList(X)) → isNatIList(X)
activate(n__nil) → nil
activate(n__isNatList(X)) → isNatList(X)
activate(n__isNat(X)) → isNat(X)
activate(n__and(X1, X2)) → and(X1, X2)
activate(X) → X

Q is empty.
We have to consider all minimal (P,Q,R)-chains.