added related work and commented out the acl2 dethms in vectorization case study because of space