MAYBE
Time: 0.315240
TRS:
 {                  cons(X1, X2) -> n__cons(X1, X2),
                             0() -> n__0(),
                         zeros() -> cons(0(), n__zeros()),
                         zeros() -> n__zeros(),
                   U12(tt(), V1) -> U13 isNatList activate V1,
       isNatIListKind n__zeros() -> tt(),
  isNatIListKind n__cons(V1, V2) -> U51(isNatKind activate V1, activate V2),
         isNatIListKind 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__cons(X1, X2) -> cons(X1, X2),
               activate n__nil() -> nil(),
                   U11(tt(), V1) -> U12(isNatIListKind activate V1, activate V1),
                        U13 tt() -> tt(),
       isNatList n__cons(V1, V2) -> U81(isNatKind activate V1, activate V1, activate V2),
              isNatList n__nil() -> tt(),
                   U22(tt(), V1) -> U23 isNat activate V1,
                isNatKind n__0() -> tt(),
          isNatKind n__length V1 -> U61 isNatIListKind activate V1,
               isNatKind n__s V1 -> U71 isNatKind activate V1,
                   U21(tt(), V1) -> U22(isNatKind activate V1, activate V1),
                        U23 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),
                    U32(tt(), V) -> U33 isNatList activate V,
                    U31(tt(), V) -> U32(isNatIListKind activate V, activate V),
                        U33 tt() -> tt(),
               U42(tt(), V1, V2) -> U43(isNatIListKind activate V2, activate V1, activate V2),
               U41(tt(), V1, V2) -> U42(isNatKind activate V1, activate V1, activate V2),
               U43(tt(), V1, V2) -> U44(isNatIListKind activate V2, activate V1, activate V2),
               U44(tt(), V1, V2) -> U45(isNat activate V1, activate V2),
                   U45(tt(), V2) -> U46 isNatIList activate V2,
                        U46 tt() -> tt(),
                    isNatIList V -> U31(isNatIListKind activate V, activate V),
           isNatIList n__zeros() -> tt(),
      isNatIList n__cons(V1, V2) -> U41(isNatKind activate V1, activate V1, activate V2),
                        U52 tt() -> tt(),
                   U51(tt(), V2) -> U52 isNatIListKind activate V2,
                        U61 tt() -> tt(),
                        U71 tt() -> tt(),
               U82(tt(), V1, V2) -> U83(isNatIListKind activate V2, activate V1, activate V2),
               U81(tt(), V1, V2) -> U82(isNatKind activate V1, activate V1, activate V2),
               U83(tt(), V1, V2) -> U84(isNatIListKind activate V2, activate V1, activate V2),
               U84(tt(), V1, V2) -> U85(isNat activate V1, activate V2),
                   U85(tt(), V2) -> U86 isNatList activate V2,
                        U86 tt() -> tt(),
                 U92(tt(), L, N) -> U93(isNat activate N, activate L, activate N),
                 U91(tt(), L, N) -> U92(isNatIListKind activate L, activate L, activate N),
                 U93(tt(), L, N) -> U94(isNatKind activate N, activate L),
                    U94(tt(), L) -> s length activate L,
                             s X -> n__s X,
                        length X -> n__length X,
               length cons(N, L) -> U91(isNatList activate L, activate L, N),
                    length nil() -> 0(),
                           nil() -> n__nil()}
 DP:
  DP:
   {                       zeros#() -> cons#(0(), n__zeros()),
                           zeros#() -> 0#(),
                     U12#(tt(), V1) -> activate# V1,
                     U12#(tt(), V1) -> U13# isNatList activate V1,
                     U12#(tt(), V1) -> isNatList# activate V1,
    isNatIListKind# n__cons(V1, V2) -> activate# V1,
    isNatIListKind# n__cons(V1, V2) -> activate# V2,
    isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1,
    isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2),
               activate# n__zeros() -> zeros#(),
                   activate# n__0() -> 0#(),
              activate# n__length X -> length# X,
                   activate# n__s X -> s# X,
          activate# n__cons(X1, X2) -> cons#(X1, X2),
                 activate# n__nil() -> nil#(),
                     U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1),
                     U11#(tt(), V1) -> isNatIListKind# activate V1,
                     U11#(tt(), V1) -> activate# V1,
         isNatList# n__cons(V1, V2) -> activate# V1,
         isNatList# n__cons(V1, V2) -> activate# V2,
         isNatList# n__cons(V1, V2) -> isNatKind# activate V1,
         isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2),
                     U22#(tt(), V1) -> activate# V1,
                     U22#(tt(), V1) -> U23# isNat activate V1,
                     U22#(tt(), V1) -> isNat# activate V1,
            isNatKind# n__length V1 -> isNatIListKind# activate V1,
            isNatKind# n__length V1 -> activate# V1,
            isNatKind# n__length V1 -> U61# isNatIListKind activate V1,
                 isNatKind# n__s V1 -> activate# V1,
                 isNatKind# n__s V1 -> isNatKind# activate V1,
                 isNatKind# n__s V1 -> U71# isNatKind activate V1,
                     U21#(tt(), V1) -> activate# V1,
                     U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1),
                     U21#(tt(), V1) -> isNatKind# activate V1,
                isNat# n__length V1 -> isNatIListKind# activate V1,
                isNat# n__length V1 -> activate# V1,
                isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1),
                     isNat# n__s V1 -> activate# V1,
                     isNat# n__s V1 -> isNatKind# activate V1,
                     isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1),
                      U32#(tt(), V) -> activate# V,
                      U32#(tt(), V) -> isNatList# activate V,
                      U32#(tt(), V) -> U33# isNatList activate V,
                      U31#(tt(), V) -> isNatIListKind# activate V,
                      U31#(tt(), V) -> activate# V,
                      U31#(tt(), V) -> U32#(isNatIListKind activate V, activate V),
                 U42#(tt(), V1, V2) -> isNatIListKind# activate V2,
                 U42#(tt(), V1, V2) -> activate# V1,
                 U42#(tt(), V1, V2) -> activate# V2,
                 U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2),
                 U41#(tt(), V1, V2) -> activate# V1,
                 U41#(tt(), V1, V2) -> activate# V2,
                 U41#(tt(), V1, V2) -> isNatKind# activate V1,
                 U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2),
                 U43#(tt(), V1, V2) -> isNatIListKind# activate V2,
                 U43#(tt(), V1, V2) -> activate# V1,
                 U43#(tt(), V1, V2) -> activate# V2,
                 U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2),
                 U44#(tt(), V1, V2) -> activate# V1,
                 U44#(tt(), V1, V2) -> activate# V2,
                 U44#(tt(), V1, V2) -> isNat# activate V1,
                 U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2),
                     U45#(tt(), V2) -> activate# V2,
                     U45#(tt(), V2) -> U46# isNatIList activate V2,
                     U45#(tt(), V2) -> isNatIList# activate V2,
                      isNatIList# V -> isNatIListKind# activate V,
                      isNatIList# V -> activate# V,
                      isNatIList# V -> U31#(isNatIListKind activate V, activate V),
        isNatIList# n__cons(V1, V2) -> activate# V1,
        isNatIList# n__cons(V1, V2) -> activate# V2,
        isNatIList# n__cons(V1, V2) -> isNatKind# activate V1,
        isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2),
                     U51#(tt(), V2) -> isNatIListKind# activate V2,
                     U51#(tt(), V2) -> activate# V2,
                     U51#(tt(), V2) -> U52# isNatIListKind activate V2,
                 U82#(tt(), V1, V2) -> isNatIListKind# activate V2,
                 U82#(tt(), V1, V2) -> activate# V1,
                 U82#(tt(), V1, V2) -> activate# V2,
                 U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2),
                 U81#(tt(), V1, V2) -> activate# V1,
                 U81#(tt(), V1, V2) -> activate# V2,
                 U81#(tt(), V1, V2) -> isNatKind# activate V1,
                 U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2),
                 U83#(tt(), V1, V2) -> isNatIListKind# activate V2,
                 U83#(tt(), V1, V2) -> activate# V1,
                 U83#(tt(), V1, V2) -> activate# V2,
                 U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2),
                 U84#(tt(), V1, V2) -> activate# V1,
                 U84#(tt(), V1, V2) -> activate# V2,
                 U84#(tt(), V1, V2) -> isNat# activate V1,
                 U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2),
                     U85#(tt(), V2) -> activate# V2,
                     U85#(tt(), V2) -> isNatList# activate V2,
                     U85#(tt(), V2) -> U86# isNatList activate V2,
                   U92#(tt(), L, N) -> activate# L,
                   U92#(tt(), L, N) -> activate# N,
                   U92#(tt(), L, N) -> isNat# activate N,
                   U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N),
                   U91#(tt(), L, N) -> isNatIListKind# activate L,
                   U91#(tt(), L, N) -> activate# L,
                   U91#(tt(), L, N) -> activate# N,
                   U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N),
                   U93#(tt(), L, N) -> activate# L,
                   U93#(tt(), L, N) -> activate# N,
                   U93#(tt(), L, N) -> isNatKind# activate N,
                   U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L),
                      U94#(tt(), L) -> activate# L,
                      U94#(tt(), L) -> s# length activate L,
                      U94#(tt(), L) -> length# activate L,
                 length# cons(N, L) -> activate# L,
                 length# cons(N, L) -> isNatList# activate L,
                 length# cons(N, L) -> U91#(isNatList activate L, activate L, N),
                      length# nil() -> 0#()}
  TRS:
  {                  cons(X1, X2) -> n__cons(X1, X2),
                              0() -> n__0(),
                          zeros() -> cons(0(), n__zeros()),
                          zeros() -> n__zeros(),
                    U12(tt(), V1) -> U13 isNatList activate V1,
        isNatIListKind n__zeros() -> tt(),
   isNatIListKind n__cons(V1, V2) -> U51(isNatKind activate V1, activate V2),
          isNatIListKind 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__cons(X1, X2) -> cons(X1, X2),
                activate n__nil() -> nil(),
                    U11(tt(), V1) -> U12(isNatIListKind activate V1, activate V1),
                         U13 tt() -> tt(),
        isNatList n__cons(V1, V2) -> U81(isNatKind activate V1, activate V1, activate V2),
               isNatList n__nil() -> tt(),
                    U22(tt(), V1) -> U23 isNat activate V1,
                 isNatKind n__0() -> tt(),
           isNatKind n__length V1 -> U61 isNatIListKind activate V1,
                isNatKind n__s V1 -> U71 isNatKind activate V1,
                    U21(tt(), V1) -> U22(isNatKind activate V1, activate V1),
                         U23 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),
                     U32(tt(), V) -> U33 isNatList activate V,
                     U31(tt(), V) -> U32(isNatIListKind activate V, activate V),
                         U33 tt() -> tt(),
                U42(tt(), V1, V2) -> U43(isNatIListKind activate V2, activate V1, activate V2),
                U41(tt(), V1, V2) -> U42(isNatKind activate V1, activate V1, activate V2),
                U43(tt(), V1, V2) -> U44(isNatIListKind activate V2, activate V1, activate V2),
                U44(tt(), V1, V2) -> U45(isNat activate V1, activate V2),
                    U45(tt(), V2) -> U46 isNatIList activate V2,
                         U46 tt() -> tt(),
                     isNatIList V -> U31(isNatIListKind activate V, activate V),
            isNatIList n__zeros() -> tt(),
       isNatIList n__cons(V1, V2) -> U41(isNatKind activate V1, activate V1, activate V2),
                         U52 tt() -> tt(),
                    U51(tt(), V2) -> U52 isNatIListKind activate V2,
                         U61 tt() -> tt(),
                         U71 tt() -> tt(),
                U82(tt(), V1, V2) -> U83(isNatIListKind activate V2, activate V1, activate V2),
                U81(tt(), V1, V2) -> U82(isNatKind activate V1, activate V1, activate V2),
                U83(tt(), V1, V2) -> U84(isNatIListKind activate V2, activate V1, activate V2),
                U84(tt(), V1, V2) -> U85(isNat activate V1, activate V2),
                    U85(tt(), V2) -> U86 isNatList activate V2,
                         U86 tt() -> tt(),
                  U92(tt(), L, N) -> U93(isNat activate N, activate L, activate N),
                  U91(tt(), L, N) -> U92(isNatIListKind activate L, activate L, activate N),
                  U93(tt(), L, N) -> U94(isNatKind activate N, activate L),
                     U94(tt(), L) -> s length activate L,
                              s X -> n__s X,
                         length X -> n__length X,
                length cons(N, L) -> U91(isNatList activate L, activate L, N),
                     length nil() -> 0(),
                            nil() -> n__nil()}
  UR:
   {                  cons(X1, X2) -> n__cons(X1, X2),
                               0() -> n__0(),
                           zeros() -> cons(0(), n__zeros()),
                           zeros() -> n__zeros(),
                     U12(tt(), V1) -> U13 isNatList activate V1,
         isNatIListKind n__zeros() -> tt(),
    isNatIListKind n__cons(V1, V2) -> U51(isNatKind activate V1, activate V2),
           isNatIListKind 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__cons(X1, X2) -> cons(X1, X2),
                 activate n__nil() -> nil(),
                     U11(tt(), V1) -> U12(isNatIListKind activate V1, activate V1),
                          U13 tt() -> tt(),
         isNatList n__cons(V1, V2) -> U81(isNatKind activate V1, activate V1, activate V2),
                isNatList n__nil() -> tt(),
                     U22(tt(), V1) -> U23 isNat activate V1,
                  isNatKind n__0() -> tt(),
            isNatKind n__length V1 -> U61 isNatIListKind activate V1,
                 isNatKind n__s V1 -> U71 isNatKind activate V1,
                     U21(tt(), V1) -> U22(isNatKind activate V1, activate V1),
                          U23 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),
                      U32(tt(), V) -> U33 isNatList activate V,
                      U31(tt(), V) -> U32(isNatIListKind activate V, activate V),
                          U33 tt() -> tt(),
                 U42(tt(), V1, V2) -> U43(isNatIListKind activate V2, activate V1, activate V2),
                 U41(tt(), V1, V2) -> U42(isNatKind activate V1, activate V1, activate V2),
                 U43(tt(), V1, V2) -> U44(isNatIListKind activate V2, activate V1, activate V2),
                 U44(tt(), V1, V2) -> U45(isNat activate V1, activate V2),
                     U45(tt(), V2) -> U46 isNatIList activate V2,
                          U46 tt() -> tt(),
                      isNatIList V -> U31(isNatIListKind activate V, activate V),
             isNatIList n__zeros() -> tt(),
        isNatIList n__cons(V1, V2) -> U41(isNatKind activate V1, activate V1, activate V2),
                          U52 tt() -> tt(),
                     U51(tt(), V2) -> U52 isNatIListKind activate V2,
                          U61 tt() -> tt(),
                          U71 tt() -> tt(),
                 U82(tt(), V1, V2) -> U83(isNatIListKind activate V2, activate V1, activate V2),
                 U81(tt(), V1, V2) -> U82(isNatKind activate V1, activate V1, activate V2),
                 U83(tt(), V1, V2) -> U84(isNatIListKind activate V2, activate V1, activate V2),
                 U84(tt(), V1, V2) -> U85(isNat activate V1, activate V2),
                     U85(tt(), V2) -> U86 isNatList activate V2,
                          U86 tt() -> tt(),
                   U92(tt(), L, N) -> U93(isNat activate N, activate L, activate N),
                   U91(tt(), L, N) -> U92(isNatIListKind activate L, activate L, activate N),
                   U93(tt(), L, N) -> U94(isNatKind activate N, activate L),
                      U94(tt(), L) -> s length activate L,
                               s X -> n__s X,
                          length X -> n__length X,
                 length cons(N, L) -> U91(isNatList activate L, activate L, N),
                      length nil() -> 0(),
                             nil() -> n__nil(),
                           a(x, y) -> x,
                           a(x, y) -> y}
   EDG:
    {
     (U92#(tt(), L, N) -> activate# L, activate# n__nil() -> nil#())
     (U92#(tt(), L, N) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U92#(tt(), L, N) -> activate# L, activate# n__s X -> s# X)
     (U92#(tt(), L, N) -> activate# L, activate# n__length X -> length# X)
     (U92#(tt(), L, N) -> activate# L, activate# n__0() -> 0#())
     (U92#(tt(), L, N) -> activate# L, activate# n__zeros() -> zeros#())
     (U93#(tt(), L, N) -> activate# L, activate# n__nil() -> nil#())
     (U93#(tt(), L, N) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U93#(tt(), L, N) -> activate# L, activate# n__s X -> s# X)
     (U93#(tt(), L, N) -> activate# L, activate# n__length X -> length# X)
     (U93#(tt(), L, N) -> activate# L, activate# n__0() -> 0#())
     (U93#(tt(), L, N) -> activate# L, activate# n__zeros() -> zeros#())
     (length# cons(N, L) -> activate# L, activate# n__nil() -> nil#())
     (length# cons(N, L) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (length# cons(N, L) -> activate# L, activate# n__s X -> s# X)
     (length# cons(N, L) -> activate# L, activate# n__length X -> length# X)
     (length# cons(N, L) -> activate# L, activate# n__0() -> 0#())
     (length# cons(N, L) -> activate# L, activate# n__zeros() -> zeros#())
     (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__s V1 -> U71# isNatKind activate V1)
     (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__s V1 -> isNatKind# activate V1)
     (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__s V1 -> activate# V1)
     (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
     (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__length V1 -> activate# V1)
     (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__length V1 -> isNatIListKind# activate V1)
     (U94#(tt(), L) -> length# activate L, length# nil() -> 0#())
     (U94#(tt(), L) -> length# activate L, length# cons(N, L) -> U91#(isNatList activate L, activate L, N))
     (U94#(tt(), L) -> length# activate L, length# cons(N, L) -> isNatList# activate L)
     (U94#(tt(), L) -> length# activate L, length# cons(N, L) -> activate# L)
     (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
     (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
     (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
     (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
     (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2))
     (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> isNatKind# activate V1)
     (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> activate# V2)
     (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> activate# V1)
     (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> U31#(isNatIListKind activate V, activate V))
     (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> activate# V)
     (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> isNatIListKind# activate V)
     (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
     (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
     (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
     (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
     (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
     (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> isNatKind# activate V1)
     (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> activate# V2)
     (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> activate# V1)
     (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
     (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
     (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> activate# V2)
     (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> activate# V1)
     (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
     (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> isNatKind# activate V1)
     (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> activate# V2)
     (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> activate# V1)
     (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
     (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
     (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V2)
     (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V1)
     (U22#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
     (U22#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
     (U22#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
     (U22#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
     (U22#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
     (U22#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1)
     (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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 -> U61# isNatIListKind activate V1)
     (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
     (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
     (isNat# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
     (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) -> activate# V2)
     (isNat# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V1)
     (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind activate V1)
     (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
     (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1)
     (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
     (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
     (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
     (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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 -> U61# isNatIListKind activate V1)
     (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
     (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
     (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
     (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
     (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
     (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
     (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
     (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1)
     (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
     (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X)
     (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X)
     (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
     (U42#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
     (U42#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U42#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
     (U42#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
     (U42#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (U42#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
     (U43#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
     (U43#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U43#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
     (U43#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
     (U43#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (U43#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
     (U45#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#())
     (U45#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U45#(tt(), V2) -> activate# V2, activate# n__s X -> s# X)
     (U45#(tt(), V2) -> activate# V2, activate# n__length X -> length# X)
     (U45#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
     (U45#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#())
     (U51#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#())
     (U51#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U51#(tt(), V2) -> activate# V2, activate# n__s X -> s# X)
     (U51#(tt(), V2) -> activate# V2, activate# n__length X -> length# X)
     (U51#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
     (U51#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#())
     (U81#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
     (U81#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U81#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
     (U81#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
     (U81#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (U81#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
     (U84#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
     (U84#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U84#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
     (U84#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
     (U84#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (U84#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
     (U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1), U12#(tt(), V1) -> isNatList# activate V1)
     (U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1), U12#(tt(), V1) -> U13# isNatList activate V1)
     (U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1), U12#(tt(), V1) -> activate# V1)
     (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> activate# V1)
     (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> isNatIListKind# activate V1)
     (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1))
     (U31#(tt(), V) -> U32#(isNatIListKind activate V, activate V), U32#(tt(), V) -> U33# isNatList activate V)
     (U31#(tt(), V) -> U32#(isNatIListKind activate V, activate V), U32#(tt(), V) -> isNatList# activate V)
     (U31#(tt(), V) -> U32#(isNatIListKind activate V, activate V), U32#(tt(), V) -> activate# V)
     (isNatIList# V -> U31#(isNatIListKind activate V, activate V), U31#(tt(), V) -> U32#(isNatIListKind activate V, 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) -> isNatIListKind# activate V)
     (U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L), U94#(tt(), L) -> length# activate L)
     (U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L), U94#(tt(), L) -> s# length activate L)
     (U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L), U94#(tt(), L) -> activate# L)
     (U31#(tt(), V) -> activate# V, activate# n__nil() -> nil#())
     (U31#(tt(), V) -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U31#(tt(), V) -> activate# V, activate# n__s X -> s# X)
     (U31#(tt(), V) -> activate# V, activate# n__length X -> length# X)
     (U31#(tt(), V) -> activate# V, activate# n__0() -> 0#())
     (U31#(tt(), V) -> activate# V, activate# n__zeros() -> zeros#())
     (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2))
     (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> isNatKind# activate V1)
     (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> activate# V2)
     (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> activate# V1)
     (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2))
     (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> activate# V2)
     (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> activate# V1)
     (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> isNatIListKind# activate V2)
     (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2))
     (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> isNatKind# activate V1)
     (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> activate# V2)
     (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> activate# V1)
     (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2))
     (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> activate# V2)
     (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> activate# V1)
     (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> isNatIListKind# activate V2)
     (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L))
     (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> isNatKind# activate N)
     (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> activate# N)
     (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> activate# L)
     (activate# n__length X -> length# X, length# nil() -> 0#())
     (activate# n__length X -> length# X, length# cons(N, L) -> U91#(isNatList activate L, activate L, N))
     (activate# n__length X -> length# X, length# cons(N, L) -> isNatList# activate L)
     (activate# n__length X -> length# X, length# cons(N, L) -> activate# L)
     (U12#(tt(), V1) -> activate# V1, activate# n__nil() -> nil#())
     (U12#(tt(), V1) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U12#(tt(), V1) -> activate# V1, activate# n__s X -> s# X)
     (U12#(tt(), V1) -> activate# V1, activate# n__length X -> length# X)
     (U12#(tt(), V1) -> activate# V1, activate# n__0() -> 0#())
     (U12#(tt(), V1) -> activate# V1, activate# n__zeros() -> zeros#())
     (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__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#())
     (U22#(tt(), V1) -> activate# V1, activate# n__nil() -> nil#())
     (U22#(tt(), V1) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U22#(tt(), V1) -> activate# V1, activate# n__s X -> s# X)
     (U22#(tt(), V1) -> activate# V1, activate# n__length X -> length# X)
     (U22#(tt(), V1) -> activate# V1, activate# n__0() -> 0#())
     (U22#(tt(), V1) -> activate# V1, activate# n__zeros() -> zeros#())
     (isNatKind# n__s V1 -> activate# V1, activate# n__nil() -> nil#())
     (isNatKind# n__s V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (isNatKind# n__s V1 -> activate# V1, activate# n__s X -> s# X)
     (isNatKind# n__s V1 -> activate# V1, activate# n__length X -> length# X)
     (isNatKind# n__s V1 -> activate# V1, activate# n__0() -> 0#())
     (isNatKind# n__s V1 -> activate# V1, activate# n__zeros() -> zeros#())
     (isNat# n__length V1 -> activate# V1, activate# n__nil() -> nil#())
     (isNat# n__length V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (isNat# n__length V1 -> activate# V1, activate# n__s X -> s# X)
     (isNat# n__length V1 -> activate# V1, activate# n__length X -> length# X)
     (isNat# n__length V1 -> activate# V1, activate# n__0() -> 0#())
     (isNat# n__length V1 -> activate# V1, activate# n__zeros() -> zeros#())
     (U42#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
     (U42#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U42#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
     (U42#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
     (U42#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
     (U42#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
     (U43#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
     (U43#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U43#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
     (U43#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
     (U43#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
     (U43#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
     (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
     (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X)
     (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X)
     (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#())
     (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
     (U81#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
     (U81#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U81#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
     (U81#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
     (U81#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
     (U81#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
     (U84#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
     (U84#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U84#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
     (U84#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
     (U84#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
     (U84#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
     (U91#(tt(), L, N) -> activate# N, activate# n__nil() -> nil#())
     (U91#(tt(), L, N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U91#(tt(), L, N) -> activate# N, activate# n__s X -> s# X)
     (U91#(tt(), L, N) -> activate# N, activate# n__length X -> length# X)
     (U91#(tt(), L, N) -> activate# N, activate# n__0() -> 0#())
     (U91#(tt(), L, N) -> activate# N, activate# n__zeros() -> zeros#())
     (U93#(tt(), L, N) -> activate# N, activate# n__zeros() -> zeros#())
     (U93#(tt(), L, N) -> activate# N, activate# n__0() -> 0#())
     (U93#(tt(), L, N) -> activate# N, activate# n__length X -> length# X)
     (U93#(tt(), L, N) -> activate# N, activate# n__s X -> s# X)
     (U93#(tt(), L, N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U93#(tt(), L, N) -> activate# N, activate# n__nil() -> nil#())
     (U92#(tt(), L, N) -> activate# N, activate# n__zeros() -> zeros#())
     (U92#(tt(), L, N) -> activate# N, activate# n__0() -> 0#())
     (U92#(tt(), L, N) -> activate# N, activate# n__length X -> length# X)
     (U92#(tt(), L, N) -> activate# N, activate# n__s X -> s# X)
     (U92#(tt(), L, N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U92#(tt(), L, N) -> activate# N, activate# n__nil() -> nil#())
     (U83#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
     (U83#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
     (U83#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
     (U83#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
     (U83#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U83#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
     (U82#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
     (U82#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
     (U82#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
     (U82#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
     (U82#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U82#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
     (U44#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
     (U44#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
     (U44#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
     (U44#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
     (U44#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U44#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
     (U41#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
     (U41#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
     (U41#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
     (U41#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
     (U41#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U41#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
     (isNat# n__s V1 -> activate# V1, activate# n__zeros() -> zeros#())
     (isNat# n__s V1 -> activate# V1, activate# n__0() -> 0#())
     (isNat# n__s V1 -> activate# V1, activate# n__length X -> length# X)
     (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# X)
     (isNat# n__s V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (isNat# n__s V1 -> activate# V1, activate# n__nil() -> nil#())
     (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__cons(X1, X2) -> cons#(X1, X2))
     (U21#(tt(), V1) -> activate# V1, activate# n__nil() -> nil#())
     (isNatKind# n__length V1 -> activate# V1, activate# n__zeros() -> zeros#())
     (isNatKind# n__length V1 -> activate# V1, activate# n__0() -> 0#())
     (isNatKind# n__length V1 -> activate# V1, activate# n__length X -> length# X)
     (isNatKind# n__length V1 -> activate# V1, activate# n__s X -> s# X)
     (isNatKind# n__length V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (isNatKind# n__length V1 -> activate# V1, activate# n__nil() -> nil#())
     (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__cons(X1, X2) -> cons#(X1, X2))
     (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
     (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__cons(X1, X2) -> cons#(X1, X2))
     (isNatIListKind# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
     (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> activate# L)
     (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> activate# N)
     (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> isNat# activate N)
     (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N))
     (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> activate# V1)
     (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> activate# V2)
     (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> isNat# activate V1)
     (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2))
     (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> isNatIListKind# activate V2)
     (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> activate# V1)
     (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> activate# V2)
     (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2))
     (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> activate# V1)
     (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> activate# V2)
     (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> isNat# activate V1)
     (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2))
     (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> isNatIListKind# activate V2)
     (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> activate# V1)
     (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> activate# V2)
     (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2))
     (isNatIList# V -> activate# V, activate# n__zeros() -> zeros#())
     (isNatIList# V -> activate# V, activate# n__0() -> 0#())
     (isNatIList# V -> activate# V, activate# n__length X -> length# X)
     (isNatIList# V -> activate# V, activate# n__s X -> s# X)
     (isNatIList# V -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (isNatIList# V -> activate# V, activate# n__nil() -> nil#())
     (U32#(tt(), V) -> activate# V, activate# n__zeros() -> zeros#())
     (U32#(tt(), V) -> activate# V, activate# n__0() -> 0#())
     (U32#(tt(), V) -> activate# V, activate# n__length X -> length# X)
     (U32#(tt(), V) -> activate# V, activate# n__s X -> s# X)
     (U32#(tt(), V) -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U32#(tt(), V) -> activate# V, activate# n__nil() -> nil#())
     (U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2), U85#(tt(), V2) -> activate# V2)
     (U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2), U85#(tt(), V2) -> isNatList# activate V2)
     (U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2), U85#(tt(), V2) -> U86# isNatList activate V2)
     (U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2), U45#(tt(), V2) -> activate# V2)
     (U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2), U45#(tt(), V2) -> U46# isNatIList activate V2)
     (U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2), U45#(tt(), V2) -> isNatIList# activate V2)
     (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> activate# V1)
     (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1))
     (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> isNatKind# activate V1)
     (U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U22#(tt(), V1) -> activate# V1)
     (U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U22#(tt(), V1) -> U23# isNat activate V1)
     (U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U22#(tt(), V1) -> isNat# activate V1)
     (isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2), U51#(tt(), V2) -> isNatIListKind# activate V2)
     (isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2), U51#(tt(), V2) -> activate# V2)
     (isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2), U51#(tt(), V2) -> U52# isNatIListKind activate V2)
     (activate# n__zeros() -> zeros#(), zeros#() -> cons#(0(), n__zeros()))
     (activate# n__zeros() -> zeros#(), zeros#() -> 0#())
     (U85#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#())
     (U85#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
     (U85#(tt(), V2) -> activate# V2, activate# n__length X -> length# X)
     (U85#(tt(), V2) -> activate# V2, activate# n__s X -> s# X)
     (U85#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U85#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#())
     (U83#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
     (U83#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (U83#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
     (U83#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
     (U83#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U83#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
     (U82#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
     (U82#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (U82#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
     (U82#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
     (U82#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U82#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
     (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
     (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X)
     (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X)
     (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
     (U44#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
     (U44#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (U44#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
     (U44#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
     (U44#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U44#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
     (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__cons(X1, X2) -> cons#(X1, X2))
     (U41#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
     (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__cons(X1, X2) -> cons#(X1, X2))
     (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
     (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> isNatIListKind# activate L)
     (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> activate# L)
     (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> activate# N)
     (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N))
     (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
     (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
     (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
     (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1)
     (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
     (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind activate V1)
     (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1)
     (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
     (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
     (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
     (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
     (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate 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__length V1 -> activate# V1)
     (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# 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)
     (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind activate V1)
     (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
     (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
     (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
     (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1)
     (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
     (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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) -> isNatKind# activate V1)
     (isNatKind# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
     (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)
     (isNatList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind 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__s V1 -> isNatKind# activate V1)
     (isNatList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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)
     (isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind 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__s V1 -> isNatKind# activate V1)
     (isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# 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) -> isNatKind# activate V1)
     (isNatIList# V -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
     (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> activate# V1)
     (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> activate# V2)
     (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> isNatKind# activate V1)
     (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
     (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
     (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
     (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
     (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
     (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
     (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
     (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
     (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
     (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
     (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
     (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
     (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
     (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> activate# V1)
     (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) -> isNatKind# activate V1)
     (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
     (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> activate# V1)
     (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> activate# V2)
     (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
     (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
     (U92#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> isNatIListKind# activate V1)
     (U92#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> activate# V1)
     (U92#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
     (U92#(tt(), L, N) -> isNat# activate N, isNat# n__s V1 -> activate# V1)
     (U92#(tt(), L, N) -> isNat# activate N, isNat# n__s V1 -> isNatKind# activate V1)
     (U92#(tt(), L, N) -> isNat# activate N, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
     (U94#(tt(), L) -> activate# L, activate# n__zeros() -> zeros#())
     (U94#(tt(), L) -> activate# L, activate# n__0() -> 0#())
     (U94#(tt(), L) -> activate# L, activate# n__length X -> length# X)
     (U94#(tt(), L) -> activate# L, activate# n__s X -> s# X)
     (U94#(tt(), L) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U94#(tt(), L) -> activate# L, activate# n__nil() -> nil#())
     (U91#(tt(), L, N) -> activate# L, activate# n__zeros() -> zeros#())
     (U91#(tt(), L, N) -> activate# L, activate# n__0() -> 0#())
     (U91#(tt(), L, N) -> activate# L, activate# n__length X -> length# X)
     (U91#(tt(), L, N) -> activate# L, activate# n__s X -> s# X)
     (U91#(tt(), L, N) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
     (U91#(tt(), L, N) -> activate# L, activate# n__nil() -> nil#())
    }
    EDG:
     {
      (U92#(tt(), L, N) -> activate# L, activate# n__nil() -> nil#())
      (U92#(tt(), L, N) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U92#(tt(), L, N) -> activate# L, activate# n__s X -> s# X)
      (U92#(tt(), L, N) -> activate# L, activate# n__length X -> length# X)
      (U92#(tt(), L, N) -> activate# L, activate# n__0() -> 0#())
      (U92#(tt(), L, N) -> activate# L, activate# n__zeros() -> zeros#())
      (U93#(tt(), L, N) -> activate# L, activate# n__nil() -> nil#())
      (U93#(tt(), L, N) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U93#(tt(), L, N) -> activate# L, activate# n__s X -> s# X)
      (U93#(tt(), L, N) -> activate# L, activate# n__length X -> length# X)
      (U93#(tt(), L, N) -> activate# L, activate# n__0() -> 0#())
      (U93#(tt(), L, N) -> activate# L, activate# n__zeros() -> zeros#())
      (length# cons(N, L) -> activate# L, activate# n__nil() -> nil#())
      (length# cons(N, L) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (length# cons(N, L) -> activate# L, activate# n__s X -> s# X)
      (length# cons(N, L) -> activate# L, activate# n__length X -> length# X)
      (length# cons(N, L) -> activate# L, activate# n__0() -> 0#())
      (length# cons(N, L) -> activate# L, activate# n__zeros() -> zeros#())
      (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__s V1 -> U71# isNatKind activate V1)
      (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__s V1 -> isNatKind# activate V1)
      (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__s V1 -> activate# V1)
      (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
      (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__length V1 -> activate# V1)
      (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__length V1 -> isNatIListKind# activate V1)
      (U94#(tt(), L) -> length# activate L, length# nil() -> 0#())
      (U94#(tt(), L) -> length# activate L, length# cons(N, L) -> U91#(isNatList activate L, activate L, N))
      (U94#(tt(), L) -> length# activate L, length# cons(N, L) -> isNatList# activate L)
      (U94#(tt(), L) -> length# activate L, length# cons(N, L) -> activate# L)
      (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
      (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
      (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
      (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
      (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2))
      (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> isNatKind# activate V1)
      (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> activate# V2)
      (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> activate# V1)
      (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> U31#(isNatIListKind activate V, activate V))
      (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> activate# V)
      (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> isNatIListKind# activate V)
      (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
      (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
      (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
      (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
      (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
      (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> isNatKind# activate V1)
      (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> activate# V2)
      (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> activate# V1)
      (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
      (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
      (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> activate# V2)
      (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> activate# V1)
      (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
      (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> isNatKind# activate V1)
      (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> activate# V2)
      (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> activate# V1)
      (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
      (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
      (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V2)
      (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V1)
      (U22#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
      (U22#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
      (U22#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
      (U22#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
      (U22#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
      (U22#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1)
      (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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 -> U61# isNatIListKind activate V1)
      (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
      (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
      (isNat# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
      (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) -> activate# V2)
      (isNat# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V1)
      (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind activate V1)
      (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
      (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1)
      (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
      (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
      (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
      (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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 -> U61# isNatIListKind activate V1)
      (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
      (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
      (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
      (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
      (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
      (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
      (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
      (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1)
      (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
      (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X)
      (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X)
      (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#())
      (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
      (U42#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
      (U42#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U42#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
      (U42#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
      (U42#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
      (U42#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
      (U43#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
      (U43#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U43#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
      (U43#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
      (U43#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
      (U43#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
      (U45#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#())
      (U45#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U45#(tt(), V2) -> activate# V2, activate# n__s X -> s# X)
      (U45#(tt(), V2) -> activate# V2, activate# n__length X -> length# X)
      (U45#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
      (U45#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#())
      (U51#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#())
      (U51#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U51#(tt(), V2) -> activate# V2, activate# n__s X -> s# X)
      (U51#(tt(), V2) -> activate# V2, activate# n__length X -> length# X)
      (U51#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
      (U51#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#())
      (U81#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
      (U81#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U81#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
      (U81#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
      (U81#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
      (U81#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
      (U84#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
      (U84#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U84#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
      (U84#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
      (U84#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
      (U84#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
      (U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1), U12#(tt(), V1) -> isNatList# activate V1)
      (U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1), U12#(tt(), V1) -> U13# isNatList activate V1)
      (U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1), U12#(tt(), V1) -> activate# V1)
      (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> activate# V1)
      (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> isNatIListKind# activate V1)
      (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1))
      (U31#(tt(), V) -> U32#(isNatIListKind activate V, activate V), U32#(tt(), V) -> U33# isNatList activate V)
      (U31#(tt(), V) -> U32#(isNatIListKind activate V, activate V), U32#(tt(), V) -> isNatList# activate V)
      (U31#(tt(), V) -> U32#(isNatIListKind activate V, activate V), U32#(tt(), V) -> activate# V)
      (isNatIList# V -> U31#(isNatIListKind activate V, activate V), U31#(tt(), V) -> U32#(isNatIListKind activate V, 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) -> isNatIListKind# activate V)
      (U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L), U94#(tt(), L) -> length# activate L)
      (U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L), U94#(tt(), L) -> s# length activate L)
      (U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L), U94#(tt(), L) -> activate# L)
      (U31#(tt(), V) -> activate# V, activate# n__nil() -> nil#())
      (U31#(tt(), V) -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U31#(tt(), V) -> activate# V, activate# n__s X -> s# X)
      (U31#(tt(), V) -> activate# V, activate# n__length X -> length# X)
      (U31#(tt(), V) -> activate# V, activate# n__0() -> 0#())
      (U31#(tt(), V) -> activate# V, activate# n__zeros() -> zeros#())
      (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2))
      (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> isNatKind# activate V1)
      (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> activate# V2)
      (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> activate# V1)
      (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2))
      (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> activate# V2)
      (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> activate# V1)
      (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> isNatIListKind# activate V2)
      (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2))
      (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> isNatKind# activate V1)
      (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> activate# V2)
      (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> activate# V1)
      (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2))
      (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> activate# V2)
      (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> activate# V1)
      (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> isNatIListKind# activate V2)
      (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L))
      (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> isNatKind# activate N)
      (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> activate# N)
      (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> activate# L)
      (activate# n__length X -> length# X, length# nil() -> 0#())
      (activate# n__length X -> length# X, length# cons(N, L) -> U91#(isNatList activate L, activate L, N))
      (activate# n__length X -> length# X, length# cons(N, L) -> isNatList# activate L)
      (activate# n__length X -> length# X, length# cons(N, L) -> activate# L)
      (U12#(tt(), V1) -> activate# V1, activate# n__nil() -> nil#())
      (U12#(tt(), V1) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U12#(tt(), V1) -> activate# V1, activate# n__s X -> s# X)
      (U12#(tt(), V1) -> activate# V1, activate# n__length X -> length# X)
      (U12#(tt(), V1) -> activate# V1, activate# n__0() -> 0#())
      (U12#(tt(), V1) -> activate# V1, activate# n__zeros() -> zeros#())
      (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__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#())
      (U22#(tt(), V1) -> activate# V1, activate# n__nil() -> nil#())
      (U22#(tt(), V1) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U22#(tt(), V1) -> activate# V1, activate# n__s X -> s# X)
      (U22#(tt(), V1) -> activate# V1, activate# n__length X -> length# X)
      (U22#(tt(), V1) -> activate# V1, activate# n__0() -> 0#())
      (U22#(tt(), V1) -> activate# V1, activate# n__zeros() -> zeros#())
      (isNatKind# n__s V1 -> activate# V1, activate# n__nil() -> nil#())
      (isNatKind# n__s V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (isNatKind# n__s V1 -> activate# V1, activate# n__s X -> s# X)
      (isNatKind# n__s V1 -> activate# V1, activate# n__length X -> length# X)
      (isNatKind# n__s V1 -> activate# V1, activate# n__0() -> 0#())
      (isNatKind# n__s V1 -> activate# V1, activate# n__zeros() -> zeros#())
      (isNat# n__length V1 -> activate# V1, activate# n__nil() -> nil#())
      (isNat# n__length V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (isNat# n__length V1 -> activate# V1, activate# n__s X -> s# X)
      (isNat# n__length V1 -> activate# V1, activate# n__length X -> length# X)
      (isNat# n__length V1 -> activate# V1, activate# n__0() -> 0#())
      (isNat# n__length V1 -> activate# V1, activate# n__zeros() -> zeros#())
      (U42#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
      (U42#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U42#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
      (U42#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
      (U42#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
      (U42#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
      (U43#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
      (U43#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U43#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
      (U43#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
      (U43#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
      (U43#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
      (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
      (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X)
      (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X)
      (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#())
      (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
      (U81#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
      (U81#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U81#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
      (U81#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
      (U81#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
      (U81#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
      (U84#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
      (U84#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U84#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
      (U84#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
      (U84#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
      (U84#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
      (U91#(tt(), L, N) -> activate# N, activate# n__nil() -> nil#())
      (U91#(tt(), L, N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U91#(tt(), L, N) -> activate# N, activate# n__s X -> s# X)
      (U91#(tt(), L, N) -> activate# N, activate# n__length X -> length# X)
      (U91#(tt(), L, N) -> activate# N, activate# n__0() -> 0#())
      (U91#(tt(), L, N) -> activate# N, activate# n__zeros() -> zeros#())
      (U93#(tt(), L, N) -> activate# N, activate# n__zeros() -> zeros#())
      (U93#(tt(), L, N) -> activate# N, activate# n__0() -> 0#())
      (U93#(tt(), L, N) -> activate# N, activate# n__length X -> length# X)
      (U93#(tt(), L, N) -> activate# N, activate# n__s X -> s# X)
      (U93#(tt(), L, N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U93#(tt(), L, N) -> activate# N, activate# n__nil() -> nil#())
      (U92#(tt(), L, N) -> activate# N, activate# n__zeros() -> zeros#())
      (U92#(tt(), L, N) -> activate# N, activate# n__0() -> 0#())
      (U92#(tt(), L, N) -> activate# N, activate# n__length X -> length# X)
      (U92#(tt(), L, N) -> activate# N, activate# n__s X -> s# X)
      (U92#(tt(), L, N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U92#(tt(), L, N) -> activate# N, activate# n__nil() -> nil#())
      (U83#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
      (U83#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
      (U83#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
      (U83#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
      (U83#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U83#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
      (U82#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
      (U82#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
      (U82#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
      (U82#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
      (U82#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U82#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
      (U44#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
      (U44#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
      (U44#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
      (U44#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
      (U44#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U44#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
      (U41#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
      (U41#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
      (U41#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
      (U41#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
      (U41#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U41#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
      (isNat# n__s V1 -> activate# V1, activate# n__zeros() -> zeros#())
      (isNat# n__s V1 -> activate# V1, activate# n__0() -> 0#())
      (isNat# n__s V1 -> activate# V1, activate# n__length X -> length# X)
      (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# X)
      (isNat# n__s V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (isNat# n__s V1 -> activate# V1, activate# n__nil() -> nil#())
      (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__cons(X1, X2) -> cons#(X1, X2))
      (U21#(tt(), V1) -> activate# V1, activate# n__nil() -> nil#())
      (isNatKind# n__length V1 -> activate# V1, activate# n__zeros() -> zeros#())
      (isNatKind# n__length V1 -> activate# V1, activate# n__0() -> 0#())
      (isNatKind# n__length V1 -> activate# V1, activate# n__length X -> length# X)
      (isNatKind# n__length V1 -> activate# V1, activate# n__s X -> s# X)
      (isNatKind# n__length V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (isNatKind# n__length V1 -> activate# V1, activate# n__nil() -> nil#())
      (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__cons(X1, X2) -> cons#(X1, X2))
      (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
      (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__cons(X1, X2) -> cons#(X1, X2))
      (isNatIListKind# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
      (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> activate# L)
      (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> activate# N)
      (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> isNat# activate N)
      (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N))
      (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> activate# V1)
      (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> activate# V2)
      (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> isNat# activate V1)
      (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2))
      (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> isNatIListKind# activate V2)
      (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> activate# V1)
      (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> activate# V2)
      (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2))
      (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> activate# V1)
      (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> activate# V2)
      (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> isNat# activate V1)
      (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2))
      (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> isNatIListKind# activate V2)
      (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> activate# V1)
      (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> activate# V2)
      (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2))
      (isNatIList# V -> activate# V, activate# n__zeros() -> zeros#())
      (isNatIList# V -> activate# V, activate# n__0() -> 0#())
      (isNatIList# V -> activate# V, activate# n__length X -> length# X)
      (isNatIList# V -> activate# V, activate# n__s X -> s# X)
      (isNatIList# V -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (isNatIList# V -> activate# V, activate# n__nil() -> nil#())
      (U32#(tt(), V) -> activate# V, activate# n__zeros() -> zeros#())
      (U32#(tt(), V) -> activate# V, activate# n__0() -> 0#())
      (U32#(tt(), V) -> activate# V, activate# n__length X -> length# X)
      (U32#(tt(), V) -> activate# V, activate# n__s X -> s# X)
      (U32#(tt(), V) -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U32#(tt(), V) -> activate# V, activate# n__nil() -> nil#())
      (U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2), U85#(tt(), V2) -> activate# V2)
      (U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2), U85#(tt(), V2) -> isNatList# activate V2)
      (U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2), U85#(tt(), V2) -> U86# isNatList activate V2)
      (U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2), U45#(tt(), V2) -> activate# V2)
      (U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2), U45#(tt(), V2) -> U46# isNatIList activate V2)
      (U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2), U45#(tt(), V2) -> isNatIList# activate V2)
      (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> activate# V1)
      (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1))
      (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> isNatKind# activate V1)
      (U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U22#(tt(), V1) -> activate# V1)
      (U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U22#(tt(), V1) -> U23# isNat activate V1)
      (U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U22#(tt(), V1) -> isNat# activate V1)
      (isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2), U51#(tt(), V2) -> isNatIListKind# activate V2)
      (isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2), U51#(tt(), V2) -> activate# V2)
      (isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2), U51#(tt(), V2) -> U52# isNatIListKind activate V2)
      (activate# n__zeros() -> zeros#(), zeros#() -> cons#(0(), n__zeros()))
      (activate# n__zeros() -> zeros#(), zeros#() -> 0#())
      (U85#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#())
      (U85#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
      (U85#(tt(), V2) -> activate# V2, activate# n__length X -> length# X)
      (U85#(tt(), V2) -> activate# V2, activate# n__s X -> s# X)
      (U85#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U85#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#())
      (U83#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
      (U83#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
      (U83#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
      (U83#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
      (U83#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U83#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
      (U82#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
      (U82#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
      (U82#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
      (U82#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
      (U82#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U82#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
      (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
      (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#())
      (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X)
      (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X)
      (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
      (U44#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
      (U44#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
      (U44#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
      (U44#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
      (U44#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U44#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
      (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__cons(X1, X2) -> cons#(X1, X2))
      (U41#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
      (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__cons(X1, X2) -> cons#(X1, X2))
      (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
      (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> isNatIListKind# activate L)
      (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> activate# L)
      (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> activate# N)
      (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N))
      (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
      (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
      (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
      (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1)
      (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
      (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind activate V1)
      (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1)
      (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
      (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
      (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
      (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
      (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate 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__length V1 -> activate# V1)
      (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# 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)
      (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind activate V1)
      (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
      (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
      (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
      (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1)
      (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
      (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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) -> isNatKind# activate V1)
      (isNatKind# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
      (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)
      (isNatList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind 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__s V1 -> isNatKind# activate V1)
      (isNatList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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)
      (isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind 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__s V1 -> isNatKind# activate V1)
      (isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# 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) -> isNatKind# activate V1)
      (isNatIList# V -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
      (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> activate# V1)
      (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> activate# V2)
      (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> isNatKind# activate V1)
      (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
      (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
      (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
      (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
      (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
      (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
      (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
      (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
      (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
      (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
      (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
      (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
      (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
      (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> activate# V1)
      (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) -> isNatKind# activate V1)
      (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
      (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> activate# V1)
      (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> activate# V2)
      (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
      (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
      (U92#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> isNatIListKind# activate V1)
      (U92#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> activate# V1)
      (U92#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
      (U92#(tt(), L, N) -> isNat# activate N, isNat# n__s V1 -> activate# V1)
      (U92#(tt(), L, N) -> isNat# activate N, isNat# n__s V1 -> isNatKind# activate V1)
      (U92#(tt(), L, N) -> isNat# activate N, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
      (U94#(tt(), L) -> activate# L, activate# n__zeros() -> zeros#())
      (U94#(tt(), L) -> activate# L, activate# n__0() -> 0#())
      (U94#(tt(), L) -> activate# L, activate# n__length X -> length# X)
      (U94#(tt(), L) -> activate# L, activate# n__s X -> s# X)
      (U94#(tt(), L) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U94#(tt(), L) -> activate# L, activate# n__nil() -> nil#())
      (U91#(tt(), L, N) -> activate# L, activate# n__zeros() -> zeros#())
      (U91#(tt(), L, N) -> activate# L, activate# n__0() -> 0#())
      (U91#(tt(), L, N) -> activate# L, activate# n__length X -> length# X)
      (U91#(tt(), L, N) -> activate# L, activate# n__s X -> s# X)
      (U91#(tt(), L, N) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
      (U91#(tt(), L, N) -> activate# L, activate# n__nil() -> nil#())
     }
     EDG:
      {
       (U92#(tt(), L, N) -> activate# L, activate# n__nil() -> nil#())
       (U92#(tt(), L, N) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U92#(tt(), L, N) -> activate# L, activate# n__s X -> s# X)
       (U92#(tt(), L, N) -> activate# L, activate# n__length X -> length# X)
       (U92#(tt(), L, N) -> activate# L, activate# n__0() -> 0#())
       (U92#(tt(), L, N) -> activate# L, activate# n__zeros() -> zeros#())
       (U93#(tt(), L, N) -> activate# L, activate# n__nil() -> nil#())
       (U93#(tt(), L, N) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U93#(tt(), L, N) -> activate# L, activate# n__s X -> s# X)
       (U93#(tt(), L, N) -> activate# L, activate# n__length X -> length# X)
       (U93#(tt(), L, N) -> activate# L, activate# n__0() -> 0#())
       (U93#(tt(), L, N) -> activate# L, activate# n__zeros() -> zeros#())
       (length# cons(N, L) -> activate# L, activate# n__nil() -> nil#())
       (length# cons(N, L) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (length# cons(N, L) -> activate# L, activate# n__s X -> s# X)
       (length# cons(N, L) -> activate# L, activate# n__length X -> length# X)
       (length# cons(N, L) -> activate# L, activate# n__0() -> 0#())
       (length# cons(N, L) -> activate# L, activate# n__zeros() -> zeros#())
       (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__s V1 -> U71# isNatKind activate V1)
       (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__s V1 -> isNatKind# activate V1)
       (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__s V1 -> activate# V1)
       (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
       (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__length V1 -> activate# V1)
       (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__length V1 -> isNatIListKind# activate V1)
       (U94#(tt(), L) -> length# activate L, length# nil() -> 0#())
       (U94#(tt(), L) -> length# activate L, length# cons(N, L) -> U91#(isNatList activate L, activate L, N))
       (U94#(tt(), L) -> length# activate L, length# cons(N, L) -> isNatList# activate L)
       (U94#(tt(), L) -> length# activate L, length# cons(N, L) -> activate# L)
       (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
       (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
       (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
       (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
       (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2))
       (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> isNatKind# activate V1)
       (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> activate# V2)
       (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> activate# V1)
       (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> U31#(isNatIListKind activate V, activate V))
       (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> activate# V)
       (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> isNatIListKind# activate V)
       (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
       (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
       (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
       (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
       (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
       (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> isNatKind# activate V1)
       (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> activate# V2)
       (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> activate# V1)
       (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
       (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
       (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> activate# V2)
       (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> activate# V1)
       (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
       (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> isNatKind# activate V1)
       (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> activate# V2)
       (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> activate# V1)
       (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
       (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
       (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V2)
       (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V1)
       (U22#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
       (U22#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
       (U22#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
       (U22#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
       (U22#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
       (U22#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1)
       (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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 -> U61# isNatIListKind activate V1)
       (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
       (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
       (isNat# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
       (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) -> activate# V2)
       (isNat# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V1)
       (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind activate V1)
       (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
       (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1)
       (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
       (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
       (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
       (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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 -> U61# isNatIListKind activate V1)
       (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
       (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
       (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
       (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
       (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
       (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
       (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
       (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1)
       (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
       (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X)
       (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X)
       (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#())
       (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
       (U42#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
       (U42#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U42#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
       (U42#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
       (U42#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
       (U42#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
       (U43#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
       (U43#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U43#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
       (U43#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
       (U43#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
       (U43#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
       (U45#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#())
       (U45#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U45#(tt(), V2) -> activate# V2, activate# n__s X -> s# X)
       (U45#(tt(), V2) -> activate# V2, activate# n__length X -> length# X)
       (U45#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
       (U45#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#())
       (U51#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#())
       (U51#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U51#(tt(), V2) -> activate# V2, activate# n__s X -> s# X)
       (U51#(tt(), V2) -> activate# V2, activate# n__length X -> length# X)
       (U51#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
       (U51#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#())
       (U81#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
       (U81#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U81#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
       (U81#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
       (U81#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
       (U81#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
       (U84#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
       (U84#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U84#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
       (U84#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
       (U84#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
       (U84#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
       (U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1), U12#(tt(), V1) -> isNatList# activate V1)
       (U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1), U12#(tt(), V1) -> U13# isNatList activate V1)
       (U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1), U12#(tt(), V1) -> activate# V1)
       (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> activate# V1)
       (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> isNatIListKind# activate V1)
       (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1))
       (U31#(tt(), V) -> U32#(isNatIListKind activate V, activate V), U32#(tt(), V) -> U33# isNatList activate V)
       (U31#(tt(), V) -> U32#(isNatIListKind activate V, activate V), U32#(tt(), V) -> isNatList# activate V)
       (U31#(tt(), V) -> U32#(isNatIListKind activate V, activate V), U32#(tt(), V) -> activate# V)
       (isNatIList# V -> U31#(isNatIListKind activate V, activate V), U31#(tt(), V) -> U32#(isNatIListKind activate V, 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) -> isNatIListKind# activate V)
       (U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L), U94#(tt(), L) -> length# activate L)
       (U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L), U94#(tt(), L) -> s# length activate L)
       (U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L), U94#(tt(), L) -> activate# L)
       (U31#(tt(), V) -> activate# V, activate# n__nil() -> nil#())
       (U31#(tt(), V) -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U31#(tt(), V) -> activate# V, activate# n__s X -> s# X)
       (U31#(tt(), V) -> activate# V, activate# n__length X -> length# X)
       (U31#(tt(), V) -> activate# V, activate# n__0() -> 0#())
       (U31#(tt(), V) -> activate# V, activate# n__zeros() -> zeros#())
       (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2))
       (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> isNatKind# activate V1)
       (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> activate# V2)
       (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> activate# V1)
       (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2))
       (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> activate# V2)
       (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> activate# V1)
       (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> isNatIListKind# activate V2)
       (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2))
       (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> isNatKind# activate V1)
       (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> activate# V2)
       (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> activate# V1)
       (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2))
       (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> activate# V2)
       (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> activate# V1)
       (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> isNatIListKind# activate V2)
       (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L))
       (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> isNatKind# activate N)
       (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> activate# N)
       (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> activate# L)
       (activate# n__length X -> length# X, length# nil() -> 0#())
       (activate# n__length X -> length# X, length# cons(N, L) -> U91#(isNatList activate L, activate L, N))
       (activate# n__length X -> length# X, length# cons(N, L) -> isNatList# activate L)
       (activate# n__length X -> length# X, length# cons(N, L) -> activate# L)
       (U12#(tt(), V1) -> activate# V1, activate# n__nil() -> nil#())
       (U12#(tt(), V1) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U12#(tt(), V1) -> activate# V1, activate# n__s X -> s# X)
       (U12#(tt(), V1) -> activate# V1, activate# n__length X -> length# X)
       (U12#(tt(), V1) -> activate# V1, activate# n__0() -> 0#())
       (U12#(tt(), V1) -> activate# V1, activate# n__zeros() -> zeros#())
       (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__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#())
       (U22#(tt(), V1) -> activate# V1, activate# n__nil() -> nil#())
       (U22#(tt(), V1) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U22#(tt(), V1) -> activate# V1, activate# n__s X -> s# X)
       (U22#(tt(), V1) -> activate# V1, activate# n__length X -> length# X)
       (U22#(tt(), V1) -> activate# V1, activate# n__0() -> 0#())
       (U22#(tt(), V1) -> activate# V1, activate# n__zeros() -> zeros#())
       (isNatKind# n__s V1 -> activate# V1, activate# n__nil() -> nil#())
       (isNatKind# n__s V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (isNatKind# n__s V1 -> activate# V1, activate# n__s X -> s# X)
       (isNatKind# n__s V1 -> activate# V1, activate# n__length X -> length# X)
       (isNatKind# n__s V1 -> activate# V1, activate# n__0() -> 0#())
       (isNatKind# n__s V1 -> activate# V1, activate# n__zeros() -> zeros#())
       (isNat# n__length V1 -> activate# V1, activate# n__nil() -> nil#())
       (isNat# n__length V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (isNat# n__length V1 -> activate# V1, activate# n__s X -> s# X)
       (isNat# n__length V1 -> activate# V1, activate# n__length X -> length# X)
       (isNat# n__length V1 -> activate# V1, activate# n__0() -> 0#())
       (isNat# n__length V1 -> activate# V1, activate# n__zeros() -> zeros#())
       (U42#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
       (U42#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U42#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
       (U42#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
       (U42#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
       (U42#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
       (U43#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
       (U43#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U43#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
       (U43#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
       (U43#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
       (U43#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
       (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
       (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X)
       (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X)
       (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#())
       (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
       (U81#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
       (U81#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U81#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
       (U81#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
       (U81#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
       (U81#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
       (U84#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
       (U84#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U84#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
       (U84#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
       (U84#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
       (U84#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
       (U91#(tt(), L, N) -> activate# N, activate# n__nil() -> nil#())
       (U91#(tt(), L, N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U91#(tt(), L, N) -> activate# N, activate# n__s X -> s# X)
       (U91#(tt(), L, N) -> activate# N, activate# n__length X -> length# X)
       (U91#(tt(), L, N) -> activate# N, activate# n__0() -> 0#())
       (U91#(tt(), L, N) -> activate# N, activate# n__zeros() -> zeros#())
       (U93#(tt(), L, N) -> activate# N, activate# n__zeros() -> zeros#())
       (U93#(tt(), L, N) -> activate# N, activate# n__0() -> 0#())
       (U93#(tt(), L, N) -> activate# N, activate# n__length X -> length# X)
       (U93#(tt(), L, N) -> activate# N, activate# n__s X -> s# X)
       (U93#(tt(), L, N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U93#(tt(), L, N) -> activate# N, activate# n__nil() -> nil#())
       (U92#(tt(), L, N) -> activate# N, activate# n__zeros() -> zeros#())
       (U92#(tt(), L, N) -> activate# N, activate# n__0() -> 0#())
       (U92#(tt(), L, N) -> activate# N, activate# n__length X -> length# X)
       (U92#(tt(), L, N) -> activate# N, activate# n__s X -> s# X)
       (U92#(tt(), L, N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U92#(tt(), L, N) -> activate# N, activate# n__nil() -> nil#())
       (U83#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
       (U83#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
       (U83#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
       (U83#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
       (U83#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U83#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
       (U82#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
       (U82#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
       (U82#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
       (U82#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
       (U82#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U82#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
       (U44#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
       (U44#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
       (U44#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
       (U44#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
       (U44#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U44#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
       (U41#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
       (U41#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
       (U41#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
       (U41#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
       (U41#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U41#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
       (isNat# n__s V1 -> activate# V1, activate# n__zeros() -> zeros#())
       (isNat# n__s V1 -> activate# V1, activate# n__0() -> 0#())
       (isNat# n__s V1 -> activate# V1, activate# n__length X -> length# X)
       (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# X)
       (isNat# n__s V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (isNat# n__s V1 -> activate# V1, activate# n__nil() -> nil#())
       (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__cons(X1, X2) -> cons#(X1, X2))
       (U21#(tt(), V1) -> activate# V1, activate# n__nil() -> nil#())
       (isNatKind# n__length V1 -> activate# V1, activate# n__zeros() -> zeros#())
       (isNatKind# n__length V1 -> activate# V1, activate# n__0() -> 0#())
       (isNatKind# n__length V1 -> activate# V1, activate# n__length X -> length# X)
       (isNatKind# n__length V1 -> activate# V1, activate# n__s X -> s# X)
       (isNatKind# n__length V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (isNatKind# n__length V1 -> activate# V1, activate# n__nil() -> nil#())
       (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__cons(X1, X2) -> cons#(X1, X2))
       (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
       (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__cons(X1, X2) -> cons#(X1, X2))
       (isNatIListKind# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
       (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> activate# L)
       (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> activate# N)
       (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> isNat# activate N)
       (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N))
       (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> activate# V1)
       (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> activate# V2)
       (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> isNat# activate V1)
       (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2))
       (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> isNatIListKind# activate V2)
       (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> activate# V1)
       (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> activate# V2)
       (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2))
       (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> activate# V1)
       (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> activate# V2)
       (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> isNat# activate V1)
       (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2))
       (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> isNatIListKind# activate V2)
       (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> activate# V1)
       (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> activate# V2)
       (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2))
       (isNatIList# V -> activate# V, activate# n__zeros() -> zeros#())
       (isNatIList# V -> activate# V, activate# n__0() -> 0#())
       (isNatIList# V -> activate# V, activate# n__length X -> length# X)
       (isNatIList# V -> activate# V, activate# n__s X -> s# X)
       (isNatIList# V -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (isNatIList# V -> activate# V, activate# n__nil() -> nil#())
       (U32#(tt(), V) -> activate# V, activate# n__zeros() -> zeros#())
       (U32#(tt(), V) -> activate# V, activate# n__0() -> 0#())
       (U32#(tt(), V) -> activate# V, activate# n__length X -> length# X)
       (U32#(tt(), V) -> activate# V, activate# n__s X -> s# X)
       (U32#(tt(), V) -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U32#(tt(), V) -> activate# V, activate# n__nil() -> nil#())
       (U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2), U85#(tt(), V2) -> activate# V2)
       (U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2), U85#(tt(), V2) -> isNatList# activate V2)
       (U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2), U85#(tt(), V2) -> U86# isNatList activate V2)
       (U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2), U45#(tt(), V2) -> activate# V2)
       (U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2), U45#(tt(), V2) -> U46# isNatIList activate V2)
       (U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2), U45#(tt(), V2) -> isNatIList# activate V2)
       (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> activate# V1)
       (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1))
       (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> isNatKind# activate V1)
       (U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U22#(tt(), V1) -> activate# V1)
       (U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U22#(tt(), V1) -> U23# isNat activate V1)
       (U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U22#(tt(), V1) -> isNat# activate V1)
       (isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2), U51#(tt(), V2) -> isNatIListKind# activate V2)
       (isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2), U51#(tt(), V2) -> activate# V2)
       (isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2), U51#(tt(), V2) -> U52# isNatIListKind activate V2)
       (activate# n__zeros() -> zeros#(), zeros#() -> cons#(0(), n__zeros()))
       (activate# n__zeros() -> zeros#(), zeros#() -> 0#())
       (U85#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#())
       (U85#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
       (U85#(tt(), V2) -> activate# V2, activate# n__length X -> length# X)
       (U85#(tt(), V2) -> activate# V2, activate# n__s X -> s# X)
       (U85#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U85#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#())
       (U83#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
       (U83#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
       (U83#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
       (U83#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
       (U83#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U83#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
       (U82#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
       (U82#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
       (U82#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
       (U82#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
       (U82#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U82#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
       (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
       (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#())
       (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X)
       (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X)
       (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
       (U44#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
       (U44#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
       (U44#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
       (U44#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
       (U44#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U44#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
       (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__cons(X1, X2) -> cons#(X1, X2))
       (U41#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
       (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__cons(X1, X2) -> cons#(X1, X2))
       (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
       (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> isNatIListKind# activate L)
       (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> activate# L)
       (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> activate# N)
       (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N))
       (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
       (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
       (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
       (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1)
       (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
       (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind activate V1)
       (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1)
       (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
       (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
       (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
       (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
       (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate 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__length V1 -> activate# V1)
       (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# 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)
       (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind activate V1)
       (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
       (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
       (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
       (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1)
       (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
       (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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) -> isNatKind# activate V1)
       (isNatKind# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
       (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)
       (isNatList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind 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__s V1 -> isNatKind# activate V1)
       (isNatList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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)
       (isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind 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__s V1 -> isNatKind# activate V1)
       (isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# 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) -> isNatKind# activate V1)
       (isNatIList# V -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
       (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> activate# V1)
       (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> activate# V2)
       (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> isNatKind# activate V1)
       (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
       (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
       (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
       (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
       (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
       (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
       (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
       (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
       (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
       (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
       (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
       (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
       (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
       (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> activate# V1)
       (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) -> isNatKind# activate V1)
       (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
       (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> activate# V1)
       (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> activate# V2)
       (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
       (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
       (U92#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> isNatIListKind# activate V1)
       (U92#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> activate# V1)
       (U92#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
       (U92#(tt(), L, N) -> isNat# activate N, isNat# n__s V1 -> activate# V1)
       (U92#(tt(), L, N) -> isNat# activate N, isNat# n__s V1 -> isNatKind# activate V1)
       (U92#(tt(), L, N) -> isNat# activate N, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
       (U94#(tt(), L) -> activate# L, activate# n__zeros() -> zeros#())
       (U94#(tt(), L) -> activate# L, activate# n__0() -> 0#())
       (U94#(tt(), L) -> activate# L, activate# n__length X -> length# X)
       (U94#(tt(), L) -> activate# L, activate# n__s X -> s# X)
       (U94#(tt(), L) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U94#(tt(), L) -> activate# L, activate# n__nil() -> nil#())
       (U91#(tt(), L, N) -> activate# L, activate# n__zeros() -> zeros#())
       (U91#(tt(), L, N) -> activate# L, activate# n__0() -> 0#())
       (U91#(tt(), L, N) -> activate# L, activate# n__length X -> length# X)
       (U91#(tt(), L, N) -> activate# L, activate# n__s X -> s# X)
       (U91#(tt(), L, N) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
       (U91#(tt(), L, N) -> activate# L, activate# n__nil() -> nil#())
      }
      EDG:
       {
        (U92#(tt(), L, N) -> activate# L, activate# n__nil() -> nil#())
        (U92#(tt(), L, N) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U92#(tt(), L, N) -> activate# L, activate# n__s X -> s# X)
        (U92#(tt(), L, N) -> activate# L, activate# n__length X -> length# X)
        (U92#(tt(), L, N) -> activate# L, activate# n__0() -> 0#())
        (U92#(tt(), L, N) -> activate# L, activate# n__zeros() -> zeros#())
        (U93#(tt(), L, N) -> activate# L, activate# n__nil() -> nil#())
        (U93#(tt(), L, N) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U93#(tt(), L, N) -> activate# L, activate# n__s X -> s# X)
        (U93#(tt(), L, N) -> activate# L, activate# n__length X -> length# X)
        (U93#(tt(), L, N) -> activate# L, activate# n__0() -> 0#())
        (U93#(tt(), L, N) -> activate# L, activate# n__zeros() -> zeros#())
        (length# cons(N, L) -> activate# L, activate# n__nil() -> nil#())
        (length# cons(N, L) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (length# cons(N, L) -> activate# L, activate# n__s X -> s# X)
        (length# cons(N, L) -> activate# L, activate# n__length X -> length# X)
        (length# cons(N, L) -> activate# L, activate# n__0() -> 0#())
        (length# cons(N, L) -> activate# L, activate# n__zeros() -> zeros#())
        (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__s V1 -> U71# isNatKind activate V1)
        (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__s V1 -> isNatKind# activate V1)
        (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__s V1 -> activate# V1)
        (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
        (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__length V1 -> activate# V1)
        (U93#(tt(), L, N) -> isNatKind# activate N, isNatKind# n__length V1 -> isNatIListKind# activate V1)
        (U94#(tt(), L) -> length# activate L, length# nil() -> 0#())
        (U94#(tt(), L) -> length# activate L, length# cons(N, L) -> U91#(isNatList activate L, activate L, N))
        (U94#(tt(), L) -> length# activate L, length# cons(N, L) -> isNatList# activate L)
        (U94#(tt(), L) -> length# activate L, length# cons(N, L) -> activate# L)
        (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
        (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
        (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
        (U42#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
        (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2))
        (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> isNatKind# activate V1)
        (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> activate# V2)
        (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# n__cons(V1, V2) -> activate# V1)
        (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> U31#(isNatIListKind activate V, activate V))
        (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> activate# V)
        (U45#(tt(), V2) -> isNatIList# activate V2, isNatIList# V -> isNatIListKind# activate V)
        (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
        (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
        (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
        (U82#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
        (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
        (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> isNatKind# activate V1)
        (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> activate# V2)
        (U85#(tt(), V2) -> isNatList# activate V2, isNatList# n__cons(V1, V2) -> activate# V1)
        (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
        (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
        (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> activate# V2)
        (U31#(tt(), V) -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> activate# V1)
        (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
        (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> isNatKind# activate V1)
        (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> activate# V2)
        (U12#(tt(), V1) -> isNatList# activate V1, isNatList# n__cons(V1, V2) -> activate# V1)
        (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
        (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
        (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V2)
        (U11#(tt(), V1) -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V1)
        (U22#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
        (U22#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
        (U22#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
        (U22#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
        (U22#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
        (U22#(tt(), V1) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1)
        (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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 -> U61# isNatIListKind activate V1)
        (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
        (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
        (isNat# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
        (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) -> activate# V2)
        (isNat# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> activate# V1)
        (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind activate V1)
        (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
        (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1)
        (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
        (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
        (U41#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
        (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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 -> U61# isNatIListKind activate V1)
        (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
        (isNatIList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
        (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
        (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
        (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
        (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
        (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
        (U84#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1)
        (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
        (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X)
        (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X)
        (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#())
        (isNatIListKind# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
        (U42#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
        (U42#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U42#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
        (U42#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
        (U42#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
        (U42#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
        (U43#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
        (U43#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U43#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
        (U43#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
        (U43#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
        (U43#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
        (U45#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#())
        (U45#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U45#(tt(), V2) -> activate# V2, activate# n__s X -> s# X)
        (U45#(tt(), V2) -> activate# V2, activate# n__length X -> length# X)
        (U45#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
        (U45#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#())
        (U51#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#())
        (U51#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U51#(tt(), V2) -> activate# V2, activate# n__s X -> s# X)
        (U51#(tt(), V2) -> activate# V2, activate# n__length X -> length# X)
        (U51#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
        (U51#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#())
        (U81#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
        (U81#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U81#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
        (U81#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
        (U81#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
        (U81#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
        (U84#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
        (U84#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U84#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
        (U84#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
        (U84#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
        (U84#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
        (U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1), U12#(tt(), V1) -> isNatList# activate V1)
        (U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1), U12#(tt(), V1) -> U13# isNatList activate V1)
        (U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1), U12#(tt(), V1) -> activate# V1)
        (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> activate# V1)
        (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> isNatIListKind# activate V1)
        (isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1), U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1))
        (U31#(tt(), V) -> U32#(isNatIListKind activate V, activate V), U32#(tt(), V) -> U33# isNatList activate V)
        (U31#(tt(), V) -> U32#(isNatIListKind activate V, activate V), U32#(tt(), V) -> isNatList# activate V)
        (U31#(tt(), V) -> U32#(isNatIListKind activate V, activate V), U32#(tt(), V) -> activate# V)
        (isNatIList# V -> U31#(isNatIListKind activate V, activate V), U31#(tt(), V) -> U32#(isNatIListKind activate V, 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) -> isNatIListKind# activate V)
        (U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L), U94#(tt(), L) -> length# activate L)
        (U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L), U94#(tt(), L) -> s# length activate L)
        (U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L), U94#(tt(), L) -> activate# L)
        (U31#(tt(), V) -> activate# V, activate# n__nil() -> nil#())
        (U31#(tt(), V) -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U31#(tt(), V) -> activate# V, activate# n__s X -> s# X)
        (U31#(tt(), V) -> activate# V, activate# n__length X -> length# X)
        (U31#(tt(), V) -> activate# V, activate# n__0() -> 0#())
        (U31#(tt(), V) -> activate# V, activate# n__zeros() -> zeros#())
        (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2))
        (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> isNatKind# activate V1)
        (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> activate# V2)
        (isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2), U81#(tt(), V1, V2) -> activate# V1)
        (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2))
        (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> activate# V2)
        (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> activate# V1)
        (U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2), U42#(tt(), V1, V2) -> isNatIListKind# activate V2)
        (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2))
        (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> isNatKind# activate V1)
        (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> activate# V2)
        (isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2), U41#(tt(), V1, V2) -> activate# V1)
        (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2))
        (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> activate# V2)
        (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> activate# V1)
        (U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2), U82#(tt(), V1, V2) -> isNatIListKind# activate V2)
        (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L))
        (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> isNatKind# activate N)
        (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> activate# N)
        (U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N), U93#(tt(), L, N) -> activate# L)
        (activate# n__length X -> length# X, length# nil() -> 0#())
        (activate# n__length X -> length# X, length# cons(N, L) -> U91#(isNatList activate L, activate L, N))
        (activate# n__length X -> length# X, length# cons(N, L) -> isNatList# activate L)
        (activate# n__length X -> length# X, length# cons(N, L) -> activate# L)
        (U12#(tt(), V1) -> activate# V1, activate# n__nil() -> nil#())
        (U12#(tt(), V1) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U12#(tt(), V1) -> activate# V1, activate# n__s X -> s# X)
        (U12#(tt(), V1) -> activate# V1, activate# n__length X -> length# X)
        (U12#(tt(), V1) -> activate# V1, activate# n__0() -> 0#())
        (U12#(tt(), V1) -> activate# V1, activate# n__zeros() -> zeros#())
        (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__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#())
        (U22#(tt(), V1) -> activate# V1, activate# n__nil() -> nil#())
        (U22#(tt(), V1) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U22#(tt(), V1) -> activate# V1, activate# n__s X -> s# X)
        (U22#(tt(), V1) -> activate# V1, activate# n__length X -> length# X)
        (U22#(tt(), V1) -> activate# V1, activate# n__0() -> 0#())
        (U22#(tt(), V1) -> activate# V1, activate# n__zeros() -> zeros#())
        (isNatKind# n__s V1 -> activate# V1, activate# n__nil() -> nil#())
        (isNatKind# n__s V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (isNatKind# n__s V1 -> activate# V1, activate# n__s X -> s# X)
        (isNatKind# n__s V1 -> activate# V1, activate# n__length X -> length# X)
        (isNatKind# n__s V1 -> activate# V1, activate# n__0() -> 0#())
        (isNatKind# n__s V1 -> activate# V1, activate# n__zeros() -> zeros#())
        (isNat# n__length V1 -> activate# V1, activate# n__nil() -> nil#())
        (isNat# n__length V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (isNat# n__length V1 -> activate# V1, activate# n__s X -> s# X)
        (isNat# n__length V1 -> activate# V1, activate# n__length X -> length# X)
        (isNat# n__length V1 -> activate# V1, activate# n__0() -> 0#())
        (isNat# n__length V1 -> activate# V1, activate# n__zeros() -> zeros#())
        (U42#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
        (U42#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U42#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
        (U42#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
        (U42#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
        (U42#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
        (U43#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
        (U43#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U43#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
        (U43#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
        (U43#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
        (U43#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
        (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
        (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__s X -> s# X)
        (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__length X -> length# X)
        (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__0() -> 0#())
        (isNatIList# n__cons(V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
        (U81#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
        (U81#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U81#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
        (U81#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
        (U81#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
        (U81#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
        (U84#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
        (U84#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U84#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
        (U84#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
        (U84#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
        (U84#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
        (U91#(tt(), L, N) -> activate# N, activate# n__nil() -> nil#())
        (U91#(tt(), L, N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U91#(tt(), L, N) -> activate# N, activate# n__s X -> s# X)
        (U91#(tt(), L, N) -> activate# N, activate# n__length X -> length# X)
        (U91#(tt(), L, N) -> activate# N, activate# n__0() -> 0#())
        (U91#(tt(), L, N) -> activate# N, activate# n__zeros() -> zeros#())
        (U93#(tt(), L, N) -> activate# N, activate# n__zeros() -> zeros#())
        (U93#(tt(), L, N) -> activate# N, activate# n__0() -> 0#())
        (U93#(tt(), L, N) -> activate# N, activate# n__length X -> length# X)
        (U93#(tt(), L, N) -> activate# N, activate# n__s X -> s# X)
        (U93#(tt(), L, N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U93#(tt(), L, N) -> activate# N, activate# n__nil() -> nil#())
        (U92#(tt(), L, N) -> activate# N, activate# n__zeros() -> zeros#())
        (U92#(tt(), L, N) -> activate# N, activate# n__0() -> 0#())
        (U92#(tt(), L, N) -> activate# N, activate# n__length X -> length# X)
        (U92#(tt(), L, N) -> activate# N, activate# n__s X -> s# X)
        (U92#(tt(), L, N) -> activate# N, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U92#(tt(), L, N) -> activate# N, activate# n__nil() -> nil#())
        (U83#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
        (U83#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
        (U83#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
        (U83#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
        (U83#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U83#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
        (U82#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
        (U82#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
        (U82#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
        (U82#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
        (U82#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U82#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
        (U44#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
        (U44#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
        (U44#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
        (U44#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
        (U44#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U44#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
        (U41#(tt(), V1, V2) -> activate# V1, activate# n__zeros() -> zeros#())
        (U41#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
        (U41#(tt(), V1, V2) -> activate# V1, activate# n__length X -> length# X)
        (U41#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
        (U41#(tt(), V1, V2) -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U41#(tt(), V1, V2) -> activate# V1, activate# n__nil() -> nil#())
        (isNat# n__s V1 -> activate# V1, activate# n__zeros() -> zeros#())
        (isNat# n__s V1 -> activate# V1, activate# n__0() -> 0#())
        (isNat# n__s V1 -> activate# V1, activate# n__length X -> length# X)
        (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# X)
        (isNat# n__s V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (isNat# n__s V1 -> activate# V1, activate# n__nil() -> nil#())
        (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__cons(X1, X2) -> cons#(X1, X2))
        (U21#(tt(), V1) -> activate# V1, activate# n__nil() -> nil#())
        (isNatKind# n__length V1 -> activate# V1, activate# n__zeros() -> zeros#())
        (isNatKind# n__length V1 -> activate# V1, activate# n__0() -> 0#())
        (isNatKind# n__length V1 -> activate# V1, activate# n__length X -> length# X)
        (isNatKind# n__length V1 -> activate# V1, activate# n__s X -> s# X)
        (isNatKind# n__length V1 -> activate# V1, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (isNatKind# n__length V1 -> activate# V1, activate# n__nil() -> nil#())
        (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__cons(X1, X2) -> cons#(X1, X2))
        (isNatList# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
        (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__cons(X1, X2) -> cons#(X1, X2))
        (isNatIListKind# n__cons(V1, V2) -> activate# V1, activate# n__nil() -> nil#())
        (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> activate# L)
        (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> activate# N)
        (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> isNat# activate N)
        (U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N), U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N))
        (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> activate# V1)
        (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> activate# V2)
        (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> isNat# activate V1)
        (U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2), U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2))
        (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> isNatIListKind# activate V2)
        (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> activate# V1)
        (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> activate# V2)
        (U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2), U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2))
        (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> activate# V1)
        (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> activate# V2)
        (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> isNat# activate V1)
        (U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2), U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2))
        (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> isNatIListKind# activate V2)
        (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> activate# V1)
        (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> activate# V2)
        (U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2), U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2))
        (isNatIList# V -> activate# V, activate# n__zeros() -> zeros#())
        (isNatIList# V -> activate# V, activate# n__0() -> 0#())
        (isNatIList# V -> activate# V, activate# n__length X -> length# X)
        (isNatIList# V -> activate# V, activate# n__s X -> s# X)
        (isNatIList# V -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (isNatIList# V -> activate# V, activate# n__nil() -> nil#())
        (U32#(tt(), V) -> activate# V, activate# n__zeros() -> zeros#())
        (U32#(tt(), V) -> activate# V, activate# n__0() -> 0#())
        (U32#(tt(), V) -> activate# V, activate# n__length X -> length# X)
        (U32#(tt(), V) -> activate# V, activate# n__s X -> s# X)
        (U32#(tt(), V) -> activate# V, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U32#(tt(), V) -> activate# V, activate# n__nil() -> nil#())
        (U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2), U85#(tt(), V2) -> activate# V2)
        (U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2), U85#(tt(), V2) -> isNatList# activate V2)
        (U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2), U85#(tt(), V2) -> U86# isNatList activate V2)
        (U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2), U45#(tt(), V2) -> activate# V2)
        (U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2), U45#(tt(), V2) -> U46# isNatIList activate V2)
        (U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2), U45#(tt(), V2) -> isNatIList# activate V2)
        (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> activate# V1)
        (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1))
        (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> isNatKind# activate V1)
        (U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U22#(tt(), V1) -> activate# V1)
        (U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U22#(tt(), V1) -> U23# isNat activate V1)
        (U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1), U22#(tt(), V1) -> isNat# activate V1)
        (isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2), U51#(tt(), V2) -> isNatIListKind# activate V2)
        (isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2), U51#(tt(), V2) -> activate# V2)
        (isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2), U51#(tt(), V2) -> U52# isNatIListKind activate V2)
        (activate# n__zeros() -> zeros#(), zeros#() -> cons#(0(), n__zeros()))
        (activate# n__zeros() -> zeros#(), zeros#() -> 0#())
        (U85#(tt(), V2) -> activate# V2, activate# n__zeros() -> zeros#())
        (U85#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
        (U85#(tt(), V2) -> activate# V2, activate# n__length X -> length# X)
        (U85#(tt(), V2) -> activate# V2, activate# n__s X -> s# X)
        (U85#(tt(), V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U85#(tt(), V2) -> activate# V2, activate# n__nil() -> nil#())
        (U83#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
        (U83#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
        (U83#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
        (U83#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
        (U83#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U83#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
        (U82#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
        (U82#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
        (U82#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
        (U82#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
        (U82#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U82#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
        (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
        (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__0() -> 0#())
        (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__length X -> length# X)
        (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__s X -> s# X)
        (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (isNatIList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
        (U44#(tt(), V1, V2) -> activate# V2, activate# n__zeros() -> zeros#())
        (U44#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
        (U44#(tt(), V1, V2) -> activate# V2, activate# n__length X -> length# X)
        (U44#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
        (U44#(tt(), V1, V2) -> activate# V2, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U44#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
        (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__cons(X1, X2) -> cons#(X1, X2))
        (U41#(tt(), V1, V2) -> activate# V2, activate# n__nil() -> nil#())
        (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__cons(X1, X2) -> cons#(X1, X2))
        (isNatList# n__cons(V1, V2) -> activate# V2, activate# n__nil() -> nil#())
        (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> isNatIListKind# activate L)
        (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> activate# L)
        (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> activate# N)
        (length# cons(N, L) -> U91#(isNatList activate L, activate L, N), U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N))
        (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
        (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
        (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
        (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1)
        (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
        (U81#(tt(), V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind activate V1)
        (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> isNatIListKind# activate V1)
        (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> activate# V1)
        (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
        (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
        (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
        (U44#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate 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__length V1 -> activate# V1)
        (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# 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)
        (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind activate V1)
        (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__length V1 -> isNatIListKind# activate V1)
        (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__length V1 -> activate# V1)
        (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind activate V1)
        (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1)
        (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
        (U21#(tt(), V1) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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) -> isNatKind# activate V1)
        (isNatKind# n__length V1 -> isNatIListKind# activate V1, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
        (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)
        (isNatList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind 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__s V1 -> isNatKind# activate V1)
        (isNatList# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# isNatKind 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)
        (isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__length V1 -> U61# isNatIListKind 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__s V1 -> isNatKind# activate V1)
        (isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> U71# 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) -> isNatKind# activate V1)
        (isNatIList# V -> isNatIListKind# activate V, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
        (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> activate# V1)
        (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> activate# V2)
        (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> isNatKind# activate V1)
        (U32#(tt(), V) -> isNatList# activate V, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
        (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
        (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
        (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
        (U83#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
        (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
        (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
        (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
        (U51#(tt(), V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
        (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V1)
        (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> activate# V2)
        (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
        (U43#(tt(), V1, V2) -> isNatIListKind# activate V2, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
        (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> activate# V1)
        (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) -> isNatKind# activate V1)
        (length# cons(N, L) -> isNatList# activate L, isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2))
        (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> activate# V1)
        (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> activate# V2)
        (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1)
        (U91#(tt(), L, N) -> isNatIListKind# activate L, isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2))
        (U92#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> isNatIListKind# activate V1)
        (U92#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> activate# V1)
        (U92#(tt(), L, N) -> isNat# activate N, isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1))
        (U92#(tt(), L, N) -> isNat# activate N, isNat# n__s V1 -> activate# V1)
        (U92#(tt(), L, N) -> isNat# activate N, isNat# n__s V1 -> isNatKind# activate V1)
        (U92#(tt(), L, N) -> isNat# activate N, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
        (U94#(tt(), L) -> activate# L, activate# n__zeros() -> zeros#())
        (U94#(tt(), L) -> activate# L, activate# n__0() -> 0#())
        (U94#(tt(), L) -> activate# L, activate# n__length X -> length# X)
        (U94#(tt(), L) -> activate# L, activate# n__s X -> s# X)
        (U94#(tt(), L) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U94#(tt(), L) -> activate# L, activate# n__nil() -> nil#())
        (U91#(tt(), L, N) -> activate# L, activate# n__zeros() -> zeros#())
        (U91#(tt(), L, N) -> activate# L, activate# n__0() -> 0#())
        (U91#(tt(), L, N) -> activate# L, activate# n__length X -> length# X)
        (U91#(tt(), L, N) -> activate# L, activate# n__s X -> s# X)
        (U91#(tt(), L, N) -> activate# L, activate# n__cons(X1, X2) -> cons#(X1, X2))
        (U91#(tt(), L, N) -> activate# L, activate# n__nil() -> nil#())
       }
       STATUS:
        arrows: 0.961391
        SCCS (2):
         Scc:
          {         U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2),
                    U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2),
                    U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2),
                    U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2),
                        U45#(tt(), V2) -> isNatIList# activate V2,
           isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, activate V1, activate V2)}
         Scc:
          {                 U12#(tt(), V1) -> activate# V1,
                            U12#(tt(), V1) -> isNatList# activate V1,
           isNatIListKind# n__cons(V1, V2) -> activate# V1,
           isNatIListKind# n__cons(V1, V2) -> activate# V2,
           isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1,
           isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2),
                     activate# n__length X -> length# X,
                            U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1),
                            U11#(tt(), V1) -> isNatIListKind# activate V1,
                            U11#(tt(), V1) -> activate# V1,
                isNatList# n__cons(V1, V2) -> activate# V1,
                isNatList# n__cons(V1, V2) -> activate# V2,
                isNatList# n__cons(V1, V2) -> isNatKind# activate V1,
                isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2),
                            U22#(tt(), V1) -> activate# V1,
                            U22#(tt(), V1) -> isNat# activate V1,
                   isNatKind# n__length V1 -> isNatIListKind# activate V1,
                   isNatKind# n__length V1 -> activate# V1,
                        isNatKind# n__s V1 -> activate# V1,
                        isNatKind# n__s V1 -> isNatKind# activate V1,
                            U21#(tt(), V1) -> activate# V1,
                            U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1),
                            U21#(tt(), V1) -> isNatKind# activate V1,
                       isNat# n__length V1 -> isNatIListKind# activate V1,
                       isNat# n__length V1 -> activate# V1,
                       isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1),
                            isNat# n__s V1 -> activate# V1,
                            isNat# n__s V1 -> isNatKind# activate V1,
                            isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1),
                            U51#(tt(), V2) -> isNatIListKind# activate V2,
                            U51#(tt(), V2) -> activate# V2,
                        U82#(tt(), V1, V2) -> isNatIListKind# activate V2,
                        U82#(tt(), V1, V2) -> activate# V1,
                        U82#(tt(), V1, V2) -> activate# V2,
                        U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2),
                        U81#(tt(), V1, V2) -> activate# V1,
                        U81#(tt(), V1, V2) -> activate# V2,
                        U81#(tt(), V1, V2) -> isNatKind# activate V1,
                        U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2),
                        U83#(tt(), V1, V2) -> isNatIListKind# activate V2,
                        U83#(tt(), V1, V2) -> activate# V1,
                        U83#(tt(), V1, V2) -> activate# V2,
                        U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2),
                        U84#(tt(), V1, V2) -> activate# V1,
                        U84#(tt(), V1, V2) -> activate# V2,
                        U84#(tt(), V1, V2) -> isNat# activate V1,
                        U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2),
                            U85#(tt(), V2) -> activate# V2,
                            U85#(tt(), V2) -> isNatList# activate V2,
                          U92#(tt(), L, N) -> activate# L,
                          U92#(tt(), L, N) -> activate# N,
                          U92#(tt(), L, N) -> isNat# activate N,
                          U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N),
                          U91#(tt(), L, N) -> isNatIListKind# activate L,
                          U91#(tt(), L, N) -> activate# L,
                          U91#(tt(), L, N) -> activate# N,
                          U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N),
                          U93#(tt(), L, N) -> activate# L,
                          U93#(tt(), L, N) -> activate# N,
                          U93#(tt(), L, N) -> isNatKind# activate N,
                          U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L),
                             U94#(tt(), L) -> activate# L,
                             U94#(tt(), L) -> length# activate L,
                        length# cons(N, L) -> activate# L,
                        length# cons(N, L) -> isNatList# activate L,
                        length# cons(N, L) -> U91#(isNatList activate L, activate L, N)}
         
         SCC (6):
          Strict:
           {         U42#(tt(), V1, V2) -> U43#(isNatIListKind activate V2, activate V1, activate V2),
                     U41#(tt(), V1, V2) -> U42#(isNatKind activate V1, activate V1, activate V2),
                     U43#(tt(), V1, V2) -> U44#(isNatIListKind activate V2, activate V1, activate V2),
                     U44#(tt(), V1, V2) -> U45#(isNat activate V1, activate V2),
                         U45#(tt(), V2) -> isNatIList# activate V2,
            isNatIList# n__cons(V1, V2) -> U41#(isNatKind activate V1, 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(), V1) -> U13 isNatList activate V1,
                isNatIListKind n__zeros() -> tt(),
           isNatIListKind n__cons(V1, V2) -> U51(isNatKind activate V1, activate V2),
                  isNatIListKind 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__cons(X1, X2) -> cons(X1, X2),
                        activate n__nil() -> nil(),
                            U11(tt(), V1) -> U12(isNatIListKind activate V1, activate V1),
                                 U13 tt() -> tt(),
                isNatList n__cons(V1, V2) -> U81(isNatKind activate V1, activate V1, activate V2),
                       isNatList n__nil() -> tt(),
                            U22(tt(), V1) -> U23 isNat activate V1,
                         isNatKind n__0() -> tt(),
                   isNatKind n__length V1 -> U61 isNatIListKind activate V1,
                        isNatKind n__s V1 -> U71 isNatKind activate V1,
                            U21(tt(), V1) -> U22(isNatKind activate V1, activate V1),
                                 U23 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),
                             U32(tt(), V) -> U33 isNatList activate V,
                             U31(tt(), V) -> U32(isNatIListKind activate V, activate V),
                                 U33 tt() -> tt(),
                        U42(tt(), V1, V2) -> U43(isNatIListKind activate V2, activate V1, activate V2),
                        U41(tt(), V1, V2) -> U42(isNatKind activate V1, activate V1, activate V2),
                        U43(tt(), V1, V2) -> U44(isNatIListKind activate V2, activate V1, activate V2),
                        U44(tt(), V1, V2) -> U45(isNat activate V1, activate V2),
                            U45(tt(), V2) -> U46 isNatIList activate V2,
                                 U46 tt() -> tt(),
                             isNatIList V -> U31(isNatIListKind activate V, activate V),
                    isNatIList n__zeros() -> tt(),
               isNatIList n__cons(V1, V2) -> U41(isNatKind activate V1, activate V1, activate V2),
                                 U52 tt() -> tt(),
                            U51(tt(), V2) -> U52 isNatIListKind activate V2,
                                 U61 tt() -> tt(),
                                 U71 tt() -> tt(),
                        U82(tt(), V1, V2) -> U83(isNatIListKind activate V2, activate V1, activate V2),
                        U81(tt(), V1, V2) -> U82(isNatKind activate V1, activate V1, activate V2),
                        U83(tt(), V1, V2) -> U84(isNatIListKind activate V2, activate V1, activate V2),
                        U84(tt(), V1, V2) -> U85(isNat activate V1, activate V2),
                            U85(tt(), V2) -> U86 isNatList activate V2,
                                 U86 tt() -> tt(),
                          U92(tt(), L, N) -> U93(isNat activate N, activate L, activate N),
                          U91(tt(), L, N) -> U92(isNatIListKind activate L, activate L, activate N),
                          U93(tt(), L, N) -> U94(isNatKind activate N, activate L),
                             U94(tt(), L) -> s length activate L,
                                      s X -> n__s X,
                                 length X -> n__length X,
                        length cons(N, L) -> U91(isNatList activate L, activate L, N),
                             length nil() -> 0(),
                                    nil() -> n__nil()}
          Open
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         
         SCC (66):
          Strict:
           {                 U12#(tt(), V1) -> activate# V1,
                             U12#(tt(), V1) -> isNatList# activate V1,
            isNatIListKind# n__cons(V1, V2) -> activate# V1,
            isNatIListKind# n__cons(V1, V2) -> activate# V2,
            isNatIListKind# n__cons(V1, V2) -> isNatKind# activate V1,
            isNatIListKind# n__cons(V1, V2) -> U51#(isNatKind activate V1, activate V2),
                      activate# n__length X -> length# X,
                             U11#(tt(), V1) -> U12#(isNatIListKind activate V1, activate V1),
                             U11#(tt(), V1) -> isNatIListKind# activate V1,
                             U11#(tt(), V1) -> activate# V1,
                 isNatList# n__cons(V1, V2) -> activate# V1,
                 isNatList# n__cons(V1, V2) -> activate# V2,
                 isNatList# n__cons(V1, V2) -> isNatKind# activate V1,
                 isNatList# n__cons(V1, V2) -> U81#(isNatKind activate V1, activate V1, activate V2),
                             U22#(tt(), V1) -> activate# V1,
                             U22#(tt(), V1) -> isNat# activate V1,
                    isNatKind# n__length V1 -> isNatIListKind# activate V1,
                    isNatKind# n__length V1 -> activate# V1,
                         isNatKind# n__s V1 -> activate# V1,
                         isNatKind# n__s V1 -> isNatKind# activate V1,
                             U21#(tt(), V1) -> activate# V1,
                             U21#(tt(), V1) -> U22#(isNatKind activate V1, activate V1),
                             U21#(tt(), V1) -> isNatKind# activate V1,
                        isNat# n__length V1 -> isNatIListKind# activate V1,
                        isNat# n__length V1 -> activate# V1,
                        isNat# n__length V1 -> U11#(isNatIListKind activate V1, activate V1),
                             isNat# n__s V1 -> activate# V1,
                             isNat# n__s V1 -> isNatKind# activate V1,
                             isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1),
                             U51#(tt(), V2) -> isNatIListKind# activate V2,
                             U51#(tt(), V2) -> activate# V2,
                         U82#(tt(), V1, V2) -> isNatIListKind# activate V2,
                         U82#(tt(), V1, V2) -> activate# V1,
                         U82#(tt(), V1, V2) -> activate# V2,
                         U82#(tt(), V1, V2) -> U83#(isNatIListKind activate V2, activate V1, activate V2),
                         U81#(tt(), V1, V2) -> activate# V1,
                         U81#(tt(), V1, V2) -> activate# V2,
                         U81#(tt(), V1, V2) -> isNatKind# activate V1,
                         U81#(tt(), V1, V2) -> U82#(isNatKind activate V1, activate V1, activate V2),
                         U83#(tt(), V1, V2) -> isNatIListKind# activate V2,
                         U83#(tt(), V1, V2) -> activate# V1,
                         U83#(tt(), V1, V2) -> activate# V2,
                         U83#(tt(), V1, V2) -> U84#(isNatIListKind activate V2, activate V1, activate V2),
                         U84#(tt(), V1, V2) -> activate# V1,
                         U84#(tt(), V1, V2) -> activate# V2,
                         U84#(tt(), V1, V2) -> isNat# activate V1,
                         U84#(tt(), V1, V2) -> U85#(isNat activate V1, activate V2),
                             U85#(tt(), V2) -> activate# V2,
                             U85#(tt(), V2) -> isNatList# activate V2,
                           U92#(tt(), L, N) -> activate# L,
                           U92#(tt(), L, N) -> activate# N,
                           U92#(tt(), L, N) -> isNat# activate N,
                           U92#(tt(), L, N) -> U93#(isNat activate N, activate L, activate N),
                           U91#(tt(), L, N) -> isNatIListKind# activate L,
                           U91#(tt(), L, N) -> activate# L,
                           U91#(tt(), L, N) -> activate# N,
                           U91#(tt(), L, N) -> U92#(isNatIListKind activate L, activate L, activate N),
                           U93#(tt(), L, N) -> activate# L,
                           U93#(tt(), L, N) -> activate# N,
                           U93#(tt(), L, N) -> isNatKind# activate N,
                           U93#(tt(), L, N) -> U94#(isNatKind activate N, activate L),
                              U94#(tt(), L) -> activate# L,
                              U94#(tt(), L) -> length# activate L,
                         length# cons(N, L) -> activate# L,
                         length# cons(N, L) -> isNatList# activate L,
                         length# cons(N, L) -> U91#(isNatList activate L, activate L, N)}
          Weak:
          {                  cons(X1, X2) -> n__cons(X1, X2),
                                      0() -> n__0(),
                                  zeros() -> cons(0(), n__zeros()),
                                  zeros() -> n__zeros(),
                            U12(tt(), V1) -> U13 isNatList activate V1,
                isNatIListKind n__zeros() -> tt(),
           isNatIListKind n__cons(V1, V2) -> U51(isNatKind activate V1, activate V2),
                  isNatIListKind 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__cons(X1, X2) -> cons(X1, X2),
                        activate n__nil() -> nil(),
                            U11(tt(), V1) -> U12(isNatIListKind activate V1, activate V1),
                                 U13 tt() -> tt(),
                isNatList n__cons(V1, V2) -> U81(isNatKind activate V1, activate V1, activate V2),
                       isNatList n__nil() -> tt(),
                            U22(tt(), V1) -> U23 isNat activate V1,
                         isNatKind n__0() -> tt(),
                   isNatKind n__length V1 -> U61 isNatIListKind activate V1,
                        isNatKind n__s V1 -> U71 isNatKind activate V1,
                            U21(tt(), V1) -> U22(isNatKind activate V1, activate V1),
                                 U23 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),
                             U32(tt(), V) -> U33 isNatList activate V,
                             U31(tt(), V) -> U32(isNatIListKind activate V, activate V),
                                 U33 tt() -> tt(),
                        U42(tt(), V1, V2) -> U43(isNatIListKind activate V2, activate V1, activate V2),
                        U41(tt(), V1, V2) -> U42(isNatKind activate V1, activate V1, activate V2),
                        U43(tt(), V1, V2) -> U44(isNatIListKind activate V2, activate V1, activate V2),
                        U44(tt(), V1, V2) -> U45(isNat activate V1, activate V2),
                            U45(tt(), V2) -> U46 isNatIList activate V2,
                                 U46 tt() -> tt(),
                             isNatIList V -> U31(isNatIListKind activate V, activate V),
                    isNatIList n__zeros() -> tt(),
               isNatIList n__cons(V1, V2) -> U41(isNatKind activate V1, activate V1, activate V2),
                                 U52 tt() -> tt(),
                            U51(tt(), V2) -> U52 isNatIListKind activate V2,
                                 U61 tt() -> tt(),
                                 U71 tt() -> tt(),
                        U82(tt(), V1, V2) -> U83(isNatIListKind activate V2, activate V1, activate V2),
                        U81(tt(), V1, V2) -> U82(isNatKind activate V1, activate V1, activate V2),
                        U83(tt(), V1, V2) -> U84(isNatIListKind activate V2, activate V1, activate V2),
                        U84(tt(), V1, V2) -> U85(isNat activate V1, activate V2),
                            U85(tt(), V2) -> U86 isNatList activate V2,
                                 U86 tt() -> tt(),
                          U92(tt(), L, N) -> U93(isNat activate N, activate L, activate N),
                          U91(tt(), L, N) -> U92(isNatIListKind activate L, activate L, activate N),
                          U93(tt(), L, N) -> U94(isNatKind activate N, activate L),
                             U94(tt(), L) -> s length activate L,
                                      s X -> n__s X,
                                 length X -> n__length X,
                        length cons(N, L) -> U91(isNatList activate L, activate L, N),
                             length nil() -> 0(),
                                    nil() -> n__nil()}
          Open