Now, let's split our lemmas into cases, so that we only have to think about one possible path for data to follow from one refinement map to the other. We begin with the operand lemma.

Consider a result returning on the result bus. That result is the
result value of a given reservation station `i`. It then
(possibly) gets stored in a register `j`. Finally it gets read as
an operand for reservation station `k`. This suggests a case split
which will reduce the size of the verification problem to just two
reservation stations and one register. For each operand arriving at
reservation station `k`, we split cases based on the reservation
station `i` that it came from (this is the ``tag'' of the operand)
and the register `j` that it passed through (this is the
source operand index, `srca` or `srcb`, that we store in the
auxiliary state for just this purpose). We also want to split cases on
the correct data value, since `WORD` is an undefined scalarset
type. Thus, here is the case splitting declaration for the ``a''
operand:

forall (i in TAG) forall (j in REG) forall (k in TAG) forall(c in WORD) subcase lemma1[i][j][c] of st[k].opra.val//lemma1 for st[k].opra.tag = i & aux[k].srca = j & aux[k].opra = c;

That is, we consider only the case where the tag (*i.e.* the producing
reservation station) is `i`, and source register is `j` and
the correct value is `c`. The ``b'' operand is similar.

For the result lemma (`lemma2`), we consider a pair of operands that
start in some reservation station `i` and pass through execution unit
`j`. Since `i` is a parameter of the lemma already, we are left
with just `j` to split cases on (this is the value of the signal
`complete_eu`). However, we now also have three data values to
split cases on: the two operands `a` and `b`, and the
result, `c = f[a][b]`. As before, this will reduce the data type
`WORD` and the table `f` down to a tractable size.
Thus, here is our case splitting declaration for `lemma2`:

forall(i in TAG) forall(j in EU) forall(a in WORD) forall(b in WORD) forall(c in WORD) subcase lemma2[i][j][a][b][c] of pout.val//lemma2[i] for aux[i].opra = a & aux[i].oprb = b & f[a][b] = c & complete_eu = j;

Finally, we have one last thing to prove, which is that the data
output is correct according to the architectural model (layer `arch`). This is quite similar to the operand lemma. That is, every
data output value was produced as a result by some instruction and
then stored in the source register for the `RD`
instruction. Therefore, when proving that data output values are
correct, we will split cases on the producing reservation station
(this is obtained from the tag of the source register) and
the source register index. In addition, as before, we consider only
the case where the correct value is some arbitrary constant `c`:

forall (i in TAG) forall (j in REG) forall (k in TAG) forall(c in WORD) subcase arch[i][j][c] of dout//arch for srca = j & ir[j].tag = i & r[j] = c;