Proving the Scalable Commutativity Rule in Coq
- model.v contains all assumptions and the definition of the implementation machine.
- helpers.v contains all the helper lemmas
- scr.v contains the statement of the actual scalable commutativity rule and other significantly important helper lemmas