add notes about removing the axiom
remove the rule that removes a completed thread; add proof of strong_progress of cfgsc/tso
adjust the diamond theorem proof according to new definitions
finish most of the proof of DRF->Well-Synchronized
add some thoughts to the rest of DRF->Well-Synchronized proof
add some more thoughts
change name append to snoc..