RGSim.v : Definitions of e-trace refinement, Correct(T), RGSim, soundness of RGSim
CompRules.v : Compositionality rules of RGSim (including SKIP, CONSEQ, STREN-alpha, WEAKEN-alpha, PAR, SEQ, IF, WHILE, TRANS, FRAME) 
ExampleLock.v : A small example of RGSim, using a lock to perform x:=x+2

**Using the Coq release v8.3pl2. 
**NOTE: It may take a long time to compile CompRules.v. Please be patient. 
