Snapshot representatives before quick-find union

ID: snapshot-representatives-before-quick-find-union

When merging two blocks in quick-find, let and be fixed saved labels. Replacing every old occurrence of by preserves all other blocks. A scan loop invariant says processed cells already have their specified final labels while unprocessed cells still have their old labels. Recomputing during this mutation can change the replacement label after the cell for is processed, causing remaining old- cells to be missed. Saving both labels makes the update criterion stable and the invariant provable.

New to topics? Read the docs here!