Minor fixes to pseudocode and proof