MAYBE
MAYBE
TRS:
 {
      U12(tt()) -> U13(isNat()),
        isNat() -> U11(and(isNatKind())),
        isNat() -> tt(),
        isNat() -> U21(isNatKind()),
        isNat() -> U31(and(isNatKind())),
      U11(tt()) -> U12(isNat()),
      U13(tt()) -> tt(),
      U22(tt()) -> tt(),
      U21(tt()) -> U22(isNat()),
      U32(tt()) -> U33(isNat()),
      U31(tt()) -> U32(isNat()),
      U33(tt()) -> tt(),
      U41(tt()) -> N,
  plus(N, s(M)) -> U51(and(and(isNat()))),
   plus(N, 0()) -> U41(and(isNat())),
      U51(tt()) -> s(plus(N, M)),
      U61(tt()) -> 0(),
     x(N, s(M)) -> U71(and(and(isNat()))),
      x(N, 0()) -> U61(and(isNat())),
      U71(tt()) -> plus(x(N, M), N),
      and(tt()) -> X,
    isNatKind() -> tt(),
    isNatKind() -> and(isNatKind()),
    isNatKind() -> isNatKind()
 }
 DUP: We consider a duplicating system.
  Trs:
   {
        U12(tt()) -> U13(isNat()),
          isNat() -> U11(and(isNatKind())),
          isNat() -> tt(),
          isNat() -> U21(isNatKind()),
          isNat() -> U31(and(isNatKind())),
        U11(tt()) -> U12(isNat()),
        U13(tt()) -> tt(),
        U22(tt()) -> tt(),
        U21(tt()) -> U22(isNat()),
        U32(tt()) -> U33(isNat()),
        U31(tt()) -> U32(isNat()),
        U33(tt()) -> tt(),
        U41(tt()) -> N,
    plus(N, s(M)) -> U51(and(and(isNat()))),
     plus(N, 0()) -> U41(and(isNat())),
        U51(tt()) -> s(plus(N, M)),
        U61(tt()) -> 0(),
       x(N, s(M)) -> U71(and(and(isNat()))),
        x(N, 0()) -> U61(and(isNat())),
        U71(tt()) -> plus(x(N, M), N),
        and(tt()) -> X,
      isNatKind() -> tt(),
      isNatKind() -> and(isNatKind()),
      isNatKind() -> isNatKind()
   }
  Fail