Proving an invariant sometimes involves two lemmas, one to show that it holds in the initial state and one to show that it's preserved by the next-state relation. Sometimes these two lemmas appear in separate generated files, which is a little odd. It would be more natural for those lemmas to be collocated in the same file.
Proving an invariant sometimes involves two lemmas, one to show that it holds in the initial state and one to show that it's preserved by the next-state relation. Sometimes these two lemmas appear in separate generated files, which is a little odd. It would be more natural for those lemmas to be collocated in the same file.