MAYBE Time: 0.318491 TRS: { and(tt(), T) -> T, isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L), isNatList n__nil() -> tt(), isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__length X -> length activate X, activate n__zeros() -> zeros(), activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__nil() -> nil(), activate n__take(X1, X2) -> take(activate X1, activate X2), isNatIList IL -> isNatList activate IL, isNatIList n__zeros() -> tt(), isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL), isNat n__0() -> tt(), isNat n__s N -> isNat activate N, isNat n__length L -> isNatList activate L, cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1 tt() -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1 isNatIList IL, take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)), s X -> n__s X, uLength(tt(), L) -> s length activate L, length X -> n__length X, length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L)} DP: DP: { isNatList# n__cons(N, L) -> and#(isNat activate N, isNatList activate L), isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> activate# N, isNatList# n__cons(N, L) -> activate# L, isNatList# n__cons(N, L) -> isNat# activate N, isNatList# n__take(N, IL) -> and#(isNat activate N, isNatIList activate IL), isNatList# n__take(N, IL) -> activate# IL, isNatList# n__take(N, IL) -> activate# N, isNatList# n__take(N, IL) -> isNatIList# activate IL, isNatList# n__take(N, IL) -> isNat# activate N, activate# n__0() -> 0#(), activate# n__s X -> activate# X, activate# n__s X -> s# activate X, activate# n__length X -> activate# X, activate# n__length X -> length# activate X, activate# n__zeros() -> zeros#(), activate# n__cons(X1, X2) -> activate# X1, activate# n__cons(X1, X2) -> cons#(activate X1, X2), activate# n__nil() -> nil#(), activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> take#(activate X1, activate X2), isNatIList# IL -> isNatList# activate IL, isNatIList# IL -> activate# IL, isNatIList# n__cons(N, IL) -> and#(isNat activate N, isNatIList activate IL), isNatIList# n__cons(N, IL) -> activate# IL, isNatIList# n__cons(N, IL) -> activate# N, isNatIList# n__cons(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> isNat# activate N, isNat# n__s N -> activate# N, isNat# n__s N -> isNat# activate N, isNat# n__length L -> isNatList# activate L, isNat# n__length L -> activate# L, zeros#() -> cons#(0(), n__zeros()), zeros#() -> 0#(), uTake1# tt() -> nil#(), take#(0(), IL) -> isNatIList# IL, take#(0(), IL) -> uTake1# isNatIList IL, take#(s M, cons(N, IL)) -> and#(isNat N, isNatIList activate IL), take#(s M, cons(N, IL)) -> and#(isNat M, and(isNat N, isNatIList activate IL)), take#(s M, cons(N, IL)) -> activate# IL, take#(s M, cons(N, IL)) -> isNatIList# activate IL, take#(s M, cons(N, IL)) -> isNat# N, take#(s M, cons(N, IL)) -> isNat# M, take#(s M, cons(N, IL)) -> uTake2#(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), uTake2#(tt(), M, N, IL) -> activate# IL, uTake2#(tt(), M, N, IL) -> activate# N, uTake2#(tt(), M, N, IL) -> activate# M, uTake2#(tt(), M, N, IL) -> cons#(activate N, n__take(activate M, activate IL)), uLength#(tt(), L) -> activate# L, uLength#(tt(), L) -> s# length activate L, uLength#(tt(), L) -> length# activate L, length# cons(N, L) -> and#(isNat N, isNatList activate L), length# cons(N, L) -> isNatList# activate L, length# cons(N, L) -> activate# L, length# cons(N, L) -> isNat# N, length# cons(N, L) -> uLength#(and(isNat N, isNatList activate L), activate L)} TRS: { and(tt(), T) -> T, isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L), isNatList n__nil() -> tt(), isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__length X -> length activate X, activate n__zeros() -> zeros(), activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__nil() -> nil(), activate n__take(X1, X2) -> take(activate X1, activate X2), isNatIList IL -> isNatList activate IL, isNatIList n__zeros() -> tt(), isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL), isNat n__0() -> tt(), isNat n__s N -> isNat activate N, isNat n__length L -> isNatList activate L, cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1 tt() -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1 isNatIList IL, take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)), s X -> n__s X, uLength(tt(), L) -> s length activate L, length X -> n__length X, length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L)} UR: { and(tt(), T) -> T, isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L), isNatList n__nil() -> tt(), isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__length X -> length activate X, activate n__zeros() -> zeros(), activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__nil() -> nil(), activate n__take(X1, X2) -> take(activate X1, activate X2), isNatIList IL -> isNatList activate IL, isNatIList n__zeros() -> tt(), isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL), isNat n__0() -> tt(), isNat n__s N -> isNat activate N, isNat n__length L -> isNatList activate L, cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1 tt() -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1 isNatIList IL, take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)), s X -> n__s X, uLength(tt(), L) -> s length activate L, length X -> n__length X, length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L), a(x, y) -> x, a(x, y) -> y} EDG: { (length# cons(N, L) -> uLength#(and(isNat N, isNatList activate L), activate L), uLength#(tt(), L) -> length# activate L) (length# cons(N, L) -> uLength#(and(isNat N, isNatList activate L), activate L), uLength#(tt(), L) -> s# length activate L) (length# cons(N, L) -> uLength#(and(isNat N, isNatList activate L), activate L), uLength#(tt(), L) -> activate# L) (activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X2) (activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X1) (activate# n__take(X1, X2) -> activate# X1, activate# n__nil() -> nil#()) (activate# n__take(X1, X2) -> activate# X1, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (activate# n__take(X1, X2) -> activate# X1, activate# n__cons(X1, X2) -> activate# X1) (activate# n__take(X1, X2) -> activate# X1, activate# n__zeros() -> zeros#()) (activate# n__take(X1, X2) -> activate# X1, activate# n__length X -> length# activate X) (activate# n__take(X1, X2) -> activate# X1, activate# n__length X -> activate# X) (activate# n__take(X1, X2) -> activate# X1, activate# n__s X -> s# activate X) (activate# n__take(X1, X2) -> activate# X1, activate# n__s X -> activate# X) (activate# n__take(X1, X2) -> activate# X1, activate# n__0() -> 0#()) (activate# n__s X -> activate# X, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (activate# n__s X -> activate# X, activate# n__take(X1, X2) -> activate# X2) (activate# n__s X -> activate# X, activate# n__take(X1, X2) -> activate# X1) (activate# n__s X -> activate# X, activate# n__nil() -> nil#()) (activate# n__s X -> activate# X, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (activate# n__s X -> activate# X, activate# n__cons(X1, X2) -> activate# X1) (activate# n__s X -> activate# X, activate# n__zeros() -> zeros#()) (activate# n__s X -> activate# X, activate# n__length X -> length# activate X) (activate# n__s X -> activate# X, activate# n__length X -> activate# X) (activate# n__s X -> activate# X, activate# n__s X -> s# activate X) (activate# n__s X -> activate# X, activate# n__s X -> activate# X) (activate# n__s X -> activate# X, activate# n__0() -> 0#()) (take#(s M, cons(N, IL)) -> isNat# M, isNat# n__length L -> activate# L) (take#(s M, cons(N, IL)) -> isNat# M, isNat# n__length L -> isNatList# activate L) (take#(s M, cons(N, IL)) -> isNat# M, isNat# n__s N -> isNat# activate N) (take#(s M, cons(N, IL)) -> isNat# M, isNat# n__s N -> activate# N) (take#(s M, cons(N, IL)) -> uTake2#(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), uTake2#(tt(), M, N, IL) -> cons#(activate N, n__take(activate M, activate IL))) (take#(s M, cons(N, IL)) -> uTake2#(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), uTake2#(tt(), M, N, IL) -> activate# M) (take#(s M, cons(N, IL)) -> uTake2#(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), uTake2#(tt(), M, N, IL) -> activate# N) (take#(s M, cons(N, IL)) -> uTake2#(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), uTake2#(tt(), M, N, IL) -> activate# IL) (isNat# n__length L -> activate# L, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (isNat# n__length L -> activate# L, activate# n__take(X1, X2) -> activate# X2) (isNat# n__length L -> activate# L, activate# n__take(X1, X2) -> activate# X1) (isNat# n__length L -> activate# L, activate# n__nil() -> nil#()) (isNat# n__length L -> activate# L, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (isNat# n__length L -> activate# L, activate# n__cons(X1, X2) -> activate# X1) (isNat# n__length L -> activate# L, activate# n__zeros() -> zeros#()) (isNat# n__length L -> activate# L, activate# n__length X -> length# activate X) (isNat# n__length L -> activate# L, activate# n__length X -> activate# X) (isNat# n__length L -> activate# L, activate# n__s X -> s# activate X) (isNat# n__length L -> activate# L, activate# n__s X -> activate# X) (isNat# n__length L -> activate# L, activate# n__0() -> 0#()) (length# cons(N, L) -> activate# L, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (length# cons(N, L) -> activate# L, activate# n__take(X1, X2) -> activate# X2) (length# cons(N, L) -> activate# L, activate# n__take(X1, X2) -> activate# X1) (length# cons(N, L) -> activate# L, activate# n__nil() -> nil#()) (length# cons(N, L) -> activate# L, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (length# cons(N, L) -> activate# L, activate# n__cons(X1, X2) -> activate# X1) (length# cons(N, L) -> activate# L, activate# n__zeros() -> zeros#()) (length# cons(N, L) -> activate# L, activate# n__length X -> length# activate X) (length# cons(N, L) -> activate# L, activate# n__length X -> activate# X) (length# cons(N, L) -> activate# L, activate# n__s X -> s# activate X) (length# cons(N, L) -> activate# L, activate# n__s X -> activate# X) (length# cons(N, L) -> activate# L, activate# n__0() -> 0#()) (isNatList# n__cons(N, L) -> activate# N, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (isNatList# n__cons(N, L) -> activate# N, activate# n__take(X1, X2) -> activate# X2) (isNatList# n__cons(N, L) -> activate# N, activate# n__take(X1, X2) -> activate# X1) (isNatList# n__cons(N, L) -> activate# N, activate# n__nil() -> nil#()) (isNatList# n__cons(N, L) -> activate# N, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (isNatList# n__cons(N, L) -> activate# N, activate# n__cons(X1, X2) -> activate# X1) (isNatList# n__cons(N, L) -> activate# N, activate# n__zeros() -> zeros#()) (isNatList# n__cons(N, L) -> activate# N, activate# n__length X -> length# activate X) (isNatList# n__cons(N, L) -> activate# N, activate# n__length X -> activate# X) (isNatList# n__cons(N, L) -> activate# N, activate# n__s X -> s# activate X) (isNatList# n__cons(N, L) -> activate# N, activate# n__s X -> activate# X) (isNatList# n__cons(N, L) -> activate# N, activate# n__0() -> 0#()) (isNatIList# n__cons(N, IL) -> activate# N, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (isNatIList# n__cons(N, IL) -> activate# N, activate# n__take(X1, X2) -> activate# X2) (isNatIList# n__cons(N, IL) -> activate# N, activate# n__take(X1, X2) -> activate# X1) (isNatIList# n__cons(N, IL) -> activate# N, activate# n__nil() -> nil#()) (isNatIList# n__cons(N, IL) -> activate# N, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (isNatIList# n__cons(N, IL) -> activate# N, activate# n__cons(X1, X2) -> activate# X1) (isNatIList# n__cons(N, IL) -> activate# N, activate# n__zeros() -> zeros#()) (isNatIList# n__cons(N, IL) -> activate# N, activate# n__length X -> length# activate X) (isNatIList# n__cons(N, IL) -> activate# N, activate# n__length X -> activate# X) (isNatIList# n__cons(N, IL) -> activate# N, activate# n__s X -> s# activate X) (isNatIList# n__cons(N, IL) -> activate# N, activate# n__s X -> activate# X) (isNatIList# n__cons(N, IL) -> activate# N, activate# n__0() -> 0#()) (take#(s M, cons(N, IL)) -> isNat# N, isNat# n__length L -> activate# L) (take#(s M, cons(N, IL)) -> isNat# N, isNat# n__length L -> isNatList# activate L) (take#(s M, cons(N, IL)) -> isNat# N, isNat# n__s N -> isNat# activate N) (take#(s M, cons(N, IL)) -> isNat# N, isNat# n__s N -> activate# N) (length# cons(N, L) -> isNat# N, isNat# n__length L -> activate# L) (length# cons(N, L) -> isNat# N, isNat# n__length L -> isNatList# activate L) (length# cons(N, L) -> isNat# N, isNat# n__s N -> isNat# activate N) (length# cons(N, L) -> isNat# N, isNat# n__s N -> activate# N) (isNat# n__length L -> isNatList# activate L, isNatList# n__take(N, IL) -> isNat# activate N) (isNat# n__length L -> isNatList# activate L, isNatList# n__take(N, IL) -> isNatIList# activate IL) (isNat# n__length L -> isNatList# activate L, isNatList# n__take(N, IL) -> activate# N) (isNat# n__length L -> isNatList# activate L, isNatList# n__take(N, IL) -> activate# IL) (isNat# n__length L -> isNatList# activate L, isNatList# n__take(N, IL) -> and#(isNat activate N, isNatIList activate IL)) (isNat# n__length L -> isNatList# activate L, isNatList# n__cons(N, L) -> isNat# activate N) (isNat# n__length L -> isNatList# activate L, isNatList# n__cons(N, L) -> activate# L) (isNat# n__length L -> isNatList# activate L, isNatList# n__cons(N, L) -> activate# N) (isNat# n__length L -> isNatList# activate L, isNatList# n__cons(N, L) -> isNatList# activate L) (isNat# n__length L -> isNatList# activate L, isNatList# n__cons(N, L) -> and#(isNat activate N, isNatList activate L)) (length# cons(N, L) -> isNatList# activate L, isNatList# n__take(N, IL) -> isNat# activate N) (length# cons(N, L) -> isNatList# activate L, isNatList# n__take(N, IL) -> isNatIList# activate IL) (length# cons(N, L) -> isNatList# activate L, isNatList# n__take(N, IL) -> activate# N) (length# cons(N, L) -> isNatList# activate L, isNatList# n__take(N, IL) -> activate# IL) (length# cons(N, L) -> isNatList# activate L, isNatList# n__take(N, IL) -> and#(isNat activate N, isNatIList activate IL)) (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> isNat# activate N) (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> activate# L) (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> activate# N) (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> isNatList# activate L) (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> and#(isNat activate N, isNatList activate L)) (isNatList# n__take(N, IL) -> isNat# activate N, isNat# n__length L -> activate# L) (isNatList# n__take(N, IL) -> isNat# activate N, isNat# n__length L -> isNatList# activate L) (isNatList# n__take(N, IL) -> isNat# activate N, isNat# n__s N -> isNat# activate N) (isNatList# n__take(N, IL) -> isNat# activate N, isNat# n__s N -> activate# N) (isNat# n__s N -> isNat# activate N, isNat# n__length L -> activate# L) (isNat# n__s N -> isNat# activate N, isNat# n__length L -> isNatList# activate L) (isNat# n__s N -> isNat# activate N, isNat# n__s N -> isNat# activate N) (isNat# n__s N -> isNat# activate N, isNat# n__s N -> activate# N) (isNatIList# IL -> isNatList# activate IL, isNatList# n__take(N, IL) -> isNat# activate N) (isNatIList# IL -> isNatList# activate IL, isNatList# n__take(N, IL) -> isNatIList# activate IL) (isNatIList# IL -> isNatList# activate IL, isNatList# n__take(N, IL) -> activate# N) (isNatIList# IL -> isNatList# activate IL, isNatList# n__take(N, IL) -> activate# IL) (isNatIList# IL -> isNatList# activate IL, isNatList# n__take(N, IL) -> and#(isNat activate N, isNatIList activate IL)) (isNatIList# IL -> isNatList# activate IL, isNatList# n__cons(N, L) -> isNat# activate N) (isNatIList# IL -> isNatList# activate IL, isNatList# n__cons(N, L) -> activate# L) (isNatIList# IL -> isNatList# activate IL, isNatList# n__cons(N, L) -> activate# N) (isNatIList# IL -> isNatList# activate IL, isNatList# n__cons(N, L) -> isNatList# activate L) (isNatIList# IL -> isNatList# activate IL, isNatList# n__cons(N, L) -> and#(isNat activate N, isNatList activate L)) (take#(0(), IL) -> uTake1# isNatIList IL, uTake1# tt() -> nil#()) (activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> activate# X2) (activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> activate# X1) (activate# n__take(X1, X2) -> activate# X2, activate# n__nil() -> nil#()) (activate# n__take(X1, X2) -> activate# X2, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (activate# n__take(X1, X2) -> activate# X2, activate# n__cons(X1, X2) -> activate# X1) (activate# n__take(X1, X2) -> activate# X2, activate# n__zeros() -> zeros#()) (activate# n__take(X1, X2) -> activate# X2, activate# n__length X -> length# activate X) (activate# n__take(X1, X2) -> activate# X2, activate# n__length X -> activate# X) (activate# n__take(X1, X2) -> activate# X2, activate# n__s X -> s# activate X) (activate# n__take(X1, X2) -> activate# X2, activate# n__s X -> activate# X) (activate# n__take(X1, X2) -> activate# X2, activate# n__0() -> 0#()) (isNatIList# n__cons(N, IL) -> activate# IL, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (isNatIList# n__cons(N, IL) -> activate# IL, activate# n__take(X1, X2) -> activate# X2) (isNatIList# n__cons(N, IL) -> activate# IL, activate# n__take(X1, X2) -> activate# X1) (isNatIList# n__cons(N, IL) -> activate# IL, activate# n__nil() -> nil#()) (isNatIList# n__cons(N, IL) -> activate# IL, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (isNatIList# n__cons(N, IL) -> activate# IL, activate# n__cons(X1, X2) -> activate# X1) (isNatIList# n__cons(N, IL) -> activate# IL, activate# n__zeros() -> zeros#()) (isNatIList# n__cons(N, IL) -> activate# IL, activate# n__length X -> length# activate X) (isNatIList# n__cons(N, IL) -> activate# IL, activate# n__length X -> activate# X) (isNatIList# n__cons(N, IL) -> activate# IL, activate# n__s X -> s# activate X) (isNatIList# n__cons(N, IL) -> activate# IL, activate# n__s X -> activate# X) (isNatIList# n__cons(N, IL) -> activate# IL, activate# n__0() -> 0#()) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__take(X1, X2) -> activate# X2) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__take(X1, X2) -> activate# X1) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__nil() -> nil#()) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__cons(X1, X2) -> activate# X1) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__zeros() -> zeros#()) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__length X -> length# activate X) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__length X -> activate# X) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__s X -> s# activate X) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__s X -> activate# X) (take#(s M, cons(N, IL)) -> activate# IL, activate# n__0() -> 0#()) (uTake2#(tt(), M, N, IL) -> activate# IL, activate# n__0() -> 0#()) (uTake2#(tt(), M, N, IL) -> activate# IL, activate# n__s X -> activate# X) (uTake2#(tt(), M, N, IL) -> activate# IL, activate# n__s X -> s# activate X) (uTake2#(tt(), M, N, IL) -> activate# IL, activate# n__length X -> activate# X) (uTake2#(tt(), M, N, IL) -> activate# IL, activate# n__length X -> length# activate X) (uTake2#(tt(), M, N, IL) -> activate# IL, activate# n__zeros() -> zeros#()) (uTake2#(tt(), M, N, IL) -> activate# IL, activate# n__cons(X1, X2) -> activate# X1) (uTake2#(tt(), M, N, IL) -> activate# IL, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (uTake2#(tt(), M, N, IL) -> activate# IL, activate# n__nil() -> nil#()) (uTake2#(tt(), M, N, IL) -> activate# IL, activate# n__take(X1, X2) -> activate# X1) (uTake2#(tt(), M, N, IL) -> activate# IL, activate# n__take(X1, X2) -> activate# X2) (uTake2#(tt(), M, N, IL) -> activate# IL, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (take#(0(), IL) -> isNatIList# IL, isNatIList# IL -> isNatList# activate IL) (take#(0(), IL) -> isNatIList# IL, isNatIList# IL -> activate# IL) (take#(0(), IL) -> isNatIList# IL, isNatIList# n__cons(N, IL) -> and#(isNat activate N, isNatIList activate IL)) (take#(0(), IL) -> isNatIList# IL, isNatIList# n__cons(N, IL) -> activate# IL) (take#(0(), IL) -> isNatIList# IL, isNatIList# n__cons(N, IL) -> activate# N) (take#(0(), IL) -> isNatIList# IL, isNatIList# n__cons(N, IL) -> isNatIList# activate IL) (take#(0(), IL) -> isNatIList# IL, isNatIList# n__cons(N, IL) -> isNat# activate N) (isNatIList# IL -> activate# IL, activate# n__0() -> 0#()) (isNatIList# IL -> activate# IL, activate# n__s X -> activate# X) (isNatIList# IL -> activate# IL, activate# n__s X -> s# activate X) (isNatIList# IL -> activate# IL, activate# n__length X -> activate# X) (isNatIList# IL -> activate# IL, activate# n__length X -> length# activate X) (isNatIList# IL -> activate# IL, activate# n__zeros() -> zeros#()) (isNatIList# IL -> activate# IL, activate# n__cons(X1, X2) -> activate# X1) (isNatIList# IL -> activate# IL, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (isNatIList# IL -> activate# IL, activate# n__nil() -> nil#()) (isNatIList# IL -> activate# IL, activate# n__take(X1, X2) -> activate# X1) (isNatIList# IL -> activate# IL, activate# n__take(X1, X2) -> activate# X2) (isNatIList# IL -> activate# IL, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (isNatList# n__take(N, IL) -> activate# IL, activate# n__0() -> 0#()) (isNatList# n__take(N, IL) -> activate# IL, activate# n__s X -> activate# X) (isNatList# n__take(N, IL) -> activate# IL, activate# n__s X -> s# activate X) (isNatList# n__take(N, IL) -> activate# IL, activate# n__length X -> activate# X) (isNatList# n__take(N, IL) -> activate# IL, activate# n__length X -> length# activate X) (isNatList# n__take(N, IL) -> activate# IL, activate# n__zeros() -> zeros#()) (isNatList# n__take(N, IL) -> activate# IL, activate# n__cons(X1, X2) -> activate# X1) (isNatList# n__take(N, IL) -> activate# IL, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (isNatList# n__take(N, IL) -> activate# IL, activate# n__nil() -> nil#()) (isNatList# n__take(N, IL) -> activate# IL, activate# n__take(X1, X2) -> activate# X1) (isNatList# n__take(N, IL) -> activate# IL, activate# n__take(X1, X2) -> activate# X2) (isNatList# n__take(N, IL) -> activate# IL, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# IL -> isNatList# activate IL) (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# IL -> activate# IL) (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> and#(isNat activate N, isNatIList activate IL)) (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> activate# IL) (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> activate# N) (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> isNatIList# activate IL) (take#(s M, cons(N, IL)) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> isNat# activate N) (isNatIList# n__cons(N, IL) -> isNatIList# activate IL, isNatIList# IL -> isNatList# activate IL) (isNatIList# n__cons(N, IL) -> isNatIList# activate IL, isNatIList# IL -> activate# IL) (isNatIList# n__cons(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> and#(isNat activate N, isNatIList activate IL)) (isNatIList# n__cons(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> activate# IL) (isNatIList# n__cons(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> activate# N) (isNatIList# n__cons(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> isNatIList# activate IL) (isNatIList# n__cons(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> isNat# activate N) (isNatList# n__take(N, IL) -> isNatIList# activate IL, isNatIList# IL -> isNatList# activate IL) (isNatList# n__take(N, IL) -> isNatIList# activate IL, isNatIList# IL -> activate# IL) (isNatList# n__take(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> and#(isNat activate N, isNatIList activate IL)) (isNatList# n__take(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> activate# IL) (isNatList# n__take(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> activate# N) (isNatList# n__take(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> isNatIList# activate IL) (isNatList# n__take(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> isNat# activate N) (isNatIList# n__cons(N, IL) -> isNat# activate N, isNat# n__s N -> activate# N) (isNatIList# n__cons(N, IL) -> isNat# activate N, isNat# n__s N -> isNat# activate N) (isNatIList# n__cons(N, IL) -> isNat# activate N, isNat# n__length L -> isNatList# activate L) (isNatIList# n__cons(N, IL) -> isNat# activate N, isNat# n__length L -> activate# L) (isNatList# n__cons(N, L) -> isNat# activate N, isNat# n__s N -> activate# N) (isNatList# n__cons(N, L) -> isNat# activate N, isNat# n__s N -> isNat# activate N) (isNatList# n__cons(N, L) -> isNat# activate N, isNat# n__length L -> isNatList# activate L) (isNatList# n__cons(N, L) -> isNat# activate N, isNat# n__length L -> activate# L) (uLength#(tt(), L) -> length# activate L, length# cons(N, L) -> and#(isNat N, isNatList activate L)) (uLength#(tt(), L) -> length# activate L, length# cons(N, L) -> isNatList# activate L) (uLength#(tt(), L) -> length# activate L, length# cons(N, L) -> activate# L) (uLength#(tt(), L) -> length# activate L, length# cons(N, L) -> isNat# N) (uLength#(tt(), L) -> length# activate L, length# cons(N, L) -> uLength#(and(isNat N, isNatList activate L), activate L)) (isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> and#(isNat activate N, isNatList activate L)) (isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> isNatList# activate L) (isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> activate# N) (isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> activate# L) (isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> isNat# activate N) (isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__take(N, IL) -> and#(isNat activate N, isNatIList activate IL)) (isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__take(N, IL) -> activate# IL) (isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__take(N, IL) -> activate# N) (isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__take(N, IL) -> isNatIList# activate IL) (isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__take(N, IL) -> isNat# activate N) (uTake2#(tt(), M, N, IL) -> activate# N, activate# n__0() -> 0#()) (uTake2#(tt(), M, N, IL) -> activate# N, activate# n__s X -> activate# X) (uTake2#(tt(), M, N, IL) -> activate# N, activate# n__s X -> s# activate X) (uTake2#(tt(), M, N, IL) -> activate# N, activate# n__length X -> activate# X) (uTake2#(tt(), M, N, IL) -> activate# N, activate# n__length X -> length# activate X) (uTake2#(tt(), M, N, IL) -> activate# N, activate# n__zeros() -> zeros#()) (uTake2#(tt(), M, N, IL) -> activate# N, activate# n__cons(X1, X2) -> activate# X1) (uTake2#(tt(), M, N, IL) -> activate# N, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (uTake2#(tt(), M, N, IL) -> activate# N, activate# n__nil() -> nil#()) (uTake2#(tt(), M, N, IL) -> activate# N, activate# n__take(X1, X2) -> activate# X1) (uTake2#(tt(), M, N, IL) -> activate# N, activate# n__take(X1, X2) -> activate# X2) (uTake2#(tt(), M, N, IL) -> activate# N, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (isNat# n__s N -> activate# N, activate# n__0() -> 0#()) (isNat# n__s N -> activate# N, activate# n__s X -> activate# X) (isNat# n__s N -> activate# N, activate# n__s X -> s# activate X) (isNat# n__s N -> activate# N, activate# n__length X -> activate# X) (isNat# n__s N -> activate# N, activate# n__length X -> length# activate X) (isNat# n__s N -> activate# N, activate# n__zeros() -> zeros#()) (isNat# n__s N -> activate# N, activate# n__cons(X1, X2) -> activate# X1) (isNat# n__s N -> activate# N, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (isNat# n__s N -> activate# N, activate# n__nil() -> nil#()) (isNat# n__s N -> activate# N, activate# n__take(X1, X2) -> activate# X1) (isNat# n__s N -> activate# N, activate# n__take(X1, X2) -> activate# X2) (isNat# n__s N -> activate# N, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (activate# n__length X -> length# activate X, length# cons(N, L) -> and#(isNat N, isNatList activate L)) (activate# n__length X -> length# activate X, length# cons(N, L) -> isNatList# activate L) (activate# n__length X -> length# activate X, length# cons(N, L) -> activate# L) (activate# n__length X -> length# activate X, length# cons(N, L) -> isNat# N) (activate# n__length X -> length# activate X, length# cons(N, L) -> uLength#(and(isNat N, isNatList activate L), activate L)) (isNatList# n__take(N, IL) -> activate# N, activate# n__0() -> 0#()) (isNatList# n__take(N, IL) -> activate# N, activate# n__s X -> activate# X) (isNatList# n__take(N, IL) -> activate# N, activate# n__s X -> s# activate X) (isNatList# n__take(N, IL) -> activate# N, activate# n__length X -> activate# X) (isNatList# n__take(N, IL) -> activate# N, activate# n__length X -> length# activate X) (isNatList# n__take(N, IL) -> activate# N, activate# n__zeros() -> zeros#()) (isNatList# n__take(N, IL) -> activate# N, activate# n__cons(X1, X2) -> activate# X1) (isNatList# n__take(N, IL) -> activate# N, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (isNatList# n__take(N, IL) -> activate# N, activate# n__nil() -> nil#()) (isNatList# n__take(N, IL) -> activate# N, activate# n__take(X1, X2) -> activate# X1) (isNatList# n__take(N, IL) -> activate# N, activate# n__take(X1, X2) -> activate# X2) (isNatList# n__take(N, IL) -> activate# N, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (uLength#(tt(), L) -> activate# L, activate# n__0() -> 0#()) (uLength#(tt(), L) -> activate# L, activate# n__s X -> activate# X) (uLength#(tt(), L) -> activate# L, activate# n__s X -> s# activate X) (uLength#(tt(), L) -> activate# L, activate# n__length X -> activate# X) (uLength#(tt(), L) -> activate# L, activate# n__length X -> length# activate X) (uLength#(tt(), L) -> activate# L, activate# n__zeros() -> zeros#()) (uLength#(tt(), L) -> activate# L, activate# n__cons(X1, X2) -> activate# X1) (uLength#(tt(), L) -> activate# L, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (uLength#(tt(), L) -> activate# L, activate# n__nil() -> nil#()) (uLength#(tt(), L) -> activate# L, activate# n__take(X1, X2) -> activate# X1) (uLength#(tt(), L) -> activate# L, activate# n__take(X1, X2) -> activate# X2) (uLength#(tt(), L) -> activate# L, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (isNatList# n__cons(N, L) -> activate# L, activate# n__0() -> 0#()) (isNatList# n__cons(N, L) -> activate# L, activate# n__s X -> activate# X) (isNatList# n__cons(N, L) -> activate# L, activate# n__s X -> s# activate X) (isNatList# n__cons(N, L) -> activate# L, activate# n__length X -> activate# X) (isNatList# n__cons(N, L) -> activate# L, activate# n__length X -> length# activate X) (isNatList# n__cons(N, L) -> activate# L, activate# n__zeros() -> zeros#()) (isNatList# n__cons(N, L) -> activate# L, activate# n__cons(X1, X2) -> activate# X1) (isNatList# n__cons(N, L) -> activate# L, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (isNatList# n__cons(N, L) -> activate# L, activate# n__nil() -> nil#()) (isNatList# n__cons(N, L) -> activate# L, activate# n__take(X1, X2) -> activate# X1) (isNatList# n__cons(N, L) -> activate# L, activate# n__take(X1, X2) -> activate# X2) (isNatList# n__cons(N, L) -> activate# L, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (activate# n__zeros() -> zeros#(), zeros#() -> cons#(0(), n__zeros())) (activate# n__zeros() -> zeros#(), zeros#() -> 0#()) (uTake2#(tt(), M, N, IL) -> activate# M, activate# n__0() -> 0#()) (uTake2#(tt(), M, N, IL) -> activate# M, activate# n__s X -> activate# X) (uTake2#(tt(), M, N, IL) -> activate# M, activate# n__s X -> s# activate X) (uTake2#(tt(), M, N, IL) -> activate# M, activate# n__length X -> activate# X) (uTake2#(tt(), M, N, IL) -> activate# M, activate# n__length X -> length# activate X) (uTake2#(tt(), M, N, IL) -> activate# M, activate# n__zeros() -> zeros#()) (uTake2#(tt(), M, N, IL) -> activate# M, activate# n__cons(X1, X2) -> activate# X1) (uTake2#(tt(), M, N, IL) -> activate# M, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (uTake2#(tt(), M, N, IL) -> activate# M, activate# n__nil() -> nil#()) (uTake2#(tt(), M, N, IL) -> activate# M, activate# n__take(X1, X2) -> activate# X1) (uTake2#(tt(), M, N, IL) -> activate# M, activate# n__take(X1, X2) -> activate# X2) (uTake2#(tt(), M, N, IL) -> activate# M, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (activate# n__length X -> activate# X, activate# n__0() -> 0#()) (activate# n__length X -> activate# X, activate# n__s X -> activate# X) (activate# n__length X -> activate# X, activate# n__s X -> s# activate X) (activate# n__length X -> activate# X, activate# n__length X -> activate# X) (activate# n__length X -> activate# X, activate# n__length X -> length# activate X) (activate# n__length X -> activate# X, activate# n__zeros() -> zeros#()) (activate# n__length X -> activate# X, activate# n__cons(X1, X2) -> activate# X1) (activate# n__length X -> activate# X, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (activate# n__length X -> activate# X, activate# n__nil() -> nil#()) (activate# n__length X -> activate# X, activate# n__take(X1, X2) -> activate# X1) (activate# n__length X -> activate# X, activate# n__take(X1, X2) -> activate# X2) (activate# n__length X -> activate# X, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (activate# n__cons(X1, X2) -> activate# X1, activate# n__0() -> 0#()) (activate# n__cons(X1, X2) -> activate# X1, activate# n__s X -> activate# X) (activate# n__cons(X1, X2) -> activate# X1, activate# n__s X -> s# activate X) (activate# n__cons(X1, X2) -> activate# X1, activate# n__length X -> activate# X) (activate# n__cons(X1, X2) -> activate# X1, activate# n__length X -> length# activate X) (activate# n__cons(X1, X2) -> activate# X1, activate# n__zeros() -> zeros#()) (activate# n__cons(X1, X2) -> activate# X1, activate# n__cons(X1, X2) -> activate# X1) (activate# n__cons(X1, X2) -> activate# X1, activate# n__cons(X1, X2) -> cons#(activate X1, X2)) (activate# n__cons(X1, X2) -> activate# X1, activate# n__nil() -> nil#()) (activate# n__cons(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X1) (activate# n__cons(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X2) (activate# n__cons(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> take#(activate X1, activate X2)) (activate# n__take(X1, X2) -> take#(activate X1, activate X2), take#(0(), IL) -> isNatIList# IL) (activate# n__take(X1, X2) -> take#(activate X1, activate X2), take#(0(), IL) -> uTake1# isNatIList IL) (activate# n__take(X1, X2) -> take#(activate X1, activate X2), take#(s M, cons(N, IL)) -> and#(isNat N, isNatIList activate IL)) (activate# n__take(X1, X2) -> take#(activate X1, activate X2), take#(s M, cons(N, IL)) -> and#(isNat M, and(isNat N, isNatIList activate IL))) (activate# n__take(X1, X2) -> take#(activate X1, activate X2), take#(s M, cons(N, IL)) -> activate# IL) (activate# n__take(X1, X2) -> take#(activate X1, activate X2), take#(s M, cons(N, IL)) -> isNatIList# activate IL) (activate# n__take(X1, X2) -> take#(activate X1, activate X2), take#(s M, cons(N, IL)) -> isNat# N) (activate# n__take(X1, X2) -> take#(activate X1, activate X2), take#(s M, cons(N, IL)) -> isNat# M) (activate# n__take(X1, X2) -> take#(activate X1, activate X2), take#(s M, cons(N, IL)) -> uTake2#(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL)) } STATUS: arrows: 0.887658 SCCS (1): Scc: { isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> activate# N, isNatList# n__cons(N, L) -> activate# L, isNatList# n__cons(N, L) -> isNat# activate N, isNatList# n__take(N, IL) -> activate# IL, isNatList# n__take(N, IL) -> activate# N, isNatList# n__take(N, IL) -> isNatIList# activate IL, isNatList# n__take(N, IL) -> isNat# activate N, activate# n__s X -> activate# X, activate# n__length X -> activate# X, activate# n__length X -> length# activate X, activate# n__cons(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> take#(activate X1, activate X2), isNatIList# IL -> isNatList# activate IL, isNatIList# IL -> activate# IL, isNatIList# n__cons(N, IL) -> activate# IL, isNatIList# n__cons(N, IL) -> activate# N, isNatIList# n__cons(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> isNat# activate N, isNat# n__s N -> activate# N, isNat# n__s N -> isNat# activate N, isNat# n__length L -> isNatList# activate L, isNat# n__length L -> activate# L, take#(0(), IL) -> isNatIList# IL, take#(s M, cons(N, IL)) -> activate# IL, take#(s M, cons(N, IL)) -> isNatIList# activate IL, take#(s M, cons(N, IL)) -> isNat# N, take#(s M, cons(N, IL)) -> isNat# M, take#(s M, cons(N, IL)) -> uTake2#(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), uTake2#(tt(), M, N, IL) -> activate# IL, uTake2#(tt(), M, N, IL) -> activate# N, uTake2#(tt(), M, N, IL) -> activate# M, uLength#(tt(), L) -> activate# L, uLength#(tt(), L) -> length# activate L, length# cons(N, L) -> isNatList# activate L, length# cons(N, L) -> activate# L, length# cons(N, L) -> isNat# N, length# cons(N, L) -> uLength#(and(isNat N, isNatList activate L), activate L)} SCC (40): Strict: { isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> activate# N, isNatList# n__cons(N, L) -> activate# L, isNatList# n__cons(N, L) -> isNat# activate N, isNatList# n__take(N, IL) -> activate# IL, isNatList# n__take(N, IL) -> activate# N, isNatList# n__take(N, IL) -> isNatIList# activate IL, isNatList# n__take(N, IL) -> isNat# activate N, activate# n__s X -> activate# X, activate# n__length X -> activate# X, activate# n__length X -> length# activate X, activate# n__cons(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> take#(activate X1, activate X2), isNatIList# IL -> isNatList# activate IL, isNatIList# IL -> activate# IL, isNatIList# n__cons(N, IL) -> activate# IL, isNatIList# n__cons(N, IL) -> activate# N, isNatIList# n__cons(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> isNat# activate N, isNat# n__s N -> activate# N, isNat# n__s N -> isNat# activate N, isNat# n__length L -> isNatList# activate L, isNat# n__length L -> activate# L, take#(0(), IL) -> isNatIList# IL, take#(s M, cons(N, IL)) -> activate# IL, take#(s M, cons(N, IL)) -> isNatIList# activate IL, take#(s M, cons(N, IL)) -> isNat# N, take#(s M, cons(N, IL)) -> isNat# M, take#(s M, cons(N, IL)) -> uTake2#(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), uTake2#(tt(), M, N, IL) -> activate# IL, uTake2#(tt(), M, N, IL) -> activate# N, uTake2#(tt(), M, N, IL) -> activate# M, uLength#(tt(), L) -> activate# L, uLength#(tt(), L) -> length# activate L, length# cons(N, L) -> isNatList# activate L, length# cons(N, L) -> activate# L, length# cons(N, L) -> isNat# N, length# cons(N, L) -> uLength#(and(isNat N, isNatList activate L), activate L)} Weak: { and(tt(), T) -> T, isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L), isNatList n__nil() -> tt(), isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__length X -> length activate X, activate n__zeros() -> zeros(), activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__nil() -> nil(), activate n__take(X1, X2) -> take(activate X1, activate X2), isNatIList IL -> isNatList activate IL, isNatIList n__zeros() -> tt(), isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL), isNat n__0() -> tt(), isNat n__s N -> isNat activate N, isNat n__length L -> isNatList activate L, cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1 tt() -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1 isNatIList IL, take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)), s X -> n__s X, uLength(tt(), L) -> s length activate L, length X -> n__length X, length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [uTake2](x0, x1, x2, x3) = x0 + x1 + x2, [and](x0, x1) = 1, [n__cons](x0, x1) = x0 + x1, [n__take](x0, x1) = x0 + x1, [cons](x0, x1) = x0 + x1, [take](x0, x1) = x0 + x1, [uLength](x0, x1) = x0 + 1, [isNatList](x0) = 0, [activate](x0) = x0, [isNatIList](x0) = 0, [isNat](x0) = 0, [n__s](x0) = x0, [n__length](x0) = x0 + 1, [uTake1](x0) = 0, [s](x0) = x0, [length](x0) = x0 + 1, [tt] = 0, [n__0] = 0, [n__zeros] = 0, [n__nil] = 0, [0] = 0, [zeros] = 0, [nil] = 0, [uTake2#](x0, x1, x2, x3) = x0 + x1 + x2, [take#](x0, x1) = x0 + x1, [uLength#](x0, x1) = x0, [isNatList#](x0) = x0, [activate#](x0) = x0, [isNatIList#](x0) = x0, [isNat#](x0) = x0, [length#](x0) = x0 Strict: length# cons(N, L) -> uLength#(and(isNat N, isNatList activate L), activate L) 0 + 1N + 1L >= 0 + 0N + 1L length# cons(N, L) -> isNat# N 0 + 1N + 1L >= 0 + 1N length# cons(N, L) -> activate# L 0 + 1N + 1L >= 0 + 1L length# cons(N, L) -> isNatList# activate L 0 + 1N + 1L >= 0 + 1L uLength#(tt(), L) -> length# activate L 0 + 1L >= 0 + 1L uLength#(tt(), L) -> activate# L 0 + 1L >= 0 + 1L uTake2#(tt(), M, N, IL) -> activate# M 0 + 1IL + 1N + 1M >= 0 + 1M uTake2#(tt(), M, N, IL) -> activate# N 0 + 1IL + 1N + 1M >= 0 + 1N uTake2#(tt(), M, N, IL) -> activate# IL 0 + 1IL + 1N + 1M >= 0 + 1IL take#(s M, cons(N, IL)) -> uTake2#(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL) 0 + 1IL + 1N + 1M >= 0 + 1IL + 1N + 1M take#(s M, cons(N, IL)) -> isNat# M 0 + 1IL + 1N + 1M >= 0 + 1M take#(s M, cons(N, IL)) -> isNat# N 0 + 1IL + 1N + 1M >= 0 + 1N take#(s M, cons(N, IL)) -> isNatIList# activate IL 0 + 1IL + 1N + 1M >= 0 + 1IL take#(s M, cons(N, IL)) -> activate# IL 0 + 1IL + 1N + 1M >= 0 + 1IL take#(0(), IL) -> isNatIList# IL 0 + 1IL >= 0 + 1IL isNat# n__length L -> activate# L 1 + 1L >= 0 + 1L isNat# n__length L -> isNatList# activate L 1 + 1L >= 0 + 1L isNat# n__s N -> isNat# activate N 0 + 1N >= 0 + 1N isNat# n__s N -> activate# N 0 + 1N >= 0 + 1N isNatIList# n__cons(N, IL) -> isNat# activate N 0 + 1IL + 1N >= 0 + 1N isNatIList# n__cons(N, IL) -> isNatIList# activate IL 0 + 1IL + 1N >= 0 + 1IL isNatIList# n__cons(N, IL) -> activate# N 0 + 1IL + 1N >= 0 + 1N isNatIList# n__cons(N, IL) -> activate# IL 0 + 1IL + 1N >= 0 + 1IL isNatIList# IL -> activate# IL 0 + 1IL >= 0 + 1IL isNatIList# IL -> isNatList# activate IL 0 + 1IL >= 0 + 1IL activate# n__take(X1, X2) -> take#(activate X1, activate X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate# n__take(X1, X2) -> activate# X2 0 + 1X1 + 1X2 >= 0 + 1X2 activate# n__take(X1, X2) -> activate# X1 0 + 1X1 + 1X2 >= 0 + 1X1 activate# n__cons(X1, X2) -> activate# X1 0 + 1X1 + 1X2 >= 0 + 1X1 activate# n__length X -> length# activate X 1 + 1X >= 0 + 1X activate# n__length X -> activate# X 1 + 1X >= 0 + 1X activate# n__s X -> activate# X 0 + 1X >= 0 + 1X isNatList# n__take(N, IL) -> isNat# activate N 0 + 1IL + 1N >= 0 + 1N isNatList# n__take(N, IL) -> isNatIList# activate IL 0 + 1IL + 1N >= 0 + 1IL isNatList# n__take(N, IL) -> activate# N 0 + 1IL + 1N >= 0 + 1N isNatList# n__take(N, IL) -> activate# IL 0 + 1IL + 1N >= 0 + 1IL isNatList# n__cons(N, L) -> isNat# activate N 0 + 1N + 1L >= 0 + 1N isNatList# n__cons(N, L) -> activate# L 0 + 1N + 1L >= 0 + 1L isNatList# n__cons(N, L) -> activate# N 0 + 1N + 1L >= 0 + 1N isNatList# n__cons(N, L) -> isNatList# activate L 0 + 1N + 1L >= 0 + 1L Weak: length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L) 1 + 1N + 1L >= 1 + 0N + 1L length X -> n__length X 1 + 1X >= 1 + 1X uLength(tt(), L) -> s length activate L 1 + 1L >= 1 + 1L s X -> n__s X 0 + 1X >= 0 + 1X uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)) 0 + 1IL + 1N + 1M >= 0 + 1IL + 1N + 1M nil() -> n__nil() 0 >= 0 take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL) 0 + 1IL + 1N + 1M >= 0 + 1IL + 1N + 1M take(0(), IL) -> uTake1 isNatIList IL 0 + 1IL >= 0 + 0IL take(X1, X2) -> n__take(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 uTake1 tt() -> nil() 0 >= 0 zeros() -> cons(0(), n__zeros()) 0 >= 0 zeros() -> n__zeros() 0 >= 0 0() -> n__0() 0 >= 0 cons(X1, X2) -> n__cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 isNat n__length L -> isNatList activate L 0 + 0L >= 0 + 0L isNat n__s N -> isNat activate N 0 + 0N >= 0 + 0N isNat n__0() -> tt() 0 >= 0 isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL) 0 + 0IL + 0N >= 1 + 0IL + 0N isNatIList n__zeros() -> tt() 0 >= 0 isNatIList IL -> isNatList activate IL 0 + 0IL >= 0 + 0IL activate n__take(X1, X2) -> take(activate X1, activate X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__nil() -> nil() 0 >= 0 activate n__cons(X1, X2) -> cons(activate X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__zeros() -> zeros() 0 >= 0 activate n__length X -> length activate X 1 + 1X >= 1 + 1X activate n__s X -> s activate X 0 + 1X >= 0 + 1X activate n__0() -> 0() 0 >= 0 activate X -> X 0 + 1X >= 1X isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL) 0 + 0IL + 0N >= 1 + 0IL + 0N isNatList n__nil() -> tt() 0 >= 0 isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L) 0 + 0N + 0L >= 1 + 0N + 0L and(tt(), T) -> T 1 + 0T >= 1T SCCS (2): Scc: { uLength#(tt(), L) -> length# activate L, length# cons(N, L) -> uLength#(and(isNat N, isNatList activate L), activate L)} Scc: { isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> activate# N, isNatList# n__cons(N, L) -> activate# L, isNatList# n__cons(N, L) -> isNat# activate N, isNatList# n__take(N, IL) -> activate# IL, isNatList# n__take(N, IL) -> activate# N, isNatList# n__take(N, IL) -> isNatIList# activate IL, isNatList# n__take(N, IL) -> isNat# activate N, activate# n__s X -> activate# X, activate# n__cons(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> take#(activate X1, activate X2), isNatIList# IL -> isNatList# activate IL, isNatIList# IL -> activate# IL, isNatIList# n__cons(N, IL) -> activate# IL, isNatIList# n__cons(N, IL) -> activate# N, isNatIList# n__cons(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> isNat# activate N, isNat# n__s N -> activate# N, isNat# n__s N -> isNat# activate N, take#(0(), IL) -> isNatIList# IL, take#(s M, cons(N, IL)) -> activate# IL, take#(s M, cons(N, IL)) -> isNatIList# activate IL, take#(s M, cons(N, IL)) -> isNat# N, take#(s M, cons(N, IL)) -> isNat# M, take#(s M, cons(N, IL)) -> uTake2#(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), uTake2#(tt(), M, N, IL) -> activate# IL, uTake2#(tt(), M, N, IL) -> activate# N, uTake2#(tt(), M, N, IL) -> activate# M} SCC (2): Strict: { uLength#(tt(), L) -> length# activate L, length# cons(N, L) -> uLength#(and(isNat N, isNatList activate L), activate L)} Weak: { and(tt(), T) -> T, isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L), isNatList n__nil() -> tt(), isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__length X -> length activate X, activate n__zeros() -> zeros(), activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__nil() -> nil(), activate n__take(X1, X2) -> take(activate X1, activate X2), isNatIList IL -> isNatList activate IL, isNatIList n__zeros() -> tt(), isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL), isNat n__0() -> tt(), isNat n__s N -> isNat activate N, isNat n__length L -> isNatList activate L, cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1 tt() -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1 isNatIList IL, take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)), s X -> n__s X, uLength(tt(), L) -> s length activate L, length X -> n__length X, length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L)} Fail SCC (30): Strict: { isNatList# n__cons(N, L) -> isNatList# activate L, isNatList# n__cons(N, L) -> activate# N, isNatList# n__cons(N, L) -> activate# L, isNatList# n__cons(N, L) -> isNat# activate N, isNatList# n__take(N, IL) -> activate# IL, isNatList# n__take(N, IL) -> activate# N, isNatList# n__take(N, IL) -> isNatIList# activate IL, isNatList# n__take(N, IL) -> isNat# activate N, activate# n__s X -> activate# X, activate# n__cons(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X1, activate# n__take(X1, X2) -> activate# X2, activate# n__take(X1, X2) -> take#(activate X1, activate X2), isNatIList# IL -> isNatList# activate IL, isNatIList# IL -> activate# IL, isNatIList# n__cons(N, IL) -> activate# IL, isNatIList# n__cons(N, IL) -> activate# N, isNatIList# n__cons(N, IL) -> isNatIList# activate IL, isNatIList# n__cons(N, IL) -> isNat# activate N, isNat# n__s N -> activate# N, isNat# n__s N -> isNat# activate N, take#(0(), IL) -> isNatIList# IL, take#(s M, cons(N, IL)) -> activate# IL, take#(s M, cons(N, IL)) -> isNatIList# activate IL, take#(s M, cons(N, IL)) -> isNat# N, take#(s M, cons(N, IL)) -> isNat# M, take#(s M, cons(N, IL)) -> uTake2#(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), uTake2#(tt(), M, N, IL) -> activate# IL, uTake2#(tt(), M, N, IL) -> activate# N, uTake2#(tt(), M, N, IL) -> activate# M} Weak: { and(tt(), T) -> T, isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L), isNatList n__nil() -> tt(), isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__length X -> length activate X, activate n__zeros() -> zeros(), activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__nil() -> nil(), activate n__take(X1, X2) -> take(activate X1, activate X2), isNatIList IL -> isNatList activate IL, isNatIList n__zeros() -> tt(), isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL), isNat n__0() -> tt(), isNat n__s N -> isNat activate N, isNat n__length L -> isNatList activate L, cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1 tt() -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1 isNatIList IL, take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)), s X -> n__s X, uLength(tt(), L) -> s length activate L, length X -> n__length X, length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [uTake2](x0, x1, x2, x3) = x0 + x1 + x2 + 1, [and](x0, x1) = 0, [n__cons](x0, x1) = x0 + x1, [n__take](x0, x1) = x0 + x1 + 1, [cons](x0, x1) = x0 + x1, [take](x0, x1) = x0 + x1 + 1, [uLength](x0, x1) = 0, [isNatList](x0) = x0, [activate](x0) = x0, [isNatIList](x0) = 0, [isNat](x0) = 0, [n__s](x0) = x0, [n__length](x0) = 0, [uTake1](x0) = 0, [s](x0) = x0, [length](x0) = 0, [tt] = 0, [n__0] = 0, [n__zeros] = 0, [n__nil] = 0, [0] = 0, [zeros] = 0, [nil] = 0, [uTake2#](x0, x1, x2, x3) = x0 + x1 + x2 + 1, [take#](x0, x1) = x0 + x1 + 1, [isNatList#](x0) = x0 + 1, [activate#](x0) = x0 + 1, [isNatIList#](x0) = x0 + 1, [isNat#](x0) = x0 + 1 Strict: uTake2#(tt(), M, N, IL) -> activate# M 1 + 1IL + 1N + 1M >= 1 + 1M uTake2#(tt(), M, N, IL) -> activate# N 1 + 1IL + 1N + 1M >= 1 + 1N uTake2#(tt(), M, N, IL) -> activate# IL 1 + 1IL + 1N + 1M >= 1 + 1IL take#(s M, cons(N, IL)) -> uTake2#(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL) 1 + 1IL + 1N + 1M >= 1 + 1IL + 1N + 1M take#(s M, cons(N, IL)) -> isNat# M 1 + 1IL + 1N + 1M >= 1 + 1M take#(s M, cons(N, IL)) -> isNat# N 1 + 1IL + 1N + 1M >= 1 + 1N take#(s M, cons(N, IL)) -> isNatIList# activate IL 1 + 1IL + 1N + 1M >= 1 + 1IL take#(s M, cons(N, IL)) -> activate# IL 1 + 1IL + 1N + 1M >= 1 + 1IL take#(0(), IL) -> isNatIList# IL 1 + 1IL >= 1 + 1IL isNat# n__s N -> isNat# activate N 1 + 1N >= 1 + 1N isNat# n__s N -> activate# N 1 + 1N >= 1 + 1N isNatIList# n__cons(N, IL) -> isNat# activate N 1 + 1IL + 1N >= 1 + 1N isNatIList# n__cons(N, IL) -> isNatIList# activate IL 1 + 1IL + 1N >= 1 + 1IL isNatIList# n__cons(N, IL) -> activate# N 1 + 1IL + 1N >= 1 + 1N isNatIList# n__cons(N, IL) -> activate# IL 1 + 1IL + 1N >= 1 + 1IL isNatIList# IL -> activate# IL 1 + 1IL >= 1 + 1IL isNatIList# IL -> isNatList# activate IL 1 + 1IL >= 1 + 1IL activate# n__take(X1, X2) -> take#(activate X1, activate X2) 2 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 activate# n__take(X1, X2) -> activate# X2 2 + 1X1 + 1X2 >= 1 + 1X2 activate# n__take(X1, X2) -> activate# X1 2 + 1X1 + 1X2 >= 1 + 1X1 activate# n__cons(X1, X2) -> activate# X1 1 + 1X1 + 1X2 >= 1 + 1X1 activate# n__s X -> activate# X 1 + 1X >= 1 + 1X isNatList# n__take(N, IL) -> isNat# activate N 2 + 1IL + 1N >= 1 + 1N isNatList# n__take(N, IL) -> isNatIList# activate IL 2 + 1IL + 1N >= 1 + 1IL isNatList# n__take(N, IL) -> activate# N 2 + 1IL + 1N >= 1 + 1N isNatList# n__take(N, IL) -> activate# IL 2 + 1IL + 1N >= 1 + 1IL isNatList# n__cons(N, L) -> isNat# activate N 1 + 1N + 1L >= 1 + 1N isNatList# n__cons(N, L) -> activate# L 1 + 1N + 1L >= 1 + 1L isNatList# n__cons(N, L) -> activate# N 1 + 1N + 1L >= 1 + 1N isNatList# n__cons(N, L) -> isNatList# activate L 1 + 1N + 1L >= 1 + 1L Weak: length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L) 0 + 0N + 0L >= 0 + 0N + 0L length X -> n__length X 0 + 0X >= 0 + 0X uLength(tt(), L) -> s length activate L 0 + 0L >= 0 + 0L s X -> n__s X 0 + 1X >= 0 + 1X uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)) 1 + 1IL + 1N + 1M >= 1 + 1IL + 1N + 1M nil() -> n__nil() 0 >= 0 take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL) 1 + 1IL + 1N + 1M >= 1 + 1IL + 1N + 1M take(0(), IL) -> uTake1 isNatIList IL 1 + 1IL >= 0 + 0IL take(X1, X2) -> n__take(X1, X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 uTake1 tt() -> nil() 0 >= 0 zeros() -> cons(0(), n__zeros()) 0 >= 0 zeros() -> n__zeros() 0 >= 0 0() -> n__0() 0 >= 0 cons(X1, X2) -> n__cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 isNat n__length L -> isNatList activate L 0 + 0L >= 0 + 1L isNat n__s N -> isNat activate N 0 + 0N >= 0 + 0N isNat n__0() -> tt() 0 >= 0 isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL) 0 + 0IL + 0N >= 0 + 0IL + 0N isNatIList n__zeros() -> tt() 0 >= 0 isNatIList IL -> isNatList activate IL 0 + 0IL >= 0 + 1IL activate n__take(X1, X2) -> take(activate X1, activate X2) 1 + 1X1 + 1X2 >= 1 + 1X1 + 1X2 activate n__nil() -> nil() 0 >= 0 activate n__cons(X1, X2) -> cons(activate X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__zeros() -> zeros() 0 >= 0 activate n__length X -> length activate X 0 + 0X >= 0 + 0X activate n__s X -> s activate X 0 + 1X >= 0 + 1X activate n__0() -> 0() 0 >= 0 activate X -> X 0 + 1X >= 1X isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL) 1 + 1IL + 1N >= 0 + 0IL + 0N isNatList n__nil() -> tt() 0 >= 0 isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L) 0 + 1N + 1L >= 0 + 0N + 0L and(tt(), T) -> T 0 + 0T >= 1T SCCS (4): Scc: {isNatIList# n__cons(N, IL) -> isNatIList# activate IL} Scc: {isNatList# n__cons(N, L) -> isNatList# activate L} Scc: {isNat# n__s N -> isNat# activate N} Scc: { activate# n__s X -> activate# X, activate# n__cons(X1, X2) -> activate# X1} SCC (1): Strict: {isNatIList# n__cons(N, IL) -> isNatIList# activate IL} Weak: { and(tt(), T) -> T, isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L), isNatList n__nil() -> tt(), isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__length X -> length activate X, activate n__zeros() -> zeros(), activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__nil() -> nil(), activate n__take(X1, X2) -> take(activate X1, activate X2), isNatIList IL -> isNatList activate IL, isNatIList n__zeros() -> tt(), isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL), isNat n__0() -> tt(), isNat n__s N -> isNat activate N, isNat n__length L -> isNatList activate L, cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1 tt() -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1 isNatIList IL, take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)), s X -> n__s X, uLength(tt(), L) -> s length activate L, length X -> n__length X, length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L)} Fail SCC (1): Strict: {isNatList# n__cons(N, L) -> isNatList# activate L} Weak: { and(tt(), T) -> T, isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L), isNatList n__nil() -> tt(), isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__length X -> length activate X, activate n__zeros() -> zeros(), activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__nil() -> nil(), activate n__take(X1, X2) -> take(activate X1, activate X2), isNatIList IL -> isNatList activate IL, isNatIList n__zeros() -> tt(), isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL), isNat n__0() -> tt(), isNat n__s N -> isNat activate N, isNat n__length L -> isNatList activate L, cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1 tt() -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1 isNatIList IL, take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)), s X -> n__s X, uLength(tt(), L) -> s length activate L, length X -> n__length X, length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L)} Fail SCC (1): Strict: {isNat# n__s N -> isNat# activate N} Weak: { and(tt(), T) -> T, isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L), isNatList n__nil() -> tt(), isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__length X -> length activate X, activate n__zeros() -> zeros(), activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__nil() -> nil(), activate n__take(X1, X2) -> take(activate X1, activate X2), isNatIList IL -> isNatList activate IL, isNatIList n__zeros() -> tt(), isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL), isNat n__0() -> tt(), isNat n__s N -> isNat activate N, isNat n__length L -> isNatList activate L, cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1 tt() -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1 isNatIList IL, take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)), s X -> n__s X, uLength(tt(), L) -> s length activate L, length X -> n__length X, length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L)} Fail SCC (2): Strict: { activate# n__s X -> activate# X, activate# n__cons(X1, X2) -> activate# X1} Weak: { and(tt(), T) -> T, isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L), isNatList n__nil() -> tt(), isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__length X -> length activate X, activate n__zeros() -> zeros(), activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__nil() -> nil(), activate n__take(X1, X2) -> take(activate X1, activate X2), isNatIList IL -> isNatList activate IL, isNatIList n__zeros() -> tt(), isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL), isNat n__0() -> tt(), isNat n__s N -> isNat activate N, isNat n__length L -> isNatList activate L, cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1 tt() -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1 isNatIList IL, take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)), s X -> n__s X, uLength(tt(), L) -> s length activate L, length X -> n__length X, length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [uTake2](x0, x1, x2, x3) = x0 + 1, [and](x0, x1) = x0 + 1, [n__cons](x0, x1) = x0 + 1, [n__take](x0, x1) = 1, [cons](x0, x1) = 0, [take](x0, x1) = 0, [uLength](x0, x1) = x0 + 1, [isNatList](x0) = x0 + 1, [activate](x0) = x0 + 1, [isNatIList](x0) = x0 + 1, [isNat](x0) = 0, [n__s](x0) = x0, [n__length](x0) = 1, [uTake1](x0) = x0 + 1, [s](x0) = x0 + 1, [length](x0) = 0, [tt] = 1, [n__0] = 1, [n__zeros] = 1, [n__nil] = 1, [0] = 0, [zeros] = 0, [nil] = 0, [activate#](x0) = x0 Strict: activate# n__cons(X1, X2) -> activate# X1 1 + 1X1 + 0X2 >= 0 + 1X1 activate# n__s X -> activate# X 0 + 1X >= 0 + 1X Weak: length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L) 0 + 0N + 0L >= 2 + 0N + 0L length X -> n__length X 0 + 0X >= 1 + 0X uLength(tt(), L) -> s length activate L 2 + 0L >= 1 + 0L s X -> n__s X 1 + 1X >= 0 + 1X uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)) 2 + 0IL + 0N + 0M >= 0 + 0IL + 0N + 0M nil() -> n__nil() 0 >= 1 take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL) 0 + 0IL + 0N + 0M >= 2 + 0IL + 0N + 0M take(0(), IL) -> uTake1 isNatIList IL 0 + 0IL >= 2 + 1IL take(X1, X2) -> n__take(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 uTake1 tt() -> nil() 2 >= 0 zeros() -> cons(0(), n__zeros()) 0 >= 0 zeros() -> n__zeros() 0 >= 1 0() -> n__0() 0 >= 1 cons(X1, X2) -> n__cons(X1, X2) 0 + 0X1 + 0X2 >= 1 + 1X1 + 0X2 isNat n__length L -> isNatList activate L 0 + 0L >= 2 + 1L isNat n__s N -> isNat activate N 0 + 0N >= 0 + 0N isNat n__0() -> tt() 0 >= 1 isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL) 2 + 0IL + 1N >= 1 + 0IL + 0N isNatIList n__zeros() -> tt() 2 >= 1 isNatIList IL -> isNatList activate IL 1 + 1IL >= 2 + 1IL activate n__take(X1, X2) -> take(activate X1, activate X2) 2 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__nil() -> nil() 2 >= 0 activate n__cons(X1, X2) -> cons(activate X1, X2) 2 + 1X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__zeros() -> zeros() 2 >= 0 activate n__length X -> length activate X 2 + 0X >= 0 + 0X activate n__s X -> s activate X 1 + 1X >= 2 + 1X activate n__0() -> 0() 2 >= 0 activate X -> X 1 + 1X >= 1X isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL) 2 + 0IL + 0N >= 1 + 0IL + 0N isNatList n__nil() -> tt() 2 >= 1 isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L) 2 + 1N + 0L >= 1 + 0N + 0L and(tt(), T) -> T 2 + 0T >= 1T SCCS (1): Scc: {activate# n__s X -> activate# X} SCC (1): Strict: {activate# n__s X -> activate# X} Weak: { and(tt(), T) -> T, isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L), isNatList n__nil() -> tt(), isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL), activate X -> X, activate n__0() -> 0(), activate n__s X -> s activate X, activate n__length X -> length activate X, activate n__zeros() -> zeros(), activate n__cons(X1, X2) -> cons(activate X1, X2), activate n__nil() -> nil(), activate n__take(X1, X2) -> take(activate X1, activate X2), isNatIList IL -> isNatList activate IL, isNatIList n__zeros() -> tt(), isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL), isNat n__0() -> tt(), isNat n__s N -> isNat activate N, isNat n__length L -> isNatList activate L, cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> n__zeros(), zeros() -> cons(0(), n__zeros()), uTake1 tt() -> nil(), take(X1, X2) -> n__take(X1, X2), take(0(), IL) -> uTake1 isNatIList IL, take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL), nil() -> n__nil(), uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)), s X -> n__s X, uLength(tt(), L) -> s length activate L, length X -> n__length X, length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [uTake2](x0, x1, x2, x3) = x0 + 1, [and](x0, x1) = x0 + 1, [n__cons](x0, x1) = 1, [n__take](x0, x1) = 1, [cons](x0, x1) = 0, [take](x0, x1) = 0, [uLength](x0, x1) = x0 + 1, [isNatList](x0) = x0 + 1, [activate](x0) = 1, [isNatIList](x0) = x0 + 1, [isNat](x0) = 0, [n__s](x0) = x0 + 1, [n__length](x0) = 0, [uTake1](x0) = x0 + 1, [s](x0) = x0 + 1, [length](x0) = 0, [tt] = 1, [n__0] = 0, [n__zeros] = 1, [n__nil] = 1, [0] = 0, [zeros] = 0, [nil] = 0, [activate#](x0) = x0 Strict: activate# n__s X -> activate# X 1 + 1X >= 0 + 1X Weak: length cons(N, L) -> uLength(and(isNat N, isNatList activate L), activate L) 0 + 0N + 0L >= 2 + 0N + 0L length X -> n__length X 0 + 0X >= 0 + 0X uLength(tt(), L) -> s length activate L 2 + 0L >= 1 + 0L s X -> n__s X 1 + 1X >= 1 + 1X uTake2(tt(), M, N, IL) -> cons(activate N, n__take(activate M, activate IL)) 2 + 0IL + 0N + 0M >= 0 + 0IL + 0N + 0M nil() -> n__nil() 0 >= 1 take(s M, cons(N, IL)) -> uTake2(and(isNat M, and(isNat N, isNatIList activate IL)), M, N, activate IL) 0 + 0IL + 0N + 0M >= 2 + 0IL + 0N + 0M take(0(), IL) -> uTake1 isNatIList IL 0 + 0IL >= 2 + 1IL take(X1, X2) -> n__take(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 uTake1 tt() -> nil() 2 >= 0 zeros() -> cons(0(), n__zeros()) 0 >= 0 zeros() -> n__zeros() 0 >= 1 0() -> n__0() 0 >= 0 cons(X1, X2) -> n__cons(X1, X2) 0 + 0X1 + 0X2 >= 1 + 0X1 + 0X2 isNat n__length L -> isNatList activate L 0 + 0L >= 2 + 0L isNat n__s N -> isNat activate N 0 + 0N >= 0 + 0N isNat n__0() -> tt() 0 >= 1 isNatIList n__cons(N, IL) -> and(isNat activate N, isNatIList activate IL) 2 + 0IL + 0N >= 1 + 0IL + 0N isNatIList n__zeros() -> tt() 2 >= 1 isNatIList IL -> isNatList activate IL 1 + 1IL >= 2 + 0IL activate n__take(X1, X2) -> take(activate X1, activate X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__nil() -> nil() 1 >= 0 activate n__cons(X1, X2) -> cons(activate X1, X2) 1 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__zeros() -> zeros() 1 >= 0 activate n__length X -> length activate X 1 + 0X >= 0 + 0X activate n__s X -> s activate X 1 + 0X >= 2 + 0X activate n__0() -> 0() 1 >= 0 activate X -> X 1 + 0X >= 1X isNatList n__take(N, IL) -> and(isNat activate N, isNatIList activate IL) 2 + 0IL + 0N >= 1 + 0IL + 0N isNatList n__nil() -> tt() 2 >= 1 isNatList n__cons(N, L) -> and(isNat activate N, isNatList activate L) 2 + 0N + 0L >= 1 + 0N + 0L and(tt(), T) -> T 2 + 0T >= 1T Qed