work on x64CorrectScript.sml - essentially finished now

there are some cheats left in it, which are things that should have been
proved elsewhere but weren't.