Jobs and machines are $Fin n$ and $Fin m$ rather than abstract finite types. The difference matters: an instance is something a machine is handed as a word, and a word presents its jobs in an order. An abstract finite type would have to be equipped with an enumeration before anything could be encoded, and the enumeration — not the type — is what the encoding would then describe.

The two standing conventions $p_j \ge 1$ and $p_j \le d_j$ are fields of the structure, as they are hypotheses of every statement in the source. Without the first, a job of processing time zero occupies an empty interval and overlaps nothing; without the second, the truncated subtraction $d_j - p_j$ would clamp to zero.

Overlap is defined on the half-open intervals, so jobs meeting end-to-start do not overlap. $Feasible$ constrains only the pairs a schedule actually places on a common machine, and says nothing about rejected jobs; $Complete$ is the separate condition that no job is rejected, which the second theorem of this submission is about.

The weight of a schedule sums over all jobs, contributing zero for a rejected one, rather than summing over the scheduled ones. The two agree, and the first needs no decidability of the set of scheduled jobs.