**Weakest Preconditions - for Gina**

P: { F1=F1SAVE & F1 < 256 & LOW < 256 }
W1: LDX 8
W2: LDA 0
W3: LOOP ROR F1
W4: BCC ZCOEF
W5: CLC
W6: ADC F2
W7: ZCOEF ROR A
W8: ROR LOW
W9: DEX
W10: BNE LOOP
Q: { LOW + A*256 == F1SAVE*F2 }

In the above, the postcondition that is intended to be proved given
`P` is `Q`. This can be done by finding the weakest
w.r.t. `Q` at `W1` and then showing that `W1`
equals `T` under the conditions of `P`. But `W1`
is not a predicate - it is a `defun` that is expressed in terms
of the `defun W7`. The assignment is to find `W7`. The
form `W7` takes is the following:
(defun W7 (F1 LOW A X C Z)
(if (..some condition..)
(..some value..)
(W7 ..new F1.. ..new LOW.. ..new A.. ..new X.. ..new C.. ..new Z..)))

The reason for the arguments is they are all variables whose values change at
some point during the multiply operation. The `..some condition..`
should state the condition by which the loop terminates in terms of
`F1, LOW, A, X, C, Z` (hint: but it should only depend on
`Z`). The `..some value..` should be the result of the
loop after termination and should somehow reflect the postcondition
`Q`. The `..new F1..` etc. are obtained by substitution
in a manner similar to what was done for `W3` in terms of
`W7` in the assignment. As a check, the value for `..new F1..` is:
(+ (* (MOD LOW 2) 128) (FLOOR F1 2))

which differs from the `..new F1..` of `W3` in terms of
`W7` only by `C` being replaced with `(MOD LOW 2)`.