Add first part of partial correctness proof.