MAYBE Time: 0.106872 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: DP: { 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)} 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)} EDG: { (U91#(tt(), IL, M, N) -> activate# M, activate# n__nil() -> nil#()) (U91#(tt(), IL, M, N) -> activate# M, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U91#(tt(), IL, M, N) -> activate# M, activate# n__s X -> s# X) (U91#(tt(), IL, M, N) -> activate# M, activate# n__length X -> length# X) (U91#(tt(), IL, M, N) -> activate# M, activate# n__0() -> 0#()) (U91#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> take#(X1, X2)) (U91#(tt(), IL, M, N) -> activate# M, activate# n__zeros() -> zeros#()) (U41#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (U41#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U41#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U41#(tt(), V2) -> activate# V2, activate# n__length X -> length# X) (U41#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U41#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U41#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#()) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (U61#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (U61#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U61#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U61#(tt(), V2) -> activate# V2, activate# n__length X -> length# X) (U61#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U61#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U61#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#()) (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) (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__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) (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#()) (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__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__s V1 -> U21# isNat 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) (isNat# n__s V1 -> isNat# activate V1, isNat# n__length V1 -> U11# isNatList activate V1) (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# n__cons(V1, V2) -> isNat# 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) -> activate# V1) (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# V -> 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 -> U31# isNatList activate V) (U72#(tt(), L) -> length# activate L, length# nil() -> 0#()) (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__s V1 -> U21# isNat 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) (U71#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> U11# isNatList 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) (U41#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> U31# isNatList 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) (U61#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> U31# isNatList activate V) (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) -> activate# V1, activate# n__nil() -> nil#()) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#()) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#()) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#()) (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#()) (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#()) (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) (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)) (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) -> activate# IL) (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# N) (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#()) (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) (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#()) (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#()) (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__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#()) (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) (U51#(tt(), V2) -> isNatList# activate V2, isNatList# n__take(V1, V2) -> 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) -> U61#(isNat activate V1, activate V2)) (U51#(tt(), V2) -> isNatList# activate V2, isNatList# n__take(V1, V2) -> isNat# activate V1) (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 -> U11# 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 -> isNatList# 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__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__take(V1, V2) -> 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) -> U61#(isNat activate V1, 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__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 -> U11# 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 -> isNatList# 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__s V1 -> activate# V1) (U91#(tt(), IL, M, N) -> isNat# activate M, isNat# n__s V1 -> isNat# activate V1) (take#(0(), IL) -> U81# isNatIList IL, U81# tt() -> nil#()) (isNat# n__length V1 -> isNatList# activate V1, isNatList# n__take(V1, V2) -> 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) -> U61#(isNat activate V1, 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__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) (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) (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#()) (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) (activate# n__zeros() -> zeros#(), zeros#() -> cons#(0(), n__zeros())) (activate# n__zeros() -> zeros#(), zeros#() -> 0#()) (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) (isNatList# n__take(V1, V2) -> U61#(isNat activate V1, activate V2), U61#(tt(), V2) -> 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) -> U62# isNatIList activate V2) (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#()) (U51#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#()) (U51#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U51#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U51#(tt(), V2) -> activate# V2, activate# n__length X -> length# X) (U51#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U51#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U51#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__length X -> length# X) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (U93#(tt(), IL, M, N) -> activate# M, activate# n__zeros() -> zeros#()) (U93#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> take#(X1, X2)) (U93#(tt(), IL, M, N) -> activate# M, activate# n__0() -> 0#()) (U93#(tt(), IL, M, N) -> activate# M, activate# n__length X -> length# X) (U93#(tt(), IL, M, N) -> activate# M, activate# n__s X -> s# X) (U93#(tt(), IL, M, N) -> activate# M, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U93#(tt(), IL, M, N) -> activate# M, activate# n__nil() -> nil#()) (U92#(tt(), IL, M, N) -> activate# M, activate# n__zeros() -> zeros#()) (U92#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> take#(X1, X2)) (U92#(tt(), IL, M, N) -> activate# M, activate# n__0() -> 0#()) (U92#(tt(), IL, M, N) -> activate# M, activate# n__length X -> length# X) (U92#(tt(), IL, M, N) -> activate# M, activate# n__s X -> s# X) (U92#(tt(), IL, M, N) -> activate# M, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U92#(tt(), IL, M, N) -> activate# M, activate# n__nil() -> nil#()) } EDG: { (U91#(tt(), IL, M, N) -> activate# M, activate# n__nil() -> nil#()) (U91#(tt(), IL, M, N) -> activate# M, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U91#(tt(), IL, M, N) -> activate# M, activate# n__s X -> s# X) (U91#(tt(), IL, M, N) -> activate# M, activate# n__length X -> length# X) (U91#(tt(), IL, M, N) -> activate# M, activate# n__0() -> 0#()) (U91#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> take#(X1, X2)) (U91#(tt(), IL, M, N) -> activate# M, activate# n__zeros() -> zeros#()) (U41#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (U41#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U41#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U41#(tt(), V2) -> activate# V2, activate# n__length X -> length# X) (U41#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U41#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U41#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#()) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (U61#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (U61#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U61#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U61#(tt(), V2) -> activate# V2, activate# n__length X -> length# X) (U61#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U61#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U61#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#()) (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) (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__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) (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#()) (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__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__s V1 -> U21# isNat 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) (isNat# n__s V1 -> isNat# activate V1, isNat# n__length V1 -> U11# isNatList activate V1) (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# n__cons(V1, V2) -> isNat# 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) -> activate# V1) (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# V -> 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 -> U31# isNatList activate V) (U72#(tt(), L) -> length# activate L, length# nil() -> 0#()) (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__s V1 -> U21# isNat 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) (U71#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> U11# isNatList 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) (U41#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> U31# isNatList 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) (U61#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> U31# isNatList activate V) (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) -> activate# V1, activate# n__nil() -> nil#()) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#()) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#()) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#()) (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#()) (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#()) (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) (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)) (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) -> activate# IL) (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# N) (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#()) (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) (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#()) (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#()) (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__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#()) (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) (U51#(tt(), V2) -> isNatList# activate V2, isNatList# n__take(V1, V2) -> 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) -> U61#(isNat activate V1, activate V2)) (U51#(tt(), V2) -> isNatList# activate V2, isNatList# n__take(V1, V2) -> isNat# activate V1) (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 -> U11# 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 -> isNatList# 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__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__take(V1, V2) -> 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) -> U61#(isNat activate V1, 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__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 -> U11# 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 -> isNatList# 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__s V1 -> activate# V1) (U91#(tt(), IL, M, N) -> isNat# activate M, isNat# n__s V1 -> isNat# activate V1) (take#(0(), IL) -> U81# isNatIList IL, U81# tt() -> nil#()) (isNat# n__length V1 -> isNatList# activate V1, isNatList# n__take(V1, V2) -> 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) -> U61#(isNat activate V1, 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__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) (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) (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#()) (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) (activate# n__zeros() -> zeros#(), zeros#() -> cons#(0(), n__zeros())) (activate# n__zeros() -> zeros#(), zeros#() -> 0#()) (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) (isNatList# n__take(V1, V2) -> U61#(isNat activate V1, activate V2), U61#(tt(), V2) -> 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) -> U62# isNatIList activate V2) (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#()) (U51#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#()) (U51#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U51#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U51#(tt(), V2) -> activate# V2, activate# n__length X -> length# X) (U51#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U51#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U51#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__length X -> length# X) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (U93#(tt(), IL, M, N) -> activate# M, activate# n__zeros() -> zeros#()) (U93#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> take#(X1, X2)) (U93#(tt(), IL, M, N) -> activate# M, activate# n__0() -> 0#()) (U93#(tt(), IL, M, N) -> activate# M, activate# n__length X -> length# X) (U93#(tt(), IL, M, N) -> activate# M, activate# n__s X -> s# X) (U93#(tt(), IL, M, N) -> activate# M, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U93#(tt(), IL, M, N) -> activate# M, activate# n__nil() -> nil#()) (U92#(tt(), IL, M, N) -> activate# M, activate# n__zeros() -> zeros#()) (U92#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> take#(X1, X2)) (U92#(tt(), IL, M, N) -> activate# M, activate# n__0() -> 0#()) (U92#(tt(), IL, M, N) -> activate# M, activate# n__length X -> length# X) (U92#(tt(), IL, M, N) -> activate# M, activate# n__s X -> s# X) (U92#(tt(), IL, M, N) -> activate# M, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U92#(tt(), IL, M, N) -> activate# M, activate# n__nil() -> nil#()) } EDG: { (U91#(tt(), IL, M, N) -> activate# M, activate# n__nil() -> nil#()) (U91#(tt(), IL, M, N) -> activate# M, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U91#(tt(), IL, M, N) -> activate# M, activate# n__s X -> s# X) (U91#(tt(), IL, M, N) -> activate# M, activate# n__length X -> length# X) (U91#(tt(), IL, M, N) -> activate# M, activate# n__0() -> 0#()) (U91#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> take#(X1, X2)) (U91#(tt(), IL, M, N) -> activate# M, activate# n__zeros() -> zeros#()) (U41#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (U41#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U41#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U41#(tt(), V2) -> activate# V2, activate# n__length X -> length# X) (U41#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U41#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U41#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#()) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (U61#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (U61#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U61#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U61#(tt(), V2) -> activate# V2, activate# n__length X -> length# X) (U61#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U61#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U61#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#()) (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) (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__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) (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#()) (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__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__s V1 -> U21# isNat 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) (isNat# n__s V1 -> isNat# activate V1, isNat# n__length V1 -> U11# isNatList activate V1) (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# n__cons(V1, V2) -> isNat# 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) -> activate# V1) (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# V -> 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 -> U31# isNatList activate V) (U72#(tt(), L) -> length# activate L, length# nil() -> 0#()) (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__s V1 -> U21# isNat 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) (U71#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> U11# isNatList 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) (U41#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> U31# isNatList 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) (U61#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> U31# isNatList activate V) (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) -> activate# V1, activate# n__nil() -> nil#()) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#()) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#()) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#()) (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#()) (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#()) (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) (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)) (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) -> activate# IL) (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# N) (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#()) (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) (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#()) (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#()) (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__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#()) (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) (U51#(tt(), V2) -> isNatList# activate V2, isNatList# n__take(V1, V2) -> 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) -> U61#(isNat activate V1, activate V2)) (U51#(tt(), V2) -> isNatList# activate V2, isNatList# n__take(V1, V2) -> isNat# activate V1) (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 -> U11# 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 -> isNatList# 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__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__take(V1, V2) -> 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) -> U61#(isNat activate V1, 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__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 -> U11# 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 -> isNatList# 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__s V1 -> activate# V1) (U91#(tt(), IL, M, N) -> isNat# activate M, isNat# n__s V1 -> isNat# activate V1) (take#(0(), IL) -> U81# isNatIList IL, U81# tt() -> nil#()) (isNat# n__length V1 -> isNatList# activate V1, isNatList# n__take(V1, V2) -> 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) -> U61#(isNat activate V1, 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__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) (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) (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#()) (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) (activate# n__zeros() -> zeros#(), zeros#() -> cons#(0(), n__zeros())) (activate# n__zeros() -> zeros#(), zeros#() -> 0#()) (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) (isNatList# n__take(V1, V2) -> U61#(isNat activate V1, activate V2), U61#(tt(), V2) -> 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) -> U62# isNatIList activate V2) (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#()) (U51#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#()) (U51#(tt(), V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (U51#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U51#(tt(), V2) -> activate# V2, activate# n__length X -> length# X) (U51#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U51#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U51#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__length X -> length# X) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatList# n__take(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__take(X1, X2) -> take#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (U93#(tt(), IL, M, N) -> activate# M, activate# n__zeros() -> zeros#()) (U93#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> take#(X1, X2)) (U93#(tt(), IL, M, N) -> activate# M, activate# n__0() -> 0#()) (U93#(tt(), IL, M, N) -> activate# M, activate# n__length X -> length# X) (U93#(tt(), IL, M, N) -> activate# M, activate# n__s X -> s# X) (U93#(tt(), IL, M, N) -> activate# M, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U93#(tt(), IL, M, N) -> activate# M, activate# n__nil() -> nil#()) (U92#(tt(), IL, M, N) -> activate# M, activate# n__zeros() -> zeros#()) (U92#(tt(), IL, M, N) -> activate# M, activate# n__take(X1, X2) -> take#(X1, X2)) (U92#(tt(), IL, M, N) -> activate# M, activate# n__0() -> 0#()) (U92#(tt(), IL, M, N) -> activate# M, activate# n__length X -> length# X) (U92#(tt(), IL, M, N) -> activate# M, activate# n__s X -> s# X) (U92#(tt(), IL, M, N) -> activate# M, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U92#(tt(), IL, M, N) -> activate# M, activate# n__nil() -> nil#()) } STATUS: arrows: 0.932653 SCCS (1): 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 (52): 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)} Open