TRS:
 {              le(0(), y) -> true(),
             le(s(x), 0()) -> false(),
            le(s(x), s(y)) -> le(x, y),
               mod(x, 0()) -> modZeroErro(),
              mod(x, s(y)) -> modIter(x, s(y), 0(), 0()),
    modIter(x, s(y), z, u) -> if(le(x, z), x, s(y), z, u),
    if(true(), x, y, z, u) -> u,
   if(false(), x, y, z, u) -> if2(le(y, s(u)), x, y, s(z), s(u)),
  if2(false(), x, y, z, u) -> modIter(x, y, z, u),
   if2(true(), x, y, z, u) -> modIter(x, y, z, 0())}
 Fail