MAYBE
Time: 0.044335
TRS:
 {            U12(tt(), V2) -> U13 isNat activate V2,
               isNat n__0() -> tt(),
      isNat n__plus(V1, V2) -> U11(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2),
              isNat n__s V1 -> U21(isNatKind activate V1, activate V1),
                 activate X -> X,
            activate n__0() -> 0(),
    activate n__isNatKind X -> isNatKind X,
   activate n__plus(X1, X2) -> plus(X1, X2),
            activate n__s X -> s X,
    activate n__and(X1, X2) -> and(X1, X2),
          U11(tt(), V1, V2) -> U12(isNat activate V1, activate V2),
                   U13 tt() -> tt(),
                   U22 tt() -> tt(),
              U21(tt(), V1) -> U22 isNat activate V1,
               U31(tt(), N) -> activate N,
                        s X -> n__s X,
               plus(N, s M) -> U41(and(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)), M, N),
               plus(N, 0()) -> U31(and(isNat N, n__isNatKind N), N),
               plus(X1, X2) -> n__plus(X1, X2),
            U41(tt(), M, N) -> s plus(activate N, activate M),
                and(X1, X2) -> n__and(X1, X2),
               and(tt(), X) -> activate X,
                isNatKind X -> n__isNatKind X,
           isNatKind n__0() -> tt(),
  isNatKind n__plus(V1, V2) -> and(isNatKind activate V1, n__isNatKind activate V2),
          isNatKind n__s V1 -> isNatKind activate V1,
                        0() -> n__0()}
 DP:
  DP:
   {            U12#(tt(), V2) -> isNat# activate V2,
                U12#(tt(), V2) -> activate# V2,
                U12#(tt(), V2) -> U13# isNat activate V2,
        isNat# n__plus(V1, V2) -> activate# V1,
        isNat# n__plus(V1, V2) -> activate# V2,
        isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2),
        isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2),
        isNat# n__plus(V1, V2) -> isNatKind# activate V1,
                isNat# n__s V1 -> activate# V1,
                isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1),
                isNat# n__s V1 -> isNatKind# activate V1,
              activate# n__0() -> 0#(),
      activate# n__isNatKind X -> isNatKind# X,
     activate# n__plus(X1, X2) -> plus#(X1, X2),
              activate# n__s X -> s# X,
      activate# n__and(X1, X2) -> and#(X1, X2),
            U11#(tt(), V1, V2) -> U12#(isNat activate V1, activate V2),
            U11#(tt(), V1, V2) -> isNat# activate V1,
            U11#(tt(), V1, V2) -> activate# V1,
            U11#(tt(), V1, V2) -> activate# V2,
                U21#(tt(), V1) -> isNat# activate V1,
                U21#(tt(), V1) -> activate# V1,
                U21#(tt(), V1) -> U22# isNat activate V1,
                 U31#(tt(), N) -> activate# N,
                 plus#(N, s M) -> isNat# N,
                 plus#(N, s M) -> isNat# M,
                 plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)), M, N),
                 plus#(N, s M) -> and#(isNat M, n__isNatKind M),
                 plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)),
                 plus#(N, 0()) -> isNat# N,
                 plus#(N, 0()) -> U31#(and(isNat N, n__isNatKind N), N),
                 plus#(N, 0()) -> and#(isNat N, n__isNatKind N),
              U41#(tt(), M, N) -> activate# N,
              U41#(tt(), M, N) -> activate# M,
              U41#(tt(), M, N) -> s# plus(activate N, activate M),
              U41#(tt(), M, N) -> plus#(activate N, activate M),
                 and#(tt(), X) -> activate# X,
    isNatKind# n__plus(V1, V2) -> activate# V1,
    isNatKind# n__plus(V1, V2) -> activate# V2,
    isNatKind# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2),
    isNatKind# n__plus(V1, V2) -> isNatKind# activate V1,
            isNatKind# n__s V1 -> activate# V1,
            isNatKind# n__s V1 -> isNatKind# activate V1}
  TRS:
  {            U12(tt(), V2) -> U13 isNat activate V2,
                isNat n__0() -> tt(),
       isNat n__plus(V1, V2) -> U11(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2),
               isNat n__s V1 -> U21(isNatKind activate V1, activate V1),
                  activate X -> X,
             activate n__0() -> 0(),
     activate n__isNatKind X -> isNatKind X,
    activate n__plus(X1, X2) -> plus(X1, X2),
             activate n__s X -> s X,
     activate n__and(X1, X2) -> and(X1, X2),
           U11(tt(), V1, V2) -> U12(isNat activate V1, activate V2),
                    U13 tt() -> tt(),
                    U22 tt() -> tt(),
               U21(tt(), V1) -> U22 isNat activate V1,
                U31(tt(), N) -> activate N,
                         s X -> n__s X,
                plus(N, s M) -> U41(and(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)), M, N),
                plus(N, 0()) -> U31(and(isNat N, n__isNatKind N), N),
                plus(X1, X2) -> n__plus(X1, X2),
             U41(tt(), M, N) -> s plus(activate N, activate M),
                 and(X1, X2) -> n__and(X1, X2),
                and(tt(), X) -> activate X,
                 isNatKind X -> n__isNatKind X,
            isNatKind n__0() -> tt(),
   isNatKind n__plus(V1, V2) -> and(isNatKind activate V1, n__isNatKind activate V2),
           isNatKind n__s V1 -> isNatKind activate V1,
                         0() -> n__0()}
  UR:
   {            U12(tt(), V2) -> U13 isNat activate V2,
                 isNat n__0() -> tt(),
        isNat n__plus(V1, V2) -> U11(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2),
                isNat n__s V1 -> U21(isNatKind activate V1, activate V1),
                   activate X -> X,
              activate n__0() -> 0(),
      activate n__isNatKind X -> isNatKind X,
     activate n__plus(X1, X2) -> plus(X1, X2),
              activate n__s X -> s X,
      activate n__and(X1, X2) -> and(X1, X2),
            U11(tt(), V1, V2) -> U12(isNat activate V1, activate V2),
                     U13 tt() -> tt(),
                     U22 tt() -> tt(),
                U21(tt(), V1) -> U22 isNat activate V1,
                 U31(tt(), N) -> activate N,
                          s X -> n__s X,
                 plus(N, s M) -> U41(and(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)), M, N),
                 plus(N, 0()) -> U31(and(isNat N, n__isNatKind N), N),
                 plus(X1, X2) -> n__plus(X1, X2),
              U41(tt(), M, N) -> s plus(activate N, activate M),
                  and(X1, X2) -> n__and(X1, X2),
                 and(tt(), X) -> activate X,
                  isNatKind X -> n__isNatKind X,
             isNatKind n__0() -> tt(),
    isNatKind n__plus(V1, V2) -> and(isNatKind activate V1, n__isNatKind activate V2),
            isNatKind n__s V1 -> isNatKind activate V1,
                          0() -> n__0(),
                      a(x, y) -> x,
                      a(x, y) -> y}
   EDG:
    {
     (activate# n__and(X1, X2) -> and#(X1, X2), and#(tt(), X) -> activate# X)
     (U11#(tt(), V1, V2) -> U12#(isNat activate V1, activate V2), U12#(tt(), V2) -> U13# isNat activate V2)
     (U11#(tt(), V1, V2) -> U12#(isNat activate V1, activate V2), U12#(tt(), V2) -> activate# V2)
     (U11#(tt(), V1, V2) -> U12#(isNat activate V1, activate V2), U12#(tt(), V2) -> isNat# activate V2)
     (plus#(N, 0()) -> and#(isNat N, n__isNatKind N), and#(tt(), X) -> activate# X)
     (plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)), and#(tt(), X) -> activate# X)
     (isNat# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2))
     (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# X)
     (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2))
     (isNat# n__s V1 -> activate# V1, activate# n__isNatKind X -> isNatKind# X)
     (isNat# n__s V1 -> activate# V1, activate# n__0() -> 0#())
     (U21#(tt(), V1) -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2))
     (U21#(tt(), V1) -> activate# V1, activate# n__s X -> s# X)
     (U21#(tt(), V1) -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2))
     (U21#(tt(), V1) -> activate# V1, activate# n__isNatKind X -> isNatKind# X)
     (U21#(tt(), V1) -> activate# V1, activate# n__0() -> 0#())
     (isNatKind# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2))
     (isNatKind# n__s V1 -> activate# V1, activate# n__s X -> s# X)
     (isNatKind# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2))
     (isNatKind# n__s V1 -> activate# V1, activate# n__isNatKind X -> isNatKind# X)
     (isNatKind# n__s V1 -> activate# V1, activate# n__0() -> 0#())
     (isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2), and#(tt(), X) -> activate# X)
     (U41#(tt(), M, N) -> activate# M, activate# n__and(X1, X2) -> and#(X1, X2))
     (U41#(tt(), M, N) -> activate# M, activate# n__s X -> s# X)
     (U41#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> plus#(X1, X2))
     (U41#(tt(), M, N) -> activate# M, activate# n__isNatKind X -> isNatKind# X)
     (U41#(tt(), M, N) -> activate# M, activate# n__0() -> 0#())
     (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
     (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1)
     (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1)
     (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V2)
     (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
     (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
     (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
     (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
     (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
     (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
     (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V2)
     (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V1)
     (isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
     (isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> activate# V1)
     (isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1)
     (isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V2)
     (isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
     (isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2), U11#(tt(), V1, V2) -> activate# V2)
     (isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2), U11#(tt(), V1, V2) -> activate# V1)
     (isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2), U11#(tt(), V1, V2) -> isNat# activate V1)
     (isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2), U11#(tt(), V1, V2) -> U12#(isNat activate V1, activate V2))
     (U31#(tt(), N) -> activate# N, activate# n__and(X1, X2) -> and#(X1, X2))
     (U31#(tt(), N) -> activate# N, activate# n__s X -> s# X)
     (U31#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> plus#(X1, X2))
     (U31#(tt(), N) -> activate# N, activate# n__isNatKind X -> isNatKind# X)
     (U31#(tt(), N) -> activate# N, activate# n__0() -> 0#())
     (plus#(N, 0()) -> isNat# N, isNat# n__s V1 -> isNatKind# activate V1)
     (plus#(N, 0()) -> isNat# N, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
     (plus#(N, 0()) -> isNat# N, isNat# n__s V1 -> activate# V1)
     (plus#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
     (plus#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (plus#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
     (plus#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> activate# V2)
     (plus#(N, 0()) -> isNat# N, isNat# n__plus(V1, V2) -> activate# V1)
     (plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)), M, N), U41#(tt(), M, N) -> plus#(activate N, activate M))
     (plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)), M, N), U41#(tt(), M, N) -> s# plus(activate N, activate M))
     (plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)), M, N), U41#(tt(), M, N) -> activate# M)
     (plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)), M, N), U41#(tt(), M, N) -> activate# N)
     (U12#(tt(), V2) -> activate# V2, activate# n__and(X1, X2) -> and#(X1, X2))
     (U12#(tt(), V2) -> activate# V2, activate# n__s X -> s# X)
     (U12#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(X1, X2))
     (U12#(tt(), V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
     (U12#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(X1, X2))
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# X)
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(X1, X2))
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(X1, X2))
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__s X -> s# X)
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(X1, X2))
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(X1, X2))
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__s X -> s# X)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(X1, X2))
     (U41#(tt(), M, N) -> activate# N, activate# n__0() -> 0#())
     (U41#(tt(), M, N) -> activate# N, activate# n__isNatKind X -> isNatKind# X)
     (U41#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> plus#(X1, X2))
     (U41#(tt(), M, N) -> activate# N, activate# n__s X -> s# X)
     (U41#(tt(), M, N) -> activate# N, activate# n__and(X1, X2) -> and#(X1, X2))
     (plus#(N, s M) -> isNat# N, isNat# n__plus(V1, V2) -> activate# V1)
     (plus#(N, s M) -> isNat# N, isNat# n__plus(V1, V2) -> activate# V2)
     (plus#(N, s M) -> isNat# N, isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
     (plus#(N, s M) -> isNat# N, isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (plus#(N, s M) -> isNat# N, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
     (plus#(N, s M) -> isNat# N, isNat# n__s V1 -> activate# V1)
     (plus#(N, s M) -> isNat# N, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
     (plus#(N, s M) -> isNat# N, isNat# n__s V1 -> isNatKind# activate V1)
     (plus#(N, 0()) -> U31#(and(isNat N, n__isNatKind N), N), U31#(tt(), N) -> activate# N)
     (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
     (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V2)
     (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> 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__s V1 -> isNatKind# activate V1)
     (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V1)
     (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V2)
     (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
     (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
     (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
     (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
     (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
     (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
     (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V2)
     (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> isNatKind# 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)
     (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> activate# V1)
     (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> activate# V2)
     (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
     (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
     (U12#(tt(), V2) -> isNat# activate V2, isNat# n__s V1 -> activate# V1)
     (U12#(tt(), V2) -> isNat# activate V2, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
     (U12#(tt(), V2) -> isNat# activate V2, isNat# n__s V1 -> isNatKind# activate V1)
     (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V1)
     (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V2)
     (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
     (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
     (plus#(N, s M) -> isNat# M, isNat# n__s V1 -> activate# V1)
     (plus#(N, s M) -> isNat# M, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
     (plus#(N, s M) -> isNat# M, isNat# n__s V1 -> isNatKind# activate V1)
     (isNatKind# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2), and#(tt(), X) -> activate# X)
     (and#(tt(), X) -> activate# X, activate# n__0() -> 0#())
     (and#(tt(), X) -> activate# X, activate# n__isNatKind X -> isNatKind# X)
     (and#(tt(), X) -> activate# X, activate# n__plus(X1, X2) -> plus#(X1, X2))
     (and#(tt(), X) -> activate# X, activate# n__s X -> s# X)
     (and#(tt(), X) -> activate# X, activate# n__and(X1, X2) -> and#(X1, X2))
     (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__plus(V1, V2) -> activate# V1)
     (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__plus(V1, V2) -> activate# V2)
     (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1)
     (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__s V1 -> activate# V1)
     (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__s V1 -> isNatKind# activate V1)
     (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__0() -> 0#())
     (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__isNatKind X -> isNatKind# X)
     (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2))
     (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__s X -> s# X)
     (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2))
     (U11#(tt(), V1, V2) -> activate# V1, activate# n__0() -> 0#())
     (U11#(tt(), V1, V2) -> activate# V1, activate# n__isNatKind X -> isNatKind# X)
     (U11#(tt(), V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2))
     (U11#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# X)
     (U11#(tt(), V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2))
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__0() -> 0#())
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__isNatKind X -> isNatKind# X)
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(X1, X2))
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__s X -> s# X)
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(X1, X2))
     (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> isNat# N)
     (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> isNat# M)
     (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)), M, N))
     (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> and#(isNat M, n__isNatKind M))
     (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)))
     (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, 0()) -> isNat# N)
     (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, 0()) -> U31#(and(isNat N, n__isNatKind N), N))
     (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, 0()) -> and#(isNat N, n__isNatKind N))
     (plus#(N, s M) -> and#(isNat M, n__isNatKind M), and#(tt(), X) -> activate# X)
     (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> isNat# activate V1)
     (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> activate# V1)
     (isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1), U21#(tt(), V1) -> U22# isNat activate V1)
     (activate# n__plus(X1, X2) -> plus#(X1, X2), plus#(N, s M) -> isNat# N)
     (activate# n__plus(X1, X2) -> plus#(X1, X2), plus#(N, s M) -> isNat# M)
     (activate# n__plus(X1, X2) -> plus#(X1, X2), plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)), M, N))
     (activate# n__plus(X1, X2) -> plus#(X1, X2), plus#(N, s M) -> and#(isNat M, n__isNatKind M))
     (activate# n__plus(X1, X2) -> plus#(X1, X2), plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)))
     (activate# n__plus(X1, X2) -> plus#(X1, X2), plus#(N, 0()) -> isNat# N)
     (activate# n__plus(X1, X2) -> plus#(X1, X2), plus#(N, 0()) -> U31#(and(isNat N, n__isNatKind N), N))
     (activate# n__plus(X1, X2) -> plus#(X1, X2), plus#(N, 0()) -> and#(isNat N, n__isNatKind N))
    }
    STATUS:
     arrows: 0.899946
     SCCS (1):
      Scc:
       {            U12#(tt(), V2) -> isNat# activate V2,
                    U12#(tt(), V2) -> activate# V2,
            isNat# n__plus(V1, V2) -> activate# V1,
            isNat# n__plus(V1, V2) -> activate# V2,
            isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2),
            isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2),
            isNat# n__plus(V1, V2) -> isNatKind# activate V1,
                    isNat# n__s V1 -> activate# V1,
                    isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1),
                    isNat# n__s V1 -> isNatKind# activate V1,
          activate# n__isNatKind X -> isNatKind# X,
         activate# n__plus(X1, X2) -> plus#(X1, X2),
          activate# n__and(X1, X2) -> and#(X1, X2),
                U11#(tt(), V1, V2) -> U12#(isNat activate V1, activate V2),
                U11#(tt(), V1, V2) -> isNat# activate V1,
                U11#(tt(), V1, V2) -> activate# V1,
                U11#(tt(), V1, V2) -> activate# V2,
                    U21#(tt(), V1) -> isNat# activate V1,
                    U21#(tt(), V1) -> activate# V1,
                     U31#(tt(), N) -> activate# N,
                     plus#(N, s M) -> isNat# N,
                     plus#(N, s M) -> isNat# M,
                     plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)), M, N),
                     plus#(N, s M) -> and#(isNat M, n__isNatKind M),
                     plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)),
                     plus#(N, 0()) -> isNat# N,
                     plus#(N, 0()) -> U31#(and(isNat N, n__isNatKind N), N),
                     plus#(N, 0()) -> and#(isNat N, n__isNatKind N),
                  U41#(tt(), M, N) -> activate# N,
                  U41#(tt(), M, N) -> activate# M,
                  U41#(tt(), M, N) -> plus#(activate N, activate M),
                     and#(tt(), X) -> activate# X,
        isNatKind# n__plus(V1, V2) -> activate# V1,
        isNatKind# n__plus(V1, V2) -> activate# V2,
        isNatKind# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2),
        isNatKind# n__plus(V1, V2) -> isNatKind# activate V1,
                isNatKind# n__s V1 -> activate# V1,
                isNatKind# n__s V1 -> isNatKind# activate V1}
      
      SCC (38):
       Strict:
        {            U12#(tt(), V2) -> isNat# activate V2,
                     U12#(tt(), V2) -> activate# V2,
             isNat# n__plus(V1, V2) -> activate# V1,
             isNat# n__plus(V1, V2) -> activate# V2,
             isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2),
             isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2),
             isNat# n__plus(V1, V2) -> isNatKind# activate V1,
                     isNat# n__s V1 -> activate# V1,
                     isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1),
                     isNat# n__s V1 -> isNatKind# activate V1,
           activate# n__isNatKind X -> isNatKind# X,
          activate# n__plus(X1, X2) -> plus#(X1, X2),
           activate# n__and(X1, X2) -> and#(X1, X2),
                 U11#(tt(), V1, V2) -> U12#(isNat activate V1, activate V2),
                 U11#(tt(), V1, V2) -> isNat# activate V1,
                 U11#(tt(), V1, V2) -> activate# V1,
                 U11#(tt(), V1, V2) -> activate# V2,
                     U21#(tt(), V1) -> isNat# activate V1,
                     U21#(tt(), V1) -> activate# V1,
                      U31#(tt(), N) -> activate# N,
                      plus#(N, s M) -> isNat# N,
                      plus#(N, s M) -> isNat# M,
                      plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)), M, N),
                      plus#(N, s M) -> and#(isNat M, n__isNatKind M),
                      plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)),
                      plus#(N, 0()) -> isNat# N,
                      plus#(N, 0()) -> U31#(and(isNat N, n__isNatKind N), N),
                      plus#(N, 0()) -> and#(isNat N, n__isNatKind N),
                   U41#(tt(), M, N) -> activate# N,
                   U41#(tt(), M, N) -> activate# M,
                   U41#(tt(), M, N) -> plus#(activate N, activate M),
                      and#(tt(), X) -> activate# X,
         isNatKind# n__plus(V1, V2) -> activate# V1,
         isNatKind# n__plus(V1, V2) -> activate# V2,
         isNatKind# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2),
         isNatKind# n__plus(V1, V2) -> isNatKind# activate V1,
                 isNatKind# n__s V1 -> activate# V1,
                 isNatKind# n__s V1 -> isNatKind# activate V1}
       Weak:
       {            U12(tt(), V2) -> U13 isNat activate V2,
                     isNat n__0() -> tt(),
            isNat n__plus(V1, V2) -> U11(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2),
                    isNat n__s V1 -> U21(isNatKind activate V1, activate V1),
                       activate X -> X,
                  activate n__0() -> 0(),
          activate n__isNatKind X -> isNatKind X,
         activate n__plus(X1, X2) -> plus(X1, X2),
                  activate n__s X -> s X,
          activate n__and(X1, X2) -> and(X1, X2),
                U11(tt(), V1, V2) -> U12(isNat activate V1, activate V2),
                         U13 tt() -> tt(),
                         U22 tt() -> tt(),
                    U21(tt(), V1) -> U22 isNat activate V1,
                     U31(tt(), N) -> activate N,
                              s X -> n__s X,
                     plus(N, s M) -> U41(and(and(isNat M, n__isNatKind M), n__and(isNat N, n__isNatKind N)), M, N),
                     plus(N, 0()) -> U31(and(isNat N, n__isNatKind N), N),
                     plus(X1, X2) -> n__plus(X1, X2),
                  U41(tt(), M, N) -> s plus(activate N, activate M),
                      and(X1, X2) -> n__and(X1, X2),
                     and(tt(), X) -> activate X,
                      isNatKind X -> n__isNatKind X,
                 isNatKind n__0() -> tt(),
        isNatKind n__plus(V1, V2) -> and(isNatKind activate V1, n__isNatKind activate V2),
                isNatKind n__s V1 -> isNatKind activate V1,
                              0() -> n__0()}
       Open