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