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