MAYBE Time: 0.056819 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()} Open 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()} Open