MAYBE
MAYBE
TRS:
 {
      U12(tt()) -> tt(),
        isNat() -> U11(isNat()),
        isNat() -> tt(),
        isNat() -> U21(isNat()),
      U11(tt()) -> U12(isNat()),
      U21(tt()) -> tt(),
      U31(tt()) -> N,
      U42(tt()) -> s(plus(N, M)),
      U41(tt()) -> U42(isNat()),
  plus(N, s(M)) -> U41(isNat()),
   plus(N, 0()) -> U31(isNat())
 }
 DUP: We consider a duplicating system.
  Trs:
   {
        U12(tt()) -> tt(),
          isNat() -> U11(isNat()),
          isNat() -> tt(),
          isNat() -> U21(isNat()),
        U11(tt()) -> U12(isNat()),
        U21(tt()) -> tt(),
        U31(tt()) -> N,
        U42(tt()) -> s(plus(N, M)),
        U41(tt()) -> U42(isNat()),
    plus(N, s(M)) -> U41(isNat()),
     plus(N, 0()) -> U31(isNat())
   }
  Fail