successfully formalized safe (I think). Added more functions so that it is possible to detect invalid states during the proof