Describing state machines mathematically
There is a general theory here, which was introduced into CS by Robin Milner, which Lamport did not go into. 

A state machine is generally given as a triple $(Q \in \mathrm{Set}, q \in Q, f \in I \times Q \to \mathcal{P}(O \times Q))$, consisting of a state set $Q$, an initial state $q$, and a transition relation $f$. 

Now, suppose we have two automata $(Q, q, f)$ and $(T, t, g)$. Let's ask a question: when are these automata equivalent? If all we are going to do is take the machines and send them inputs and listen to the outputs, we don't want to require the state sets to be the same (for example, if $(T, t, g)$ is the result of running a DFA minimization algorithm on $(Q, q, f)$). 

It turns out that the right notion of equivalence is bisimulation.  The idea is that we take two state machines to be the same, if we can produce a relation $R \subseteq Q \times T$, such that 


$(q,t) \in R$
for all $(q,t) \in R$ and $i \in I$ and $o \in O$ then:

for all $q' \in Q$, if $(o, q') \in f(i, q)$, then there is a $t' \in T$ such that $(o, t') \in g(i, t)$. 
for all $t' \in T$, if $(o, t') \in g(i, t)$, then there is a $q' \in Q$ such that $(o, q') \in f(i, q)$. 



This says that if we can figure out any relation such that (a) the initial states are related, and (b) from related initial states, any I/O action the first machine can take can be mimicked by the second machine in a way that keeps you in the relation, and (c) similarly, the first machine can mimic anything the second can do.

Lamport's notation with primes is a way of concisely describing input-output relations. In this case, the state sets are the program counter of the first program, and the two program counters of the second program. The bisimulation relation is $R(pc, (p, c)) \triangleq pc = p \oplus c$, and then the bisimulation conditions follow trivially (since the relation expressions are equal under the subsitution). 

The general theory at work is the theory of coinduction. State machines are representions of corecursively defined sets, and bisimulations tell you when two state machines are representations of the same potentially-infinite object. 

Incidentally, this paper is written in a rather polemical style. Equally polemically, I'll point out that the style he advocates in this paper simply fails should you ever need to verify part of a program in isolation -- for example, if you want to prove a library implementation correct, or verifying a program using higher-order functions (or even just dynamic linking). 

But both of us will use coinduction, nonetheless.