Finished the liveness-related theorems
Also consistently use "clash sets" in comments