009_lz77: working on verifiying it.  Making good progress, but encountered some kind of bug related to including preconditions from external methods.