In the Composition Rule from section 10.2 of Specifying Systems, what is F_ij?

[Andrew Wilcox]

In Specifying Systems section 10.1, Lamport derives a composition rule for composing two systems (equation 10.1 on page 138).  The first disjunct in the next-state action of the right hand side reads:

N_1 /\ N_2

In section 10.2 (also on page 139) Lamport generalizes for multiple components and describes the Composition Rule.  The corresponding disjunction in the general rule appears as:

\E i, j \in C : (i # j) /\ N_i /\ N_j /\ F_ij

and the rule concludes with "for some actions F_ij".

For the two component case with C = {1, 2}, this disjunction is equivalent to:

\/ N_1 /\ N_2 /\ F_12

\/ N_1 /\ N_2 /\ F_21

or, if F_12 is the same as F_21, I guess just N_1 /\ N_2 /\ F_12.  In any case, it appears to be the same as the two component case, except for the addition of F.

I was following along up to this point, but here I got lost.  What is F?  Why is it needed?

Thank you!

Andrew