Changed the linking invariant to use built-in constructions rather than quantifications.
Updated the initialization.
Refactoring.
Strengthened loop invariants.
Discharged some proofs.