 In this definition, the worlds of \(M[A]\) are obtained by making multiple copies of the worlds of M, one copy per event \(f\in E^A\). The event-f copy of a world v in M is represented by the pair \((v,f)\). Such a pair is to be included in the worlds of \(M[A]\) if and only if \((M,v)\) satisfies the precondition \(\pre^A(f)\) of event f. The term “product update” comes from the fact that the set \(W[A]\) of worlds of \(M[A]\) is specified by restricting the full Cartesian product \(W^M\times E^A\) to those pairs \((v,f)\) whose indicated world v satisfies the precondition \(\pre^A(f)\) of the indicated event f; that is, the “product update” is based on a restricted Cartesian product, hence the name. 