for i0, i1 being Integer st i0 < i1 holds
i0 + 1 <= i1