MAYBE
MAYBE
TRS:
 {
            p(s(x)) -> x,
             p(0()) -> s(s(0())),
         p(p(s(x))) -> p(x),
     le(s(x), s(y)) -> le(x, y),
      le(s(x), 0()) -> false(),
         le(0(), y) -> true(),
     le(p(s(x)), x) -> le(x, x),
   if(true(), x, y) -> 0(),
  if(false(), x, y) -> s(minus(p(x), y)),
        minus(x, y) -> if(le(x, y), x, y)
 }
 DUP: We consider a duplicating system.
  Trs:
   {
              p(s(x)) -> x,
               p(0()) -> s(s(0())),
           p(p(s(x))) -> p(x),
       le(s(x), s(y)) -> le(x, y),
        le(s(x), 0()) -> false(),
           le(0(), y) -> true(),
       le(p(s(x)), x) -> le(x, x),
     if(true(), x, y) -> 0(),
    if(false(), x, y) -> s(minus(p(x), y)),
          minus(x, y) -> if(le(x, y), x, y)
   }
  Fail