MAYBE Time: 30.715679 TRS: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L), length nil() -> 0(), activate X -> X, activate n__zeros() -> zeros(), activate n__0() -> 0(), activate n__length X -> length X, activate n__s X -> s X, activate n__isNatIList X -> isNatIList X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__isNatList X -> isNatList X, activate n__isNat X -> isNat X, U11(tt(), L) -> s length activate L, and(tt(), X) -> activate X, isNat X -> n__isNat X, isNat n__0() -> tt(), isNat n__length V1 -> isNatList activate V1, isNat n__s V1 -> isNat activate V1, isNatList X -> n__isNatList X, isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2), isNatList n__nil() -> tt(), isNatIList X -> n__isNatIList X, isNatIList V -> isNatList activate V, isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2), nil() -> n__nil()} DP: DP: { zeros#() -> cons#(0(), n__zeros()), zeros#() -> 0#(), length# cons(N, L) -> activate# L, length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L), length# cons(N, L) -> and#(isNatList activate L, n__isNat N), length# cons(N, L) -> isNatList# activate L, length# nil() -> 0#(), activate# n__zeros() -> zeros#(), activate# n__0() -> 0#(), activate# n__length X -> length# X, activate# n__s X -> s# X, activate# n__isNatIList X -> isNatIList# X, activate# n__cons(X1, X2) -> cons#(X1, X2), activate# n__nil() -> nil#(), activate# n__isNatList X -> isNatList# X, activate# n__isNat X -> isNat# X, U11#(tt(), L) -> s# length activate L, U11#(tt(), L) -> length# activate L, U11#(tt(), L) -> activate# L, and#(tt(), X) -> activate# X, 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, isNatList# n__cons(V1, V2) -> activate# V1, isNatList# n__cons(V1, V2) -> activate# V2, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2), isNatList# n__cons(V1, V2) -> isNat# activate V1, isNatIList# V -> activate# V, isNatIList# V -> isNatList# activate V, isNatIList# n__cons(V1, V2) -> activate# V1, isNatIList# n__cons(V1, V2) -> activate# V2, isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2), isNatIList# n__cons(V1, V2) -> isNat# activate V1} TRS: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L), length nil() -> 0(), activate X -> X, activate n__zeros() -> zeros(), activate n__0() -> 0(), activate n__length X -> length X, activate n__s X -> s X, activate n__isNatIList X -> isNatIList X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__isNatList X -> isNatList X, activate n__isNat X -> isNat X, U11(tt(), L) -> s length activate L, and(tt(), X) -> activate X, isNat X -> n__isNat X, isNat n__0() -> tt(), isNat n__length V1 -> isNatList activate V1, isNat n__s V1 -> isNat activate V1, isNatList X -> n__isNatList X, isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2), isNatList n__nil() -> tt(), isNatIList X -> n__isNatIList X, isNatIList V -> isNatList activate V, isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2), nil() -> n__nil()} UR: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L), length nil() -> 0(), activate X -> X, activate n__zeros() -> zeros(), activate n__0() -> 0(), activate n__length X -> length X, activate n__s X -> s X, activate n__isNatIList X -> isNatIList X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__isNatList X -> isNatList X, activate n__isNat X -> isNat X, U11(tt(), L) -> s length activate L, and(tt(), X) -> activate X, isNat X -> n__isNat X, isNat n__0() -> tt(), isNat n__length V1 -> isNatList activate V1, isNat n__s V1 -> isNat activate V1, isNatList X -> n__isNatList X, isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2), isNatList n__nil() -> tt(), isNatIList X -> n__isNatIList X, isNatIList V -> isNatList activate V, isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2), nil() -> n__nil(), a(x, y) -> x, a(x, y) -> y} EDG: { (length# cons(N, L) -> and#(isNatList activate L, n__isNat N), and#(tt(), X) -> activate# X) (isNat# n__length V1 -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> isNat# activate V1) (isNat# n__length V1 -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2)) (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) (isNatList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNat# activate V1) (isNatList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1) (isNatList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatList# activate V1) (isNatList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1) (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> isNat# activate V1) (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2)) (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) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__isNatList X -> isNatList# X) (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__isNatIList X -> isNatIList# X) (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__zeros() -> zeros#()) (isNat# n__length V1 -> activate# V1, activate# n__isNat X -> isNat# X) (isNat# n__length V1 -> activate# V1, activate# n__isNatList X -> isNatList# X) (isNat# n__length V1 -> activate# V1, activate# n__nil() -> nil#()) (isNat# n__length V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNat# n__length V1 -> activate# V1, activate# n__isNatIList X -> isNatIList# X) (isNat# n__length V1 -> activate# V1, activate# n__s X -> s# X) (isNat# n__length V1 -> activate# V1, activate# n__length X -> length# X) (isNat# n__length V1 -> activate# V1, activate# n__0() -> 0#()) (isNat# n__length V1 -> activate# V1, activate# n__zeros() -> zeros#()) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__isNatList X -> isNatList# X) (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__isNatIList X -> isNatIList# X) (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__zeros() -> zeros#()) (length# cons(N, L) -> activate# L, activate# n__isNat X -> isNat# X) (length# cons(N, L) -> activate# L, activate# n__isNatList X -> isNatList# X) (length# cons(N, L) -> activate# L, activate# n__nil() -> nil#()) (length# cons(N, L) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2)) (length# cons(N, L) -> activate# L, activate# n__isNatIList X -> isNatIList# X) (length# cons(N, L) -> activate# L, activate# n__s X -> s# X) (length# cons(N, L) -> activate# L, activate# n__length X -> length# X) (length# cons(N, L) -> activate# L, activate# n__0() -> 0#()) (length# cons(N, L) -> 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) -> isNatList# activate L) (activate# n__length X -> length# X, length# cons(N, L) -> and#(isNatList activate L, n__isNat N)) (activate# n__length X -> length# X, length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L)) (activate# n__length X -> length# X, length# cons(N, L) -> activate# L) (activate# n__isNatIList X -> isNatIList# X, isNatIList# n__cons(V1, V2) -> isNat# activate V1) (activate# n__isNatIList X -> isNatIList# X, isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2)) (activate# n__isNatIList X -> isNatIList# X, isNatIList# n__cons(V1, V2) -> activate# V2) (activate# n__isNatIList X -> isNatIList# X, isNatIList# n__cons(V1, V2) -> activate# V1) (activate# n__isNatIList X -> isNatIList# X, isNatIList# V -> isNatList# activate V) (activate# n__isNatIList X -> isNatIList# X, isNatIList# V -> activate# V) (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> isNat# activate V1) (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> activate# V1) (activate# n__isNat X -> isNat# X, isNat# n__length V1 -> isNatList# activate V1) (activate# n__isNat X -> isNat# X, isNat# n__length V1 -> activate# V1) (isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2), and#(tt(), X) -> activate# X) (activate# n__zeros() -> zeros#(), zeros#() -> 0#()) (activate# n__zeros() -> zeros#(), zeros#() -> cons#(0(), n__zeros())) (isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2), and#(tt(), X) -> activate# X) (and#(tt(), X) -> activate# X, activate# n__zeros() -> zeros#()) (and#(tt(), X) -> activate# X, activate# n__0() -> 0#()) (and#(tt(), X) -> activate# X, activate# n__length X -> length# X) (and#(tt(), X) -> activate# X, activate# n__s X -> s# X) (and#(tt(), X) -> activate# X, activate# n__isNatIList X -> isNatIList# X) (and#(tt(), X) -> activate# X, activate# n__cons(X1, X2) -> cons#(X1, X2)) (and#(tt(), X) -> activate# X, activate# n__nil() -> nil#()) (and#(tt(), X) -> activate# X, activate# n__isNatList X -> isNatList# X) (and#(tt(), X) -> activate# X, activate# n__isNat X -> isNat# X) (activate# n__isNatList X -> isNatList# X, isNatList# n__cons(V1, V2) -> activate# V1) (activate# n__isNatList X -> isNatList# X, isNatList# n__cons(V1, V2) -> activate# V2) (activate# n__isNatList X -> isNatList# X, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2)) (activate# n__isNatList X -> isNatList# X, isNatList# n__cons(V1, V2) -> isNat# activate V1) (isNatIList# V -> activate# V, activate# n__zeros() -> zeros#()) (isNatIList# V -> activate# V, activate# n__0() -> 0#()) (isNatIList# V -> activate# V, activate# n__length X -> length# X) (isNatIList# V -> activate# V, activate# n__s X -> s# X) (isNatIList# V -> activate# V, activate# n__isNatIList X -> isNatIList# X) (isNatIList# V -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatIList# V -> activate# V, activate# n__nil() -> nil#()) (isNatIList# V -> activate# V, activate# n__isNatList X -> isNatList# X) (isNatIList# V -> activate# V, activate# n__isNat X -> isNat# X) (U11#(tt(), L) -> activate# L, activate# n__zeros() -> zeros#()) (U11#(tt(), L) -> activate# L, activate# n__0() -> 0#()) (U11#(tt(), L) -> activate# L, activate# n__length X -> length# X) (U11#(tt(), L) -> activate# L, activate# n__s X -> s# X) (U11#(tt(), L) -> activate# L, activate# n__isNatIList X -> isNatIList# X) (U11#(tt(), L) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U11#(tt(), L) -> activate# L, activate# n__nil() -> nil#()) (U11#(tt(), L) -> activate# L, activate# n__isNatList X -> isNatList# X) (U11#(tt(), L) -> activate# L, activate# n__isNat X -> isNat# X) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#()) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__isNatIList X -> isNatIList# X) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#()) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__isNatList X -> isNatList# X) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X) (isNat# n__s V1 -> activate# V1, activate# n__zeros() -> zeros#()) (isNat# n__s V1 -> activate# V1, activate# n__0() -> 0#()) (isNat# n__s V1 -> activate# V1, activate# n__length X -> length# X) (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# X) (isNat# n__s V1 -> activate# V1, activate# n__isNatIList X -> isNatIList# X) (isNat# n__s V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNat# n__s V1 -> activate# V1, activate# n__nil() -> nil#()) (isNat# n__s V1 -> activate# V1, activate# n__isNatList X -> isNatList# X) (isNat# n__s V1 -> activate# V1, activate# n__isNat X -> isNat# X) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (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__isNatIList X -> isNatIList# 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#()) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__isNatList X -> isNatList# X) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X) (U11#(tt(), L) -> length# activate L, length# cons(N, L) -> activate# L) (U11#(tt(), L) -> length# activate L, length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L)) (U11#(tt(), L) -> length# activate L, length# cons(N, L) -> and#(isNatList activate L, n__isNat N)) (U11#(tt(), L) -> length# activate L, length# cons(N, L) -> isNatList# activate L) (U11#(tt(), L) -> length# activate L, length# nil() -> 0#()) (isNatIList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1) (isNatIList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatList# activate V1) (isNatIList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1) (isNatIList# n__cons(V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNat# activate V1) (isNat# n__s V1 -> isNat# activate V1, isNat# n__length V1 -> activate# V1) (isNat# n__s V1 -> isNat# activate V1, isNat# n__length V1 -> isNatList# activate V1) (isNat# n__s V1 -> isNat# activate V1, isNat# n__s V1 -> activate# V1) (isNat# n__s V1 -> isNat# activate V1, isNat# n__s V1 -> isNat# activate V1) (isNatIList# V -> isNatList# activate V, isNatList# n__cons(V1, V2) -> activate# V1) (isNatIList# V -> isNatList# activate V, isNatList# n__cons(V1, V2) -> activate# V2) (isNatIList# V -> isNatList# activate V, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2)) (isNatIList# V -> isNatList# activate V, isNatList# n__cons(V1, V2) -> isNat# activate V1) (length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L), U11#(tt(), L) -> s# length activate L) (length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L), U11#(tt(), L) -> length# activate L) (length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L), U11#(tt(), L) -> activate# L) } STATUS: arrows: 0.873702 SCCS (1): Scc: { length# cons(N, L) -> activate# L, length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L), length# cons(N, L) -> and#(isNatList activate L, n__isNat N), length# cons(N, L) -> isNatList# activate L, activate# n__length X -> length# X, activate# n__isNatIList X -> isNatIList# X, activate# n__isNatList X -> isNatList# X, activate# n__isNat X -> isNat# X, U11#(tt(), L) -> length# activate L, U11#(tt(), L) -> activate# L, and#(tt(), X) -> activate# X, 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, isNatList# n__cons(V1, V2) -> activate# V1, isNatList# n__cons(V1, V2) -> activate# V2, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2), isNatList# n__cons(V1, V2) -> isNat# activate V1, isNatIList# V -> activate# V, isNatIList# V -> isNatList# activate V, isNatIList# n__cons(V1, V2) -> activate# V1, isNatIList# n__cons(V1, V2) -> activate# V2, isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2), isNatIList# n__cons(V1, V2) -> isNat# activate V1} SCC (25): Strict: { length# cons(N, L) -> activate# L, length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L), length# cons(N, L) -> and#(isNatList activate L, n__isNat N), length# cons(N, L) -> isNatList# activate L, activate# n__length X -> length# X, activate# n__isNatIList X -> isNatIList# X, activate# n__isNatList X -> isNatList# X, activate# n__isNat X -> isNat# X, U11#(tt(), L) -> length# activate L, U11#(tt(), L) -> activate# L, and#(tt(), X) -> activate# X, 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, isNatList# n__cons(V1, V2) -> activate# V1, isNatList# n__cons(V1, V2) -> activate# V2, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2), isNatList# n__cons(V1, V2) -> isNat# activate V1, isNatIList# V -> activate# V, isNatIList# V -> isNatList# activate V, isNatIList# n__cons(V1, V2) -> activate# V1, isNatIList# n__cons(V1, V2) -> activate# V2, isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2), isNatIList# n__cons(V1, V2) -> isNat# activate V1} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L), length nil() -> 0(), activate X -> X, activate n__zeros() -> zeros(), activate n__0() -> 0(), activate n__length X -> length X, activate n__s X -> s X, activate n__isNatIList X -> isNatIList X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__isNatList X -> isNatList X, activate n__isNat X -> isNat X, U11(tt(), L) -> s length activate L, and(tt(), X) -> activate X, isNat X -> n__isNat X, isNat n__0() -> tt(), isNat n__length V1 -> isNatList activate V1, isNat n__s V1 -> isNat activate V1, isNatList X -> n__isNatList X, isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2), isNatList n__nil() -> tt(), isNatIList X -> n__isNatIList X, isNatIList V -> isNatList activate V, isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2), nil() -> n__nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [U11](x0, x1) = x0 + 1, [and](x0, x1) = x0, [n__cons](x0, x1) = x0 + x1, [s](x0) = x0, [length](x0) = x0 + 1, [activate](x0) = x0, [isNat](x0) = x0, [isNatList](x0) = x0, [n__length](x0) = x0 + 1, [n__s](x0) = x0, [isNatIList](x0) = x0, [n__isNatIList](x0) = x0, [n__isNatList](x0) = x0, [n__isNat](x0) = x0, [0] = 0, [n__zeros] = 0, [zeros] = 0, [tt] = 0, [n__0] = 0, [n__nil] = 0, [nil] = 0, [U11#](x0, x1) = x0, [and#](x0, x1) = x0, [length#](x0) = x0, [activate#](x0) = x0, [isNat#](x0) = x0, [isNatList#](x0) = x0, [isNatIList#](x0) = x0 Strict: isNatIList# n__cons(V1, V2) -> isNat# activate V1 0 + 1V1 + 1V2 >= 0 + 1V1 isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2) 0 + 1V1 + 1V2 >= 0 + 0V1 + 1V2 isNatIList# n__cons(V1, V2) -> activate# V2 0 + 1V1 + 1V2 >= 0 + 1V2 isNatIList# n__cons(V1, V2) -> activate# V1 0 + 1V1 + 1V2 >= 0 + 1V1 isNatIList# V -> isNatList# activate V 0 + 1V >= 0 + 1V isNatIList# V -> activate# V 0 + 1V >= 0 + 1V isNatList# n__cons(V1, V2) -> isNat# activate V1 0 + 1V1 + 1V2 >= 0 + 1V1 isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2) 0 + 1V1 + 1V2 >= 0 + 0V1 + 1V2 isNatList# n__cons(V1, V2) -> activate# V2 0 + 1V1 + 1V2 >= 0 + 1V2 isNatList# n__cons(V1, V2) -> activate# V1 0 + 1V1 + 1V2 >= 0 + 1V1 isNat# n__s V1 -> isNat# activate V1 0 + 1V1 >= 0 + 1V1 isNat# n__s V1 -> activate# V1 0 + 1V1 >= 0 + 1V1 isNat# n__length V1 -> isNatList# activate V1 1 + 1V1 >= 0 + 1V1 isNat# n__length V1 -> activate# V1 1 + 1V1 >= 0 + 1V1 and#(tt(), X) -> activate# X 0 + 1X >= 0 + 1X U11#(tt(), L) -> activate# L 0 + 1L >= 0 + 1L U11#(tt(), L) -> length# activate L 0 + 1L >= 0 + 1L activate# n__isNat X -> isNat# X 0 + 1X >= 0 + 1X activate# n__isNatList X -> isNatList# X 0 + 1X >= 0 + 1X activate# n__isNatIList X -> isNatIList# X 0 + 1X >= 0 + 1X activate# n__length X -> length# X 1 + 1X >= 0 + 1X length# cons(N, L) -> isNatList# activate L 0 + 1L + 1N >= 0 + 1L length# cons(N, L) -> and#(isNatList activate L, n__isNat N) 0 + 1L + 1N >= 0 + 0L + 1N length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L) 0 + 1L + 1N >= 0 + 1L + 0N length# cons(N, L) -> activate# L 0 + 1L + 1N >= 0 + 1L Weak: nil() -> n__nil() 0 >= 0 isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2) 0 + 1V1 + 1V2 >= 0 + 0V1 + 1V2 isNatIList n__zeros() -> tt() 0 >= 0 isNatIList V -> isNatList activate V 0 + 1V >= 0 + 1V isNatIList X -> n__isNatIList X 0 + 1X >= 0 + 1X isNatList n__nil() -> tt() 0 >= 0 isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2) 0 + 1V1 + 1V2 >= 0 + 0V1 + 1V2 isNatList X -> n__isNatList X 0 + 1X >= 0 + 1X isNat n__s V1 -> isNat activate V1 0 + 1V1 >= 0 + 1V1 isNat n__length V1 -> isNatList activate V1 1 + 1V1 >= 0 + 1V1 isNat n__0() -> tt() 0 >= 0 isNat X -> n__isNat X 0 + 1X >= 0 + 1X and(tt(), X) -> activate X 0 + 1X >= 0 + 1X U11(tt(), L) -> s length activate L 1 + 1L >= 1 + 1L activate n__isNat X -> isNat X 0 + 1X >= 0 + 1X activate n__isNatList X -> isNatList X 0 + 1X >= 0 + 1X activate n__nil() -> nil() 0 >= 0 activate n__cons(X1, X2) -> cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__isNatIList X -> isNatIList X 0 + 1X >= 0 + 1X activate n__s X -> s X 0 + 1X >= 0 + 1X activate n__length X -> length X 1 + 1X >= 1 + 1X activate n__0() -> 0() 0 >= 0 activate n__zeros() -> zeros() 0 >= 0 activate X -> X 0 + 1X >= 1X length nil() -> 0() 1 >= 0 length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L) 1 + 1L + 1N >= 1 + 1L + 0N length X -> n__length X 1 + 1X >= 1 + 1X s X -> n__s X 0 + 1X >= 0 + 1X zeros() -> n__zeros() 0 >= 0 zeros() -> cons(0(), n__zeros()) 0 >= 0 0() -> n__0() 0 >= 0 cons(X1, X2) -> n__cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 SCCS (2): Scc: {length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L), U11#(tt(), L) -> length# activate L} Scc: { activate# n__isNatIList X -> isNatIList# X, activate# n__isNatList X -> isNatList# X, activate# n__isNat X -> isNat# X, and#(tt(), X) -> activate# X, isNat# n__s V1 -> activate# V1, isNat# n__s V1 -> isNat# activate V1, isNatList# n__cons(V1, V2) -> activate# V1, isNatList# n__cons(V1, V2) -> activate# V2, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2), isNatList# n__cons(V1, V2) -> isNat# activate V1, isNatIList# V -> activate# V, isNatIList# V -> isNatList# activate V, isNatIList# n__cons(V1, V2) -> activate# V1, isNatIList# n__cons(V1, V2) -> activate# V2, isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2), isNatIList# n__cons(V1, V2) -> isNat# activate V1} SCC (2): Strict: {length# cons(N, L) -> U11#(and(isNatList activate L, n__isNat N), activate L), U11#(tt(), L) -> length# activate L} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L), length nil() -> 0(), activate X -> X, activate n__zeros() -> zeros(), activate n__0() -> 0(), activate n__length X -> length X, activate n__s X -> s X, activate n__isNatIList X -> isNatIList X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__isNatList X -> isNatList X, activate n__isNat X -> isNat X, U11(tt(), L) -> s length activate L, and(tt(), X) -> activate X, isNat X -> n__isNat X, isNat n__0() -> tt(), isNat n__length V1 -> isNatList activate V1, isNat n__s V1 -> isNat activate V1, isNatList X -> n__isNatList X, isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2), isNatList n__nil() -> tt(), isNatIList X -> n__isNatIList X, isNatIList V -> isNatList activate V, isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2), nil() -> n__nil()} Fail SCC (16): Strict: { activate# n__isNatIList X -> isNatIList# X, activate# n__isNatList X -> isNatList# X, activate# n__isNat X -> isNat# X, and#(tt(), X) -> activate# X, isNat# n__s V1 -> activate# V1, isNat# n__s V1 -> isNat# activate V1, isNatList# n__cons(V1, V2) -> activate# V1, isNatList# n__cons(V1, V2) -> activate# V2, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2), isNatList# n__cons(V1, V2) -> isNat# activate V1, isNatIList# V -> activate# V, isNatIList# V -> isNatList# activate V, isNatIList# n__cons(V1, V2) -> activate# V1, isNatIList# n__cons(V1, V2) -> activate# V2, isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2), isNatIList# n__cons(V1, V2) -> isNat# activate V1} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L), length nil() -> 0(), activate X -> X, activate n__zeros() -> zeros(), activate n__0() -> 0(), activate n__length X -> length X, activate n__s X -> s X, activate n__isNatIList X -> isNatIList X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__isNatList X -> isNatList X, activate n__isNat X -> isNat X, U11(tt(), L) -> s length activate L, and(tt(), X) -> activate X, isNat X -> n__isNat X, isNat n__0() -> tt(), isNat n__length V1 -> isNatList activate V1, isNat n__s V1 -> isNat activate V1, isNatList X -> n__isNatList X, isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2), isNatList n__nil() -> tt(), isNatIList X -> n__isNatIList X, isNatIList V -> isNatList activate V, isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2), nil() -> n__nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [U11](x0, x1) = x0, [and](x0, x1) = x0, [n__cons](x0, x1) = x0 + x1, [s](x0) = x0, [length](x0) = x0, [activate](x0) = x0, [isNat](x0) = x0 + 1, [isNatList](x0) = x0, [n__length](x0) = x0, [n__s](x0) = x0, [isNatIList](x0) = x0, [n__isNatIList](x0) = x0, [n__isNatList](x0) = x0, [n__isNat](x0) = x0 + 1, [0] = 0, [n__zeros] = 0, [zeros] = 0, [tt] = 0, [n__0] = 0, [n__nil] = 0, [nil] = 0, [and#](x0, x1) = x0, [activate#](x0) = x0, [isNat#](x0) = x0, [isNatList#](x0) = x0, [isNatIList#](x0) = x0 Strict: isNatIList# n__cons(V1, V2) -> isNat# activate V1 0 + 1V1 + 1V2 >= 0 + 1V1 isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2) 0 + 1V1 + 1V2 >= 0 + 0V1 + 1V2 isNatIList# n__cons(V1, V2) -> activate# V2 0 + 1V1 + 1V2 >= 0 + 1V2 isNatIList# n__cons(V1, V2) -> activate# V1 0 + 1V1 + 1V2 >= 0 + 1V1 isNatIList# V -> isNatList# activate V 0 + 1V >= 0 + 1V isNatIList# V -> activate# V 0 + 1V >= 0 + 1V isNatList# n__cons(V1, V2) -> isNat# activate V1 0 + 1V1 + 1V2 >= 0 + 1V1 isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2) 0 + 1V1 + 1V2 >= 0 + 0V1 + 1V2 isNatList# n__cons(V1, V2) -> activate# V2 0 + 1V1 + 1V2 >= 0 + 1V2 isNatList# n__cons(V1, V2) -> activate# V1 0 + 1V1 + 1V2 >= 0 + 1V1 isNat# n__s V1 -> isNat# activate V1 0 + 1V1 >= 0 + 1V1 isNat# n__s V1 -> activate# V1 0 + 1V1 >= 0 + 1V1 and#(tt(), X) -> activate# X 0 + 1X >= 0 + 1X activate# n__isNat X -> isNat# X 1 + 1X >= 0 + 1X activate# n__isNatList X -> isNatList# X 0 + 1X >= 0 + 1X activate# n__isNatIList X -> isNatIList# X 0 + 1X >= 0 + 1X Weak: nil() -> n__nil() 0 >= 0 isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2) 0 + 1V1 + 1V2 >= 0 + 0V1 + 1V2 isNatIList n__zeros() -> tt() 0 >= 0 isNatIList V -> isNatList activate V 0 + 1V >= 0 + 1V isNatIList X -> n__isNatIList X 0 + 1X >= 0 + 1X isNatList n__nil() -> tt() 0 >= 0 isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2) 0 + 1V1 + 1V2 >= 0 + 0V1 + 1V2 isNatList X -> n__isNatList X 0 + 1X >= 0 + 1X isNat n__s V1 -> isNat activate V1 1 + 1V1 >= 1 + 1V1 isNat n__length V1 -> isNatList activate V1 1 + 1V1 >= 0 + 1V1 isNat n__0() -> tt() 1 >= 0 isNat X -> n__isNat X 1 + 1X >= 1 + 1X and(tt(), X) -> activate X 0 + 1X >= 0 + 1X U11(tt(), L) -> s length activate L 0 + 1L >= 0 + 1L activate n__isNat X -> isNat X 1 + 1X >= 1 + 1X activate n__isNatList X -> isNatList X 0 + 1X >= 0 + 1X activate n__nil() -> nil() 0 >= 0 activate n__cons(X1, X2) -> cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__isNatIList X -> isNatIList X 0 + 1X >= 0 + 1X activate n__s X -> s X 0 + 1X >= 0 + 1X activate n__length X -> length X 0 + 1X >= 0 + 1X activate n__0() -> 0() 0 >= 0 activate n__zeros() -> zeros() 0 >= 0 activate X -> X 0 + 1X >= 1X length nil() -> 0() 0 >= 0 length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L) 0 + 1L + 1N >= 0 + 1L + 0N length X -> n__length X 0 + 1X >= 0 + 1X s X -> n__s X 0 + 1X >= 0 + 1X zeros() -> n__zeros() 0 >= 0 zeros() -> cons(0(), n__zeros()) 0 >= 0 0() -> n__0() 0 >= 0 cons(X1, X2) -> n__cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 SCCS (1): Scc: { activate# n__isNatIList X -> isNatIList# X, activate# n__isNatList X -> isNatList# X, and#(tt(), X) -> activate# X, isNat# n__s V1 -> activate# V1, isNat# n__s V1 -> isNat# activate V1, isNatList# n__cons(V1, V2) -> activate# V1, isNatList# n__cons(V1, V2) -> activate# V2, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2), isNatList# n__cons(V1, V2) -> isNat# activate V1, isNatIList# V -> activate# V, isNatIList# V -> isNatList# activate V, isNatIList# n__cons(V1, V2) -> activate# V1, isNatIList# n__cons(V1, V2) -> activate# V2, isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2), isNatIList# n__cons(V1, V2) -> isNat# activate V1} SCC (15): Strict: { activate# n__isNatIList X -> isNatIList# X, activate# n__isNatList X -> isNatList# X, and#(tt(), X) -> activate# X, isNat# n__s V1 -> activate# V1, isNat# n__s V1 -> isNat# activate V1, isNatList# n__cons(V1, V2) -> activate# V1, isNatList# n__cons(V1, V2) -> activate# V2, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2), isNatList# n__cons(V1, V2) -> isNat# activate V1, isNatIList# V -> activate# V, isNatIList# V -> isNatList# activate V, isNatIList# n__cons(V1, V2) -> activate# V1, isNatIList# n__cons(V1, V2) -> activate# V2, isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2), isNatIList# n__cons(V1, V2) -> isNat# activate V1} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L), length nil() -> 0(), activate X -> X, activate n__zeros() -> zeros(), activate n__0() -> 0(), activate n__length X -> length X, activate n__s X -> s X, activate n__isNatIList X -> isNatIList X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__isNatList X -> isNatList X, activate n__isNat X -> isNat X, U11(tt(), L) -> s length activate L, and(tt(), X) -> activate X, isNat X -> n__isNat X, isNat n__0() -> tt(), isNat n__length V1 -> isNatList activate V1, isNat n__s V1 -> isNat activate V1, isNatList X -> n__isNatList X, isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2), isNatList n__nil() -> tt(), isNatIList X -> n__isNatIList X, isNatIList V -> isNatList activate V, isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2), nil() -> n__nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [U11](x0, x1) = x0, [and](x0, x1) = x0, [n__cons](x0, x1) = x0 + x1, [s](x0) = x0, [length](x0) = x0, [activate](x0) = x0, [isNat](x0) = x0 + 1, [isNatList](x0) = x0, [n__length](x0) = x0, [n__s](x0) = x0, [isNatIList](x0) = x0 + 1, [n__isNatIList](x0) = x0 + 1, [n__isNatList](x0) = x0, [n__isNat](x0) = x0 + 1, [0] = 0, [n__zeros] = 0, [zeros] = 0, [tt] = 0, [n__0] = 0, [n__nil] = 0, [nil] = 0, [and#](x0, x1) = x0, [activate#](x0) = x0, [isNat#](x0) = x0, [isNatList#](x0) = x0, [isNatIList#](x0) = x0 + 1 Strict: isNatIList# n__cons(V1, V2) -> isNat# activate V1 1 + 1V1 + 1V2 >= 0 + 1V1 isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2) 1 + 1V1 + 1V2 >= 1 + 0V1 + 1V2 isNatIList# n__cons(V1, V2) -> activate# V2 1 + 1V1 + 1V2 >= 0 + 1V2 isNatIList# n__cons(V1, V2) -> activate# V1 1 + 1V1 + 1V2 >= 0 + 1V1 isNatIList# V -> isNatList# activate V 1 + 1V >= 0 + 1V isNatIList# V -> activate# V 1 + 1V >= 0 + 1V isNatList# n__cons(V1, V2) -> isNat# activate V1 0 + 1V1 + 1V2 >= 0 + 1V1 isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2) 0 + 1V1 + 1V2 >= 0 + 0V1 + 1V2 isNatList# n__cons(V1, V2) -> activate# V2 0 + 1V1 + 1V2 >= 0 + 1V2 isNatList# n__cons(V1, V2) -> activate# V1 0 + 1V1 + 1V2 >= 0 + 1V1 isNat# n__s V1 -> isNat# activate V1 0 + 1V1 >= 0 + 1V1 isNat# n__s V1 -> activate# V1 0 + 1V1 >= 0 + 1V1 and#(tt(), X) -> activate# X 0 + 1X >= 0 + 1X activate# n__isNatList X -> isNatList# X 0 + 1X >= 0 + 1X activate# n__isNatIList X -> isNatIList# X 1 + 1X >= 1 + 1X Weak: nil() -> n__nil() 0 >= 0 isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2) 1 + 1V1 + 1V2 >= 1 + 0V1 + 1V2 isNatIList n__zeros() -> tt() 1 >= 0 isNatIList V -> isNatList activate V 1 + 1V >= 0 + 1V isNatIList X -> n__isNatIList X 1 + 1X >= 1 + 1X isNatList n__nil() -> tt() 0 >= 0 isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2) 0 + 1V1 + 1V2 >= 0 + 0V1 + 1V2 isNatList X -> n__isNatList X 0 + 1X >= 0 + 1X isNat n__s V1 -> isNat activate V1 1 + 1V1 >= 1 + 1V1 isNat n__length V1 -> isNatList activate V1 1 + 1V1 >= 0 + 1V1 isNat n__0() -> tt() 1 >= 0 isNat X -> n__isNat X 1 + 1X >= 1 + 1X and(tt(), X) -> activate X 0 + 1X >= 0 + 1X U11(tt(), L) -> s length activate L 0 + 1L >= 0 + 1L activate n__isNat X -> isNat X 1 + 1X >= 1 + 1X activate n__isNatList X -> isNatList X 0 + 1X >= 0 + 1X activate n__nil() -> nil() 0 >= 0 activate n__cons(X1, X2) -> cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__isNatIList X -> isNatIList X 1 + 1X >= 1 + 1X activate n__s X -> s X 0 + 1X >= 0 + 1X activate n__length X -> length X 0 + 1X >= 0 + 1X activate n__0() -> 0() 0 >= 0 activate n__zeros() -> zeros() 0 >= 0 activate X -> X 0 + 1X >= 1X length nil() -> 0() 0 >= 0 length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L) 0 + 1L + 1N >= 0 + 1L + 0N length X -> n__length X 0 + 1X >= 0 + 1X s X -> n__s X 0 + 1X >= 0 + 1X zeros() -> n__zeros() 0 >= 0 zeros() -> cons(0(), n__zeros()) 0 >= 0 0() -> n__0() 0 >= 0 cons(X1, X2) -> n__cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 SCCS (1): Scc: { activate# n__isNatIList X -> isNatIList# X, activate# n__isNatList X -> isNatList# X, and#(tt(), X) -> activate# X, isNat# n__s V1 -> activate# V1, isNat# n__s V1 -> isNat# activate V1, isNatList# n__cons(V1, V2) -> activate# V1, isNatList# n__cons(V1, V2) -> activate# V2, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2), isNatList# n__cons(V1, V2) -> isNat# activate V1, isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2)} SCC (10): Strict: { activate# n__isNatIList X -> isNatIList# X, activate# n__isNatList X -> isNatList# X, and#(tt(), X) -> activate# X, isNat# n__s V1 -> activate# V1, isNat# n__s V1 -> isNat# activate V1, isNatList# n__cons(V1, V2) -> activate# V1, isNatList# n__cons(V1, V2) -> activate# V2, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2), isNatList# n__cons(V1, V2) -> isNat# activate V1, isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2)} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L), length nil() -> 0(), activate X -> X, activate n__zeros() -> zeros(), activate n__0() -> 0(), activate n__length X -> length X, activate n__s X -> s X, activate n__isNatIList X -> isNatIList X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__isNatList X -> isNatList X, activate n__isNat X -> isNat X, U11(tt(), L) -> s length activate L, and(tt(), X) -> activate X, isNat X -> n__isNat X, isNat n__0() -> tt(), isNat n__length V1 -> isNatList activate V1, isNat n__s V1 -> isNat activate V1, isNatList X -> n__isNatList X, isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2), isNatList n__nil() -> tt(), isNatIList X -> n__isNatIList X, isNatIList V -> isNatList activate V, isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2), nil() -> n__nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0 + x1, [U11](x0, x1) = x0 + 1, [and](x0, x1) = x0, [n__cons](x0, x1) = x0 + x1, [s](x0) = x0, [length](x0) = x0 + 1, [activate](x0) = x0, [isNat](x0) = x0, [isNatList](x0) = x0 + 1, [n__length](x0) = x0 + 1, [n__s](x0) = x0, [isNatIList](x0) = x0 + 1, [n__isNatIList](x0) = x0 + 1, [n__isNatList](x0) = x0 + 1, [n__isNat](x0) = x0, [0] = 0, [n__zeros] = 0, [zeros] = 0, [tt] = 0, [n__0] = 0, [n__nil] = 1, [nil] = 1, [and#](x0, x1) = x0, [activate#](x0) = x0, [isNat#](x0) = x0, [isNatList#](x0) = x0 + 1, [isNatIList#](x0) = x0 + 1 Strict: isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2) 1 + 1V1 + 1V2 >= 1 + 0V1 + 1V2 isNatList# n__cons(V1, V2) -> isNat# activate V1 1 + 1V1 + 1V2 >= 0 + 1V1 isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2) 1 + 1V1 + 1V2 >= 1 + 0V1 + 1V2 isNatList# n__cons(V1, V2) -> activate# V2 1 + 1V1 + 1V2 >= 0 + 1V2 isNatList# n__cons(V1, V2) -> activate# V1 1 + 1V1 + 1V2 >= 0 + 1V1 isNat# n__s V1 -> isNat# activate V1 0 + 1V1 >= 0 + 1V1 isNat# n__s V1 -> activate# V1 0 + 1V1 >= 0 + 1V1 and#(tt(), X) -> activate# X 0 + 1X >= 0 + 1X activate# n__isNatList X -> isNatList# X 1 + 1X >= 1 + 1X activate# n__isNatIList X -> isNatIList# X 1 + 1X >= 1 + 1X Weak: nil() -> n__nil() 1 >= 1 isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2) 1 + 1V1 + 1V2 >= 1 + 0V1 + 1V2 isNatIList n__zeros() -> tt() 1 >= 0 isNatIList V -> isNatList activate V 1 + 1V >= 1 + 1V isNatIList X -> n__isNatIList X 1 + 1X >= 1 + 1X isNatList n__nil() -> tt() 2 >= 0 isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2) 1 + 1V1 + 1V2 >= 1 + 0V1 + 1V2 isNatList X -> n__isNatList X 1 + 1X >= 1 + 1X isNat n__s V1 -> isNat activate V1 0 + 1V1 >= 0 + 1V1 isNat n__length V1 -> isNatList activate V1 1 + 1V1 >= 1 + 1V1 isNat n__0() -> tt() 0 >= 0 isNat X -> n__isNat X 0 + 1X >= 0 + 1X and(tt(), X) -> activate X 0 + 1X >= 0 + 1X U11(tt(), L) -> s length activate L 1 + 1L >= 1 + 1L activate n__isNat X -> isNat X 0 + 1X >= 0 + 1X activate n__isNatList X -> isNatList X 1 + 1X >= 1 + 1X activate n__nil() -> nil() 1 >= 1 activate n__cons(X1, X2) -> cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__isNatIList X -> isNatIList X 1 + 1X >= 1 + 1X activate n__s X -> s X 0 + 1X >= 0 + 1X activate n__length X -> length X 1 + 1X >= 1 + 1X activate n__0() -> 0() 0 >= 0 activate n__zeros() -> zeros() 0 >= 0 activate X -> X 0 + 1X >= 1X length nil() -> 0() 2 >= 0 length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L) 1 + 1L + 1N >= 1 + 1L + 0N length X -> n__length X 1 + 1X >= 1 + 1X s X -> n__s X 0 + 1X >= 0 + 1X zeros() -> n__zeros() 0 >= 0 zeros() -> cons(0(), n__zeros()) 0 >= 0 0() -> n__0() 0 >= 0 cons(X1, X2) -> n__cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 SCCS (2): Scc: {isNat# n__s V1 -> isNat# activate V1} Scc: { activate# n__isNatIList X -> isNatIList# X, activate# n__isNatList X -> isNatList# X, and#(tt(), X) -> activate# X, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2), isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2)} SCC (1): Strict: {isNat# n__s V1 -> isNat# activate V1} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L), length nil() -> 0(), activate X -> X, activate n__zeros() -> zeros(), activate n__0() -> 0(), activate n__length X -> length X, activate n__s X -> s X, activate n__isNatIList X -> isNatIList X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__isNatList X -> isNatList X, activate n__isNat X -> isNat X, U11(tt(), L) -> s length activate L, and(tt(), X) -> activate X, isNat X -> n__isNat X, isNat n__0() -> tt(), isNat n__length V1 -> isNatList activate V1, isNat n__s V1 -> isNat activate V1, isNatList X -> n__isNatList X, isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2), isNatList n__nil() -> tt(), isNatIList X -> n__isNatIList X, isNatIList V -> isNatList activate V, isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2), nil() -> n__nil()} Fail SCC (5): Strict: { activate# n__isNatIList X -> isNatIList# X, activate# n__isNatList X -> isNatList# X, and#(tt(), X) -> activate# X, isNatList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatList activate V2), isNatIList# n__cons(V1, V2) -> and#(isNat activate V1, n__isNatIList activate V2)} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U11(and(isNatList activate L, n__isNat N), activate L), length nil() -> 0(), activate X -> X, activate n__zeros() -> zeros(), activate n__0() -> 0(), activate n__length X -> length X, activate n__s X -> s X, activate n__isNatIList X -> isNatIList X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__isNatList X -> isNatList X, activate n__isNat X -> isNat X, U11(tt(), L) -> s length activate L, and(tt(), X) -> activate X, isNat X -> n__isNat X, isNat n__0() -> tt(), isNat n__length V1 -> isNatList activate V1, isNat n__s V1 -> isNat activate V1, isNatList X -> n__isNatList X, isNatList n__cons(V1, V2) -> and(isNat activate V1, n__isNatList activate V2), isNatList n__nil() -> tt(), isNatIList X -> n__isNatIList X, isNatIList V -> isNatList activate V, isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> and(isNat activate V1, n__isNatIList activate V2), nil() -> n__nil()} Fail