MAYBE
MAYBE
TRS:
 {
     U102(tt()) -> U103(isNat()),
    isNatKind() -> tt(),
    isNatKind() -> U41(isNatKind()),
    isNatKind() -> U51(isNatKind()),
    isNatKind() -> U61(isNatKind()),
     U101(tt()) -> U102(isNatKind()),
     U103(tt()) -> U104(isNatKind()),
        isNat() -> tt(),
        isNat() -> U11(isNatKind()),
        isNat() -> U21(isNatKind()),
        isNat() -> U31(isNatKind()),
     U104(tt()) -> plus(x(N, M), N),
  plus(N, s(M)) -> U81(isNat()),
   plus(N, 0()) -> U71(isNat()),
     x(N, s(M)) -> U101(isNat()),
      x(N, 0()) -> U91(isNat()),
      U12(tt()) -> U13(isNatKind()),
      U11(tt()) -> U12(isNatKind()),
      U13(tt()) -> U14(isNatKind()),
      U14(tt()) -> U15(isNat()),
      U15(tt()) -> U16(isNat()),
      U16(tt()) -> tt(),
      U22(tt()) -> U23(isNat()),
      U21(tt()) -> U22(isNatKind()),
      U23(tt()) -> tt(),
      U32(tt()) -> U33(isNatKind()),
      U31(tt()) -> U32(isNatKind()),
      U33(tt()) -> U34(isNatKind()),
      U34(tt()) -> U35(isNat()),
      U35(tt()) -> U36(isNat()),
      U36(tt()) -> tt(),
      U42(tt()) -> tt(),
      U41(tt()) -> U42(isNatKind()),
      U51(tt()) -> tt(),
      U62(tt()) -> tt(),
      U61(tt()) -> U62(isNatKind()),
      U72(tt()) -> N,
      U71(tt()) -> U72(isNatKind()),
      U82(tt()) -> U83(isNat()),
      U81(tt()) -> U82(isNatKind()),
      U83(tt()) -> U84(isNatKind()),
      U84(tt()) -> s(plus(N, M)),
      U92(tt()) -> 0(),
      U91(tt()) -> U92(isNatKind())
 }
 DUP: We consider a duplicating system.
  Trs:
   {
       U102(tt()) -> U103(isNat()),
      isNatKind() -> tt(),
      isNatKind() -> U41(isNatKind()),
      isNatKind() -> U51(isNatKind()),
      isNatKind() -> U61(isNatKind()),
       U101(tt()) -> U102(isNatKind()),
       U103(tt()) -> U104(isNatKind()),
          isNat() -> tt(),
          isNat() -> U11(isNatKind()),
          isNat() -> U21(isNatKind()),
          isNat() -> U31(isNatKind()),
       U104(tt()) -> plus(x(N, M), N),
    plus(N, s(M)) -> U81(isNat()),
     plus(N, 0()) -> U71(isNat()),
       x(N, s(M)) -> U101(isNat()),
        x(N, 0()) -> U91(isNat()),
        U12(tt()) -> U13(isNatKind()),
        U11(tt()) -> U12(isNatKind()),
        U13(tt()) -> U14(isNatKind()),
        U14(tt()) -> U15(isNat()),
        U15(tt()) -> U16(isNat()),
        U16(tt()) -> tt(),
        U22(tt()) -> U23(isNat()),
        U21(tt()) -> U22(isNatKind()),
        U23(tt()) -> tt(),
        U32(tt()) -> U33(isNatKind()),
        U31(tt()) -> U32(isNatKind()),
        U33(tt()) -> U34(isNatKind()),
        U34(tt()) -> U35(isNat()),
        U35(tt()) -> U36(isNat()),
        U36(tt()) -> tt(),
        U42(tt()) -> tt(),
        U41(tt()) -> U42(isNatKind()),
        U51(tt()) -> tt(),
        U62(tt()) -> tt(),
        U61(tt()) -> U62(isNatKind()),
        U72(tt()) -> N,
        U71(tt()) -> U72(isNatKind()),
        U82(tt()) -> U83(isNat()),
        U81(tt()) -> U82(isNatKind()),
        U83(tt()) -> U84(isNatKind()),
        U84(tt()) -> s(plus(N, M)),
        U92(tt()) -> 0(),
        U91(tt()) -> U92(isNatKind())
   }
  Fail