Fixed invariant bug in implementation, added some proofs to design ideas