In other words,
what we want to show is that if ej happens before Pj records its own state, meaning
ej actually belongs to the cut calculated by the Global Snapshot algorithm,
then it must also be true that ei happens before Pi records its own state, that is
ei is also a part of the cut calculated by the Global Snapshot algorithm.
So let's prove this by contradiction.
Let's assume that the first condition is true, which is that ej is a part of
the cut, so ej happens before Pj records its own state.
But that the second condition is not true which is that Pi records its own state is
in fact happens before ei, okay?
So, because all the events at Pi are ordered linearly because Pi's clock,
if its not true that ei happened before Pi records its own state, the reverse
must be true which is that Pi records its own state must happen before ei.
Along with this, you also have the fact that ei happened before ej.
So, consider the causal path that goes from ei to ej,
along that causal path consider all the sequences of process timelines, and
all the channels on which messages pass along that causal path.
Due to the FIFO ordering on the causal paths and
the linear ordering of events at each process, it must be true that
the markers on each link above proceed the regular application messages.
Why do the markers proceed the regular application messages?
Because Pi records its own state before ei happens and so
the markers are sent out when Pi records its own state, and so the markers which
proceed on the causal path from ei to ej will proceed the ei to ej messages.
But then this automatically means that the marker is received at
the process Pj before the event ej happens that crosses Pj.
But then this means that Pj must have received the marker before ej, and
so it cannot be true that ej happened before Pj records its own state.
And so we have a contradiction here.
And so what we assumed in the green statement over here at the top of
the slide must be false.
And so it must be true that if ej belongs to the cut,
then ei also belongs to the cut.