rename {first,last}InputIndex as {first,last}Index: it is clear that the index is about the input because it is a field on the InputRange structure, also we save some characters.
remove empty set check on input range: we don't need to check if the input range is empty or not, because they will be useless to validating outputs anyway, because you can't prove that it contains some input index.
rename
{first,last}InputIndexas{first,last}Index: it is clear that the index is about the input because it is a field on theInputRangestructure, also we save some characters.remove empty set check on input range: we don't need to check if the input range is empty or not, because they will be useless to validating outputs anyway, because you can't prove that it contains some input index.