To prove , for any non-nested Splice program , first observe that it is rather straightforward to prove that if then . The proof proceeds by induction on the structure of , which is possible in PVS because we have defined programs as an abstract data type. Most cases are trivial, only for the statement one has to observe that given a strict total order on the events, this order can be used as the required order on the read events and also as the local order for each process identity.
The proof that implies also proceeds by induction on . The main issue here is again the proof for the statement; given a strict total order on all read events () and for each process identifier a total order on all events (--see the definition of ), we have to construct a global strict total order on all events.
To do this, we introduced in PVS an axiom stating that there exists some total order on the set of all events . This order is used to construct a so-called minimal extension of the order on the read events:
The idea is that write events are ordered as early as possible in the sense that any read event that does not preceed a write event in is ordered after by . Hence this minimal extension orders all write events not later than any of the local orders. We have proved that this minimal extension satisfies the condition on the read events in the definition of the global semantics (which is equal to the one in the definition of ), because this condition is invariant under the operation of ordering write events earlier.