MAYBE
Time: 0.078649
TRS:
 {            U12(tt(), V2) -> U13 isNat activate V2,
                    isNat X -> n__isNat X,
               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(activate X1, activate X2),
            activate n__s X -> s activate X,
    activate n__and(X1, X2) -> and(activate X1, X2),
        activate n__isNat X -> isNat X,
          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(n__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) -> activate# X1,
     activate# n__plus(X1, X2) -> activate# X2,
     activate# n__plus(X1, X2) -> plus#(activate X1, activate X2),
              activate# n__s X -> activate# X,
              activate# n__s X -> s# activate X,
      activate# n__and(X1, X2) -> activate# X1,
      activate# n__and(X1, X2) -> and#(activate X1, X2),
          activate# n__isNat X -> isNat# X,
            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# M,
                 plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(n__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(n__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 X -> n__isNat X,
                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(activate X1, activate X2),
             activate n__s X -> s activate X,
     activate n__and(X1, X2) -> and(activate X1, X2),
         activate n__isNat X -> isNat X,
           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(n__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()}
  EDG:
   {
    (U12#(tt(), V2) -> isNat# activate V2, isNat# n__s V1 -> isNatKind# 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 -> activate# V1)
    (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
    (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) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
    (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> activate# V2)
    (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> 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 -> activate# V1)
    (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1)
    (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) -> activate# V2)
    (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
    (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
    (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
    (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
    (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
    (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) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
    (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V2)
    (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> 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__plus(V1, V2) -> isNatKind# activate V1)
    (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) -> activate# V2)
    (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
    (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, 0()) -> and#(isNat N, n__isNatKind N))
    (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, 0()) -> U31#(and(isNat N, n__isNatKind N), N))
    (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, 0()) -> isNat# N)
    (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)))
    (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> and#(isNat M, n__isNatKind M))
    (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)), M, N))
    (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> isNat# M)
    (plus#(N, s M) -> and#(isNat M, n__isNatKind M), and#(tt(), X) -> activate# X)
    (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, 0()) -> and#(isNat N, n__isNatKind 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()) -> isNat# N)
    (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind 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) -> U41#(and(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)), M, N))
    (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> isNat# M)
    (plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)), and#(tt(), X) -> activate# X)
    (activate# n__plus(X1, X2) -> activate# X1, activate# n__isNat X -> isNat# X)
    (activate# n__plus(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (activate# n__plus(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> activate# X1)
    (activate# n__plus(X1, X2) -> activate# X1, activate# n__s X -> s# activate X)
    (activate# n__plus(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
    (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X2)
    (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X1)
    (activate# n__plus(X1, X2) -> activate# X1, activate# n__isNatKind X -> isNatKind# X)
    (activate# n__plus(X1, X2) -> activate# X1, activate# n__0() -> 0#())
    (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__s V1 -> isNatKind# activate V1)
    (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__s V1 -> activate# V1)
    (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1)
    (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) -> activate# V2)
    (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__plus(V1, V2) -> activate# V1)
    (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> isNatKind# activate V1)
    (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
    (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> activate# V1)
    (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
    (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
    (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
    (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> activate# V2)
    (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> activate# V1)
    (plus#(N, s M) -> isNat# M, isNat# n__s V1 -> isNatKind# 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 -> activate# V1)
    (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
    (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) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
    (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V2)
    (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V1)
    (U41#(tt(), M, N) -> activate# M, activate# n__isNat X -> isNat# X)
    (U41#(tt(), M, N) -> activate# M, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (U41#(tt(), M, N) -> activate# M, activate# n__and(X1, X2) -> activate# X1)
    (U41#(tt(), M, N) -> activate# M, activate# n__s X -> s# activate X)
    (U41#(tt(), M, N) -> activate# M, activate# n__s X -> activate# X)
    (U41#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (U41#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> activate# X2)
    (U41#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> activate# X1)
    (U41#(tt(), M, N) -> activate# M, activate# n__isNatKind X -> isNatKind# X)
    (U41#(tt(), M, N) -> activate# M, 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(n__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(n__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(n__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(n__isNat N, n__isNatKind N)), M, N), U41#(tt(), M, N) -> activate# N)
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__s X -> s# activate X)
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__s X -> activate# X)
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
    (isNat# n__plus(V1, V2) -> activate# V2, activate# n__0() -> 0#())
    (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
    (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
    (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__s X -> s# activate X)
    (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__s X -> activate# X)
    (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
    (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
    (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
    (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__0() -> 0#())
    (isNatKind# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2), and#(tt(), X) -> activate# X)
    (isNat# n__s V1 -> activate# V1, activate# n__isNat X -> isNat# X)
    (isNat# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (isNat# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
    (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# activate X)
    (isNat# n__s V1 -> activate# V1, activate# n__s X -> activate# X)
    (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
    (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X1)
    (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__isNat X -> isNat# X)
    (U21#(tt(), V1) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (U21#(tt(), V1) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
    (U21#(tt(), V1) -> activate# V1, activate# n__s X -> s# activate X)
    (U21#(tt(), V1) -> activate# V1, activate# n__s X -> activate# X)
    (U21#(tt(), V1) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (U21#(tt(), V1) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
    (U21#(tt(), V1) -> activate# V1, activate# n__plus(X1, X2) -> activate# X1)
    (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__isNat X -> isNat# X)
    (isNatKind# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (isNatKind# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
    (isNatKind# n__s V1 -> activate# V1, activate# n__s X -> s# activate X)
    (isNatKind# n__s V1 -> activate# V1, activate# n__s X -> activate# X)
    (isNatKind# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (isNatKind# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
    (isNatKind# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X1)
    (isNatKind# n__s V1 -> activate# V1, activate# n__isNatKind X -> isNatKind# X)
    (isNatKind# n__s V1 -> activate# V1, activate# n__0() -> 0#())
    (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) -> activate# X1)
    (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
    (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__s X -> activate# X)
    (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__s X -> s# activate X)
    (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
    (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
    (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) -> activate# X1)
    (U11#(tt(), V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
    (U11#(tt(), V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (U11#(tt(), V1, V2) -> activate# V1, activate# n__s X -> activate# X)
    (U11#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# activate X)
    (U11#(tt(), V1, V2) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
    (U11#(tt(), V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (U11#(tt(), V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
    (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) -> activate# X1)
    (isNat# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
    (isNat# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (isNat# n__plus(V1, V2) -> activate# V1, activate# n__s X -> activate# X)
    (isNat# n__plus(V1, V2) -> activate# V1, activate# n__s X -> s# activate X)
    (isNat# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
    (isNat# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (isNat# n__plus(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
    (isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2), and#(tt(), X) -> activate# X)
    (U11#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
    (U11#(tt(), V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
    (U11#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
    (U11#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
    (U11#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (U11#(tt(), V1, V2) -> activate# V2, activate# n__s X -> activate# X)
    (U11#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# activate X)
    (U11#(tt(), V1, V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
    (U11#(tt(), V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (U11#(tt(), V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
    (U12#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
    (U12#(tt(), V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
    (U12#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
    (U12#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
    (U12#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (U12#(tt(), V2) -> activate# V2, activate# n__s X -> activate# X)
    (U12#(tt(), V2) -> activate# V2, activate# n__s X -> s# activate X)
    (U12#(tt(), V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
    (U12#(tt(), V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (U12#(tt(), V2) -> activate# V2, activate# n__isNat X -> isNat# X)
    (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) -> activate# X1)
    (U41#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> activate# X2)
    (U41#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (U41#(tt(), M, N) -> activate# N, activate# n__s X -> activate# X)
    (U41#(tt(), M, N) -> activate# N, activate# n__s X -> s# activate X)
    (U41#(tt(), M, N) -> activate# N, activate# n__and(X1, X2) -> activate# X1)
    (U41#(tt(), M, N) -> activate# N, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (U41#(tt(), M, N) -> activate# N, activate# n__isNat X -> isNat# X)
    (U31#(tt(), N) -> activate# N, activate# n__0() -> 0#())
    (U31#(tt(), N) -> activate# N, activate# n__isNatKind X -> isNatKind# X)
    (U31#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> activate# X1)
    (U31#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> activate# X2)
    (U31#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (U31#(tt(), N) -> activate# N, activate# n__s X -> activate# X)
    (U31#(tt(), N) -> activate# N, activate# n__s X -> s# activate X)
    (U31#(tt(), N) -> activate# N, activate# n__and(X1, X2) -> activate# X1)
    (U31#(tt(), N) -> activate# N, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (U31#(tt(), N) -> activate# N, activate# n__isNat X -> isNat# X)
    (plus#(N, 0()) -> U31#(and(isNat N, n__isNatKind N), N), U31#(tt(), N) -> activate# N)
    (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) -> activate# X1)
    (and#(tt(), X) -> activate# X, activate# n__plus(X1, X2) -> activate# X2)
    (and#(tt(), X) -> activate# X, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (and#(tt(), X) -> activate# X, activate# n__s X -> activate# X)
    (and#(tt(), X) -> activate# X, activate# n__s X -> s# activate X)
    (and#(tt(), X) -> activate# X, activate# n__and(X1, X2) -> activate# X1)
    (and#(tt(), X) -> activate# X, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (and#(tt(), X) -> activate# X, activate# n__isNat X -> isNat# X)
    (activate# n__s X -> activate# X, activate# n__0() -> 0#())
    (activate# n__s X -> activate# X, activate# n__isNatKind X -> isNatKind# X)
    (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> activate# X1)
    (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> activate# X2)
    (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (activate# n__s X -> activate# X, activate# n__s X -> activate# X)
    (activate# n__s X -> activate# X, activate# n__s X -> s# activate X)
    (activate# n__s X -> activate# X, activate# n__and(X1, X2) -> activate# X1)
    (activate# n__s X -> activate# X, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (activate# n__s X -> activate# X, activate# n__isNat X -> isNat# X)
    (activate# n__and(X1, X2) -> activate# X1, activate# n__0() -> 0#())
    (activate# n__and(X1, X2) -> activate# X1, activate# n__isNatKind X -> isNatKind# X)
    (activate# n__and(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X1)
    (activate# n__and(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X2)
    (activate# n__and(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (activate# n__and(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
    (activate# n__and(X1, X2) -> activate# X1, activate# n__s X -> s# activate X)
    (activate# n__and(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> activate# X1)
    (activate# n__and(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (activate# n__and(X1, X2) -> activate# X1, activate# n__isNat X -> isNat# X)
    (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))
    (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) -> 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)
    (activate# n__plus(X1, X2) -> activate# X2, activate# n__0() -> 0#())
    (activate# n__plus(X1, X2) -> activate# X2, activate# n__isNatKind X -> isNatKind# X)
    (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> activate# X1)
    (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> activate# X2)
    (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
    (activate# n__plus(X1, X2) -> activate# X2, activate# n__s X -> activate# X)
    (activate# n__plus(X1, X2) -> activate# X2, activate# n__s X -> s# activate X)
    (activate# n__plus(X1, X2) -> activate# X2, activate# n__and(X1, X2) -> activate# X1)
    (activate# n__plus(X1, X2) -> activate# X2, activate# n__and(X1, X2) -> and#(activate X1, X2))
    (activate# n__plus(X1, X2) -> activate# X2, activate# n__isNat X -> isNat# X)
    (activate# n__and(X1, X2) -> and#(activate X1, X2), and#(tt(), X) -> activate# X)
    (plus#(N, 0()) -> and#(isNat N, n__isNatKind N), and#(tt(), X) -> activate# X)
    (U11#(tt(), V1, V2) -> U12#(isNat activate V1, activate V2), U12#(tt(), V2) -> 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) -> U13# isNat activate V2)
    (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)
    (isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
    (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) -> and#(isNatKind activate V1, n__isNatKind activate V2))
    (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__s V1 -> activate# V1)
    (isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
    (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V1)
    (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) -> 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) -> and#(isNatKind activate V1, n__isNatKind activate V2))
    (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
    (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> 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 -> isNatKind# activate V1)
    (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
    (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) -> and#(isNatKind activate V1, n__isNatKind activate V2))
    (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__s V1 -> activate# V1)
    (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
   }
   EDG:
    {
     (U12#(tt(), V2) -> isNat# activate V2, isNat# n__s V1 -> isNatKind# 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 -> activate# V1)
     (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
     (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) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
     (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> activate# V2)
     (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> 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 -> activate# V1)
     (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1)
     (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) -> activate# V2)
     (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
     (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
     (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
     (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
     (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
     (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) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
     (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V2)
     (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> 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__plus(V1, V2) -> isNatKind# activate V1)
     (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) -> activate# V2)
     (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
     (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, 0()) -> and#(isNat N, n__isNatKind N))
     (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, 0()) -> U31#(and(isNat N, n__isNatKind N), N))
     (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, 0()) -> isNat# N)
     (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)))
     (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> and#(isNat M, n__isNatKind M))
     (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)), M, N))
     (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> isNat# M)
     (plus#(N, s M) -> and#(isNat M, n__isNatKind M), and#(tt(), X) -> activate# X)
     (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, 0()) -> and#(isNat N, n__isNatKind 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()) -> isNat# N)
     (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind 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) -> U41#(and(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)), M, N))
     (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> isNat# M)
     (plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)), and#(tt(), X) -> activate# X)
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__isNat X -> isNat# X)
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> activate# X1)
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__s X -> s# activate X)
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X2)
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X1)
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__isNatKind X -> isNatKind# X)
     (activate# n__plus(X1, X2) -> activate# X1, activate# n__0() -> 0#())
     (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__s V1 -> isNatKind# activate V1)
     (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__s V1 -> activate# V1)
     (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1)
     (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) -> activate# V2)
     (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__plus(V1, V2) -> activate# V1)
     (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> isNatKind# activate V1)
     (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
     (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> activate# V1)
     (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
     (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
     (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> activate# V2)
     (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> activate# V1)
     (plus#(N, s M) -> isNat# M, isNat# n__s V1 -> isNatKind# 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 -> activate# V1)
     (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
     (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) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
     (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V2)
     (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V1)
     (U41#(tt(), M, N) -> activate# M, activate# n__isNat X -> isNat# X)
     (U41#(tt(), M, N) -> activate# M, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (U41#(tt(), M, N) -> activate# M, activate# n__and(X1, X2) -> activate# X1)
     (U41#(tt(), M, N) -> activate# M, activate# n__s X -> s# activate X)
     (U41#(tt(), M, N) -> activate# M, activate# n__s X -> activate# X)
     (U41#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (U41#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> activate# X2)
     (U41#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> activate# X1)
     (U41#(tt(), M, N) -> activate# M, activate# n__isNatKind X -> isNatKind# X)
     (U41#(tt(), M, N) -> activate# M, 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(n__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(n__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(n__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(n__isNat N, n__isNatKind N)), M, N), U41#(tt(), M, N) -> activate# N)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__s X -> s# activate X)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__s X -> activate# X)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
     (isNat# n__plus(V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__s X -> s# activate X)
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__s X -> activate# X)
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
     (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (isNatKind# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2), and#(tt(), X) -> activate# X)
     (isNat# n__s V1 -> activate# V1, activate# n__isNat X -> isNat# X)
     (isNat# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (isNat# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
     (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# activate X)
     (isNat# n__s V1 -> activate# V1, activate# n__s X -> activate# X)
     (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
     (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X1)
     (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__isNat X -> isNat# X)
     (U21#(tt(), V1) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (U21#(tt(), V1) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
     (U21#(tt(), V1) -> activate# V1, activate# n__s X -> s# activate X)
     (U21#(tt(), V1) -> activate# V1, activate# n__s X -> activate# X)
     (U21#(tt(), V1) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (U21#(tt(), V1) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
     (U21#(tt(), V1) -> activate# V1, activate# n__plus(X1, X2) -> activate# X1)
     (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__isNat X -> isNat# X)
     (isNatKind# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (isNatKind# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
     (isNatKind# n__s V1 -> activate# V1, activate# n__s X -> s# activate X)
     (isNatKind# n__s V1 -> activate# V1, activate# n__s X -> activate# X)
     (isNatKind# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (isNatKind# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
     (isNatKind# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X1)
     (isNatKind# n__s V1 -> activate# V1, activate# n__isNatKind X -> isNatKind# X)
     (isNatKind# n__s V1 -> activate# V1, activate# n__0() -> 0#())
     (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) -> activate# X1)
     (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
     (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__s X -> activate# X)
     (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__s X -> s# activate X)
     (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
     (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
     (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) -> activate# X1)
     (U11#(tt(), V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
     (U11#(tt(), V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (U11#(tt(), V1, V2) -> activate# V1, activate# n__s X -> activate# X)
     (U11#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# activate X)
     (U11#(tt(), V1, V2) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
     (U11#(tt(), V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (U11#(tt(), V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
     (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) -> activate# X1)
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__s X -> activate# X)
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__s X -> s# activate X)
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (isNat# n__plus(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
     (isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2), and#(tt(), X) -> activate# X)
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__s X -> activate# X)
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# activate X)
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (U11#(tt(), V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
     (U12#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
     (U12#(tt(), V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
     (U12#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
     (U12#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
     (U12#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (U12#(tt(), V2) -> activate# V2, activate# n__s X -> activate# X)
     (U12#(tt(), V2) -> activate# V2, activate# n__s X -> s# activate X)
     (U12#(tt(), V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
     (U12#(tt(), V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (U12#(tt(), V2) -> activate# V2, activate# n__isNat X -> isNat# X)
     (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) -> activate# X1)
     (U41#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> activate# X2)
     (U41#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (U41#(tt(), M, N) -> activate# N, activate# n__s X -> activate# X)
     (U41#(tt(), M, N) -> activate# N, activate# n__s X -> s# activate X)
     (U41#(tt(), M, N) -> activate# N, activate# n__and(X1, X2) -> activate# X1)
     (U41#(tt(), M, N) -> activate# N, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (U41#(tt(), M, N) -> activate# N, activate# n__isNat X -> isNat# X)
     (U31#(tt(), N) -> activate# N, activate# n__0() -> 0#())
     (U31#(tt(), N) -> activate# N, activate# n__isNatKind X -> isNatKind# X)
     (U31#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> activate# X1)
     (U31#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> activate# X2)
     (U31#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (U31#(tt(), N) -> activate# N, activate# n__s X -> activate# X)
     (U31#(tt(), N) -> activate# N, activate# n__s X -> s# activate X)
     (U31#(tt(), N) -> activate# N, activate# n__and(X1, X2) -> activate# X1)
     (U31#(tt(), N) -> activate# N, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (U31#(tt(), N) -> activate# N, activate# n__isNat X -> isNat# X)
     (plus#(N, 0()) -> U31#(and(isNat N, n__isNatKind N), N), U31#(tt(), N) -> activate# N)
     (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) -> activate# X1)
     (and#(tt(), X) -> activate# X, activate# n__plus(X1, X2) -> activate# X2)
     (and#(tt(), X) -> activate# X, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (and#(tt(), X) -> activate# X, activate# n__s X -> activate# X)
     (and#(tt(), X) -> activate# X, activate# n__s X -> s# activate X)
     (and#(tt(), X) -> activate# X, activate# n__and(X1, X2) -> activate# X1)
     (and#(tt(), X) -> activate# X, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (and#(tt(), X) -> activate# X, activate# n__isNat X -> isNat# X)
     (activate# n__s X -> activate# X, activate# n__0() -> 0#())
     (activate# n__s X -> activate# X, activate# n__isNatKind X -> isNatKind# X)
     (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> activate# X1)
     (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> activate# X2)
     (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (activate# n__s X -> activate# X, activate# n__s X -> activate# X)
     (activate# n__s X -> activate# X, activate# n__s X -> s# activate X)
     (activate# n__s X -> activate# X, activate# n__and(X1, X2) -> activate# X1)
     (activate# n__s X -> activate# X, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (activate# n__s X -> activate# X, activate# n__isNat X -> isNat# X)
     (activate# n__and(X1, X2) -> activate# X1, activate# n__0() -> 0#())
     (activate# n__and(X1, X2) -> activate# X1, activate# n__isNatKind X -> isNatKind# X)
     (activate# n__and(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X1)
     (activate# n__and(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X2)
     (activate# n__and(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (activate# n__and(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
     (activate# n__and(X1, X2) -> activate# X1, activate# n__s X -> s# activate X)
     (activate# n__and(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> activate# X1)
     (activate# n__and(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (activate# n__and(X1, X2) -> activate# X1, activate# n__isNat X -> isNat# X)
     (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))
     (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) -> 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)
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__0() -> 0#())
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__isNatKind X -> isNatKind# X)
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> activate# X1)
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> activate# X2)
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__s X -> activate# X)
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__s X -> s# activate X)
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__and(X1, X2) -> activate# X1)
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__and(X1, X2) -> and#(activate X1, X2))
     (activate# n__plus(X1, X2) -> activate# X2, activate# n__isNat X -> isNat# X)
     (activate# n__and(X1, X2) -> and#(activate X1, X2), and#(tt(), X) -> activate# X)
     (plus#(N, 0()) -> and#(isNat N, n__isNatKind N), and#(tt(), X) -> activate# X)
     (U11#(tt(), V1, V2) -> U12#(isNat activate V1, activate V2), U12#(tt(), V2) -> 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) -> U13# isNat activate V2)
     (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)
     (isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
     (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) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (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__s V1 -> activate# V1)
     (isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
     (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V1)
     (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) -> 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) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
     (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> 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 -> isNatKind# activate V1)
     (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
     (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) -> and#(isNatKind activate V1, n__isNatKind activate V2))
     (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__s V1 -> activate# V1)
     (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
    }
    EDG:
     {
      (U12#(tt(), V2) -> isNat# activate V2, isNat# n__s V1 -> isNatKind# 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 -> activate# V1)
      (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
      (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) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
      (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> activate# V2)
      (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> 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 -> activate# V1)
      (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1)
      (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) -> activate# V2)
      (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
      (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
      (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
      (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
      (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
      (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) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
      (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V2)
      (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> 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__plus(V1, V2) -> isNatKind# activate V1)
      (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) -> activate# V2)
      (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
      (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, 0()) -> and#(isNat N, n__isNatKind N))
      (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, 0()) -> U31#(and(isNat N, n__isNatKind N), N))
      (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, 0()) -> isNat# N)
      (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)))
      (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> and#(isNat M, n__isNatKind M))
      (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)), M, N))
      (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> isNat# M)
      (plus#(N, s M) -> and#(isNat M, n__isNatKind M), and#(tt(), X) -> activate# X)
      (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, 0()) -> and#(isNat N, n__isNatKind 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()) -> isNat# N)
      (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind 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) -> U41#(and(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)), M, N))
      (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> isNat# M)
      (plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)), and#(tt(), X) -> activate# X)
      (activate# n__plus(X1, X2) -> activate# X1, activate# n__isNat X -> isNat# X)
      (activate# n__plus(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (activate# n__plus(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> activate# X1)
      (activate# n__plus(X1, X2) -> activate# X1, activate# n__s X -> s# activate X)
      (activate# n__plus(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
      (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X2)
      (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X1)
      (activate# n__plus(X1, X2) -> activate# X1, activate# n__isNatKind X -> isNatKind# X)
      (activate# n__plus(X1, X2) -> activate# X1, activate# n__0() -> 0#())
      (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__s V1 -> isNatKind# activate V1)
      (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__s V1 -> activate# V1)
      (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1)
      (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) -> activate# V2)
      (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__plus(V1, V2) -> activate# V1)
      (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> isNatKind# activate V1)
      (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
      (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> activate# V1)
      (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
      (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
      (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
      (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> activate# V2)
      (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> activate# V1)
      (plus#(N, s M) -> isNat# M, isNat# n__s V1 -> isNatKind# 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 -> activate# V1)
      (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
      (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) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
      (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V2)
      (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V1)
      (U41#(tt(), M, N) -> activate# M, activate# n__isNat X -> isNat# X)
      (U41#(tt(), M, N) -> activate# M, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (U41#(tt(), M, N) -> activate# M, activate# n__and(X1, X2) -> activate# X1)
      (U41#(tt(), M, N) -> activate# M, activate# n__s X -> s# activate X)
      (U41#(tt(), M, N) -> activate# M, activate# n__s X -> activate# X)
      (U41#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (U41#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> activate# X2)
      (U41#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> activate# X1)
      (U41#(tt(), M, N) -> activate# M, activate# n__isNatKind X -> isNatKind# X)
      (U41#(tt(), M, N) -> activate# M, 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(n__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(n__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(n__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(n__isNat N, n__isNatKind N)), M, N), U41#(tt(), M, N) -> activate# N)
      (isNat# n__plus(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
      (isNat# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (isNat# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
      (isNat# n__plus(V1, V2) -> activate# V2, activate# n__s X -> s# activate X)
      (isNat# n__plus(V1, V2) -> activate# V2, activate# n__s X -> activate# X)
      (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
      (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
      (isNat# n__plus(V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
      (isNat# n__plus(V1, V2) -> activate# V2, activate# n__0() -> 0#())
      (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
      (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
      (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__s X -> s# activate X)
      (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__s X -> activate# X)
      (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
      (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
      (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
      (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__0() -> 0#())
      (isNatKind# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2), and#(tt(), X) -> activate# X)
      (isNat# n__s V1 -> activate# V1, activate# n__isNat X -> isNat# X)
      (isNat# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (isNat# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
      (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# activate X)
      (isNat# n__s V1 -> activate# V1, activate# n__s X -> activate# X)
      (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
      (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X1)
      (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__isNat X -> isNat# X)
      (U21#(tt(), V1) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (U21#(tt(), V1) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
      (U21#(tt(), V1) -> activate# V1, activate# n__s X -> s# activate X)
      (U21#(tt(), V1) -> activate# V1, activate# n__s X -> activate# X)
      (U21#(tt(), V1) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (U21#(tt(), V1) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
      (U21#(tt(), V1) -> activate# V1, activate# n__plus(X1, X2) -> activate# X1)
      (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__isNat X -> isNat# X)
      (isNatKind# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (isNatKind# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
      (isNatKind# n__s V1 -> activate# V1, activate# n__s X -> s# activate X)
      (isNatKind# n__s V1 -> activate# V1, activate# n__s X -> activate# X)
      (isNatKind# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (isNatKind# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
      (isNatKind# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X1)
      (isNatKind# n__s V1 -> activate# V1, activate# n__isNatKind X -> isNatKind# X)
      (isNatKind# n__s V1 -> activate# V1, activate# n__0() -> 0#())
      (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) -> activate# X1)
      (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
      (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__s X -> activate# X)
      (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__s X -> s# activate X)
      (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
      (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
      (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) -> activate# X1)
      (U11#(tt(), V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
      (U11#(tt(), V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (U11#(tt(), V1, V2) -> activate# V1, activate# n__s X -> activate# X)
      (U11#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# activate X)
      (U11#(tt(), V1, V2) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
      (U11#(tt(), V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (U11#(tt(), V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
      (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) -> activate# X1)
      (isNat# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
      (isNat# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (isNat# n__plus(V1, V2) -> activate# V1, activate# n__s X -> activate# X)
      (isNat# n__plus(V1, V2) -> activate# V1, activate# n__s X -> s# activate X)
      (isNat# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
      (isNat# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (isNat# n__plus(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
      (isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2), and#(tt(), X) -> activate# X)
      (U11#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
      (U11#(tt(), V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
      (U11#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
      (U11#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
      (U11#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (U11#(tt(), V1, V2) -> activate# V2, activate# n__s X -> activate# X)
      (U11#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# activate X)
      (U11#(tt(), V1, V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
      (U11#(tt(), V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (U11#(tt(), V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
      (U12#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
      (U12#(tt(), V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
      (U12#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
      (U12#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
      (U12#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (U12#(tt(), V2) -> activate# V2, activate# n__s X -> activate# X)
      (U12#(tt(), V2) -> activate# V2, activate# n__s X -> s# activate X)
      (U12#(tt(), V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
      (U12#(tt(), V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (U12#(tt(), V2) -> activate# V2, activate# n__isNat X -> isNat# X)
      (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) -> activate# X1)
      (U41#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> activate# X2)
      (U41#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (U41#(tt(), M, N) -> activate# N, activate# n__s X -> activate# X)
      (U41#(tt(), M, N) -> activate# N, activate# n__s X -> s# activate X)
      (U41#(tt(), M, N) -> activate# N, activate# n__and(X1, X2) -> activate# X1)
      (U41#(tt(), M, N) -> activate# N, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (U41#(tt(), M, N) -> activate# N, activate# n__isNat X -> isNat# X)
      (U31#(tt(), N) -> activate# N, activate# n__0() -> 0#())
      (U31#(tt(), N) -> activate# N, activate# n__isNatKind X -> isNatKind# X)
      (U31#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> activate# X1)
      (U31#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> activate# X2)
      (U31#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (U31#(tt(), N) -> activate# N, activate# n__s X -> activate# X)
      (U31#(tt(), N) -> activate# N, activate# n__s X -> s# activate X)
      (U31#(tt(), N) -> activate# N, activate# n__and(X1, X2) -> activate# X1)
      (U31#(tt(), N) -> activate# N, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (U31#(tt(), N) -> activate# N, activate# n__isNat X -> isNat# X)
      (plus#(N, 0()) -> U31#(and(isNat N, n__isNatKind N), N), U31#(tt(), N) -> activate# N)
      (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) -> activate# X1)
      (and#(tt(), X) -> activate# X, activate# n__plus(X1, X2) -> activate# X2)
      (and#(tt(), X) -> activate# X, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (and#(tt(), X) -> activate# X, activate# n__s X -> activate# X)
      (and#(tt(), X) -> activate# X, activate# n__s X -> s# activate X)
      (and#(tt(), X) -> activate# X, activate# n__and(X1, X2) -> activate# X1)
      (and#(tt(), X) -> activate# X, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (and#(tt(), X) -> activate# X, activate# n__isNat X -> isNat# X)
      (activate# n__s X -> activate# X, activate# n__0() -> 0#())
      (activate# n__s X -> activate# X, activate# n__isNatKind X -> isNatKind# X)
      (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> activate# X1)
      (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> activate# X2)
      (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (activate# n__s X -> activate# X, activate# n__s X -> activate# X)
      (activate# n__s X -> activate# X, activate# n__s X -> s# activate X)
      (activate# n__s X -> activate# X, activate# n__and(X1, X2) -> activate# X1)
      (activate# n__s X -> activate# X, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (activate# n__s X -> activate# X, activate# n__isNat X -> isNat# X)
      (activate# n__and(X1, X2) -> activate# X1, activate# n__0() -> 0#())
      (activate# n__and(X1, X2) -> activate# X1, activate# n__isNatKind X -> isNatKind# X)
      (activate# n__and(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X1)
      (activate# n__and(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X2)
      (activate# n__and(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (activate# n__and(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
      (activate# n__and(X1, X2) -> activate# X1, activate# n__s X -> s# activate X)
      (activate# n__and(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> activate# X1)
      (activate# n__and(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (activate# n__and(X1, X2) -> activate# X1, activate# n__isNat X -> isNat# X)
      (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))
      (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) -> 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)
      (activate# n__plus(X1, X2) -> activate# X2, activate# n__0() -> 0#())
      (activate# n__plus(X1, X2) -> activate# X2, activate# n__isNatKind X -> isNatKind# X)
      (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> activate# X1)
      (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> activate# X2)
      (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
      (activate# n__plus(X1, X2) -> activate# X2, activate# n__s X -> activate# X)
      (activate# n__plus(X1, X2) -> activate# X2, activate# n__s X -> s# activate X)
      (activate# n__plus(X1, X2) -> activate# X2, activate# n__and(X1, X2) -> activate# X1)
      (activate# n__plus(X1, X2) -> activate# X2, activate# n__and(X1, X2) -> and#(activate X1, X2))
      (activate# n__plus(X1, X2) -> activate# X2, activate# n__isNat X -> isNat# X)
      (activate# n__and(X1, X2) -> and#(activate X1, X2), and#(tt(), X) -> activate# X)
      (plus#(N, 0()) -> and#(isNat N, n__isNatKind N), and#(tt(), X) -> activate# X)
      (U11#(tt(), V1, V2) -> U12#(isNat activate V1, activate V2), U12#(tt(), V2) -> 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) -> U13# isNat activate V2)
      (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)
      (isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
      (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) -> and#(isNatKind activate V1, n__isNatKind activate V2))
      (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__s V1 -> activate# V1)
      (isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
      (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V1)
      (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) -> 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) -> and#(isNatKind activate V1, n__isNatKind activate V2))
      (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
      (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> 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 -> isNatKind# activate V1)
      (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
      (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) -> and#(isNatKind activate V1, n__isNatKind activate V2))
      (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__s V1 -> activate# V1)
      (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
     }
     EDG:
      {
       (U12#(tt(), V2) -> isNat# activate V2, isNat# n__s V1 -> isNatKind# 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 -> activate# V1)
       (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
       (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) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
       (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> activate# V2)
       (U12#(tt(), V2) -> isNat# activate V2, isNat# n__plus(V1, V2) -> 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 -> activate# V1)
       (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1)
       (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) -> activate# V2)
       (isNat# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
       (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> isNatKind# activate V1)
       (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
       (U21#(tt(), V1) -> isNat# activate V1, isNat# n__s V1 -> activate# V1)
       (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
       (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) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
       (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V2)
       (U21#(tt(), V1) -> isNat# activate V1, isNat# n__plus(V1, V2) -> 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__plus(V1, V2) -> isNatKind# activate V1)
       (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) -> activate# V2)
       (isNatKind# n__s V1 -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
       (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, 0()) -> and#(isNat N, n__isNatKind N))
       (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, 0()) -> U31#(and(isNat N, n__isNatKind N), N))
       (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, 0()) -> isNat# N)
       (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)))
       (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> and#(isNat M, n__isNatKind M))
       (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)), M, N))
       (activate# n__plus(X1, X2) -> plus#(activate X1, activate X2), plus#(N, s M) -> isNat# M)
       (plus#(N, s M) -> and#(isNat M, n__isNatKind M), and#(tt(), X) -> activate# X)
       (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, 0()) -> and#(isNat N, n__isNatKind 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()) -> isNat# N)
       (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind 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) -> U41#(and(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)), M, N))
       (U41#(tt(), M, N) -> plus#(activate N, activate M), plus#(N, s M) -> isNat# M)
       (plus#(N, s M) -> and#(and(isNat M, n__isNatKind M), n__and(n__isNat N, n__isNatKind N)), and#(tt(), X) -> activate# X)
       (activate# n__plus(X1, X2) -> activate# X1, activate# n__isNat X -> isNat# X)
       (activate# n__plus(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (activate# n__plus(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> activate# X1)
       (activate# n__plus(X1, X2) -> activate# X1, activate# n__s X -> s# activate X)
       (activate# n__plus(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
       (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X2)
       (activate# n__plus(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X1)
       (activate# n__plus(X1, X2) -> activate# X1, activate# n__isNatKind X -> isNatKind# X)
       (activate# n__plus(X1, X2) -> activate# X1, activate# n__0() -> 0#())
       (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__s V1 -> isNatKind# activate V1)
       (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__s V1 -> activate# V1)
       (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__plus(V1, V2) -> isNatKind# activate V1)
       (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) -> activate# V2)
       (activate# n__isNatKind X -> isNatKind# X, isNatKind# n__plus(V1, V2) -> activate# V1)
       (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> isNatKind# activate V1)
       (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> U21#(isNatKind activate V1, activate V1))
       (activate# n__isNat X -> isNat# X, isNat# n__s V1 -> activate# V1)
       (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
       (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2))
       (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
       (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> activate# V2)
       (activate# n__isNat X -> isNat# X, isNat# n__plus(V1, V2) -> activate# V1)
       (plus#(N, s M) -> isNat# M, isNat# n__s V1 -> isNatKind# 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 -> activate# V1)
       (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
       (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) -> U11#(and(isNatKind activate V1, n__isNatKind activate V2), activate V1, activate V2))
       (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V2)
       (plus#(N, s M) -> isNat# M, isNat# n__plus(V1, V2) -> activate# V1)
       (U41#(tt(), M, N) -> activate# M, activate# n__isNat X -> isNat# X)
       (U41#(tt(), M, N) -> activate# M, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (U41#(tt(), M, N) -> activate# M, activate# n__and(X1, X2) -> activate# X1)
       (U41#(tt(), M, N) -> activate# M, activate# n__s X -> s# activate X)
       (U41#(tt(), M, N) -> activate# M, activate# n__s X -> activate# X)
       (U41#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (U41#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> activate# X2)
       (U41#(tt(), M, N) -> activate# M, activate# n__plus(X1, X2) -> activate# X1)
       (U41#(tt(), M, N) -> activate# M, activate# n__isNatKind X -> isNatKind# X)
       (U41#(tt(), M, N) -> activate# M, 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(n__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(n__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(n__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(n__isNat N, n__isNatKind N)), M, N), U41#(tt(), M, N) -> activate# N)
       (isNat# n__plus(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
       (isNat# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (isNat# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
       (isNat# n__plus(V1, V2) -> activate# V2, activate# n__s X -> s# activate X)
       (isNat# n__plus(V1, V2) -> activate# V2, activate# n__s X -> activate# X)
       (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
       (isNat# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
       (isNat# n__plus(V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
       (isNat# n__plus(V1, V2) -> activate# V2, activate# n__0() -> 0#())
       (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
       (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
       (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__s X -> s# activate X)
       (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__s X -> activate# X)
       (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
       (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
       (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
       (isNatKind# n__plus(V1, V2) -> activate# V2, activate# n__0() -> 0#())
       (isNatKind# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2), and#(tt(), X) -> activate# X)
       (isNat# n__s V1 -> activate# V1, activate# n__isNat X -> isNat# X)
       (isNat# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (isNat# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
       (isNat# n__s V1 -> activate# V1, activate# n__s X -> s# activate X)
       (isNat# n__s V1 -> activate# V1, activate# n__s X -> activate# X)
       (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
       (isNat# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X1)
       (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__isNat X -> isNat# X)
       (U21#(tt(), V1) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (U21#(tt(), V1) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
       (U21#(tt(), V1) -> activate# V1, activate# n__s X -> s# activate X)
       (U21#(tt(), V1) -> activate# V1, activate# n__s X -> activate# X)
       (U21#(tt(), V1) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (U21#(tt(), V1) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
       (U21#(tt(), V1) -> activate# V1, activate# n__plus(X1, X2) -> activate# X1)
       (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__isNat X -> isNat# X)
       (isNatKind# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (isNatKind# n__s V1 -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
       (isNatKind# n__s V1 -> activate# V1, activate# n__s X -> s# activate X)
       (isNatKind# n__s V1 -> activate# V1, activate# n__s X -> activate# X)
       (isNatKind# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (isNatKind# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
       (isNatKind# n__s V1 -> activate# V1, activate# n__plus(X1, X2) -> activate# X1)
       (isNatKind# n__s V1 -> activate# V1, activate# n__isNatKind X -> isNatKind# X)
       (isNatKind# n__s V1 -> activate# V1, activate# n__0() -> 0#())
       (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) -> activate# X1)
       (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
       (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__s X -> activate# X)
       (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__s X -> s# activate X)
       (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
       (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (isNatKind# n__plus(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
       (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) -> activate# X1)
       (U11#(tt(), V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
       (U11#(tt(), V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (U11#(tt(), V1, V2) -> activate# V1, activate# n__s X -> activate# X)
       (U11#(tt(), V1, V2) -> activate# V1, activate# n__s X -> s# activate X)
       (U11#(tt(), V1, V2) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
       (U11#(tt(), V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (U11#(tt(), V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
       (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) -> activate# X1)
       (isNat# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> activate# X2)
       (isNat# n__plus(V1, V2) -> activate# V1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (isNat# n__plus(V1, V2) -> activate# V1, activate# n__s X -> activate# X)
       (isNat# n__plus(V1, V2) -> activate# V1, activate# n__s X -> s# activate X)
       (isNat# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> activate# X1)
       (isNat# n__plus(V1, V2) -> activate# V1, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (isNat# n__plus(V1, V2) -> activate# V1, activate# n__isNat X -> isNat# X)
       (isNat# n__plus(V1, V2) -> and#(isNatKind activate V1, n__isNatKind activate V2), and#(tt(), X) -> activate# X)
       (U11#(tt(), V1, V2) -> activate# V2, activate# n__0() -> 0#())
       (U11#(tt(), V1, V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
       (U11#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
       (U11#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
       (U11#(tt(), V1, V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (U11#(tt(), V1, V2) -> activate# V2, activate# n__s X -> activate# X)
       (U11#(tt(), V1, V2) -> activate# V2, activate# n__s X -> s# activate X)
       (U11#(tt(), V1, V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
       (U11#(tt(), V1, V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (U11#(tt(), V1, V2) -> activate# V2, activate# n__isNat X -> isNat# X)
       (U12#(tt(), V2) -> activate# V2, activate# n__0() -> 0#())
       (U12#(tt(), V2) -> activate# V2, activate# n__isNatKind X -> isNatKind# X)
       (U12#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X1)
       (U12#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> activate# X2)
       (U12#(tt(), V2) -> activate# V2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (U12#(tt(), V2) -> activate# V2, activate# n__s X -> activate# X)
       (U12#(tt(), V2) -> activate# V2, activate# n__s X -> s# activate X)
       (U12#(tt(), V2) -> activate# V2, activate# n__and(X1, X2) -> activate# X1)
       (U12#(tt(), V2) -> activate# V2, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (U12#(tt(), V2) -> activate# V2, activate# n__isNat X -> isNat# X)
       (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) -> activate# X1)
       (U41#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> activate# X2)
       (U41#(tt(), M, N) -> activate# N, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (U41#(tt(), M, N) -> activate# N, activate# n__s X -> activate# X)
       (U41#(tt(), M, N) -> activate# N, activate# n__s X -> s# activate X)
       (U41#(tt(), M, N) -> activate# N, activate# n__and(X1, X2) -> activate# X1)
       (U41#(tt(), M, N) -> activate# N, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (U41#(tt(), M, N) -> activate# N, activate# n__isNat X -> isNat# X)
       (U31#(tt(), N) -> activate# N, activate# n__0() -> 0#())
       (U31#(tt(), N) -> activate# N, activate# n__isNatKind X -> isNatKind# X)
       (U31#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> activate# X1)
       (U31#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> activate# X2)
       (U31#(tt(), N) -> activate# N, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (U31#(tt(), N) -> activate# N, activate# n__s X -> activate# X)
       (U31#(tt(), N) -> activate# N, activate# n__s X -> s# activate X)
       (U31#(tt(), N) -> activate# N, activate# n__and(X1, X2) -> activate# X1)
       (U31#(tt(), N) -> activate# N, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (U31#(tt(), N) -> activate# N, activate# n__isNat X -> isNat# X)
       (plus#(N, 0()) -> U31#(and(isNat N, n__isNatKind N), N), U31#(tt(), N) -> activate# N)
       (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) -> activate# X1)
       (and#(tt(), X) -> activate# X, activate# n__plus(X1, X2) -> activate# X2)
       (and#(tt(), X) -> activate# X, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (and#(tt(), X) -> activate# X, activate# n__s X -> activate# X)
       (and#(tt(), X) -> activate# X, activate# n__s X -> s# activate X)
       (and#(tt(), X) -> activate# X, activate# n__and(X1, X2) -> activate# X1)
       (and#(tt(), X) -> activate# X, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (and#(tt(), X) -> activate# X, activate# n__isNat X -> isNat# X)
       (activate# n__s X -> activate# X, activate# n__0() -> 0#())
       (activate# n__s X -> activate# X, activate# n__isNatKind X -> isNatKind# X)
       (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> activate# X1)
       (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> activate# X2)
       (activate# n__s X -> activate# X, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (activate# n__s X -> activate# X, activate# n__s X -> activate# X)
       (activate# n__s X -> activate# X, activate# n__s X -> s# activate X)
       (activate# n__s X -> activate# X, activate# n__and(X1, X2) -> activate# X1)
       (activate# n__s X -> activate# X, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (activate# n__s X -> activate# X, activate# n__isNat X -> isNat# X)
       (activate# n__and(X1, X2) -> activate# X1, activate# n__0() -> 0#())
       (activate# n__and(X1, X2) -> activate# X1, activate# n__isNatKind X -> isNatKind# X)
       (activate# n__and(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X1)
       (activate# n__and(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> activate# X2)
       (activate# n__and(X1, X2) -> activate# X1, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (activate# n__and(X1, X2) -> activate# X1, activate# n__s X -> activate# X)
       (activate# n__and(X1, X2) -> activate# X1, activate# n__s X -> s# activate X)
       (activate# n__and(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> activate# X1)
       (activate# n__and(X1, X2) -> activate# X1, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (activate# n__and(X1, X2) -> activate# X1, activate# n__isNat X -> isNat# X)
       (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))
       (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) -> 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)
       (activate# n__plus(X1, X2) -> activate# X2, activate# n__0() -> 0#())
       (activate# n__plus(X1, X2) -> activate# X2, activate# n__isNatKind X -> isNatKind# X)
       (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> activate# X1)
       (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> activate# X2)
       (activate# n__plus(X1, X2) -> activate# X2, activate# n__plus(X1, X2) -> plus#(activate X1, activate X2))
       (activate# n__plus(X1, X2) -> activate# X2, activate# n__s X -> activate# X)
       (activate# n__plus(X1, X2) -> activate# X2, activate# n__s X -> s# activate X)
       (activate# n__plus(X1, X2) -> activate# X2, activate# n__and(X1, X2) -> activate# X1)
       (activate# n__plus(X1, X2) -> activate# X2, activate# n__and(X1, X2) -> and#(activate X1, X2))
       (activate# n__plus(X1, X2) -> activate# X2, activate# n__isNat X -> isNat# X)
       (activate# n__and(X1, X2) -> and#(activate X1, X2), and#(tt(), X) -> activate# X)
       (plus#(N, 0()) -> and#(isNat N, n__isNatKind N), and#(tt(), X) -> activate# X)
       (U11#(tt(), V1, V2) -> U12#(isNat activate V1, activate V2), U12#(tt(), V2) -> 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) -> U13# isNat activate V2)
       (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)
       (isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
       (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) -> and#(isNatKind activate V1, n__isNatKind activate V2))
       (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__s V1 -> activate# V1)
       (isNatKind# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
       (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> activate# V1)
       (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) -> 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) -> and#(isNatKind activate V1, n__isNatKind activate V2))
       (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__plus(V1, V2) -> isNatKind# activate V1)
       (U11#(tt(), V1, V2) -> isNat# activate V1, isNat# n__s V1 -> 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 -> isNatKind# activate V1)
       (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__plus(V1, V2) -> activate# V1)
       (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) -> and#(isNatKind activate V1, n__isNatKind activate V2))
       (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__s V1 -> activate# V1)
       (isNat# n__plus(V1, V2) -> isNatKind# activate V1, isNatKind# n__s V1 -> isNatKind# activate V1)
      }
      STATUS:
       arrows: 0.867361
       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) -> activate# X1,
           activate# n__plus(X1, X2) -> activate# X2,
           activate# n__plus(X1, X2) -> plus#(activate X1, activate X2),
                    activate# n__s X -> activate# X,
            activate# n__and(X1, X2) -> activate# X1,
            activate# n__and(X1, X2) -> and#(activate X1, X2),
                activate# n__isNat X -> isNat# X,
                  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# M,
                       plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(n__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(n__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 (42):
         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) -> activate# X1,
            activate# n__plus(X1, X2) -> activate# X2,
            activate# n__plus(X1, X2) -> plus#(activate X1, activate X2),
                     activate# n__s X -> activate# X,
             activate# n__and(X1, X2) -> activate# X1,
             activate# n__and(X1, X2) -> and#(activate X1, X2),
                 activate# n__isNat X -> isNat# X,
                   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# M,
                        plus#(N, s M) -> U41#(and(and(isNat M, n__isNatKind M), n__and(n__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(n__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 X -> n__isNat X,
                       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(activate X1, activate X2),
                    activate n__s X -> s activate X,
            activate n__and(X1, X2) -> and(activate X1, X2),
                activate n__isNat X -> isNat X,
                  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(n__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