Added value declarations and added subsections
Simplified Wrap slightly
Cleared up correctness formulations a bit