Up to now, we've proved a certain relationship between the abstract model and the implementation, but we haven't really proved that the circuit observably implements its specification. This is because the pipeline has no outputs. We could easily, however, give the processor and output instruction (perhaps one that outputs the sum of two registers). In this case the output of our pipeline would likely appear with some delay, relative to the specification. This means we would need to write a refinement map for the pipeline output that delays the abstract model output by some fixed amount. In this case, since the delay is finitely bounded, writing such a map is straightforward (we'll leave it as an ``exercise for the reader''). If there isn't a known fixed bound on the output delay, we might, for example, borrow a technique from a previous section. That is, we could attach an index to each instruction, so that we know which instruction's value is appearing at any given time at the output. We could then use induction, as before, to show that the output values appear in the correct order.
In any event, in the next section, we'll see an example of a more interesting implementation, with an output.