I can relax somewhat. As of this minute, I have written two correctness proofs. Truly splendid. What remains now is first to simplify the placement of the exceptional annotations so we actually have a M18 report. Then, I will insert a semantics for ghost variables and summarize a correctness proof for our annotations. What is left then is to tidy up the symbolic automaton semantics, correct the figures and tidy up the Level II section as much as I can. Then I am off to bed.
For tomorrow, what remains is to read the whole thing (45 pages??) and make cosmetic changes.
I suspect that today I will make it to at least 3.
With this, I am so much closer to finishing my results.