MAYBE
Trs:
 {            mod(x, s(y)) -> modIter(x, s(y), 0(), 0()),
               mod(x, 0()) -> modZeroErro(),
   if(false(), x, y, z, u) -> if2(le(y, s(u)), x, y, s(z), s(u)),
    if(true(), x, y, z, u) -> u,
            le(s(x), s(y)) -> le(x, y),
             le(s(x), 0()) -> false(),
                le(0(), y) -> true(),
  if2(false(), x, y, z, u) -> modIter(x, y, z, u),
   if2(true(), x, y, z, u) -> modIter(x, y, z, 0()),
    modIter(x, s(y), z, u) -> if(le(x, z), x, s(y), z, u)}
 Comment:
  We consider a duplicating trs.
  FAIL:
   Open