Hallerstede, Stefan Structured Event-B Models and Proofs. [Rodin Archive]