MAYBE
TRS:
{ cons(X1, X2) -> n__cons(X1, X2),
0() -> n__0(),
zeros() -> cons(0(), n__zeros()),
zeros() -> n__zeros(),
U11(tt()) -> tt(),
U21(tt()) -> tt(),
U31(tt()) -> tt(),
U42(tt()) -> tt(),
isNatIList(V) -> U31(isNatList(activate(V))),
isNatIList(n__zeros()) -> tt(),
isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)),
activate(X) -> X,
activate(n__zeros()) -> zeros(),
activate(n__take(X1, X2)) -> take(X1, X2),
activate(n__0()) -> 0(),
activate(n__length(X)) -> length(X),
activate(n__s(X)) -> s(X),
activate(n__cons(X1, X2)) -> cons(X1, X2),
activate(n__nil()) -> nil(),
U41(tt(), V2) -> U42(isNatIList(activate(V2))),
U52(tt()) -> tt(),
isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)),
isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)),
isNatList(n__nil()) -> tt(),
U51(tt(), V2) -> U52(isNatList(activate(V2))),
U62(tt()) -> tt(),
U61(tt(), V2) -> U62(isNatIList(activate(V2))),
U72(tt(), L) -> s(length(activate(L))),
isNat(n__0()) -> tt(),
isNat(n__length(V1)) -> U11(isNatList(activate(V1))),
isNat(n__s(V1)) -> U21(isNat(activate(V1))),
U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)),
s(X) -> n__s(X),
length(X) -> n__length(X),
length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N),
length(nil()) -> 0(),
nil() -> n__nil(),
U81(tt()) -> nil(),
U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)),
U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)),
U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))),
take(X1, X2) -> n__take(X1, X2),
take(0(), IL) -> U81(isNatIList(IL)),
take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)}
DP:
Strict:
{ zeros#() -> cons#(0(), n__zeros()),
zeros#() -> 0#(),
isNatIList#(V) -> U31#(isNatList(activate(V))),
isNatIList#(V) -> activate#(V),
isNatIList#(V) -> isNatList#(activate(V)),
isNatIList#(n__cons(V1, V2)) -> activate#(V2),
isNatIList#(n__cons(V1, V2)) -> activate#(V1),
isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)),
isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)),
activate#(n__zeros()) -> zeros#(),
activate#(n__take(X1, X2)) -> take#(X1, X2),
activate#(n__0()) -> 0#(),
activate#(n__length(X)) -> length#(X),
activate#(n__s(X)) -> s#(X),
activate#(n__cons(X1, X2)) -> cons#(X1, X2),
activate#(n__nil()) -> nil#(),
U41#(tt(), V2) -> U42#(isNatIList(activate(V2))),
U41#(tt(), V2) -> isNatIList#(activate(V2)),
U41#(tt(), V2) -> activate#(V2),
isNatList#(n__take(V1, V2)) -> activate#(V2),
isNatList#(n__take(V1, V2)) -> activate#(V1),
isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)),
isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)),
isNatList#(n__cons(V1, V2)) -> activate#(V2),
isNatList#(n__cons(V1, V2)) -> activate#(V1),
isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)),
isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)),
U51#(tt(), V2) -> activate#(V2),
U51#(tt(), V2) -> U52#(isNatList(activate(V2))),
U51#(tt(), V2) -> isNatList#(activate(V2)),
U61#(tt(), V2) -> isNatIList#(activate(V2)),
U61#(tt(), V2) -> activate#(V2),
U61#(tt(), V2) -> U62#(isNatIList(activate(V2))),
U72#(tt(), L) -> activate#(L),
U72#(tt(), L) -> s#(length(activate(L))),
U72#(tt(), L) -> length#(activate(L)),
isNat#(n__length(V1)) -> U11#(isNatList(activate(V1))),
isNat#(n__length(V1)) -> activate#(V1),
isNat#(n__length(V1)) -> isNatList#(activate(V1)),
isNat#(n__s(V1)) -> U21#(isNat(activate(V1))),
isNat#(n__s(V1)) -> activate#(V1),
isNat#(n__s(V1)) -> isNat#(activate(V1)),
U71#(tt(), L, N) -> activate#(N),
U71#(tt(), L, N) -> activate#(L),
U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)),
U71#(tt(), L, N) -> isNat#(activate(N)),
length#(cons(N, L)) -> activate#(L),
length#(cons(N, L)) -> isNatList#(activate(L)),
length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N),
length#(nil()) -> 0#(),
U81#(tt()) -> nil#(),
U92#(tt(), IL, M, N) -> activate#(N),
U92#(tt(), IL, M, N) -> activate#(M),
U92#(tt(), IL, M, N) -> activate#(IL),
U92#(tt(), IL, M, N) -> isNat#(activate(N)),
U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)),
U91#(tt(), IL, M, N) -> activate#(N),
U91#(tt(), IL, M, N) -> activate#(M),
U91#(tt(), IL, M, N) -> activate#(IL),
U91#(tt(), IL, M, N) -> isNat#(activate(M)),
U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)),
U93#(tt(), IL, M, N) -> cons#(activate(N), n__take(activate(M), activate(IL))),
U93#(tt(), IL, M, N) -> activate#(N),
U93#(tt(), IL, M, N) -> activate#(M),
U93#(tt(), IL, M, N) -> activate#(IL),
take#(0(), IL) -> isNatIList#(IL),
take#(0(), IL) -> U81#(isNatIList(IL)),
take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)),
take#(s(M), cons(N, IL)) -> activate#(IL),
take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N)}
Weak:
{ cons(X1, X2) -> n__cons(X1, X2),
0() -> n__0(),
zeros() -> cons(0(), n__zeros()),
zeros() -> n__zeros(),
U11(tt()) -> tt(),
U21(tt()) -> tt(),
U31(tt()) -> tt(),
U42(tt()) -> tt(),
isNatIList(V) -> U31(isNatList(activate(V))),
isNatIList(n__zeros()) -> tt(),
isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)),
activate(X) -> X,
activate(n__zeros()) -> zeros(),
activate(n__take(X1, X2)) -> take(X1, X2),
activate(n__0()) -> 0(),
activate(n__length(X)) -> length(X),
activate(n__s(X)) -> s(X),
activate(n__cons(X1, X2)) -> cons(X1, X2),
activate(n__nil()) -> nil(),
U41(tt(), V2) -> U42(isNatIList(activate(V2))),
U52(tt()) -> tt(),
isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)),
isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)),
isNatList(n__nil()) -> tt(),
U51(tt(), V2) -> U52(isNatList(activate(V2))),
U62(tt()) -> tt(),
U61(tt(), V2) -> U62(isNatIList(activate(V2))),
U72(tt(), L) -> s(length(activate(L))),
isNat(n__0()) -> tt(),
isNat(n__length(V1)) -> U11(isNatList(activate(V1))),
isNat(n__s(V1)) -> U21(isNat(activate(V1))),
U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)),
s(X) -> n__s(X),
length(X) -> n__length(X),
length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N),
length(nil()) -> 0(),
nil() -> n__nil(),
U81(tt()) -> nil(),
U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)),
U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)),
U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))),
take(X1, X2) -> n__take(X1, X2),
take(0(), IL) -> U81(isNatIList(IL)),
take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)}
EDG:
{
(U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__nil()) -> nil#())
(U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(X)) -> s#(X))
(U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(X))
(U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__0()) -> 0#())
(U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__zeros()) -> zeros#())
(take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)))
(take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> activate#(V1))
(take#(0(), IL) -> isNatIList#(IL), isNatIList#(n__cons(V1, V2)) -> activate#(V2))
(take#(0(), IL) -> isNatIList#(IL), isNatIList#(V) -> isNatList#(activate(V)))
(take#(0(), IL) -> isNatIList#(IL), isNatIList#(V) -> activate#(V))
(take#(0(), IL) -> isNatIList#(IL), isNatIList#(V) -> U31#(isNatList(activate(V))))
(U71#(tt(), L, N) -> activate#(N), activate#(n__nil()) -> nil#())
(U71#(tt(), L, N) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U71#(tt(), L, N) -> activate#(N), activate#(n__s(X)) -> s#(X))
(U71#(tt(), L, N) -> activate#(N), activate#(n__length(X)) -> length#(X))
(U71#(tt(), L, N) -> activate#(N), activate#(n__0()) -> 0#())
(U71#(tt(), L, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U71#(tt(), L, N) -> activate#(N), activate#(n__zeros()) -> zeros#())
(U91#(tt(), IL, M, N) -> activate#(N), activate#(n__nil()) -> nil#())
(U91#(tt(), IL, M, N) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U91#(tt(), IL, M, N) -> activate#(N), activate#(n__s(X)) -> s#(X))
(U91#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(X))
(U91#(tt(), IL, M, N) -> activate#(N), activate#(n__0()) -> 0#())
(U91#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U91#(tt(), IL, M, N) -> activate#(N), activate#(n__zeros()) -> zeros#())
(activate#(n__take(X1, X2)) -> take#(X1, X2), take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N))
(activate#(n__take(X1, X2)) -> take#(X1, X2), take#(s(M), cons(N, IL)) -> activate#(IL))
(activate#(n__take(X1, X2)) -> take#(X1, X2), take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)))
(activate#(n__take(X1, X2)) -> take#(X1, X2), take#(0(), IL) -> U81#(isNatIList(IL)))
(activate#(n__take(X1, X2)) -> take#(X1, X2), take#(0(), IL) -> isNatIList#(IL))
(isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), U41#(tt(), V2) -> activate#(V2))
(isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), U41#(tt(), V2) -> isNatIList#(activate(V2)))
(isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), U41#(tt(), V2) -> U42#(isNatIList(activate(V2))))
(isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)), U61#(tt(), V2) -> U62#(isNatIList(activate(V2))))
(isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)), U61#(tt(), V2) -> activate#(V2))
(isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)), U61#(tt(), V2) -> isNatIList#(activate(V2)))
(isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> isNatList#(activate(V2)))
(isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> U52#(isNatList(activate(V2))))
(isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> activate#(V2))
(isNat#(n__s(V1)) -> activate#(V1), activate#(n__nil()) -> nil#())
(isNat#(n__s(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(isNat#(n__s(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(X))
(isNat#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(X))
(isNat#(n__s(V1)) -> activate#(V1), activate#(n__0()) -> 0#())
(isNat#(n__s(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNat#(n__s(V1)) -> activate#(V1), activate#(n__zeros()) -> zeros#())
(isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1))
(isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1))))
(isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1)))
(isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1))
(isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1))))
(isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1))
(isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1))))
(isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1)))
(isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1))
(isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1))))
(isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)))
(isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1))
(isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V2))
(isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)))
(isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)))
(isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> activate#(V1))
(isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__take(V1, V2)) -> activate#(V2))
(U71#(tt(), L, N) -> activate#(L), activate#(n__nil()) -> nil#())
(U71#(tt(), L, N) -> activate#(L), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U71#(tt(), L, N) -> activate#(L), activate#(n__s(X)) -> s#(X))
(U71#(tt(), L, N) -> activate#(L), activate#(n__length(X)) -> length#(X))
(U71#(tt(), L, N) -> activate#(L), activate#(n__0()) -> 0#())
(U71#(tt(), L, N) -> activate#(L), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U71#(tt(), L, N) -> activate#(L), activate#(n__zeros()) -> zeros#())
(take#(0(), IL) -> U81#(isNatIList(IL)), U81#(tt()) -> nil#())
(U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__s(V1)) -> activate#(V1))
(U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1))))
(U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__length(V1)) -> isNatList#(activate(V1)))
(U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__length(V1)) -> activate#(V1))
(U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1))))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V1))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V2))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(V1, V2)) -> activate#(V1))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__take(V1, V2)) -> activate#(V2))
(U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1))
(U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1))))
(U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> isNatList#(activate(V1)))
(U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> activate#(V1))
(U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1))))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> activate#(V1))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> activate#(V2))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__take(V1, V2)) -> activate#(V1))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__take(V1, V2)) -> activate#(V2))
(activate#(n__length(X)) -> length#(X), length#(nil()) -> 0#())
(activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N))
(activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> isNatList#(activate(L)))
(activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> activate#(L))
(isNatIList#(V) -> activate#(V), activate#(n__nil()) -> nil#())
(isNatIList#(V) -> activate#(V), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(isNatIList#(V) -> activate#(V), activate#(n__s(X)) -> s#(X))
(isNatIList#(V) -> activate#(V), activate#(n__length(X)) -> length#(X))
(isNatIList#(V) -> activate#(V), activate#(n__0()) -> 0#())
(isNatIList#(V) -> activate#(V), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNatIList#(V) -> activate#(V), activate#(n__zeros()) -> zeros#())
(U92#(tt(), IL, M, N) -> activate#(M), activate#(n__nil()) -> nil#())
(U92#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U92#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> s#(X))
(U92#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(X))
(U92#(tt(), IL, M, N) -> activate#(M), activate#(n__0()) -> 0#())
(U92#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U92#(tt(), IL, M, N) -> activate#(M), activate#(n__zeros()) -> zeros#())
(U93#(tt(), IL, M, N) -> activate#(M), activate#(n__nil()) -> nil#())
(U93#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U93#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> s#(X))
(U93#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(X))
(U93#(tt(), IL, M, N) -> activate#(M), activate#(n__0()) -> 0#())
(U93#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U93#(tt(), IL, M, N) -> activate#(M), activate#(n__zeros()) -> zeros#())
(activate#(n__zeros()) -> zeros#(), zeros#() -> 0#())
(activate#(n__zeros()) -> zeros#(), zeros#() -> cons#(0(), n__zeros()))
(isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#())
(isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(X))
(isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(X))
(isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#())
(isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__zeros()) -> zeros#())
(isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#())
(isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(X))
(isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(X))
(isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#())
(isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNatList#(n__take(V1, V2)) -> activate#(V2), activate#(n__zeros()) -> zeros#())
(U51#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#())
(U51#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U51#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(X))
(U51#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(X))
(U51#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#())
(U51#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U51#(tt(), V2) -> activate#(V2), activate#(n__zeros()) -> zeros#())
(U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)))
(U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> isNat#(activate(N)))
(U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> activate#(IL))
(U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> activate#(M))
(U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> activate#(N))
(U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> cons#(activate(N), n__take(activate(M), activate(IL))))
(U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(N))
(U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(M))
(U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(IL))
(U61#(tt(), V2) -> activate#(V2), activate#(n__zeros()) -> zeros#())
(U61#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U61#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#())
(U61#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(X))
(U61#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(X))
(U61#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U61#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#())
(isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__zeros()) -> zeros#())
(isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__0()) -> 0#())
(isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(X))
(isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__s(X)) -> s#(X))
(isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__nil()) -> nil#())
(U41#(tt(), V2) -> activate#(V2), activate#(n__zeros()) -> zeros#())
(U41#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U41#(tt(), V2) -> activate#(V2), activate#(n__0()) -> 0#())
(U41#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(X))
(U41#(tt(), V2) -> activate#(V2), activate#(n__s(X)) -> s#(X))
(U41#(tt(), V2) -> activate#(V2), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U41#(tt(), V2) -> activate#(V2), activate#(n__nil()) -> nil#())
(take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N), U91#(tt(), IL, M, N) -> activate#(N))
(take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N), U91#(tt(), IL, M, N) -> activate#(M))
(take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N), U91#(tt(), IL, M, N) -> activate#(IL))
(take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N), U91#(tt(), IL, M, N) -> isNat#(activate(M)))
(take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N), U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)))
(U91#(tt(), IL, M, N) -> activate#(M), activate#(n__zeros()) -> zeros#())
(U91#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U91#(tt(), IL, M, N) -> activate#(M), activate#(n__0()) -> 0#())
(U91#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(X))
(U91#(tt(), IL, M, N) -> activate#(M), activate#(n__s(X)) -> s#(X))
(U91#(tt(), IL, M, N) -> activate#(M), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U91#(tt(), IL, M, N) -> activate#(M), activate#(n__nil()) -> nil#())
(length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> activate#(N))
(length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> activate#(L))
(length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)))
(length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> isNat#(activate(N)))
(U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> U31#(isNatList(activate(V))))
(U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> activate#(V))
(U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> isNatList#(activate(V)))
(U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V2))
(U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V1))
(U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)))
(U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> U31#(isNatList(activate(V))))
(U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> activate#(V))
(U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> isNatList#(activate(V)))
(U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V2))
(U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V1))
(U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)))
(U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1))))
(U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> activate#(V1))
(U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> isNatList#(activate(V1)))
(U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1))))
(U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1))
(U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> activate#(L))
(U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L)))
(U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N))
(U72#(tt(), L) -> length#(activate(L)), length#(nil()) -> 0#())
(take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(V) -> U31#(isNatList(activate(V))))
(take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(V) -> activate#(V))
(take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(V) -> isNatList#(activate(V)))
(take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> activate#(V2))
(take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> activate#(V1))
(take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)))
(take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(length#(cons(N, L)) -> activate#(L), activate#(n__zeros()) -> zeros#())
(length#(cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> take#(X1, X2))
(length#(cons(N, L)) -> activate#(L), activate#(n__0()) -> 0#())
(length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> length#(X))
(length#(cons(N, L)) -> activate#(L), activate#(n__s(X)) -> s#(X))
(length#(cons(N, L)) -> activate#(L), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(length#(cons(N, L)) -> activate#(L), activate#(n__nil()) -> nil#())
(isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1))))
(isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1))
(isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1)))
(isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1))))
(isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1))
(isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(U72#(tt(), L) -> activate#(L), activate#(n__zeros()) -> zeros#())
(U72#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U72#(tt(), L) -> activate#(L), activate#(n__0()) -> 0#())
(U72#(tt(), L) -> activate#(L), activate#(n__length(X)) -> length#(X))
(U72#(tt(), L) -> activate#(L), activate#(n__s(X)) -> s#(X))
(U72#(tt(), L) -> activate#(L), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U72#(tt(), L) -> activate#(L), activate#(n__nil()) -> nil#())
(isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> U11#(isNatList(activate(V1))))
(isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1))
(isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1)))
(isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> U21#(isNat(activate(V1))))
(isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1))
(isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> activate#(V2))
(isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> activate#(V1))
(isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)))
(isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)))
(isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> activate#(V2))
(isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> activate#(V1))
(isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)))
(isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U72#(tt(), L) -> activate#(L))
(U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U72#(tt(), L) -> s#(length(activate(L))))
(U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U72#(tt(), L) -> length#(activate(L)))
(isNat#(n__length(V1)) -> activate#(V1), activate#(n__zeros()) -> zeros#())
(isNat#(n__length(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNat#(n__length(V1)) -> activate#(V1), activate#(n__0()) -> 0#())
(isNat#(n__length(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(X))
(isNat#(n__length(V1)) -> activate#(V1), activate#(n__s(X)) -> s#(X))
(isNat#(n__length(V1)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(isNat#(n__length(V1)) -> activate#(V1), activate#(n__nil()) -> nil#())
(isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#())
(isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#())
(isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(X))
(isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(X))
(isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#())
(isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#())
(isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#())
(isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(X))
(isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(X))
(isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(isNatList#(n__take(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#())
(isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__zeros()) -> zeros#())
(isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__0()) -> 0#())
(isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(X))
(isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__s(X)) -> s#(X))
(isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__nil()) -> nil#())
(U93#(tt(), IL, M, N) -> activate#(N), activate#(n__zeros()) -> zeros#())
(U93#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U93#(tt(), IL, M, N) -> activate#(N), activate#(n__0()) -> 0#())
(U93#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(X))
(U93#(tt(), IL, M, N) -> activate#(N), activate#(n__s(X)) -> s#(X))
(U93#(tt(), IL, M, N) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U93#(tt(), IL, M, N) -> activate#(N), activate#(n__nil()) -> nil#())
(U92#(tt(), IL, M, N) -> activate#(N), activate#(n__zeros()) -> zeros#())
(U92#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U92#(tt(), IL, M, N) -> activate#(N), activate#(n__0()) -> 0#())
(U92#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(X))
(U92#(tt(), IL, M, N) -> activate#(N), activate#(n__s(X)) -> s#(X))
(U92#(tt(), IL, M, N) -> activate#(N), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U92#(tt(), IL, M, N) -> activate#(N), activate#(n__nil()) -> nil#())
(take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__zeros()) -> zeros#())
(take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(X1, X2))
(take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__0()) -> 0#())
(take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__length(X)) -> length#(X))
(take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__s(X)) -> s#(X))
(take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(take#(s(M), cons(N, IL)) -> activate#(IL), activate#(n__nil()) -> nil#())
(U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__zeros()) -> zeros#())
(U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__0()) -> 0#())
(U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(X))
(U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(X)) -> s#(X))
(U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__nil()) -> nil#())
(U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__zeros()) -> zeros#())
(U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__0()) -> 0#())
(U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(X))
(U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__s(X)) -> s#(X))
(U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__cons(X1, X2)) -> cons#(X1, X2))
(U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__nil()) -> nil#())
}
SCCS:
Scc:
{ isNatIList#(V) -> activate#(V),
isNatIList#(V) -> isNatList#(activate(V)),
isNatIList#(n__cons(V1, V2)) -> activate#(V2),
isNatIList#(n__cons(V1, V2)) -> activate#(V1),
isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)),
isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)),
activate#(n__take(X1, X2)) -> take#(X1, X2),
activate#(n__length(X)) -> length#(X),
U41#(tt(), V2) -> isNatIList#(activate(V2)),
U41#(tt(), V2) -> activate#(V2),
isNatList#(n__take(V1, V2)) -> activate#(V2),
isNatList#(n__take(V1, V2)) -> activate#(V1),
isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)),
isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)),
isNatList#(n__cons(V1, V2)) -> activate#(V2),
isNatList#(n__cons(V1, V2)) -> activate#(V1),
isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)),
isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)),
U51#(tt(), V2) -> activate#(V2),
U51#(tt(), V2) -> isNatList#(activate(V2)),
U61#(tt(), V2) -> isNatIList#(activate(V2)),
U61#(tt(), V2) -> activate#(V2),
U72#(tt(), L) -> activate#(L),
U72#(tt(), L) -> length#(activate(L)),
isNat#(n__length(V1)) -> activate#(V1),
isNat#(n__length(V1)) -> isNatList#(activate(V1)),
isNat#(n__s(V1)) -> activate#(V1),
isNat#(n__s(V1)) -> isNat#(activate(V1)),
U71#(tt(), L, N) -> activate#(N),
U71#(tt(), L, N) -> activate#(L),
U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)),
U71#(tt(), L, N) -> isNat#(activate(N)),
length#(cons(N, L)) -> activate#(L),
length#(cons(N, L)) -> isNatList#(activate(L)),
length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N),
U92#(tt(), IL, M, N) -> activate#(N),
U92#(tt(), IL, M, N) -> activate#(M),
U92#(tt(), IL, M, N) -> activate#(IL),
U92#(tt(), IL, M, N) -> isNat#(activate(N)),
U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)),
U91#(tt(), IL, M, N) -> activate#(N),
U91#(tt(), IL, M, N) -> activate#(M),
U91#(tt(), IL, M, N) -> activate#(IL),
U91#(tt(), IL, M, N) -> isNat#(activate(M)),
U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)),
U93#(tt(), IL, M, N) -> activate#(N),
U93#(tt(), IL, M, N) -> activate#(M),
U93#(tt(), IL, M, N) -> activate#(IL),
take#(0(), IL) -> isNatIList#(IL),
take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)),
take#(s(M), cons(N, IL)) -> activate#(IL),
take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N)}
SCC:
Strict:
{ isNatIList#(V) -> activate#(V),
isNatIList#(V) -> isNatList#(activate(V)),
isNatIList#(n__cons(V1, V2)) -> activate#(V2),
isNatIList#(n__cons(V1, V2)) -> activate#(V1),
isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)),
isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)),
activate#(n__take(X1, X2)) -> take#(X1, X2),
activate#(n__length(X)) -> length#(X),
U41#(tt(), V2) -> isNatIList#(activate(V2)),
U41#(tt(), V2) -> activate#(V2),
isNatList#(n__take(V1, V2)) -> activate#(V2),
isNatList#(n__take(V1, V2)) -> activate#(V1),
isNatList#(n__take(V1, V2)) -> U61#(isNat(activate(V1)), activate(V2)),
isNatList#(n__take(V1, V2)) -> isNat#(activate(V1)),
isNatList#(n__cons(V1, V2)) -> activate#(V2),
isNatList#(n__cons(V1, V2)) -> activate#(V1),
isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)),
isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)),
U51#(tt(), V2) -> activate#(V2),
U51#(tt(), V2) -> isNatList#(activate(V2)),
U61#(tt(), V2) -> isNatIList#(activate(V2)),
U61#(tt(), V2) -> activate#(V2),
U72#(tt(), L) -> activate#(L),
U72#(tt(), L) -> length#(activate(L)),
isNat#(n__length(V1)) -> activate#(V1),
isNat#(n__length(V1)) -> isNatList#(activate(V1)),
isNat#(n__s(V1)) -> activate#(V1),
isNat#(n__s(V1)) -> isNat#(activate(V1)),
U71#(tt(), L, N) -> activate#(N),
U71#(tt(), L, N) -> activate#(L),
U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)),
U71#(tt(), L, N) -> isNat#(activate(N)),
length#(cons(N, L)) -> activate#(L),
length#(cons(N, L)) -> isNatList#(activate(L)),
length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N),
U92#(tt(), IL, M, N) -> activate#(N),
U92#(tt(), IL, M, N) -> activate#(M),
U92#(tt(), IL, M, N) -> activate#(IL),
U92#(tt(), IL, M, N) -> isNat#(activate(N)),
U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)),
U91#(tt(), IL, M, N) -> activate#(N),
U91#(tt(), IL, M, N) -> activate#(M),
U91#(tt(), IL, M, N) -> activate#(IL),
U91#(tt(), IL, M, N) -> isNat#(activate(M)),
U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)),
U93#(tt(), IL, M, N) -> activate#(N),
U93#(tt(), IL, M, N) -> activate#(M),
U93#(tt(), IL, M, N) -> activate#(IL),
take#(0(), IL) -> isNatIList#(IL),
take#(s(M), cons(N, IL)) -> isNatIList#(activate(IL)),
take#(s(M), cons(N, IL)) -> activate#(IL),
take#(s(M), cons(N, IL)) -> U91#(isNatIList(activate(IL)), activate(IL), M, N)}
Weak:
{ cons(X1, X2) -> n__cons(X1, X2),
0() -> n__0(),
zeros() -> cons(0(), n__zeros()),
zeros() -> n__zeros(),
U11(tt()) -> tt(),
U21(tt()) -> tt(),
U31(tt()) -> tt(),
U42(tt()) -> tt(),
isNatIList(V) -> U31(isNatList(activate(V))),
isNatIList(n__zeros()) -> tt(),
isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)),
activate(X) -> X,
activate(n__zeros()) -> zeros(),
activate(n__take(X1, X2)) -> take(X1, X2),
activate(n__0()) -> 0(),
activate(n__length(X)) -> length(X),
activate(n__s(X)) -> s(X),
activate(n__cons(X1, X2)) -> cons(X1, X2),
activate(n__nil()) -> nil(),
U41(tt(), V2) -> U42(isNatIList(activate(V2))),
U52(tt()) -> tt(),
isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)),
isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)),
isNatList(n__nil()) -> tt(),
U51(tt(), V2) -> U52(isNatList(activate(V2))),
U62(tt()) -> tt(),
U61(tt(), V2) -> U62(isNatIList(activate(V2))),
U72(tt(), L) -> s(length(activate(L))),
isNat(n__0()) -> tt(),
isNat(n__length(V1)) -> U11(isNatList(activate(V1))),
isNat(n__s(V1)) -> U21(isNat(activate(V1))),
U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)),
s(X) -> n__s(X),
length(X) -> n__length(X),
length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N),
length(nil()) -> 0(),
nil() -> n__nil(),
U81(tt()) -> nil(),
U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)),
U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)),
U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))),
take(X1, X2) -> n__take(X1, X2),
take(0(), IL) -> U81(isNatIList(IL)),
take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)}
POLY:
Argument Filtering:
pi(take#) = [0,1], pi(take) = [0,1], pi(n__nil) = [], pi(n__cons) = [0,1], pi(n__s) = 0, pi(n__length) = 0, pi(n__0) = [], pi(n__take) = [0,1], pi(U93#) = [1,2,3], pi(U93) = [1,2,3], pi(U91#) = [1,2,3], pi(U91) = [1,2,3], pi(U92#) = [1,2,3], pi(U92) = [1,2,3], pi(U81) = [], pi(nil) = [], pi(length#) = 0, pi(length) = 0, pi(s) = 0, pi(U71#) = [1,2], pi(U71) = 1, pi(isNat#) = 0, pi(isNat) = [], pi(U72#) = 1, pi(U72) = 1, pi(U61#) = 1, pi(U61) = [], pi(U62) = [], pi(U51#) = 1, pi(U51) = [], pi(isNatList#) = 0, pi(isNatList) = [], pi(U52) = [], pi(U41#) = 1, pi(U41) = [], pi(activate#) = 0, pi(activate) = 0, pi(isNatIList#) = 0, pi(isNatIList) = [], pi(U42) = [], pi(U31) = [], pi(U21) = [], pi(U11) = [], pi(tt) = [], pi(zeros) = [], pi(n__zeros) = [], pi(0) = [], pi(cons) = [0,1]
Usable Rules:
{}
Interpretation:
[U93#](x0, x1, x2) = x0 + x1 + x2,
[U91#](x0, x1, x2) = x0 + x1 + x2,
[U92#](x0, x1, x2) = x0 + x1 + x2,
[U71#](x0, x1) = x0 + x1,
[take#](x0, x1) = x0 + x1 + 1,
[n__cons](x0, x1) = x0 + x1,
[n__take](x0, x1) = x0 + x1 + 1,
[cons](x0, x1) = x0 + x1,
[0] = 0
Strict:
{ isNatIList#(V) -> activate#(V),
isNatIList#(V) -> isNatList#(activate(V)),
isNatIList#(n__cons(V1, V2)) -> activate#(V2),
isNatIList#(n__cons(V1, V2)) -> activate#(V1),
isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)),
isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)),
activate#(n__take(X1, X2)) -> take#(X1, X2),
activate#(n__length(X)) -> length#(X),
U41#(tt(), V2) -> isNatIList#(activate(V2)),
U41#(tt(), V2) -> activate#(V2),
isNatList#(n__cons(V1, V2)) -> activate#(V2),
isNatList#(n__cons(V1, V2)) -> activate#(V1),
isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)),
isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)),
U51#(tt(), V2) -> activate#(V2),
U51#(tt(), V2) -> isNatList#(activate(V2)),
U61#(tt(), V2) -> isNatIList#(activate(V2)),
U61#(tt(), V2) -> activate#(V2),
U72#(tt(), L) -> activate#(L),
U72#(tt(), L) -> length#(activate(L)),
isNat#(n__length(V1)) -> activate#(V1),
isNat#(n__length(V1)) -> isNatList#(activate(V1)),
isNat#(n__s(V1)) -> activate#(V1),
isNat#(n__s(V1)) -> isNat#(activate(V1)),
U71#(tt(), L, N) -> activate#(N),
U71#(tt(), L, N) -> activate#(L),
U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)),
U71#(tt(), L, N) -> isNat#(activate(N)),
length#(cons(N, L)) -> activate#(L),
length#(cons(N, L)) -> isNatList#(activate(L)),
length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N),
U92#(tt(), IL, M, N) -> activate#(N),
U92#(tt(), IL, M, N) -> activate#(M),
U92#(tt(), IL, M, N) -> activate#(IL),
U92#(tt(), IL, M, N) -> isNat#(activate(N)),
U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)),
U91#(tt(), IL, M, N) -> activate#(N),
U91#(tt(), IL, M, N) -> activate#(M),
U91#(tt(), IL, M, N) -> activate#(IL),
U91#(tt(), IL, M, N) -> isNat#(activate(M)),
U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)),
U93#(tt(), IL, M, N) -> activate#(N),
U93#(tt(), IL, M, N) -> activate#(M),
U93#(tt(), IL, M, N) -> activate#(IL)}
Weak:
{ cons(X1, X2) -> n__cons(X1, X2),
0() -> n__0(),
zeros() -> cons(0(), n__zeros()),
zeros() -> n__zeros(),
U11(tt()) -> tt(),
U21(tt()) -> tt(),
U31(tt()) -> tt(),
U42(tt()) -> tt(),
isNatIList(V) -> U31(isNatList(activate(V))),
isNatIList(n__zeros()) -> tt(),
isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)),
activate(X) -> X,
activate(n__zeros()) -> zeros(),
activate(n__take(X1, X2)) -> take(X1, X2),
activate(n__0()) -> 0(),
activate(n__length(X)) -> length(X),
activate(n__s(X)) -> s(X),
activate(n__cons(X1, X2)) -> cons(X1, X2),
activate(n__nil()) -> nil(),
U41(tt(), V2) -> U42(isNatIList(activate(V2))),
U52(tt()) -> tt(),
isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)),
isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)),
isNatList(n__nil()) -> tt(),
U51(tt(), V2) -> U52(isNatList(activate(V2))),
U62(tt()) -> tt(),
U61(tt(), V2) -> U62(isNatIList(activate(V2))),
U72(tt(), L) -> s(length(activate(L))),
isNat(n__0()) -> tt(),
isNat(n__length(V1)) -> U11(isNatList(activate(V1))),
isNat(n__s(V1)) -> U21(isNat(activate(V1))),
U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)),
s(X) -> n__s(X),
length(X) -> n__length(X),
length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N),
length(nil()) -> 0(),
nil() -> n__nil(),
U81(tt()) -> nil(),
U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)),
U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)),
U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))),
take(X1, X2) -> n__take(X1, X2),
take(0(), IL) -> U81(isNatIList(IL)),
take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)}
EDG:
{
(U41#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(X))
(U41#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U51#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(X))
(U51#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U71#(tt(), L, N) -> activate#(N), activate#(n__length(X)) -> length#(X))
(U71#(tt(), L, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U91#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(X))
(U91#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U72#(tt(), L) -> activate#(L), activate#(n__length(X)) -> length#(X))
(U72#(tt(), L) -> activate#(L), activate#(n__take(X1, X2)) -> take#(X1, X2))
(length#(cons(N, L)) -> activate#(L), activate#(n__length(X)) -> length#(X))
(length#(cons(N, L)) -> activate#(L), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U91#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(X))
(U91#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(X))
(U92#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(X))
(U93#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(X))
(isNatList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNat#(n__s(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(X))
(isNat#(n__s(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(X1, X2))
(activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N))
(activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> isNatList#(activate(L)))
(activate#(n__length(X)) -> length#(X), length#(cons(N, L)) -> activate#(L))
(length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> isNat#(activate(N)))
(length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)))
(length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> activate#(L))
(length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> activate#(N))
(isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> isNatList#(activate(V2)))
(isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> activate#(V2))
(U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(IL))
(U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(M))
(U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)), U93#(tt(), IL, M, N) -> activate#(N))
(isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)))
(isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> activate#(V1))
(isNatIList#(V) -> isNatList#(activate(V)), isNatList#(n__cons(V1, V2)) -> activate#(V2))
(isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1))
(isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1)))
(isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1))
(isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1))
(isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1)))
(isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1))
(U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N))
(U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L)))
(U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> activate#(L))
(U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1))
(U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> isNatList#(activate(V1)))
(U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> activate#(V1))
(U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)))
(U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V1))
(U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V2))
(U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> isNatList#(activate(V)))
(U41#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> activate#(V))
(U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)))
(U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V1))
(U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(n__cons(V1, V2)) -> activate#(V2))
(U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> isNatList#(activate(V)))
(U61#(tt(), V2) -> isNatIList#(activate(V2)), isNatIList#(V) -> activate#(V))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> activate#(V2))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> activate#(V1))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> activate#(V1))
(U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__length(V1)) -> isNatList#(activate(V1)))
(U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1))
(U92#(tt(), IL, M, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V2))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V1))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__length(V1)) -> activate#(V1))
(U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__length(V1)) -> isNatList#(activate(V1)))
(U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__s(V1)) -> activate#(V1))
(U91#(tt(), IL, M, N) -> isNat#(activate(M)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V2))
(isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> activate#(V1))
(isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)))
(isNat#(n__length(V1)) -> isNatList#(activate(V1)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> activate#(V1))
(isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__length(V1)) -> isNatList#(activate(V1)))
(isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1))
(isNatIList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> activate#(N))
(U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> activate#(M))
(U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> activate#(IL))
(U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> isNat#(activate(N)))
(U91#(tt(), IL, M, N) -> U92#(isNat(activate(M)), activate(IL), activate(M), activate(N)), U92#(tt(), IL, M, N) -> U93#(isNat(activate(N)), activate(IL), activate(M), activate(N)))
(U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U72#(tt(), L) -> activate#(L))
(U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U72#(tt(), L) -> length#(activate(L)))
(isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), U41#(tt(), V2) -> isNatIList#(activate(V2)))
(isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)), U41#(tt(), V2) -> activate#(V2))
(isNatIList#(V) -> activate#(V), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNatIList#(V) -> activate#(V), activate#(n__length(X)) -> length#(X))
(isNat#(n__length(V1)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNat#(n__length(V1)) -> activate#(V1), activate#(n__length(X)) -> length#(X))
(isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNatIList#(n__cons(V1, V2)) -> activate#(V1), activate#(n__length(X)) -> length#(X))
(U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U91#(tt(), IL, M, N) -> activate#(IL), activate#(n__length(X)) -> length#(X))
(U93#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U93#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(X))
(U92#(tt(), IL, M, N) -> activate#(M), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U92#(tt(), IL, M, N) -> activate#(M), activate#(n__length(X)) -> length#(X))
(U71#(tt(), L, N) -> activate#(L), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U71#(tt(), L, N) -> activate#(L), activate#(n__length(X)) -> length#(X))
(U93#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U93#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(X))
(U92#(tt(), IL, M, N) -> activate#(N), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U92#(tt(), IL, M, N) -> activate#(N), activate#(n__length(X)) -> length#(X))
(U61#(tt(), V2) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(X1, X2))
(U61#(tt(), V2) -> activate#(V2), activate#(n__length(X)) -> length#(X))
(isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNatList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(X))
(isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__take(X1, X2)) -> take#(X1, X2))
(isNatIList#(n__cons(V1, V2)) -> activate#(V2), activate#(n__length(X)) -> length#(X))
}
SCCS:
Scc:
{ activate#(n__length(X)) -> length#(X),
isNatList#(n__cons(V1, V2)) -> activate#(V2),
isNatList#(n__cons(V1, V2)) -> activate#(V1),
isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)),
isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)),
U51#(tt(), V2) -> activate#(V2),
U51#(tt(), V2) -> isNatList#(activate(V2)),
U72#(tt(), L) -> activate#(L),
U72#(tt(), L) -> length#(activate(L)),
isNat#(n__length(V1)) -> activate#(V1),
isNat#(n__length(V1)) -> isNatList#(activate(V1)),
isNat#(n__s(V1)) -> activate#(V1),
isNat#(n__s(V1)) -> isNat#(activate(V1)),
U71#(tt(), L, N) -> activate#(N),
U71#(tt(), L, N) -> activate#(L),
U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)),
U71#(tt(), L, N) -> isNat#(activate(N)),
length#(cons(N, L)) -> activate#(L),
length#(cons(N, L)) -> isNatList#(activate(L)),
length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N)}
Scc:
{isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)),
U41#(tt(), V2) -> isNatIList#(activate(V2))}
SCC:
Strict:
{ activate#(n__length(X)) -> length#(X),
isNatList#(n__cons(V1, V2)) -> activate#(V2),
isNatList#(n__cons(V1, V2)) -> activate#(V1),
isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)),
isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)),
U51#(tt(), V2) -> activate#(V2),
U51#(tt(), V2) -> isNatList#(activate(V2)),
U72#(tt(), L) -> activate#(L),
U72#(tt(), L) -> length#(activate(L)),
isNat#(n__length(V1)) -> activate#(V1),
isNat#(n__length(V1)) -> isNatList#(activate(V1)),
isNat#(n__s(V1)) -> activate#(V1),
isNat#(n__s(V1)) -> isNat#(activate(V1)),
U71#(tt(), L, N) -> activate#(N),
U71#(tt(), L, N) -> activate#(L),
U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)),
U71#(tt(), L, N) -> isNat#(activate(N)),
length#(cons(N, L)) -> activate#(L),
length#(cons(N, L)) -> isNatList#(activate(L)),
length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N)}
Weak:
{ cons(X1, X2) -> n__cons(X1, X2),
0() -> n__0(),
zeros() -> cons(0(), n__zeros()),
zeros() -> n__zeros(),
U11(tt()) -> tt(),
U21(tt()) -> tt(),
U31(tt()) -> tt(),
U42(tt()) -> tt(),
isNatIList(V) -> U31(isNatList(activate(V))),
isNatIList(n__zeros()) -> tt(),
isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)),
activate(X) -> X,
activate(n__zeros()) -> zeros(),
activate(n__take(X1, X2)) -> take(X1, X2),
activate(n__0()) -> 0(),
activate(n__length(X)) -> length(X),
activate(n__s(X)) -> s(X),
activate(n__cons(X1, X2)) -> cons(X1, X2),
activate(n__nil()) -> nil(),
U41(tt(), V2) -> U42(isNatIList(activate(V2))),
U52(tt()) -> tt(),
isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)),
isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)),
isNatList(n__nil()) -> tt(),
U51(tt(), V2) -> U52(isNatList(activate(V2))),
U62(tt()) -> tt(),
U61(tt(), V2) -> U62(isNatIList(activate(V2))),
U72(tt(), L) -> s(length(activate(L))),
isNat(n__0()) -> tt(),
isNat(n__length(V1)) -> U11(isNatList(activate(V1))),
isNat(n__s(V1)) -> U21(isNat(activate(V1))),
U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)),
s(X) -> n__s(X),
length(X) -> n__length(X),
length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N),
length(nil()) -> 0(),
nil() -> n__nil(),
U81(tt()) -> nil(),
U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)),
U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)),
U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))),
take(X1, X2) -> n__take(X1, X2),
take(0(), IL) -> U81(isNatIList(IL)),
take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)}
POLY:
Argument Filtering:
pi(take) = 1, pi(n__nil) = [], pi(n__cons) = [0,1], pi(n__s) = 0, pi(n__length) = [0], pi(n__0) = [], pi(n__take) = 1, pi(U93) = [1,3], pi(U91) = [1,3], pi(U92) = [1,3], pi(U81) = [], pi(nil) = [], pi(length#) = 0, pi(length) = [0], pi(s) = 0, pi(U71#) = [1,2], pi(U71) = [1], pi(isNat#) = 0, pi(isNat) = [], pi(U72#) = 1, pi(U72) = [1], pi(U61) = [], pi(U62) = [], pi(U51#) = 1, pi(U51) = [], pi(isNatList#) = 0, pi(isNatList) = [], pi(U52) = [], pi(U41) = [], pi(activate#) = 0, pi(activate) = 0, pi(isNatIList) = [], pi(U42) = [], pi(U31) = [], pi(U21) = [], pi(U11) = [], pi(tt) = [], pi(zeros) = [], pi(n__zeros) = [], pi(0) = [], pi(cons) = [0,1]
Usable Rules:
{}
Interpretation:
[U71#](x0, x1) = x0 + x1,
[n__cons](x0, x1) = x0 + x1,
[cons](x0, x1) = x0 + x1,
[n__length](x0) = x0 + 1
Strict:
{isNatList#(n__cons(V1, V2)) -> activate#(V2),
isNatList#(n__cons(V1, V2)) -> activate#(V1),
isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)),
isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)),
U51#(tt(), V2) -> activate#(V2),
U51#(tt(), V2) -> isNatList#(activate(V2)),
U72#(tt(), L) -> activate#(L),
U72#(tt(), L) -> length#(activate(L)),
isNat#(n__s(V1)) -> activate#(V1),
isNat#(n__s(V1)) -> isNat#(activate(V1)),
U71#(tt(), L, N) -> activate#(N),
U71#(tt(), L, N) -> activate#(L),
U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)),
U71#(tt(), L, N) -> isNat#(activate(N)),
length#(cons(N, L)) -> activate#(L),
length#(cons(N, L)) -> isNatList#(activate(L)),
length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N)}
Weak:
{ cons(X1, X2) -> n__cons(X1, X2),
0() -> n__0(),
zeros() -> cons(0(), n__zeros()),
zeros() -> n__zeros(),
U11(tt()) -> tt(),
U21(tt()) -> tt(),
U31(tt()) -> tt(),
U42(tt()) -> tt(),
isNatIList(V) -> U31(isNatList(activate(V))),
isNatIList(n__zeros()) -> tt(),
isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)),
activate(X) -> X,
activate(n__zeros()) -> zeros(),
activate(n__take(X1, X2)) -> take(X1, X2),
activate(n__0()) -> 0(),
activate(n__length(X)) -> length(X),
activate(n__s(X)) -> s(X),
activate(n__cons(X1, X2)) -> cons(X1, X2),
activate(n__nil()) -> nil(),
U41(tt(), V2) -> U42(isNatIList(activate(V2))),
U52(tt()) -> tt(),
isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)),
isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)),
isNatList(n__nil()) -> tt(),
U51(tt(), V2) -> U52(isNatList(activate(V2))),
U62(tt()) -> tt(),
U61(tt(), V2) -> U62(isNatIList(activate(V2))),
U72(tt(), L) -> s(length(activate(L))),
isNat(n__0()) -> tt(),
isNat(n__length(V1)) -> U11(isNatList(activate(V1))),
isNat(n__s(V1)) -> U21(isNat(activate(V1))),
U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)),
s(X) -> n__s(X),
length(X) -> n__length(X),
length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N),
length(nil()) -> 0(),
nil() -> n__nil(),
U81(tt()) -> nil(),
U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)),
U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)),
U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))),
take(X1, X2) -> n__take(X1, X2),
take(0(), IL) -> U81(isNatIList(IL)),
take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)}
EDG:
{(U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U72#(tt(), L) -> length#(activate(L)))
(U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)), U72#(tt(), L) -> activate#(L))
(isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(isNat#(n__s(V1)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V1))
(length#(cons(N, L)) -> isNatList#(activate(L)), isNatList#(n__cons(V1, V2)) -> activate#(V2))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> activate#(V1))
(U51#(tt(), V2) -> isNatList#(activate(V2)), isNatList#(n__cons(V1, V2)) -> activate#(V2))
(length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> isNat#(activate(N)))
(length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)))
(length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> activate#(L))
(length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N), U71#(tt(), L, N) -> activate#(N))
(U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> activate#(V1))
(U71#(tt(), L, N) -> isNat#(activate(N)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> activate#(L))
(U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> isNatList#(activate(L)))
(U72#(tt(), L) -> length#(activate(L)), length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N))
(isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> activate#(V1))
(isNatList#(n__cons(V1, V2)) -> isNat#(activate(V1)), isNat#(n__s(V1)) -> isNat#(activate(V1)))
(isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> activate#(V2))
(isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)), U51#(tt(), V2) -> isNatList#(activate(V2)))}
SCCS:
Scc:
{isNat#(n__s(V1)) -> isNat#(activate(V1))}
Scc:
{ U72#(tt(), L) -> length#(activate(L)),
U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)),
length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N)}
Scc:
{isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)),
U51#(tt(), V2) -> isNatList#(activate(V2))}
SCC:
Strict:
{isNat#(n__s(V1)) -> isNat#(activate(V1))}
Weak:
{ cons(X1, X2) -> n__cons(X1, X2),
0() -> n__0(),
zeros() -> cons(0(), n__zeros()),
zeros() -> n__zeros(),
U11(tt()) -> tt(),
U21(tt()) -> tt(),
U31(tt()) -> tt(),
U42(tt()) -> tt(),
isNatIList(V) -> U31(isNatList(activate(V))),
isNatIList(n__zeros()) -> tt(),
isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)),
activate(X) -> X,
activate(n__zeros()) -> zeros(),
activate(n__take(X1, X2)) -> take(X1, X2),
activate(n__0()) -> 0(),
activate(n__length(X)) -> length(X),
activate(n__s(X)) -> s(X),
activate(n__cons(X1, X2)) -> cons(X1, X2),
activate(n__nil()) -> nil(),
U41(tt(), V2) -> U42(isNatIList(activate(V2))),
U52(tt()) -> tt(),
isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)),
isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)),
isNatList(n__nil()) -> tt(),
U51(tt(), V2) -> U52(isNatList(activate(V2))),
U62(tt()) -> tt(),
U61(tt(), V2) -> U62(isNatIList(activate(V2))),
U72(tt(), L) -> s(length(activate(L))),
isNat(n__0()) -> tt(),
isNat(n__length(V1)) -> U11(isNatList(activate(V1))),
isNat(n__s(V1)) -> U21(isNat(activate(V1))),
U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)),
s(X) -> n__s(X),
length(X) -> n__length(X),
length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N),
length(nil()) -> 0(),
nil() -> n__nil(),
U81(tt()) -> nil(),
U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)),
U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)),
U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))),
take(X1, X2) -> n__take(X1, X2),
take(0(), IL) -> U81(isNatIList(IL)),
take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)}
Fail
SCC:
Strict:
{ U72#(tt(), L) -> length#(activate(L)),
U71#(tt(), L, N) -> U72#(isNat(activate(N)), activate(L)),
length#(cons(N, L)) -> U71#(isNatList(activate(L)), activate(L), N)}
Weak:
{ cons(X1, X2) -> n__cons(X1, X2),
0() -> n__0(),
zeros() -> cons(0(), n__zeros()),
zeros() -> n__zeros(),
U11(tt()) -> tt(),
U21(tt()) -> tt(),
U31(tt()) -> tt(),
U42(tt()) -> tt(),
isNatIList(V) -> U31(isNatList(activate(V))),
isNatIList(n__zeros()) -> tt(),
isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)),
activate(X) -> X,
activate(n__zeros()) -> zeros(),
activate(n__take(X1, X2)) -> take(X1, X2),
activate(n__0()) -> 0(),
activate(n__length(X)) -> length(X),
activate(n__s(X)) -> s(X),
activate(n__cons(X1, X2)) -> cons(X1, X2),
activate(n__nil()) -> nil(),
U41(tt(), V2) -> U42(isNatIList(activate(V2))),
U52(tt()) -> tt(),
isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)),
isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)),
isNatList(n__nil()) -> tt(),
U51(tt(), V2) -> U52(isNatList(activate(V2))),
U62(tt()) -> tt(),
U61(tt(), V2) -> U62(isNatIList(activate(V2))),
U72(tt(), L) -> s(length(activate(L))),
isNat(n__0()) -> tt(),
isNat(n__length(V1)) -> U11(isNatList(activate(V1))),
isNat(n__s(V1)) -> U21(isNat(activate(V1))),
U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)),
s(X) -> n__s(X),
length(X) -> n__length(X),
length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N),
length(nil()) -> 0(),
nil() -> n__nil(),
U81(tt()) -> nil(),
U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)),
U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)),
U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))),
take(X1, X2) -> n__take(X1, X2),
take(0(), IL) -> U81(isNatIList(IL)),
take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)}
Fail
SCC:
Strict:
{isNatList#(n__cons(V1, V2)) -> U51#(isNat(activate(V1)), activate(V2)),
U51#(tt(), V2) -> isNatList#(activate(V2))}
Weak:
{ cons(X1, X2) -> n__cons(X1, X2),
0() -> n__0(),
zeros() -> cons(0(), n__zeros()),
zeros() -> n__zeros(),
U11(tt()) -> tt(),
U21(tt()) -> tt(),
U31(tt()) -> tt(),
U42(tt()) -> tt(),
isNatIList(V) -> U31(isNatList(activate(V))),
isNatIList(n__zeros()) -> tt(),
isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)),
activate(X) -> X,
activate(n__zeros()) -> zeros(),
activate(n__take(X1, X2)) -> take(X1, X2),
activate(n__0()) -> 0(),
activate(n__length(X)) -> length(X),
activate(n__s(X)) -> s(X),
activate(n__cons(X1, X2)) -> cons(X1, X2),
activate(n__nil()) -> nil(),
U41(tt(), V2) -> U42(isNatIList(activate(V2))),
U52(tt()) -> tt(),
isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)),
isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)),
isNatList(n__nil()) -> tt(),
U51(tt(), V2) -> U52(isNatList(activate(V2))),
U62(tt()) -> tt(),
U61(tt(), V2) -> U62(isNatIList(activate(V2))),
U72(tt(), L) -> s(length(activate(L))),
isNat(n__0()) -> tt(),
isNat(n__length(V1)) -> U11(isNatList(activate(V1))),
isNat(n__s(V1)) -> U21(isNat(activate(V1))),
U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)),
s(X) -> n__s(X),
length(X) -> n__length(X),
length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N),
length(nil()) -> 0(),
nil() -> n__nil(),
U81(tt()) -> nil(),
U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)),
U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)),
U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))),
take(X1, X2) -> n__take(X1, X2),
take(0(), IL) -> U81(isNatIList(IL)),
take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)}
Fail
SCC:
Strict:
{isNatIList#(n__cons(V1, V2)) -> U41#(isNat(activate(V1)), activate(V2)),
U41#(tt(), V2) -> isNatIList#(activate(V2))}
Weak:
{ cons(X1, X2) -> n__cons(X1, X2),
0() -> n__0(),
zeros() -> cons(0(), n__zeros()),
zeros() -> n__zeros(),
U11(tt()) -> tt(),
U21(tt()) -> tt(),
U31(tt()) -> tt(),
U42(tt()) -> tt(),
isNatIList(V) -> U31(isNatList(activate(V))),
isNatIList(n__zeros()) -> tt(),
isNatIList(n__cons(V1, V2)) -> U41(isNat(activate(V1)), activate(V2)),
activate(X) -> X,
activate(n__zeros()) -> zeros(),
activate(n__take(X1, X2)) -> take(X1, X2),
activate(n__0()) -> 0(),
activate(n__length(X)) -> length(X),
activate(n__s(X)) -> s(X),
activate(n__cons(X1, X2)) -> cons(X1, X2),
activate(n__nil()) -> nil(),
U41(tt(), V2) -> U42(isNatIList(activate(V2))),
U52(tt()) -> tt(),
isNatList(n__take(V1, V2)) -> U61(isNat(activate(V1)), activate(V2)),
isNatList(n__cons(V1, V2)) -> U51(isNat(activate(V1)), activate(V2)),
isNatList(n__nil()) -> tt(),
U51(tt(), V2) -> U52(isNatList(activate(V2))),
U62(tt()) -> tt(),
U61(tt(), V2) -> U62(isNatIList(activate(V2))),
U72(tt(), L) -> s(length(activate(L))),
isNat(n__0()) -> tt(),
isNat(n__length(V1)) -> U11(isNatList(activate(V1))),
isNat(n__s(V1)) -> U21(isNat(activate(V1))),
U71(tt(), L, N) -> U72(isNat(activate(N)), activate(L)),
s(X) -> n__s(X),
length(X) -> n__length(X),
length(cons(N, L)) -> U71(isNatList(activate(L)), activate(L), N),
length(nil()) -> 0(),
nil() -> n__nil(),
U81(tt()) -> nil(),
U92(tt(), IL, M, N) -> U93(isNat(activate(N)), activate(IL), activate(M), activate(N)),
U91(tt(), IL, M, N) -> U92(isNat(activate(M)), activate(IL), activate(M), activate(N)),
U93(tt(), IL, M, N) -> cons(activate(N), n__take(activate(M), activate(IL))),
take(X1, X2) -> n__take(X1, X2),
take(0(), IL) -> U81(isNatIList(IL)),
take(s(M), cons(N, IL)) -> U91(isNatIList(activate(IL)), activate(IL), M, N)}
Fail