The difficulty, of course, is that each \(P_i\) is allowed to occur in one or more \(\phi_j\), possibly even in \(\phi_i\), and so \(E\) is self-referential. In many computer programming languages one sees things like \(x = x+1\). It is explained to beginning programmers that this takes the current value of \(x\), adds 1, and calls the result \(x\) again. Occurrences of \(x\) on the right have ‘before’ values, occurrences on the left have ‘after’ values. Analogously, let us think of the members of \(E\) as (simultaneous) assignment statements. Occurrences of \(P_i\) on the right of \(\simeq\) are current values, occurrences on the left are next values. Taking all of \(P_1\), …, \(P_k\) into account, we can think of \(E\) as defining a functional that maps \(k\)-tuples of partial relations (‘before’ values of these relation symbols) to \(k\)-tuples of partial relations (‘after’ values of these relation symbols). Now here are the details a bit more formally.