The whole program $prog$, correct by $prog_spec$, compiled and wrapped through the pipeline: decides $Yes x$ for every decision word of a one-machine, unit-weight instance with positive processing times that fits, within $c (n+1)²$ instructions. The domain restricts to positive processing times — the paper's own standing assumption for Lemma 1's recursion — which the concept's stated domain does not yet carry; see the module notes.