MAYBE Time: 0.757421 TRS: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12 tt() -> tt(), isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList n__nil() -> tt(), 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__isNatIListKind X -> isNatIListKind X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__and(X1, X2) -> and(X1, X2), activate n__isNatKind X -> isNatKind X, U11(tt(), V1) -> U12 isNatList activate V1, U22 tt() -> tt(), isNat n__0() -> tt(), isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1), isNat n__s V1 -> U21(isNatKind activate V1, activate V1), U21(tt(), V1) -> U22 isNat activate V1, U32 tt() -> tt(), U31(tt(), V) -> U32 isNatList activate V, U42(tt(), V2) -> U43 isNatIList activate V2, U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2), U43 tt() -> tt(), isNatIList V -> U31(isNatIListKind activate V, activate V), isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52(tt(), V2) -> U53 isNatList activate V2, U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2), U53 tt() -> tt(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length nil() -> 0(), U61(tt(), L) -> s length activate L, and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate X, isNatIListKind X -> n__isNatIListKind X, isNatIListKind n__zeros() -> tt(), isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind n__nil() -> tt(), isNatKind X -> n__isNatKind X, isNatKind n__0() -> tt(), isNatKind n__length V1 -> isNatIListKind activate V1, isNatKind n__s V1 -> isNatKind activate V1, nil() -> n__nil()} DP: DP: { zeros#() -> cons#(0(), n__zeros()), zeros#() -> 0#(), isNatList# n__cons(V1, V2) -> activate# V1, isNatList# n__cons(V1, V2) -> activate# V2, isNatList# n__cons(V1, V2) -> U51#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2), isNatList# n__cons(V1, V2) -> isNatKind# activate V1, activate# n__zeros() -> zeros#(), activate# n__0() -> 0#(), activate# n__length X -> length# X, activate# n__s X -> s# X, activate# n__isNatIListKind X -> isNatIListKind# X, activate# n__cons(X1, X2) -> cons#(X1, X2), activate# n__nil() -> nil#(), activate# n__and(X1, X2) -> and#(X1, X2), activate# n__isNatKind X -> isNatKind# X, U11#(tt(), V1) -> U12# isNatList activate V1, U11#(tt(), V1) -> isNatList# activate V1, U11#(tt(), V1) -> activate# V1, isNat# n__length V1 -> activate# V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), isNat# n__length V1 -> isNatIListKind# activate V1, isNat# n__s V1 -> activate# V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), isNat# n__s V1 -> isNatKind# activate V1, U21#(tt(), V1) -> activate# V1, U21#(tt(), V1) -> U22# isNat activate V1, U21#(tt(), V1) -> isNat# activate V1, U31#(tt(), V) -> isNatList# activate V, U31#(tt(), V) -> activate# V, U31#(tt(), V) -> U32# isNatList activate V, U42#(tt(), V2) -> activate# V2, U42#(tt(), V2) -> U43# isNatIList activate V2, U42#(tt(), V2) -> isNatIList# activate V2, U41#(tt(), V1, V2) -> activate# V1, U41#(tt(), V1, V2) -> activate# V2, U41#(tt(), V1, V2) -> isNat# activate V1, U41#(tt(), V1, V2) -> U42#(isNat activate V1, activate V2), isNatIList# V -> activate# V, isNatIList# V -> U31#(isNatIListKind activate V, activate V), isNatIList# V -> isNatIListKind# activate V, isNatIList# n__cons(V1, V2) -> activate# V1, isNatIList# n__cons(V1, V2) -> activate# V2, isNatIList# n__cons(V1, V2) -> U41#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatIList# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2), isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, U52#(tt(), V2) -> isNatList# activate V2, U52#(tt(), V2) -> activate# V2, U52#(tt(), V2) -> U53# isNatList activate V2, U51#(tt(), V1, V2) -> activate# V1, U51#(tt(), V1, V2) -> activate# V2, U51#(tt(), V1, V2) -> isNat# activate V1, U51#(tt(), V1, V2) -> U52#(isNat activate V1, activate V2), length# cons(N, L) -> isNatList# activate L, length# cons(N, L) -> activate# L, length# cons(N, L) -> isNat# N, length# cons(N, L) -> U61#(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length# cons(N, L) -> and#(isNatList activate L, n__isNatIListKind activate L), length# cons(N, L) -> and#(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), length# nil() -> 0#(), U61#(tt(), L) -> activate# L, U61#(tt(), L) -> s# length activate L, U61#(tt(), L) -> length# activate L, and#(tt(), X) -> activate# X, isNatIListKind# n__cons(V1, V2) -> activate# V1, isNatIListKind# n__cons(V1, V2) -> activate# V2, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1, isNatKind# n__length V1 -> isNatIListKind# activate V1, isNatKind# n__s V1 -> activate# V1, isNatKind# n__s V1 -> isNatKind# activate V1} TRS: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12 tt() -> tt(), isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList n__nil() -> tt(), 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__isNatIListKind X -> isNatIListKind X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__and(X1, X2) -> and(X1, X2), activate n__isNatKind X -> isNatKind X, U11(tt(), V1) -> U12 isNatList activate V1, U22 tt() -> tt(), isNat n__0() -> tt(), isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1), isNat n__s V1 -> U21(isNatKind activate V1, activate V1), U21(tt(), V1) -> U22 isNat activate V1, U32 tt() -> tt(), U31(tt(), V) -> U32 isNatList activate V, U42(tt(), V2) -> U43 isNatIList activate V2, U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2), U43 tt() -> tt(), isNatIList V -> U31(isNatIListKind activate V, activate V), isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52(tt(), V2) -> U53 isNatList activate V2, U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2), U53 tt() -> tt(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length nil() -> 0(), U61(tt(), L) -> s length activate L, and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate X, isNatIListKind X -> n__isNatIListKind X, isNatIListKind n__zeros() -> tt(), isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind n__nil() -> tt(), isNatKind X -> n__isNatKind X, isNatKind n__0() -> tt(), isNatKind n__length V1 -> isNatIListKind activate V1, isNatKind n__s V1 -> isNatKind activate V1, nil() -> n__nil()} UR: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12 tt() -> tt(), isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList n__nil() -> tt(), 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__isNatIListKind X -> isNatIListKind X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__and(X1, X2) -> and(X1, X2), activate n__isNatKind X -> isNatKind X, U11(tt(), V1) -> U12 isNatList activate V1, U22 tt() -> tt(), isNat n__0() -> tt(), isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1), isNat n__s V1 -> U21(isNatKind activate V1, activate V1), U21(tt(), V1) -> U22 isNat activate V1, U32 tt() -> tt(), U31(tt(), V) -> U32 isNatList activate V, U42(tt(), V2) -> U43 isNatIList activate V2, U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2), U43 tt() -> tt(), isNatIList V -> U31(isNatIListKind activate V, activate V), isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52(tt(), V2) -> U53 isNatList activate V2, U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2), U53 tt() -> tt(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length nil() -> 0(), U61(tt(), L) -> s length activate L, and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate X, isNatIListKind X -> n__isNatIListKind X, isNatIListKind n__zeros() -> tt(), isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind n__nil() -> tt(), isNatKind X -> n__isNatKind X, isNatKind n__0() -> tt(), isNatKind n__length V1 -> isNatIListKind activate V1, isNatKind n__s V1 -> isNatKind activate V1, nil() -> n__nil(), a(x, y) -> x, a(x, y) -> y} EDG: { (U42#(tt(), V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X) (U42#(tt(), V2) -> activate# V2, activate# n__and(X1, X2) -> and#(X1, X2)) (U42#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (U42#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U42#(tt(), V2) -> activate# V2, activate# n__isNatIListKind X -> isNatIListKind# X) (U42#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U42#(tt(), V2) -> activate# V2, activate# n__length X -> length# X) (U42#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U42#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#()) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__isNatIListKind X -> isNatIListKind# X) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (U51#(tt(), V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X) (U51#(tt(), V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(X1, X2)) (U51#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (U51#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U51#(tt(), V1, V2) -> activate# V2, activate# n__isNatIListKind X -> isNatIListKind# X) (U51#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X) (U51#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X) (U51#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#()) (U51#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (isNatIList# V -> activate# V, activate# n__isNatKind X -> isNatKind# X) (isNatIList# V -> activate# V, activate# n__and(X1, X2) -> and#(X1, X2)) (isNatIList# V -> activate# V, activate# n__nil() -> nil#()) (isNatIList# V -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatIList# V -> activate# V, activate# n__isNatIListKind X -> isNatIListKind# X) (isNatIList# V -> activate# V, activate# n__s X -> s# X) (isNatIList# V -> activate# V, activate# n__length X -> length# X) (isNatIList# V -> activate# V, activate# n__0() -> 0#()) (isNatIList# V -> activate# V, activate# n__zeros() -> zeros#()) (isNatIList# n__cons(V1, V2) -> U41#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U41#(tt(), V1, V2) -> U42#(isNat activate V1, activate V2)) (isNatIList# n__cons(V1, V2) -> U41#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U41#(tt(), V1, V2) -> isNat# activate V1) (isNatIList# n__cons(V1, V2) -> U41#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U41#(tt(), V1, V2) -> activate# V2) (isNatIList# n__cons(V1, V2) -> U41#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U41#(tt(), V1, V2) -> activate# V1) (U11#(tt(), V1) -> activate# V1, activate# n__isNatKind X -> isNatKind# X) (U11#(tt(), V1) -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2)) (U11#(tt(), V1) -> activate# V1, activate# n__nil() -> nil#()) (U11#(tt(), V1) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U11#(tt(), V1) -> activate# V1, activate# n__isNatIListKind X -> isNatIListKind# X) (U11#(tt(), V1) -> activate# V1, activate# n__s X -> s# X) (U11#(tt(), V1) -> activate# V1, activate# n__length X -> length# X) (U11#(tt(), V1) -> activate# V1, activate# n__0() -> 0#()) (U11#(tt(), V1) -> activate# V1, activate# n__zeros() -> zeros#()) (isNat# n__s V1 -> activate# V1, activate# n__isNatKind X -> isNatKind# X) (isNat# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2)) (isNat# n__s V1 -> activate# V1, activate# n__nil() -> nil#()) (isNat# n__s V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNat# n__s V1 -> activate# V1, activate# n__isNatIListKind X -> isNatIListKind# X) (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# X) (isNat# n__s V1 -> activate# V1, activate# n__length X -> length# X) (isNat# n__s V1 -> activate# V1, activate# n__0() -> 0#()) (isNat# n__s V1 -> activate# V1, activate# n__zeros() -> zeros#()) (U41#(tt(), V1, V2) -> activate# V1, activate# n__isNatKind X -> isNatKind# X) (U41#(tt(), V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2)) (U41#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#()) (U41#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U41#(tt(), V1, V2) -> activate# V1, activate# n__isNatIListKind X -> isNatIListKind# X) (U41#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X) (U41#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X) (U41#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#()) (U41#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#()) (U51#(tt(), V1, V2) -> activate# V1, activate# n__isNatKind X -> isNatKind# X) (U51#(tt(), V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2)) (U51#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#()) (U51#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U51#(tt(), V1, V2) -> activate# V1, activate# n__isNatIListKind X -> isNatIListKind# X) (U51#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X) (U51#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X) (U51#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#()) (U51#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#()) (isNatKind# n__length V1 -> activate# V1, activate# n__isNatKind X -> isNatKind# X) (isNatKind# n__length V1 -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2)) (isNatKind# n__length V1 -> activate# V1, activate# n__nil() -> nil#()) (isNatKind# n__length V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatKind# n__length V1 -> activate# V1, activate# n__isNatIListKind X -> isNatIListKind# X) (isNatKind# n__length V1 -> activate# V1, activate# n__s X -> s# X) (isNatKind# n__length V1 -> activate# V1, activate# n__length X -> length# X) (isNatKind# n__length V1 -> activate# V1, activate# n__0() -> 0#()) (isNatKind# n__length V1 -> activate# V1, activate# n__zeros() -> zeros#()) (isNatList# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2), and#(tt(), X) -> activate# X) (length# cons(N, L) -> and#(isNatList activate L, n__isNatIListKind activate L), and#(tt(), X) -> activate# X) (length# cons(N, L) -> and#(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), and#(tt(), X) -> activate# X) (activate# n__zeros() -> zeros#(), zeros#() -> 0#()) (activate# n__zeros() -> zeros#(), zeros#() -> cons#(0(), n__zeros())) (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> isNatKind# activate V1) (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2)) (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> U51#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, 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) (U42#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> isNatKind# activate V1) (U42#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2)) (U42#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> U41#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2)) (U42#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> activate# V2) (U42#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> activate# V1) (U42#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> isNatIListKind# activate V) (U42#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> U31#(isNatIListKind activate V, activate V)) (U42#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> activate# V) (U31#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> isNatKind# activate V1) (U31#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2)) (U31#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> U51#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2)) (U31#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> activate# V2) (U31#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> activate# V1) (isNatList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1) (isNatList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1) (isNatList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1) (isNatList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1) (isNat# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1) (isNat# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2)) (isNat# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V2) (isNat# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V1) (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1) (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1)) (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> activate# V1) (U21#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1) (U21#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1)) (U21#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> activate# V1) (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1) (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1) (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1) (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1) (isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1) (isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1) (isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1) (isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1) (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1) (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1) (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1) (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1) (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> isNat# activate V1) (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> U22# isNat activate V1) (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> activate# V1) (isNatIList# V -> U31#(isNatIListKind activate V, activate V), U31#(tt(), V) -> U32# isNatList activate V) (isNatIList# V -> U31#(isNatIListKind activate V, activate V), U31#(tt(), V) -> activate# V) (isNatIList# V -> U31#(isNatIListKind activate V, activate V), U31#(tt(), V) -> isNatList# activate V) (length# cons(N, L) -> U61#(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), U61#(tt(), L) -> length# activate L) (length# cons(N, L) -> U61#(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), U61#(tt(), L) -> s# length activate L) (length# cons(N, L) -> U61#(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), U61#(tt(), L) -> activate# L) (activate# n__and(X1, X2) -> and#(X1, X2), and#(tt(), X) -> activate# X) (activate# n__length X -> length# X, length# nil() -> 0#()) (activate# n__length X -> length# X, length# cons(N, L) -> and#(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N))) (activate# n__length X -> length# X, length# cons(N, L) -> and#(isNatList activate L, n__isNatIListKind activate L)) (activate# n__length X -> length# X, length# cons(N, L) -> U61#(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L)) (activate# n__length X -> length# X, length# cons(N, L) -> isNat# N) (activate# n__length X -> length# X, length# cons(N, L) -> activate# L) (activate# n__length X -> length# X, length# cons(N, L) -> isNatList# activate L) (activate# n__isNatIListKind X -> isNatIListKind# X, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1) (activate# n__isNatIListKind X -> isNatIListKind# X, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2)) (activate# n__isNatIListKind X -> isNatIListKind# X, isNatIListKind# n__cons(V1, V2) -> activate# V2) (activate# n__isNatIListKind X -> isNatIListKind# X, isNatIListKind# n__cons(V1, V2) -> activate# V1) (and#(tt(), X) -> activate# X, activate# n__isNatKind X -> isNatKind# X) (and#(tt(), X) -> activate# X, activate# n__and(X1, X2) -> and#(X1, X2)) (and#(tt(), X) -> activate# X, activate# n__nil() -> nil#()) (and#(tt(), X) -> activate# X, activate# n__cons(X1, X2) -> cons#(X1, X2)) (and#(tt(), X) -> activate# X, activate# n__isNatIListKind X -> isNatIListKind# X) (and#(tt(), X) -> activate# X, activate# n__s X -> s# X) (and#(tt(), X) -> activate# X, activate# n__length X -> length# X) (and#(tt(), X) -> activate# X, activate# n__0() -> 0#()) (and#(tt(), X) -> activate# X, activate# n__zeros() -> zeros#()) (U61#(tt(), L) -> activate# L, activate# n__isNatKind X -> isNatKind# X) (U61#(tt(), L) -> activate# L, activate# n__and(X1, X2) -> and#(X1, X2)) (U61#(tt(), L) -> activate# L, activate# n__nil() -> nil#()) (U61#(tt(), L) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U61#(tt(), L) -> activate# L, activate# n__isNatIListKind X -> isNatIListKind# X) (U61#(tt(), L) -> activate# L, activate# n__s X -> s# X) (U61#(tt(), L) -> activate# L, activate# n__length X -> length# X) (U61#(tt(), L) -> activate# L, activate# n__0() -> 0#()) (U61#(tt(), L) -> activate# L, activate# n__zeros() -> zeros#()) (length# cons(N, L) -> activate# L, activate# n__zeros() -> zeros#()) (length# cons(N, L) -> activate# L, activate# n__0() -> 0#()) (length# cons(N, L) -> activate# L, activate# n__length X -> length# X) (length# cons(N, L) -> activate# L, activate# n__s X -> s# X) (length# cons(N, L) -> activate# L, activate# n__isNatIListKind X -> isNatIListKind# X) (length# cons(N, L) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2)) (length# cons(N, L) -> activate# L, activate# n__nil() -> nil#()) (length# cons(N, L) -> activate# L, activate# n__and(X1, X2) -> and#(X1, X2)) (length# cons(N, L) -> activate# L, activate# n__isNatKind X -> isNatKind# X) (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__length V1 -> activate# V1) (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__length V1 -> isNatIListKind# activate V1) (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__s V1 -> activate# V1) (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__s V1 -> isNatKind# activate V1) (length# cons(N, L) -> isNat# N, isNat# n__length V1 -> activate# V1) (length# cons(N, L) -> isNat# N, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1)) (length# cons(N, L) -> isNat# N, isNat# n__length V1 -> isNatIListKind# activate V1) (length# cons(N, L) -> isNat# N, isNat# n__s V1 -> activate# V1) (length# cons(N, L) -> isNat# N, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1)) (length# cons(N, L) -> isNat# N, isNat# n__s V1 -> isNatKind# activate V1) (U51#(tt(), V1, V2) -> U52#(isNat activate V1, activate V2), U52#(tt(), V2) -> isNatList# activate V2) (U51#(tt(), V1, V2) -> U52#(isNat activate V1, activate V2), U52#(tt(), V2) -> activate# V2) (U51#(tt(), V1, V2) -> U52#(isNat activate V1, activate V2), U52#(tt(), V2) -> U53# isNatList activate V2) (U41#(tt(), V1, V2) -> U42#(isNat activate V1, activate V2), U42#(tt(), V2) -> activate# V2) (U41#(tt(), V1, V2) -> U42#(isNat activate V1, activate V2), U42#(tt(), V2) -> U43# isNatIList activate V2) (U41#(tt(), V1, V2) -> U42#(isNat activate V1, activate V2), U42#(tt(), V2) -> isNatIList# activate V2) (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> U12# isNatList activate V1) (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> isNatList# activate V1) (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> activate# V1) (isNatKind# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V1) (isNatKind# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V2) (isNatKind# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2)) (isNatKind# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1) (U51#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1) (U51#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1)) (U51#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1) (U51#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1) (U51#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1)) (U51#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1) (U41#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1) (U41#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1)) (U41#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1) (U41#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1) (U41#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1)) (U41#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1) (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1) (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1) (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1) (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1) (U11#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> activate# V1) (U11#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> activate# V2) (U11#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> U51#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2)) (U11#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2)) (U11#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> isNatKind# activate V1) (isNatIList# V -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> activate# V1) (isNatIList# V -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> activate# V2) (isNatIList# V -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2)) (isNatIList# V -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1) (U52#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> activate# V1) (U52#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> activate# V2) (U52#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> U51#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2)) (U52#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2)) (U52#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> isNatKind# activate V1) (U61#(tt(), L) -> length# activate L, length# cons(N, L) -> isNatList# activate L) (U61#(tt(), L) -> length# activate L, length# cons(N, L) -> activate# L) (U61#(tt(), L) -> length# activate L, length# cons(N, L) -> isNat# N) (U61#(tt(), L) -> length# activate L, length# cons(N, L) -> U61#(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L)) (U61#(tt(), L) -> length# activate L, length# cons(N, L) -> and#(isNatList activate L, n__isNatIListKind activate L)) (U61#(tt(), L) -> length# activate L, length# cons(N, L) -> and#(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N))) (U61#(tt(), L) -> length# activate L, length# nil() -> 0#()) (isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2), and#(tt(), X) -> activate# X) (isNatIList# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2), and#(tt(), X) -> activate# X) (isNatKind# n__s V1 -> activate# V1, activate# n__zeros() -> zeros#()) (isNatKind# n__s V1 -> activate# V1, activate# n__0() -> 0#()) (isNatKind# n__s V1 -> activate# V1, activate# n__length X -> length# X) (isNatKind# n__s V1 -> activate# V1, activate# n__s X -> s# X) (isNatKind# n__s V1 -> activate# V1, activate# n__isNatIListKind X -> isNatIListKind# X) (isNatKind# n__s V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatKind# n__s V1 -> activate# V1, activate# n__nil() -> nil#()) (isNatKind# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2)) (isNatKind# n__s V1 -> activate# V1, activate# n__isNatKind X -> isNatKind# X) (isNatIListKind# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#()) (isNatIListKind# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isNatIListKind# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X) (isNatIListKind# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isNatIListKind# n__cons(V1, V2) -> activate# V1, activate# n__isNatIListKind X -> isNatIListKind# X) (isNatIListKind# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatIListKind# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#()) (isNatIListKind# n__cons(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2)) (isNatIListKind# n__cons(V1, V2) -> activate# V1, activate# n__isNatKind X -> isNatKind# 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__isNatIListKind X -> isNatIListKind# 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__and(X1, X2) -> and#(X1, X2)) (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__isNatKind X -> isNatKind# X) (U21#(tt(), V1) -> activate# V1, activate# n__zeros() -> zeros#()) (U21#(tt(), V1) -> activate# V1, activate# n__0() -> 0#()) (U21#(tt(), V1) -> activate# V1, activate# n__length X -> length# X) (U21#(tt(), V1) -> activate# V1, activate# n__s X -> s# X) (U21#(tt(), V1) -> activate# V1, activate# n__isNatIListKind X -> isNatIListKind# X) (U21#(tt(), V1) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U21#(tt(), V1) -> activate# V1, activate# n__nil() -> nil#()) (U21#(tt(), V1) -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2)) (U21#(tt(), V1) -> activate# V1, activate# n__isNatKind X -> isNatKind# X) (isNat# n__length V1 -> activate# V1, activate# n__zeros() -> zeros#()) (isNat# n__length V1 -> activate# V1, activate# n__0() -> 0#()) (isNat# n__length V1 -> activate# V1, activate# n__length X -> length# X) (isNat# n__length V1 -> activate# V1, activate# n__s X -> s# X) (isNat# n__length V1 -> activate# V1, activate# n__isNatIListKind X -> isNatIListKind# X) (isNat# n__length V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNat# n__length V1 -> activate# V1, activate# n__nil() -> nil#()) (isNat# n__length V1 -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2)) (isNat# n__length V1 -> activate# V1, activate# n__isNatKind X -> isNatKind# X) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#()) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#()) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__isNatIListKind X -> isNatIListKind# X) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#()) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__isNatKind X -> isNatKind# X) (isNatList# n__cons(V1, V2) -> U51#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U51#(tt(), V1, V2) -> activate# V1) (isNatList# n__cons(V1, V2) -> U51#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U51#(tt(), V1, V2) -> activate# V2) (isNatList# n__cons(V1, V2) -> U51#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U51#(tt(), V1, V2) -> isNat# activate V1) (isNatList# n__cons(V1, V2) -> U51#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U51#(tt(), V1, V2) -> U52#(isNat activate V1, activate V2)) (U31#(tt(), V) -> activate# V, activate# n__zeros() -> zeros#()) (U31#(tt(), V) -> activate# V, activate# n__0() -> 0#()) (U31#(tt(), V) -> activate# V, activate# n__length X -> length# X) (U31#(tt(), V) -> activate# V, activate# n__s X -> s# X) (U31#(tt(), V) -> activate# V, activate# n__isNatIListKind X -> isNatIListKind# X) (U31#(tt(), V) -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U31#(tt(), V) -> activate# V, activate# n__nil() -> nil#()) (U31#(tt(), V) -> activate# V, activate# n__and(X1, X2) -> and#(X1, X2)) (U31#(tt(), V) -> activate# V, activate# n__isNatKind X -> isNatKind# X) (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X) (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__isNatIListKind X -> isNatIListKind# X) (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(X1, X2)) (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X) (U52#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#()) (U52#(tt(), V2) -> activate# V2, activate# n__0() -> 0#()) (U52#(tt(), V2) -> activate# V2, activate# n__length X -> length# X) (U52#(tt(), V2) -> activate# V2, activate# n__s X -> s# X) (U52#(tt(), V2) -> activate# V2, activate# n__isNatIListKind X -> isNatIListKind# X) (U52#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U52#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#()) (U52#(tt(), V2) -> activate# V2, activate# n__and(X1, X2) -> and#(X1, X2)) (U52#(tt(), V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X) (U41#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (U41#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#()) (U41#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X) (U41#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X) (U41#(tt(), V1, V2) -> activate# V2, activate# n__isNatIListKind X -> isNatIListKind# X) (U41#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (U41#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (U41#(tt(), V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(X1, X2)) (U41#(tt(), V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#()) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#()) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__isNatIListKind X -> isNatIListKind# X) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#()) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(X1, X2)) (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X) } STATUS: arrows: 0.933063 SCCS (2): Scc: { U42#(tt(), V2) -> isNatIList# activate V2, U41#(tt(), V1, V2) -> U42#(isNat activate V1, activate V2), isNatIList# n__cons(V1, V2) -> U41#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2)} Scc: { isNatList# n__cons(V1, V2) -> activate# V1, isNatList# n__cons(V1, V2) -> activate# V2, isNatList# n__cons(V1, V2) -> U51#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2), isNatList# n__cons(V1, V2) -> isNatKind# activate V1, activate# n__length X -> length# X, activate# n__isNatIListKind X -> isNatIListKind# X, activate# n__and(X1, X2) -> and#(X1, X2), activate# n__isNatKind X -> isNatKind# X, U11#(tt(), V1) -> isNatList# activate V1, U11#(tt(), V1) -> activate# V1, isNat# n__length V1 -> activate# V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), isNat# n__length V1 -> isNatIListKind# activate V1, isNat# n__s V1 -> activate# V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), isNat# n__s V1 -> isNatKind# activate V1, U21#(tt(), V1) -> activate# V1, U21#(tt(), V1) -> isNat# activate V1, U52#(tt(), V2) -> isNatList# activate V2, U52#(tt(), V2) -> activate# V2, U51#(tt(), V1, V2) -> activate# V1, U51#(tt(), V1, V2) -> activate# V2, U51#(tt(), V1, V2) -> isNat# activate V1, U51#(tt(), V1, V2) -> U52#(isNat activate V1, activate V2), length# cons(N, L) -> isNatList# activate L, length# cons(N, L) -> activate# L, length# cons(N, L) -> isNat# N, length# cons(N, L) -> U61#(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length# cons(N, L) -> and#(isNatList activate L, n__isNatIListKind activate L), length# cons(N, L) -> and#(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), U61#(tt(), L) -> activate# L, U61#(tt(), L) -> length# activate L, and#(tt(), X) -> activate# X, isNatIListKind# n__cons(V1, V2) -> activate# V1, isNatIListKind# n__cons(V1, V2) -> activate# V2, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1, isNatKind# n__length V1 -> isNatIListKind# activate V1, isNatKind# n__s V1 -> activate# V1, isNatKind# n__s V1 -> isNatKind# activate V1} SCC (3): Strict: { U42#(tt(), V2) -> isNatIList# activate V2, U41#(tt(), V1, V2) -> U42#(isNat activate V1, activate V2), isNatIList# n__cons(V1, V2) -> U41#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2)} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12 tt() -> tt(), isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList n__nil() -> tt(), 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__isNatIListKind X -> isNatIListKind X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__and(X1, X2) -> and(X1, X2), activate n__isNatKind X -> isNatKind X, U11(tt(), V1) -> U12 isNatList activate V1, U22 tt() -> tt(), isNat n__0() -> tt(), isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1), isNat n__s V1 -> U21(isNatKind activate V1, activate V1), U21(tt(), V1) -> U22 isNat activate V1, U32 tt() -> tt(), U31(tt(), V) -> U32 isNatList activate V, U42(tt(), V2) -> U43 isNatIList activate V2, U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2), U43 tt() -> tt(), isNatIList V -> U31(isNatIListKind activate V, activate V), isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52(tt(), V2) -> U53 isNatList activate V2, U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2), U53 tt() -> tt(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length nil() -> 0(), U61(tt(), L) -> s length activate L, and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate X, isNatIListKind X -> n__isNatIListKind X, isNatIListKind n__zeros() -> tt(), isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind n__nil() -> tt(), isNatKind X -> n__isNatKind X, isNatKind n__0() -> tt(), isNatKind n__length V1 -> isNatIListKind activate V1, isNatKind n__s V1 -> isNatKind activate V1, nil() -> n__nil()} Fail SCC (42): Strict: { isNatList# n__cons(V1, V2) -> activate# V1, isNatList# n__cons(V1, V2) -> activate# V2, isNatList# n__cons(V1, V2) -> U51#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2), isNatList# n__cons(V1, V2) -> isNatKind# activate V1, activate# n__length X -> length# X, activate# n__isNatIListKind X -> isNatIListKind# X, activate# n__and(X1, X2) -> and#(X1, X2), activate# n__isNatKind X -> isNatKind# X, U11#(tt(), V1) -> isNatList# activate V1, U11#(tt(), V1) -> activate# V1, isNat# n__length V1 -> activate# V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), isNat# n__length V1 -> isNatIListKind# activate V1, isNat# n__s V1 -> activate# V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), isNat# n__s V1 -> isNatKind# activate V1, U21#(tt(), V1) -> activate# V1, U21#(tt(), V1) -> isNat# activate V1, U52#(tt(), V2) -> isNatList# activate V2, U52#(tt(), V2) -> activate# V2, U51#(tt(), V1, V2) -> activate# V1, U51#(tt(), V1, V2) -> activate# V2, U51#(tt(), V1, V2) -> isNat# activate V1, U51#(tt(), V1, V2) -> U52#(isNat activate V1, activate V2), length# cons(N, L) -> isNatList# activate L, length# cons(N, L) -> activate# L, length# cons(N, L) -> isNat# N, length# cons(N, L) -> U61#(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length# cons(N, L) -> and#(isNatList activate L, n__isNatIListKind activate L), length# cons(N, L) -> and#(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), U61#(tt(), L) -> activate# L, U61#(tt(), L) -> length# activate L, and#(tt(), X) -> activate# X, isNatIListKind# n__cons(V1, V2) -> activate# V1, isNatIListKind# n__cons(V1, V2) -> activate# V2, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1, isNatKind# n__length V1 -> isNatIListKind# activate V1, isNatKind# n__s V1 -> activate# V1, isNatKind# n__s V1 -> isNatKind# activate V1} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12 tt() -> tt(), isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList n__nil() -> tt(), 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__isNatIListKind X -> isNatIListKind X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__and(X1, X2) -> and(X1, X2), activate n__isNatKind X -> isNatKind X, U11(tt(), V1) -> U12 isNatList activate V1, U22 tt() -> tt(), isNat n__0() -> tt(), isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1), isNat n__s V1 -> U21(isNatKind activate V1, activate V1), U21(tt(), V1) -> U22 isNat activate V1, U32 tt() -> tt(), U31(tt(), V) -> U32 isNatList activate V, U42(tt(), V2) -> U43 isNatIList activate V2, U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2), U43 tt() -> tt(), isNatIList V -> U31(isNatIListKind activate V, activate V), isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52(tt(), V2) -> U53 isNatList activate V2, U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2), U53 tt() -> tt(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length nil() -> 0(), U61(tt(), L) -> s length activate L, and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate X, isNatIListKind X -> n__isNatIListKind X, isNatIListKind n__zeros() -> tt(), isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind n__nil() -> tt(), isNatKind X -> n__isNatKind X, isNatKind n__0() -> tt(), isNatKind n__length V1 -> isNatIListKind activate V1, isNatKind n__s V1 -> isNatKind activate V1, nil() -> n__nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U41](x0, x1, x2) = x0 + x1, [U51](x0, x1, x2) = 0, [cons](x0, x1) = x0 + x1, [U11](x0, x1) = 0, [U21](x0, x1) = 0, [U31](x0, x1) = x0 + x1, [U42](x0, x1) = 0, [U52](x0, x1) = 0, [U61](x0, x1) = x0 + x1 + 1, [and](x0, x1) = x0, [n__cons](x0, x1) = x0 + x1, [n__and](x0, x1) = x0, [U12](x0) = 0, [isNatList](x0) = 0, [activate](x0) = x0, [U22](x0) = 0, [isNat](x0) = 0, [U32](x0) = 0, [U43](x0) = 0, [isNatIList](x0) = 0, [U53](x0) = 0, [s](x0) = x0, [length](x0) = x0 + 1, [isNatIListKind](x0) = x0, [n__length](x0) = x0 + 1, [isNatKind](x0) = x0, [n__s](x0) = x0, [n__isNatIListKind](x0) = x0, [n__isNatKind](x0) = x0, [0] = 0, [n__zeros] = 0, [zeros] = 0, [tt] = 0, [n__0] = 0, [n__nil] = 1, [nil] = 1, [U51#](x0, x1, x2) = x0 + x1, [U11#](x0, x1) = x0, [U21#](x0, x1) = x0, [U52#](x0, x1) = x0, [U61#](x0, x1) = x0, [and#](x0, x1) = x0, [isNatList#](x0) = x0, [activate#](x0) = x0, [isNat#](x0) = x0, [length#](x0) = x0, [isNatIListKind#](x0) = x0, [isNatKind#](x0) = x0 Strict: isNatKind# n__s V1 -> isNatKind# activate V1 0 + 1V1 >= 0 + 1V1 isNatKind# n__s V1 -> activate# V1 0 + 1V1 >= 0 + 1V1 isNatKind# n__length V1 -> isNatIListKind# activate V1 1 + 1V1 >= 0 + 1V1 isNatKind# n__length V1 -> activate# V1 1 + 1V1 >= 0 + 1V1 isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1 0 + 1V1 + 1V2 >= 0 + 1V1 isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2) 0 + 1V1 + 1V2 >= 0 + 0V1 + 1V2 isNatIListKind# n__cons(V1, V2) -> activate# V2 0 + 1V1 + 1V2 >= 0 + 1V2 isNatIListKind# n__cons(V1, V2) -> activate# V1 0 + 1V1 + 1V2 >= 0 + 1V1 and#(tt(), X) -> activate# X 0 + 1X >= 0 + 1X U61#(tt(), L) -> length# activate L 0 + 1L >= 0 + 1L U61#(tt(), L) -> activate# L 0 + 1L >= 0 + 1L length# cons(N, L) -> and#(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)) 0 + 1L + 1N >= 0 + 0L + 1N length# cons(N, L) -> and#(isNatList activate L, n__isNatIListKind activate L) 0 + 1L + 1N >= 0 + 1L length# cons(N, L) -> U61#(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L) 0 + 1L + 1N >= 0 + 1L + 0N length# cons(N, L) -> isNat# N 0 + 1L + 1N >= 0 + 1N length# cons(N, L) -> activate# L 0 + 1L + 1N >= 0 + 1L length# cons(N, L) -> isNatList# activate L 0 + 1L + 1N >= 0 + 1L U51#(tt(), V1, V2) -> U52#(isNat activate V1, activate V2) 0 + 1V1 + 1V2 >= 0 + 0V1 + 1V2 U51#(tt(), V1, V2) -> isNat# activate V1 0 + 1V1 + 1V2 >= 0 + 1V1 U51#(tt(), V1, V2) -> activate# V2 0 + 1V1 + 1V2 >= 0 + 1V2 U51#(tt(), V1, V2) -> activate# V1 0 + 1V1 + 1V2 >= 0 + 1V1 U52#(tt(), V2) -> activate# V2 0 + 1V2 >= 0 + 1V2 U52#(tt(), V2) -> isNatList# activate V2 0 + 1V2 >= 0 + 1V2 U21#(tt(), V1) -> isNat# activate V1 0 + 1V1 >= 0 + 1V1 U21#(tt(), V1) -> activate# V1 0 + 1V1 >= 0 + 1V1 isNat# n__s V1 -> isNatKind# activate V1 0 + 1V1 >= 0 + 1V1 isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1) 0 + 1V1 >= 0 + 1V1 isNat# n__s V1 -> activate# V1 0 + 1V1 >= 0 + 1V1 isNat# n__length V1 -> isNatIListKind# activate V1 1 + 1V1 >= 0 + 1V1 isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1) 1 + 1V1 >= 0 + 1V1 isNat# n__length V1 -> activate# V1 1 + 1V1 >= 0 + 1V1 U11#(tt(), V1) -> activate# V1 0 + 1V1 >= 0 + 1V1 U11#(tt(), V1) -> isNatList# activate V1 0 + 1V1 >= 0 + 1V1 activate# n__isNatKind X -> isNatKind# X 0 + 1X >= 0 + 1X activate# n__and(X1, X2) -> and#(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 activate# n__isNatIListKind X -> isNatIListKind# X 0 + 1X >= 0 + 1X activate# n__length X -> length# X 1 + 1X >= 0 + 1X isNatList# n__cons(V1, V2) -> isNatKind# activate V1 0 + 1V1 + 1V2 >= 0 + 1V1 isNatList# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2) 0 + 1V1 + 1V2 >= 0 + 0V1 + 1V2 isNatList# n__cons(V1, V2) -> U51#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2) 0 + 1V1 + 1V2 >= 0 + 1V1 + 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 Weak: nil() -> n__nil() 1 >= 1 isNatKind n__s V1 -> isNatKind activate V1 0 + 1V1 >= 0 + 1V1 isNatKind n__length V1 -> isNatIListKind activate V1 1 + 1V1 >= 0 + 1V1 isNatKind n__0() -> tt() 0 >= 0 isNatKind X -> n__isNatKind X 0 + 1X >= 0 + 1X isNatIListKind n__nil() -> tt() 1 >= 0 isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2) 0 + 1V1 + 1V2 >= 0 + 0V1 + 1V2 isNatIListKind n__zeros() -> tt() 0 >= 0 isNatIListKind X -> n__isNatIListKind X 0 + 1X >= 0 + 1X and(tt(), X) -> activate X 0 + 1X >= 0 + 1X and(X1, X2) -> n__and(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 U61(tt(), L) -> s length activate L 1 + 1L >= 1 + 1L length nil() -> 0() 2 >= 0 length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L) 1 + 1L + 1N >= 1 + 1L + 1N length X -> n__length X 1 + 1X >= 1 + 1X s X -> n__s X 0 + 1X >= 0 + 1X U53 tt() -> tt() 0 >= 0 U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2) 0 + 0V1 + 0V2 >= 0 + 0V1 + 0V2 U52(tt(), V2) -> U53 isNatList activate V2 0 + 0V2 >= 0 + 0V2 isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2) 0 + 0V1 + 0V2 >= 0 + 0V1 + 2V2 isNatIList n__zeros() -> tt() 0 >= 0 isNatIList V -> U31(isNatIListKind activate V, activate V) 0 + 0V >= 0 + 2V U43 tt() -> tt() 0 >= 0 U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2) 0 + 0V1 + 1V2 >= 0 + 0V1 + 0V2 U42(tt(), V2) -> U43 isNatIList activate V2 0 + 0V2 >= 0 + 0V2 U31(tt(), V) -> U32 isNatList activate V 0 + 1V >= 0 + 0V U32 tt() -> tt() 0 >= 0 U21(tt(), V1) -> U22 isNat activate V1 0 + 0V1 >= 0 + 0V1 isNat n__s V1 -> U21(isNatKind activate V1, activate V1) 0 + 0V1 >= 0 + 0V1 isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1) 0 + 0V1 >= 0 + 0V1 isNat n__0() -> tt() 0 >= 0 U22 tt() -> tt() 0 >= 0 U11(tt(), V1) -> U12 isNatList activate V1 0 + 0V1 >= 0 + 0V1 activate n__isNatKind X -> isNatKind X 0 + 1X >= 0 + 1X activate n__and(X1, X2) -> and(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 activate n__nil() -> nil() 1 >= 1 activate n__cons(X1, X2) -> cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__isNatIListKind X -> isNatIListKind 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 isNatList n__nil() -> tt() 0 >= 0 isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2) 0 + 0V1 + 0V2 >= 0 + 0V1 + 0V2 U12 tt() -> tt() 0 >= 0 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 (4): Scc: {length# cons(N, L) -> U61#(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), U61#(tt(), L) -> length# activate L} Scc: {isNatList# n__cons(V1, V2) -> U51#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52#(tt(), V2) -> isNatList# activate V2, U51#(tt(), V1, V2) -> U52#(isNat activate V1, activate V2)} Scc: {isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> isNat# activate V1} Scc: { activate# n__isNatIListKind X -> isNatIListKind# X, activate# n__and(X1, X2) -> and#(X1, X2), activate# n__isNatKind X -> isNatKind# X, and#(tt(), X) -> activate# X, isNatIListKind# n__cons(V1, V2) -> activate# V1, isNatIListKind# n__cons(V1, V2) -> activate# V2, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1, isNatKind# n__s V1 -> isNatKind# activate V1} SCC (2): Strict: {length# cons(N, L) -> U61#(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), U61#(tt(), L) -> length# activate L} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12 tt() -> tt(), isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList n__nil() -> tt(), 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__isNatIListKind X -> isNatIListKind X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__and(X1, X2) -> and(X1, X2), activate n__isNatKind X -> isNatKind X, U11(tt(), V1) -> U12 isNatList activate V1, U22 tt() -> tt(), isNat n__0() -> tt(), isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1), isNat n__s V1 -> U21(isNatKind activate V1, activate V1), U21(tt(), V1) -> U22 isNat activate V1, U32 tt() -> tt(), U31(tt(), V) -> U32 isNatList activate V, U42(tt(), V2) -> U43 isNatIList activate V2, U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2), U43 tt() -> tt(), isNatIList V -> U31(isNatIListKind activate V, activate V), isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52(tt(), V2) -> U53 isNatList activate V2, U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2), U53 tt() -> tt(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length nil() -> 0(), U61(tt(), L) -> s length activate L, and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate X, isNatIListKind X -> n__isNatIListKind X, isNatIListKind n__zeros() -> tt(), isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind n__nil() -> tt(), isNatKind X -> n__isNatKind X, isNatKind n__0() -> tt(), isNatKind n__length V1 -> isNatIListKind activate V1, isNatKind n__s V1 -> isNatKind activate V1, nil() -> n__nil()} Fail SCC (3): Strict: {isNatList# n__cons(V1, V2) -> U51#(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52#(tt(), V2) -> isNatList# activate V2, U51#(tt(), V1, V2) -> U52#(isNat activate V1, activate V2)} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12 tt() -> tt(), isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList n__nil() -> tt(), 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__isNatIListKind X -> isNatIListKind X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__and(X1, X2) -> and(X1, X2), activate n__isNatKind X -> isNatKind X, U11(tt(), V1) -> U12 isNatList activate V1, U22 tt() -> tt(), isNat n__0() -> tt(), isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1), isNat n__s V1 -> U21(isNatKind activate V1, activate V1), U21(tt(), V1) -> U22 isNat activate V1, U32 tt() -> tt(), U31(tt(), V) -> U32 isNatList activate V, U42(tt(), V2) -> U43 isNatIList activate V2, U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2), U43 tt() -> tt(), isNatIList V -> U31(isNatIListKind activate V, activate V), isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52(tt(), V2) -> U53 isNatList activate V2, U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2), U53 tt() -> tt(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length nil() -> 0(), U61(tt(), L) -> s length activate L, and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate X, isNatIListKind X -> n__isNatIListKind X, isNatIListKind n__zeros() -> tt(), isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind n__nil() -> tt(), isNatKind X -> n__isNatKind X, isNatKind n__0() -> tt(), isNatKind n__length V1 -> isNatIListKind activate V1, isNatKind n__s V1 -> isNatKind activate V1, nil() -> n__nil()} Fail SCC (2): Strict: {isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> isNat# activate V1} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12 tt() -> tt(), isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList n__nil() -> tt(), 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__isNatIListKind X -> isNatIListKind X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__and(X1, X2) -> and(X1, X2), activate n__isNatKind X -> isNatKind X, U11(tt(), V1) -> U12 isNatList activate V1, U22 tt() -> tt(), isNat n__0() -> tt(), isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1), isNat n__s V1 -> U21(isNatKind activate V1, activate V1), U21(tt(), V1) -> U22 isNat activate V1, U32 tt() -> tt(), U31(tt(), V) -> U32 isNatList activate V, U42(tt(), V2) -> U43 isNatIList activate V2, U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2), U43 tt() -> tt(), isNatIList V -> U31(isNatIListKind activate V, activate V), isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52(tt(), V2) -> U53 isNatList activate V2, U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2), U53 tt() -> tt(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length nil() -> 0(), U61(tt(), L) -> s length activate L, and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate X, isNatIListKind X -> n__isNatIListKind X, isNatIListKind n__zeros() -> tt(), isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind n__nil() -> tt(), isNatKind X -> n__isNatKind X, isNatKind n__0() -> tt(), isNatKind n__length V1 -> isNatIListKind activate V1, isNatKind n__s V1 -> isNatKind activate V1, nil() -> n__nil()} Fail SCC (10): Strict: { activate# n__isNatIListKind X -> isNatIListKind# X, activate# n__and(X1, X2) -> and#(X1, X2), activate# n__isNatKind X -> isNatKind# X, and#(tt(), X) -> activate# X, isNatIListKind# n__cons(V1, V2) -> activate# V1, isNatIListKind# n__cons(V1, V2) -> activate# V2, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1, isNatKind# n__s V1 -> isNatKind# activate V1} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12 tt() -> tt(), isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList n__nil() -> tt(), 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__isNatIListKind X -> isNatIListKind X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__and(X1, X2) -> and(X1, X2), activate n__isNatKind X -> isNatKind X, U11(tt(), V1) -> U12 isNatList activate V1, U22 tt() -> tt(), isNat n__0() -> tt(), isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1), isNat n__s V1 -> U21(isNatKind activate V1, activate V1), U21(tt(), V1) -> U22 isNat activate V1, U32 tt() -> tt(), U31(tt(), V) -> U32 isNatList activate V, U42(tt(), V2) -> U43 isNatIList activate V2, U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2), U43 tt() -> tt(), isNatIList V -> U31(isNatIListKind activate V, activate V), isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52(tt(), V2) -> U53 isNatList activate V2, U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2), U53 tt() -> tt(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length nil() -> 0(), U61(tt(), L) -> s length activate L, and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate X, isNatIListKind X -> n__isNatIListKind X, isNatIListKind n__zeros() -> tt(), isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind n__nil() -> tt(), isNatKind X -> n__isNatKind X, isNatKind n__0() -> tt(), isNatKind n__length V1 -> isNatIListKind activate V1, isNatKind n__s V1 -> isNatKind activate V1, nil() -> n__nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U41](x0, x1, x2) = 0, [U51](x0, x1, x2) = x0 + x1, [cons](x0, x1) = x0 + x1, [U11](x0, x1) = 0, [U21](x0, x1) = x0 + x1, [U31](x0, x1) = 0, [U42](x0, x1) = 0, [U52](x0, x1) = 0, [U61](x0, x1) = x0 + 1, [and](x0, x1) = x0 + x1, [n__cons](x0, x1) = x0 + x1, [n__and](x0, x1) = x0 + x1, [U12](x0) = 0, [isNatList](x0) = x0, [activate](x0) = x0, [U22](x0) = 0, [isNat](x0) = 0, [U32](x0) = 0, [U43](x0) = 0, [isNatIList](x0) = 0, [U53](x0) = 0, [s](x0) = x0, [length](x0) = x0 + 1, [isNatIListKind](x0) = x0 + 1, [n__length](x0) = x0 + 1, [isNatKind](x0) = x0, [n__s](x0) = x0, [n__isNatIListKind](x0) = x0 + 1, [n__isNatKind](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, [isNatIListKind#](x0) = x0 + 1, [isNatKind#](x0) = x0 Strict: isNatKind# n__s V1 -> isNatKind# activate V1 0 + 1V1 >= 0 + 1V1 isNatKind# n__s V1 -> activate# V1 0 + 1V1 >= 0 + 1V1 isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1 1 + 1V1 + 1V2 >= 0 + 1V1 isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2) 1 + 1V1 + 1V2 >= 1 + 0V1 + 1V2 isNatIListKind# n__cons(V1, V2) -> activate# V2 1 + 1V1 + 1V2 >= 0 + 1V2 isNatIListKind# n__cons(V1, V2) -> activate# V1 1 + 1V1 + 1V2 >= 0 + 1V1 and#(tt(), X) -> activate# X 0 + 1X >= 0 + 1X activate# n__isNatKind X -> isNatKind# X 0 + 1X >= 0 + 1X activate# n__and(X1, X2) -> and#(X1, X2) 0 + 1X1 + 1X2 >= 0 + 0X1 + 1X2 activate# n__isNatIListKind X -> isNatIListKind# X 1 + 1X >= 1 + 1X Weak: nil() -> n__nil() 1 >= 1 isNatKind n__s V1 -> isNatKind activate V1 0 + 1V1 >= 0 + 1V1 isNatKind n__length V1 -> isNatIListKind activate V1 1 + 1V1 >= 1 + 1V1 isNatKind n__0() -> tt() 0 >= 0 isNatKind X -> n__isNatKind X 0 + 1X >= 0 + 1X isNatIListKind n__nil() -> tt() 2 >= 0 isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2) 1 + 1V1 + 1V2 >= 1 + 1V1 + 1V2 isNatIListKind n__zeros() -> tt() 1 >= 0 isNatIListKind X -> n__isNatIListKind X 1 + 1X >= 1 + 1X and(tt(), X) -> activate X 0 + 1X >= 0 + 1X and(X1, X2) -> n__and(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 U61(tt(), L) -> s length activate L 1 + 1L >= 1 + 1L length nil() -> 0() 2 >= 0 length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind 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 U53 tt() -> tt() 0 >= 0 U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2) 0 + 0V1 + 1V2 >= 0 + 0V1 + 0V2 U52(tt(), V2) -> U53 isNatList activate V2 0 + 0V2 >= 0 + 0V2 isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2) 0 + 0V1 + 0V2 >= 0 + 0V1 + 0V2 isNatIList n__zeros() -> tt() 0 >= 0 isNatIList V -> U31(isNatIListKind activate V, activate V) 0 + 0V >= 0 + 0V U43 tt() -> tt() 0 >= 0 U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2) 0 + 0V1 + 0V2 >= 0 + 0V1 + 0V2 U42(tt(), V2) -> U43 isNatIList activate V2 0 + 0V2 >= 0 + 0V2 U31(tt(), V) -> U32 isNatList activate V 0 + 0V >= 0 + 0V U32 tt() -> tt() 0 >= 0 U21(tt(), V1) -> U22 isNat activate V1 0 + 1V1 >= 0 + 0V1 isNat n__s V1 -> U21(isNatKind activate V1, activate V1) 0 + 0V1 >= 0 + 2V1 isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1) 0 + 0V1 >= 0 + 0V1 isNat n__0() -> tt() 0 >= 0 U22 tt() -> tt() 0 >= 0 U11(tt(), V1) -> U12 isNatList activate V1 0 + 0V1 >= 0 + 0V1 activate n__isNatKind X -> isNatKind X 0 + 1X >= 0 + 1X activate n__and(X1, X2) -> and(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__nil() -> nil() 1 >= 1 activate n__cons(X1, X2) -> cons(X1, X2) 0 + 1X1 + 1X2 >= 0 + 1X1 + 1X2 activate n__isNatIListKind X -> isNatIListKind 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 isNatList n__nil() -> tt() 1 >= 0 isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2) 0 + 1V1 + 1V2 >= 1 + 1V1 + 2V2 U12 tt() -> tt() 0 >= 0 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__isNatIListKind X -> isNatIListKind# X, activate# n__and(X1, X2) -> and#(X1, X2), activate# n__isNatKind X -> isNatKind# X, and#(tt(), X) -> activate# X, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2), isNatKind# n__s V1 -> activate# V1, isNatKind# n__s V1 -> isNatKind# activate V1} SCC (7): Strict: { activate# n__isNatIListKind X -> isNatIListKind# X, activate# n__and(X1, X2) -> and#(X1, X2), activate# n__isNatKind X -> isNatKind# X, and#(tt(), X) -> activate# X, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2), isNatKind# n__s V1 -> activate# V1, isNatKind# n__s V1 -> isNatKind# activate V1} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12 tt() -> tt(), isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList n__nil() -> tt(), 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__isNatIListKind X -> isNatIListKind X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__and(X1, X2) -> and(X1, X2), activate n__isNatKind X -> isNatKind X, U11(tt(), V1) -> U12 isNatList activate V1, U22 tt() -> tt(), isNat n__0() -> tt(), isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1), isNat n__s V1 -> U21(isNatKind activate V1, activate V1), U21(tt(), V1) -> U22 isNat activate V1, U32 tt() -> tt(), U31(tt(), V) -> U32 isNatList activate V, U42(tt(), V2) -> U43 isNatIList activate V2, U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2), U43 tt() -> tt(), isNatIList V -> U31(isNatIListKind activate V, activate V), isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52(tt(), V2) -> U53 isNatList activate V2, U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2), U53 tt() -> tt(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length nil() -> 0(), U61(tt(), L) -> s length activate L, and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate X, isNatIListKind X -> n__isNatIListKind X, isNatIListKind n__zeros() -> tt(), isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind n__nil() -> tt(), isNatKind X -> n__isNatKind X, isNatKind n__0() -> tt(), isNatKind n__length V1 -> isNatIListKind activate V1, isNatKind n__s V1 -> isNatKind activate V1, nil() -> n__nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U41](x0, x1, x2) = 0, [U51](x0, x1, x2) = 0, [cons](x0, x1) = 0, [U11](x0, x1) = 0, [U21](x0, x1) = 0, [U31](x0, x1) = 0, [U42](x0, x1) = 1, [U52](x0, x1) = 0, [U61](x0, x1) = 1, [and](x0, x1) = x0, [n__cons](x0, x1) = 0, [n__and](x0, x1) = x0, [U12](x0) = 0, [isNatList](x0) = 0, [activate](x0) = x0, [U22](x0) = 0, [isNat](x0) = 0, [U32](x0) = 0, [U43](x0) = 0, [isNatIList](x0) = 0, [U53](x0) = 0, [s](x0) = x0, [length](x0) = 1, [isNatIListKind](x0) = 0, [n__length](x0) = 1, [isNatKind](x0) = x0 + 1, [n__s](x0) = x0, [n__isNatIListKind](x0) = 0, [n__isNatKind](x0) = x0 + 1, [0] = 1, [n__zeros] = 0, [zeros] = 0, [tt] = 0, [n__0] = 1, [n__nil] = 0, [nil] = 0, [and#](x0, x1) = x0 + 1, [activate#](x0) = x0 + 1, [isNatIListKind#](x0) = 1, [isNatKind#](x0) = x0 + 1 Strict: isNatKind# n__s V1 -> isNatKind# activate V1 1 + 1V1 >= 1 + 1V1 isNatKind# n__s V1 -> activate# V1 1 + 1V1 >= 1 + 1V1 isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2) 1 + 0V1 + 0V2 >= 1 + 0V1 + 0V2 and#(tt(), X) -> activate# X 1 + 1X >= 1 + 1X activate# n__isNatKind X -> isNatKind# X 2 + 1X >= 1 + 1X activate# n__and(X1, X2) -> and#(X1, X2) 1 + 0X1 + 1X2 >= 1 + 0X1 + 1X2 activate# n__isNatIListKind X -> isNatIListKind# X 1 + 0X >= 1 + 0X Weak: nil() -> n__nil() 0 >= 0 isNatKind n__s V1 -> isNatKind activate V1 1 + 1V1 >= 1 + 1V1 isNatKind n__length V1 -> isNatIListKind activate V1 2 + 0V1 >= 0 + 0V1 isNatKind n__0() -> tt() 2 >= 0 isNatKind X -> n__isNatKind X 1 + 1X >= 1 + 1X isNatIListKind n__nil() -> tt() 0 >= 0 isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2) 0 + 0V1 + 0V2 >= 0 + 0V1 + 0V2 isNatIListKind n__zeros() -> tt() 0 >= 0 isNatIListKind X -> n__isNatIListKind X 0 + 0X >= 0 + 0X and(tt(), X) -> activate X 0 + 1X >= 0 + 1X and(X1, X2) -> n__and(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 U61(tt(), L) -> s length activate L 1 + 0L >= 1 + 0L length nil() -> 0() 1 >= 1 length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L) 1 + 0L + 0N >= 1 + 0L + 0N length X -> n__length X 1 + 0X >= 1 + 0X s X -> n__s X 0 + 1X >= 0 + 1X U53 tt() -> tt() 0 >= 0 U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2) 0 + 0V1 + 0V2 >= 0 + 0V1 + 0V2 U52(tt(), V2) -> U53 isNatList activate V2 0 + 0V2 >= 0 + 0V2 isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2) 0 + 0V1 + 0V2 >= 0 + 0V1 + 0V2 isNatIList n__zeros() -> tt() 0 >= 0 isNatIList V -> U31(isNatIListKind activate V, activate V) 0 + 0V >= 0 + 0V U43 tt() -> tt() 0 >= 0 U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2) 0 + 0V1 + 0V2 >= 1 + 0V1 + 0V2 U42(tt(), V2) -> U43 isNatIList activate V2 1 + 0V2 >= 0 + 0V2 U31(tt(), V) -> U32 isNatList activate V 0 + 0V >= 0 + 0V U32 tt() -> tt() 0 >= 0 U21(tt(), V1) -> U22 isNat activate V1 0 + 0V1 >= 0 + 0V1 isNat n__s V1 -> U21(isNatKind activate V1, activate V1) 0 + 0V1 >= 0 + 0V1 isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1) 0 + 0V1 >= 0 + 0V1 isNat n__0() -> tt() 0 >= 0 U22 tt() -> tt() 0 >= 0 U11(tt(), V1) -> U12 isNatList activate V1 0 + 0V1 >= 0 + 0V1 activate n__isNatKind X -> isNatKind X 1 + 1X >= 1 + 1X activate n__and(X1, X2) -> and(X1, X2) 0 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 activate n__nil() -> nil() 0 >= 0 activate n__cons(X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__isNatIListKind X -> isNatIListKind X 0 + 0X >= 0 + 0X activate n__s X -> s X 0 + 1X >= 0 + 1X activate n__length X -> length X 1 + 0X >= 1 + 0X activate n__0() -> 0() 1 >= 1 activate n__zeros() -> zeros() 0 >= 0 activate X -> X 0 + 1X >= 1X isNatList n__nil() -> tt() 0 >= 0 isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2) 0 + 0V1 + 0V2 >= 0 + 0V1 + 0V2 U12 tt() -> tt() 0 >= 0 zeros() -> n__zeros() 0 >= 0 zeros() -> cons(0(), n__zeros()) 0 >= 0 0() -> n__0() 1 >= 1 cons(X1, X2) -> n__cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (2): Scc: {isNatKind# n__s V1 -> isNatKind# activate V1} Scc: { activate# n__isNatIListKind X -> isNatIListKind# X, activate# n__and(X1, X2) -> and#(X1, X2), and#(tt(), X) -> activate# X, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2)} SCC (1): Strict: {isNatKind# n__s V1 -> isNatKind# activate V1} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12 tt() -> tt(), isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList n__nil() -> tt(), 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__isNatIListKind X -> isNatIListKind X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__and(X1, X2) -> and(X1, X2), activate n__isNatKind X -> isNatKind X, U11(tt(), V1) -> U12 isNatList activate V1, U22 tt() -> tt(), isNat n__0() -> tt(), isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1), isNat n__s V1 -> U21(isNatKind activate V1, activate V1), U21(tt(), V1) -> U22 isNat activate V1, U32 tt() -> tt(), U31(tt(), V) -> U32 isNatList activate V, U42(tt(), V2) -> U43 isNatIList activate V2, U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2), U43 tt() -> tt(), isNatIList V -> U31(isNatIListKind activate V, activate V), isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52(tt(), V2) -> U53 isNatList activate V2, U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2), U53 tt() -> tt(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length nil() -> 0(), U61(tt(), L) -> s length activate L, and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate X, isNatIListKind X -> n__isNatIListKind X, isNatIListKind n__zeros() -> tt(), isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind n__nil() -> tt(), isNatKind X -> n__isNatKind X, isNatKind n__0() -> tt(), isNatKind n__length V1 -> isNatIListKind activate V1, isNatKind n__s V1 -> isNatKind activate V1, nil() -> n__nil()} Fail SCC (4): Strict: { activate# n__isNatIListKind X -> isNatIListKind# X, activate# n__and(X1, X2) -> and#(X1, X2), and#(tt(), X) -> activate# X, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2)} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12 tt() -> tt(), isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList n__nil() -> tt(), 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__isNatIListKind X -> isNatIListKind X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__and(X1, X2) -> and(X1, X2), activate n__isNatKind X -> isNatKind X, U11(tt(), V1) -> U12 isNatList activate V1, U22 tt() -> tt(), isNat n__0() -> tt(), isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1), isNat n__s V1 -> U21(isNatKind activate V1, activate V1), U21(tt(), V1) -> U22 isNat activate V1, U32 tt() -> tt(), U31(tt(), V) -> U32 isNatList activate V, U42(tt(), V2) -> U43 isNatIList activate V2, U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2), U43 tt() -> tt(), isNatIList V -> U31(isNatIListKind activate V, activate V), isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52(tt(), V2) -> U53 isNatList activate V2, U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2), U53 tt() -> tt(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length nil() -> 0(), U61(tt(), L) -> s length activate L, and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate X, isNatIListKind X -> n__isNatIListKind X, isNatIListKind n__zeros() -> tt(), isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind n__nil() -> tt(), isNatKind X -> n__isNatKind X, isNatKind n__0() -> tt(), isNatKind n__length V1 -> isNatIListKind activate V1, isNatKind n__s V1 -> isNatKind activate V1, nil() -> n__nil()} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [U41](x0, x1, x2) = x0, [U51](x0, x1, x2) = 0, [cons](x0, x1) = 0, [U11](x0, x1) = 0, [U21](x0, x1) = 0, [U31](x0, x1) = 0, [U42](x0, x1) = 0, [U52](x0, x1) = 0, [U61](x0, x1) = x0, [and](x0, x1) = x0 + 1, [n__cons](x0, x1) = 0, [n__and](x0, x1) = x0 + 1, [U12](x0) = 0, [isNatList](x0) = 0, [activate](x0) = 0, [U22](x0) = 0, [isNat](x0) = 0, [U32](x0) = 0, [U43](x0) = 0, [isNatIList](x0) = 0, [U53](x0) = 0, [s](x0) = 0, [length](x0) = 0, [isNatIListKind](x0) = 0, [n__length](x0) = 0, [isNatKind](x0) = 0, [n__s](x0) = 0, [n__isNatIListKind](x0) = 0, [n__isNatKind](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, [isNatIListKind#](x0) = 0 Strict: isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2) 0 + 0V1 + 0V2 >= 0 + 0V1 + 0V2 and#(tt(), X) -> activate# X 0 + 1X >= 0 + 1X activate# n__and(X1, X2) -> and#(X1, X2) 1 + 0X1 + 1X2 >= 0 + 0X1 + 1X2 activate# n__isNatIListKind X -> isNatIListKind# X 0 + 0X >= 0 + 0X Weak: nil() -> n__nil() 0 >= 0 isNatKind n__s V1 -> isNatKind activate V1 0 + 0V1 >= 0 + 0V1 isNatKind n__length V1 -> isNatIListKind activate V1 0 + 0V1 >= 0 + 0V1 isNatKind n__0() -> tt() 0 >= 0 isNatKind X -> n__isNatKind X 0 + 0X >= 1 + 0X isNatIListKind n__nil() -> tt() 0 >= 0 isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2) 0 + 0V1 + 0V2 >= 1 + 0V1 + 0V2 isNatIListKind n__zeros() -> tt() 0 >= 0 isNatIListKind X -> n__isNatIListKind X 0 + 0X >= 0 + 0X and(tt(), X) -> activate X 1 + 0X >= 0 + 0X and(X1, X2) -> n__and(X1, X2) 1 + 1X1 + 0X2 >= 1 + 0X1 + 1X2 U61(tt(), L) -> s length activate L 0 + 0L >= 0 + 0L length nil() -> 0() 0 >= 0 length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L) 0 + 0L + 0N >= 2 + 0L + 0N length X -> n__length X 0 + 0X >= 0 + 0X s X -> n__s X 0 + 0X >= 0 + 0X U53 tt() -> tt() 0 >= 0 U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2) 0 + 0V1 + 0V2 >= 0 + 0V1 + 0V2 U52(tt(), V2) -> U53 isNatList activate V2 0 + 0V2 >= 0 + 0V2 isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2) 0 + 0V1 + 0V2 >= 1 + 0V1 + 0V2 isNatIList n__zeros() -> tt() 0 >= 0 isNatIList V -> U31(isNatIListKind activate V, activate V) 0 + 0V >= 0 + 0V U43 tt() -> tt() 0 >= 0 U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2) 0 + 0V1 + 0V2 >= 0 + 0V1 + 0V2 U42(tt(), V2) -> U43 isNatIList activate V2 0 + 0V2 >= 0 + 0V2 U31(tt(), V) -> U32 isNatList activate V 0 + 0V >= 0 + 0V U32 tt() -> tt() 0 >= 0 U21(tt(), V1) -> U22 isNat activate V1 0 + 0V1 >= 0 + 0V1 isNat n__s V1 -> U21(isNatKind activate V1, activate V1) 0 + 0V1 >= 0 + 0V1 isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1) 0 + 0V1 >= 0 + 0V1 isNat n__0() -> tt() 0 >= 0 U22 tt() -> tt() 0 >= 0 U11(tt(), V1) -> U12 isNatList activate V1 0 + 0V1 >= 0 + 0V1 activate n__isNatKind X -> isNatKind X 0 + 0X >= 0 + 0X activate n__and(X1, X2) -> and(X1, X2) 0 + 0X1 + 0X2 >= 1 + 1X1 + 0X2 activate n__nil() -> nil() 0 >= 0 activate n__cons(X1, X2) -> cons(X1, X2) 0 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 activate n__isNatIListKind X -> isNatIListKind X 0 + 0X >= 0 + 0X activate n__s X -> s X 0 + 0X >= 0 + 0X activate n__length X -> length X 0 + 0X >= 0 + 0X activate n__0() -> 0() 0 >= 0 activate n__zeros() -> zeros() 0 >= 0 activate X -> X 0 + 0X >= 1X isNatList n__nil() -> tt() 0 >= 0 isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2) 0 + 0V1 + 0V2 >= 0 + 0V1 + 0V2 U12 tt() -> tt() 0 >= 0 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 + 0X1 + 0X2 >= 0 + 0X1 + 0X2 SCCS (1): Scc: { activate# n__isNatIListKind X -> isNatIListKind# X, and#(tt(), X) -> activate# X, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2)} SCC (3): Strict: { activate# n__isNatIListKind X -> isNatIListKind# X, and#(tt(), X) -> activate# X, isNatIListKind# n__cons(V1, V2) -> and#(isNatKind activate V1, n__isNatIListKind activate V2)} Weak: { cons(X1, X2) -> n__cons(X1, X2), 0() -> n__0(), zeros() -> cons(0(), n__zeros()), zeros() -> n__zeros(), U12 tt() -> tt(), isNatList n__cons(V1, V2) -> U51(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), isNatList n__nil() -> tt(), 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__isNatIListKind X -> isNatIListKind X, activate n__cons(X1, X2) -> cons(X1, X2), activate n__nil() -> nil(), activate n__and(X1, X2) -> and(X1, X2), activate n__isNatKind X -> isNatKind X, U11(tt(), V1) -> U12 isNatList activate V1, U22 tt() -> tt(), isNat n__0() -> tt(), isNat n__length V1 -> U11(isNatIListKind activate V1, activate V1), isNat n__s V1 -> U21(isNatKind activate V1, activate V1), U21(tt(), V1) -> U22 isNat activate V1, U32 tt() -> tt(), U31(tt(), V) -> U32 isNatList activate V, U42(tt(), V2) -> U43 isNatIList activate V2, U41(tt(), V1, V2) -> U42(isNat activate V1, activate V2), U43 tt() -> tt(), isNatIList V -> U31(isNatIListKind activate V, activate V), isNatIList n__zeros() -> tt(), isNatIList n__cons(V1, V2) -> U41(and(isNatKind activate V1, n__isNatIListKind activate V2), activate V1, activate V2), U52(tt(), V2) -> U53 isNatList activate V2, U51(tt(), V1, V2) -> U52(isNat activate V1, activate V2), U53 tt() -> tt(), s X -> n__s X, length X -> n__length X, length cons(N, L) -> U61(and(and(isNatList activate L, n__isNatIListKind activate L), n__and(isNat N, n__isNatKind N)), activate L), length nil() -> 0(), U61(tt(), L) -> s length activate L, and(X1, X2) -> n__and(X1, X2), and(tt(), X) -> activate X, isNatIListKind X -> n__isNatIListKind X, isNatIListKind n__zeros() -> tt(), isNatIListKind n__cons(V1, V2) -> and(isNatKind activate V1, n__isNatIListKind activate V2), isNatIListKind n__nil() -> tt(), isNatKind X -> n__isNatKind X, isNatKind n__0() -> tt(), isNatKind n__length V1 -> isNatIListKind activate V1, isNatKind n__s V1 -> isNatKind activate V1, nil() -> n__nil()} Fail