Extra Assertions

These are a collection of additional assertions used for testing, but which are (currently) not included in the specification. These are candidates for being put in the specification and are given here only to stage them in order to facilitate timely generation of the implementation report. In the final report this list should probably be empty.