(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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 → 01
U111(tt, L) → S(length(activate(L)))
U111(tt, L) → LENGTH(activate(L))
U111(tt, L) → ACTIVATE(L)
U211(tt) → NIL
U311(tt, IL, M, N) → CONS(activate(N), n__take(activate(M), activate(IL)))
U311(tt, IL, M, N) → ACTIVATE(N)
U311(tt, IL, M, N) → ACTIVATE(M)
U311(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) → 01
LENGTH(cons(N, L)) → U111(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) → U211(isNatIList(IL))
TAKE(0, IL) → ISNATILIST(IL)
TAKE(s(M), cons(N, IL)) → U311(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
TAKE(s(M), cons(N, IL)) → AND(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(activate(IL))
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
ACTIVATE(n__zeros) → ZEROS
ACTIVATE(n__take(X1, X2)) → TAKE(activate(X1), activate(X2))
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__0) → 01
ACTIVATE(n__length(X)) → LENGTH(activate(X))
ACTIVATE(n__length(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → S(activate(X))
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → CONS(activate(X1), X2)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
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(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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(activate(X1), activate(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__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__length(X)) → LENGTH(activate(X))
LENGTH(cons(N, L)) → U111(and(isNatList(activate(L)), n__isNat(N)), activate(L))
U111(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__length(X)) → ACTIVATE(X)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
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(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
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)
U111(tt, L) → ACTIVATE(L)
TAKE(s(M), cons(N, IL)) → U311(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
U311(tt, IL, M, N) → ACTIVATE(N)
U311(tt, IL, M, N) → ACTIVATE(M)
U311(tt, IL, M, N) → ACTIVATE(IL)
TAKE(s(M), cons(N, IL)) → AND(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(activate(IL))
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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(activate(X))
ISNAT(n__length(V1)) → ISNATLIST(activate(V1))
ACTIVATE(n__length(X)) → ACTIVATE(X)
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(x1)) = x1
POL(AND(x1, x2)) = x2
POL(ISNAT(x1)) = x1
POL(ISNATILIST(x1)) = x1
POL(ISNATLIST(x1)) = x1
POL(LENGTH(x1)) = x1
POL(TAKE(x1, x2)) = x1 + x2
POL(U11(x1, x2)) = 1 + x2
POL(U111(x1, x2)) = x2
POL(U21(x1)) = 0
POL(U31(x1, x2, x3, x4)) = x2 + x3 + x4
POL(U311(x1, x2, x3, x4)) = x2 + x3 + x4
POL(activate(x1)) = x1
POL(and(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = x1 + x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = x1
POL(isNatList(x1)) = x1
POL(length(x1)) = 1 + x1
POL(n__0) = 0
POL(n__and(x1, x2)) = x1 + x2
POL(n__cons(x1, x2)) = x1 + x2
POL(n__isNat(x1)) = x1
POL(n__isNatIList(x1)) = x1
POL(n__isNatList(x1)) = x1
POL(n__length(x1)) = 1 + x1
POL(n__nil) = 0
POL(n__s(x1)) = x1
POL(n__take(x1, x2)) = x1 + x2
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = x1 + x2
POL(tt) = 0
POL(zeros) = 0
The following usable rules [FROCOS05] were oriented:
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
nil → n__nil
isNatIList(X) → n__isNatIList(X)
isNat(X) → n__isNat(X)
isNatList(X) → n__isNatList(X)
length(X) → n__length(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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)
activate(n__and(X1, X2)) → and(activate(X1), X2)
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)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(X) → X
activate(n__nil) → nil
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
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(activate(X1), activate(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__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
LENGTH(cons(N, L)) → U111(and(isNatList(activate(L)), n__isNat(N)), activate(L))
U111(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__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
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(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
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)
U111(tt, L) → ACTIVATE(L)
TAKE(s(M), cons(N, IL)) → U311(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
U311(tt, IL, M, N) → ACTIVATE(N)
U311(tt, IL, M, N) → ACTIVATE(M)
U311(tt, IL, M, N) → ACTIVATE(IL)
TAKE(s(M), cons(N, IL)) → AND(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(activate(IL))
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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(activate(X1), activate(X2))
TAKE(s(M), cons(N, IL)) → U311(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
U311(tt, IL, M, N) → ACTIVATE(N)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X2)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
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(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
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)
U311(tt, IL, M, N) → ACTIVATE(M)
U311(tt, IL, M, N) → ACTIVATE(IL)
TAKE(s(M), cons(N, IL)) → AND(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(activate(IL))
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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.
TAKE(0, IL) → ISNATILIST(IL)
TAKE(s(M), cons(N, IL)) → U311(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(X1)
ACTIVATE(n__take(X1, X2)) → ACTIVATE(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)
TAKE(s(M), cons(N, IL)) → AND(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N)))
TAKE(s(M), cons(N, IL)) → ISNATILIST(activate(IL))
TAKE(s(M), cons(N, IL)) → ACTIVATE(IL)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(ACTIVATE(x1)) = x1
POL(AND(x1, x2)) = x2
POL(ISNAT(x1)) = x1
POL(ISNATILIST(x1)) = x1
POL(ISNATLIST(x1)) = x1
POL(TAKE(x1, x2)) = 1 + x1 + x2
POL(U11(x1, x2)) = x2
POL(U21(x1)) = 0
POL(U31(x1, x2, x3, x4)) = 1 + x2 + x3 + x4
POL(U311(x1, x2, x3, x4)) = x2 + x3 + x4
POL(activate(x1)) = x1
POL(and(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = x1 + x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = x1
POL(isNatList(x1)) = x1
POL(length(x1)) = x1
POL(n__0) = 0
POL(n__and(x1, x2)) = x1 + x2
POL(n__cons(x1, x2)) = x1 + x2
POL(n__isNat(x1)) = x1
POL(n__isNatIList(x1)) = x1
POL(n__isNatList(x1)) = x1
POL(n__length(x1)) = x1
POL(n__nil) = 0
POL(n__s(x1)) = x1
POL(n__take(x1, x2)) = 1 + x1 + x2
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = 1 + x1 + x2
POL(tt) = 0
POL(zeros) = 0
The following usable rules [FROCOS05] were oriented:
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
nil → n__nil
isNatIList(X) → n__isNatIList(X)
isNat(X) → n__isNat(X)
isNatList(X) → n__isNatList(X)
length(X) → n__length(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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)
activate(n__and(X1, X2)) → and(activate(X1), X2)
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)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(X) → X
activate(n__nil) → nil
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
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(activate(X1), activate(X2))
U311(tt, IL, M, N) → ACTIVATE(N)
ACTIVATE(n__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
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(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
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)
U311(tt, IL, M, N) → ACTIVATE(M)
U311(tt, IL, M, N) → ACTIVATE(IL)
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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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 4 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__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
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(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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.
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(x1)) = x1
POL(AND(x1, x2)) = x2
POL(ISNAT(x1)) = x1
POL(ISNATILIST(x1)) = 1 + x1
POL(ISNATLIST(x1)) = x1
POL(U11(x1, x2)) = x2
POL(U21(x1)) = 0
POL(U31(x1, x2, x3, x4)) = 1 + x2 + x3 + x4
POL(activate(x1)) = x1
POL(and(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = x1 + x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = 1 + x1
POL(isNatList(x1)) = x1
POL(length(x1)) = x1
POL(n__0) = 0
POL(n__and(x1, x2)) = x1 + x2
POL(n__cons(x1, x2)) = x1 + x2
POL(n__isNat(x1)) = x1
POL(n__isNatIList(x1)) = 1 + x1
POL(n__isNatList(x1)) = x1
POL(n__length(x1)) = x1
POL(n__nil) = 0
POL(n__s(x1)) = x1
POL(n__take(x1, x2)) = 1 + x1 + x2
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = 1 + x1 + x2
POL(tt) = 0
POL(zeros) = 0
The following usable rules [FROCOS05] were oriented:
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
nil → n__nil
isNatIList(X) → n__isNatIList(X)
isNat(X) → n__isNat(X)
isNatList(X) → n__isNatList(X)
length(X) → n__length(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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)
activate(n__and(X1, X2)) → and(activate(X1), X2)
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)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(X) → X
activate(n__nil) → nil
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
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__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
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__isNat(X)) → ISNAT(X)
ACTIVATE(n__and(X1, X2)) → AND(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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.
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(x1)) = x1
POL(AND(x1, x2)) = x2
POL(ISNAT(x1)) = x1
POL(ISNATILIST(x1)) = 1 + x1
POL(ISNATLIST(x1)) = 1 + x1
POL(U11(x1, x2)) = 1 + x2
POL(U21(x1)) = 0
POL(U31(x1, x2, x3, x4)) = x2 + x3 + x4
POL(activate(x1)) = x1
POL(and(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = x1 + x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = 1 + x1
POL(isNatList(x1)) = 1 + x1
POL(length(x1)) = 1 + x1
POL(n__0) = 0
POL(n__and(x1, x2)) = x1 + x2
POL(n__cons(x1, x2)) = x1 + x2
POL(n__isNat(x1)) = x1
POL(n__isNatIList(x1)) = 1 + x1
POL(n__isNatList(x1)) = 1 + x1
POL(n__length(x1)) = 1 + x1
POL(n__nil) = 0
POL(n__s(x1)) = x1
POL(n__take(x1, x2)) = x1 + x2
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = x1 + x2
POL(tt) = 0
POL(zeros) = 0
The following usable rules [FROCOS05] were oriented:
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
nil → n__nil
isNatIList(X) → n__isNatIList(X)
isNat(X) → n__isNat(X)
isNatList(X) → n__isNatList(X)
length(X) → n__length(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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)
activate(n__and(X1, X2)) → and(activate(X1), X2)
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)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(X) → X
activate(n__nil) → nil
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
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__s(X)) → ACTIVATE(X)
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
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__isNat(X)) → ISNAT(X)
ACTIVATE(n__and(X1, X2)) → AND(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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.
ACTIVATE(n__cons(X1, X2)) → ACTIVATE(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(ISNATLIST(x1)) = | | + | | · | x1 |
POL(n__cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(AND(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(activate(x1)) = | | + | | · | x1 |
POL(n__isNatList(x1)) = | | + | | · | x1 |
POL(ACTIVATE(x1)) = | | + | | · | x1 |
POL(n__isNatIList(x1)) = | | + | | · | x1 |
POL(ISNATILIST(x1)) = | | + | | · | x1 |
POL(n__isNat(x1)) = | | + | | · | x1 |
POL(n__and(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U31(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(and(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(isNatIList(x1)) = | | + | | · | x1 |
POL(n__take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(isNatList(x1)) = | | + | | · | x1 |
POL(n__length(x1)) = | | + | | · | x1 |
The following usable rules [FROCOS05] were oriented:
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
nil → n__nil
isNatIList(X) → n__isNatIList(X)
isNat(X) → n__isNat(X)
isNatList(X) → n__isNatList(X)
length(X) → n__length(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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)
activate(n__and(X1, X2)) → and(activate(X1), X2)
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)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(X) → X
activate(n__nil) → nil
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
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__s(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__isNat(X)) → ISNAT(X)
ACTIVATE(n__and(X1, X2)) → AND(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(X1), X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(20) 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: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(ISNATLIST(x1)) = | 0A | + | 1A | · | x1 |
POL(n__cons(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(AND(x1, x2)) = | -I | + | -I | · | x1 | + | 0A | · | x2 |
POL(isNat(x1)) = | 1A | + | 1A | · | x1 |
POL(activate(x1)) = | 0A | + | 0A | · | x1 |
POL(n__isNatList(x1)) = | 0A | + | 1A | · | x1 |
POL(ACTIVATE(x1)) = | -I | + | 0A | · | x1 |
POL(n__s(x1)) = | -I | + | 0A | · | x1 |
POL(n__isNatIList(x1)) = | 1A | + | 1A | · | x1 |
POL(ISNATILIST(x1)) = | -I | + | 1A | · | x1 |
POL(ISNAT(x1)) = | 0A | + | 0A | · | x1 |
POL(n__isNat(x1)) = | 1A | + | 1A | · | x1 |
POL(n__and(x1, x2)) = | -I | + | 0A | · | x1 | + | 0A | · | x2 |
POL(take(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(cons(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(U31(x1, x2, x3, x4)) = | 0A | + | -I | · | x1 | + | 0A | · | x2 | + | 0A | · | x3 | + | 0A | · | x4 |
POL(and(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(isNatIList(x1)) = | 1A | + | 1A | · | x1 |
POL(U21(x1)) = | 0A | + | -I | · | x1 |
POL(n__take(x1, x2)) = | 0A | + | 0A | · | x1 | + | 0A | · | x2 |
POL(length(x1)) = | 0A | + | 0A | · | x1 |
POL(U11(x1, x2)) = | 0A | + | -I | · | x1 | + | 0A | · | x2 |
POL(isNatList(x1)) = | 0A | + | 1A | · | x1 |
POL(n__length(x1)) = | -I | + | 0A | · | x1 |
The following usable rules [FROCOS05] were oriented:
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
nil → n__nil
isNatIList(X) → n__isNatIList(X)
isNat(X) → n__isNat(X)
isNatList(X) → n__isNatList(X)
length(X) → n__length(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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)
activate(n__and(X1, X2)) → and(activate(X1), X2)
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)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(X) → X
activate(n__nil) → nil
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt
(21) 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__s(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(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(X1), X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(22) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 1 less node.
(23) Complex Obligation (AND)
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
AND(tt, X) → ACTIVATE(X)
ACTIVATE(n__s(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(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(X1), X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(25) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
ACTIVATE(n__s(X)) → ACTIVATE(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(ACTIVATE(x1)) = x1
POL(AND(x1, x2)) = x2
POL(ISNATILIST(x1)) = 0
POL(ISNATLIST(x1)) = 0
POL(U11(x1, x2)) = 0
POL(U21(x1)) = 0
POL(U31(x1, x2, x3, x4)) = 0
POL(activate(x1)) = 0
POL(and(x1, x2)) = 0
POL(cons(x1, x2)) = 0
POL(isNat(x1)) = 0
POL(isNatIList(x1)) = 0
POL(isNatList(x1)) = 0
POL(length(x1)) = 0
POL(n__0) = 0
POL(n__and(x1, x2)) = x1 + x2
POL(n__cons(x1, x2)) = 0
POL(n__isNat(x1)) = 0
POL(n__isNatIList(x1)) = 0
POL(n__isNatList(x1)) = 0
POL(n__length(x1)) = 0
POL(n__nil) = 0
POL(n__s(x1)) = 1 + x1
POL(n__take(x1, x2)) = 0
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = 0
POL(take(x1, x2)) = 0
POL(tt) = 0
POL(zeros) = 0
The following usable rules [FROCOS05] were oriented:
none
(26) 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(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(X1), X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(27) 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(activate(X1), X2)
ACTIVATE(n__and(X1, X2)) → ACTIVATE(X1)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(ACTIVATE(x1)) = x1
POL(AND(x1, x2)) = x2
POL(ISNATILIST(x1)) = 0
POL(ISNATLIST(x1)) = 0
POL(U11(x1, x2)) = 0
POL(U21(x1)) = 0
POL(U31(x1, x2, x3, x4)) = 0
POL(activate(x1)) = 0
POL(and(x1, x2)) = 0
POL(cons(x1, x2)) = 0
POL(isNat(x1)) = 0
POL(isNatIList(x1)) = 0
POL(isNatList(x1)) = 0
POL(length(x1)) = 0
POL(n__0) = 0
POL(n__and(x1, x2)) = 1 + x1 + x2
POL(n__cons(x1, x2)) = 0
POL(n__isNat(x1)) = 0
POL(n__isNatIList(x1)) = 0
POL(n__isNatList(x1)) = 0
POL(n__length(x1)) = 0
POL(n__nil) = 0
POL(n__s(x1)) = 0
POL(n__take(x1, x2)) = 0
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = 0
POL(take(x1, x2)) = 0
POL(tt) = 0
POL(zeros) = 0
The following usable rules [FROCOS05] were oriented:
none
(28) 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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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
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(activate(x0), activate(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(activate(x0))), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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(activate(x0), x1)), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatIList(activate(y1)))
(30) 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(activate(x0), activate(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(activate(x0))), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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:
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(activate(x0), activate(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(activate(x0))), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(X1), X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(33) 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(activate(x0), activate(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(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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(activate(x0), x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(x0, y1)) → AND(isNat(x0), n__isNatList(activate(y1)))
(34) 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(activate(x0), activate(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(activate(x0))), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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(activate(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(activate(x0), activate(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(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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 1 SCC with 1 less node.
(36) 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(activate(x0), activate(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(activate(x0))), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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(activate(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(activate(x0), activate(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(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(X1), X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(37) 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))
(38) 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(activate(x0), activate(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(activate(x0))), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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(activate(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(activate(x0), activate(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(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(X1), X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(39) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs.
(40) Complex Obligation (AND)
(41) 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(activate(x0), activate(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(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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__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(x1)) = x1
POL(AND(x1, x2)) = x2
POL(ISNATLIST(x1)) = x1
POL(U11(x1, x2)) = x2
POL(U21(x1)) = x1
POL(U31(x1, x2, x3, x4)) = x2 + x3 + x4
POL(activate(x1)) = x1
POL(and(x1, x2)) = x2
POL(cons(x1, x2)) = x1 + x2
POL(isNat(x1)) = 1 + x1
POL(isNatIList(x1)) = x1
POL(isNatList(x1)) = x1
POL(length(x1)) = x1
POL(n__0) = 0
POL(n__and(x1, x2)) = x2
POL(n__cons(x1, x2)) = x1 + x2
POL(n__isNat(x1)) = 1 + x1
POL(n__isNatIList(x1)) = x1
POL(n__isNatList(x1)) = x1
POL(n__length(x1)) = x1
POL(n__nil) = 0
POL(n__s(x1)) = x1
POL(n__take(x1, x2)) = x1 + x2
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = x1 + x2
POL(tt) = 0
POL(zeros) = 0
The following usable rules [FROCOS05] were oriented:
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
nil → n__nil
isNatIList(X) → n__isNatIList(X)
isNat(X) → n__isNat(X)
isNatList(X) → n__isNatList(X)
length(X) → n__length(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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)
activate(n__and(X1, X2)) → and(activate(X1), X2)
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)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(X) → X
activate(n__nil) → nil
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt
(43) 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(activate(x0), activate(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(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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__and(x0, x1), y1)) → AND(isNat(and(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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__zeros, y1)) → AND(isNat(zeros), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__length(x0), y1)) → AND(isNat(length(activate(x0))), n__isNatList(activate(y1)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(ACTIVATE(x1)) = x1
POL(AND(x1, x2)) = x2
POL(ISNATLIST(x1)) = x1
POL(U11(x1, x2)) = 1 + x2
POL(U21(x1)) = x1
POL(U31(x1, x2, x3, x4)) = x2 + x4
POL(activate(x1)) = x1
POL(and(x1, x2)) = x2
POL(cons(x1, x2)) = x1 + x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = x1
POL(isNatList(x1)) = x1
POL(length(x1)) = 1 + x1
POL(n__0) = 0
POL(n__and(x1, x2)) = x2
POL(n__cons(x1, x2)) = x1 + x2
POL(n__isNat(x1)) = x1
POL(n__isNatIList(x1)) = x1
POL(n__isNatList(x1)) = x1
POL(n__length(x1)) = 1 + x1
POL(n__nil) = 0
POL(n__s(x1)) = x1
POL(n__take(x1, x2)) = x2
POL(n__zeros) = 1
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = x2
POL(tt) = 0
POL(zeros) = 1
The following usable rules [FROCOS05] were oriented:
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
nil → n__nil
isNatIList(X) → n__isNatIList(X)
isNat(X) → n__isNat(X)
isNatList(X) → n__isNatList(X)
length(X) → n__length(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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)
activate(n__and(X1, X2)) → and(activate(X1), X2)
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)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(X) → X
activate(n__nil) → nil
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
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__take(x0, x1), y1)) → AND(isNat(take(activate(x0), activate(x1))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__0, y1)) → AND(isNat(0), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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__and(x0, x1), y1)) → AND(isNat(and(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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__take(x0, x1), y1)) → AND(isNat(take(activate(x0), activate(x1))), n__isNatList(activate(y1)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(0) = 0
POL(ACTIVATE(x1)) = x1
POL(AND(x1, x2)) = x2
POL(ISNATLIST(x1)) = x1
POL(U11(x1, x2)) = x2
POL(U21(x1)) = 1 + x1
POL(U31(x1, x2, x3, x4)) = 1 + x2 + x4
POL(activate(x1)) = x1
POL(and(x1, x2)) = x2
POL(cons(x1, x2)) = x1 + x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = x1
POL(isNatList(x1)) = x1
POL(length(x1)) = x1
POL(n__0) = 0
POL(n__and(x1, x2)) = x2
POL(n__cons(x1, x2)) = x1 + x2
POL(n__isNat(x1)) = x1
POL(n__isNatIList(x1)) = x1
POL(n__isNatList(x1)) = x1
POL(n__length(x1)) = x1
POL(n__nil) = 0
POL(n__s(x1)) = x1
POL(n__take(x1, x2)) = 1 + x2
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = 1 + x2
POL(tt) = 0
POL(zeros) = 0
The following usable rules [FROCOS05] were oriented:
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
nil → n__nil
isNatIList(X) → n__isNatIList(X)
isNat(X) → n__isNat(X)
isNatList(X) → n__isNatList(X)
length(X) → n__length(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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)
activate(n__and(X1, X2)) → and(activate(X1), X2)
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)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(X) → X
activate(n__nil) → nil
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
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(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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__and(x0, x1), y1)) → AND(isNat(and(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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__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(x1)) = x1
POL(AND(x1, x2)) = x2
POL(ISNATLIST(x1)) = x1
POL(U11(x1, x2)) = x2
POL(U21(x1)) = 1
POL(U31(x1, x2, x3, x4)) = 1 + x2 + x3 + x4
POL(activate(x1)) = x1
POL(and(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = x1 + x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = 1 + x1
POL(isNatList(x1)) = x1
POL(length(x1)) = x1
POL(n__0) = 0
POL(n__and(x1, x2)) = x1 + x2
POL(n__cons(x1, x2)) = x1 + x2
POL(n__isNat(x1)) = x1
POL(n__isNatIList(x1)) = 1 + x1
POL(n__isNatList(x1)) = x1
POL(n__length(x1)) = x1
POL(n__nil) = 0
POL(n__s(x1)) = x1
POL(n__take(x1, x2)) = 1 + x1 + x2
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = 1 + x1 + x2
POL(tt) = 0
POL(zeros) = 0
The following usable rules [FROCOS05] were oriented:
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
nil → n__nil
isNatIList(X) → n__isNatIList(X)
isNat(X) → n__isNat(X)
isNatList(X) → n__isNatList(X)
length(X) → n__length(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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)
activate(n__and(X1, X2)) → and(activate(X1), X2)
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)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(X) → X
activate(n__nil) → nil
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
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(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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__and(x0, x1), y1)) → AND(isNat(and(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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__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(x1)) = x1
POL(AND(x1, x2)) = x2
POL(ISNATLIST(x1)) = x1
POL(U11(x1, x2)) = x2
POL(U21(x1)) = 1
POL(U31(x1, x2, x3, x4)) = 1 + x2 + x4
POL(activate(x1)) = x1
POL(and(x1, x2)) = x2
POL(cons(x1, x2)) = x1 + x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = x1
POL(isNatList(x1)) = x1
POL(length(x1)) = x1
POL(n__0) = 0
POL(n__and(x1, x2)) = x2
POL(n__cons(x1, x2)) = x1 + x2
POL(n__isNat(x1)) = x1
POL(n__isNatIList(x1)) = x1
POL(n__isNatList(x1)) = x1
POL(n__length(x1)) = x1
POL(n__nil) = 1
POL(n__s(x1)) = x1
POL(n__take(x1, x2)) = 1 + x2
POL(n__zeros) = 0
POL(nil) = 1
POL(s(x1)) = x1
POL(take(x1, x2)) = 1 + x2
POL(tt) = 0
POL(zeros) = 0
The following usable rules [FROCOS05] were oriented:
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
nil → n__nil
isNatIList(X) → n__isNatIList(X)
isNat(X) → n__isNat(X)
isNatList(X) → n__isNatList(X)
length(X) → n__length(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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)
activate(n__and(X1, X2)) → and(activate(X1), X2)
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)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(X) → X
activate(n__nil) → nil
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
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(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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__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(x1)) = x1
POL(AND(x1, x2)) = x2
POL(ISNATLIST(x1)) = 1 + x1
POL(U11(x1, x2)) = 1 + x2
POL(U21(x1)) = 0
POL(U31(x1, x2, x3, x4)) = x2 + x4
POL(activate(x1)) = x1
POL(and(x1, x2)) = x2
POL(cons(x1, x2)) = x1 + x2
POL(isNat(x1)) = x1
POL(isNatIList(x1)) = 1 + x1
POL(isNatList(x1)) = 1 + x1
POL(length(x1)) = 1 + x1
POL(n__0) = 0
POL(n__and(x1, x2)) = x2
POL(n__cons(x1, x2)) = x1 + x2
POL(n__isNat(x1)) = x1
POL(n__isNatIList(x1)) = 1 + x1
POL(n__isNatList(x1)) = 1 + x1
POL(n__length(x1)) = 1 + x1
POL(n__nil) = 0
POL(n__s(x1)) = x1
POL(n__take(x1, x2)) = x2
POL(n__zeros) = 0
POL(nil) = 0
POL(s(x1)) = x1
POL(take(x1, x2)) = x2
POL(tt) = 0
POL(zeros) = 0
The following usable rules [FROCOS05] were oriented:
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
nil → n__nil
isNatIList(X) → n__isNatIList(X)
isNat(X) → n__isNat(X)
isNatList(X) → n__isNatList(X)
length(X) → n__length(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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)
activate(n__and(X1, X2)) → and(activate(X1), X2)
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)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(X) → X
activate(n__nil) → nil
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
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__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(x0), x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(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__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatList(activate(y1)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(AND(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(n__isNatList(x1)) = | | + | | · | x1 |
POL(ACTIVATE(x1)) = | | + | | · | x1 |
POL(ISNATLIST(x1)) = | | + | | · | x1 |
POL(n__cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(activate(x1)) = | | + | | · | x1 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(n__and(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(and(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U31(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(isNatIList(x1)) = | | + | | · | x1 |
POL(n__isNat(x1)) = | | + | | · | x1 |
POL(n__take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(isNatList(x1)) = | | + | | · | x1 |
POL(n__isNatIList(x1)) = | | + | | · | x1 |
POL(n__length(x1)) = | | + | | · | x1 |
The following usable rules [FROCOS05] were oriented:
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
nil → n__nil
isNatIList(X) → n__isNatIList(X)
isNat(X) → n__isNat(X)
isNatList(X) → n__isNatList(X)
length(X) → n__length(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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)
activate(n__and(X1, X2)) → and(activate(X1), X2)
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)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(X) → X
activate(n__nil) → nil
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
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__cons(x0, x1), y1)) → AND(isNat(cons(activate(x0), x1)), n__isNatList(activate(y1)))
ISNATLIST(n__cons(n__and(x0, x1), y1)) → AND(isNat(and(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(X1), X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(56) 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(activate(x0), x1)), n__isNatList(activate(y1)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(AND(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(n__isNatList(x1)) = | | + | | · | x1 |
POL(ACTIVATE(x1)) = | | + | | · | x1 |
POL(ISNATLIST(x1)) = | | + | | · | x1 |
POL(n__cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(activate(x1)) = | | + | | · | x1 |
POL(cons(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(n__and(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(and(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U31(x1, x2, x3, x4)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 | + | | · | x4 |
POL(isNatIList(x1)) = | | + | | · | x1 |
POL(n__isNat(x1)) = | | + | | · | x1 |
POL(n__take(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U11(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(isNatList(x1)) = | | + | | · | x1 |
POL(n__isNatIList(x1)) = | | + | | · | x1 |
POL(n__length(x1)) = | | + | | · | x1 |
The following usable rules [FROCOS05] were oriented:
take(s(M), cons(N, IL)) → U31(and(isNatIList(activate(IL)), n__and(n__isNat(M), n__isNat(N))), activate(IL), M, N)
take(0, IL) → U21(isNatIList(IL))
take(X1, X2) → n__take(X1, X2)
zeros → n__zeros
length(cons(N, L)) → U11(and(isNatList(activate(L)), n__isNat(N)), activate(L))
length(nil) → 0
nil → n__nil
isNatIList(X) → n__isNatIList(X)
isNat(X) → n__isNat(X)
isNatList(X) → n__isNatList(X)
length(X) → n__length(X)
0 → n__0
cons(X1, X2) → n__cons(X1, X2)
s(X) → n__s(X)
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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)
activate(n__and(X1, X2)) → and(activate(X1), X2)
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)
isNat(n__length(V1)) → isNatList(activate(V1))
activate(n__isNatList(X)) → isNatList(X)
and(X1, X2) → n__and(X1, X2)
activate(n__zeros) → zeros
activate(n__take(X1, X2)) → take(activate(X1), activate(X2))
activate(n__0) → 0
activate(X) → X
activate(n__nil) → nil
U21(tt) → nil
U31(tt, IL, M, N) → cons(activate(N), n__take(activate(M), activate(IL)))
zeros → cons(0, n__zeros)
U11(tt, L) → s(length(activate(L)))
isNat(n__0) → tt
isNatList(n__nil) → tt
isNatIList(n__zeros) → tt
(57) 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(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(X1), X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(58) 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:
- Matcher: [ ]
- Semiunifier: [ ]
Rewriting sequenceACTIVATE(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.
(59) FALSE
(60) 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(activate(x0), activate(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(activate(x0))), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__s(x0), y1)) → AND(isNat(s(activate(x0))), n__isNatIList(activate(y1)))
ISNATILIST(n__cons(n__cons(x0, x1), y1)) → AND(isNat(cons(activate(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(activate(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(X1), X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(61) 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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(X1), X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(62) Obligation:
Q DP problem:
The TRS P consists of the following rules:
LENGTH(cons(N, L)) → U111(and(isNatList(activate(L)), n__isNat(N)), activate(L))
U111(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(n__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(activate(X1), activate(X2))
activate(n__0) → 0
activate(n__length(X)) → length(activate(X))
activate(n__s(X)) → s(activate(X))
activate(n__cons(X1, X2)) → cons(activate(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(activate(X1), X2)
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.