We describe how to prove that the algorithm has the property

        pc(s,i) = l2 |--> pc(s,i) = cs

which means that if process i wants to enter the critical section, then process i  will eventually enter there.

- qlock.mod
- invariants.mod  describes invariants to prove.
- ensures.mod  describes ensures properties to prove.
- otslogic.mod describes OTS logic (similar to UNITY logic, a kind of temporal logic) and inference rules.
- leadsto.mod describes leadsto (|-->) properties to prove.
- proof1.mod for invariant 1
- proof2.mod for invariant 2
- proof3.mod for invariant 3
- proof4.mod for invariant 4
- proof5.mod for invariant 5
- proof6.mod for invariant 6
- proof7.mod for invariant 7
- proof8.mod for invariant 8
- proof9.mod for invariant 9
- proof10.mod for invariant 10
- proof11.mod for ensures 11
- proof12.mod for ensures 12
- proof13.mod for ensures 13
- proof14.mod for leadsto 14
- proof15.mod for  leadsto15
- proof16.mod for leadsto 16
- proof17.mod  for leadsto 17
- proof18.mod for leadsto 18