The above may have seemed like a great deal of effort to verify such a simple design. However, we will find that the proof becomes only incrementally more complex when we move to a much more complex implementation - an instruction processor using Tomasulo's algorithm.