Runs

A run of a program P is a sequence [ : n < ] of states where:

• every nonfinal is an appropriate state for P and the final state (if any) is a state of the internal vocabulary of P , and
• every is obtained from by firing P at .