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