Improved the frame-property and re-proven all the commands and rules.
Modified the send+recv Hoare-rules to use ** for the has_ST predicate.