Added defun/defthms for scalar-vector merge. Cleaned up the semantics for the machine