I am currently studying the textbook *Principles of Program Analysis* by Flemming Nielson, Hanne R. Nielson, and Chris Hankin. Chapter **1.3 Data Flow Analysis** says the following:

The least solution.The above system of equations defines the twelve sets

$$text{RD}_text{entry}(1), dots, text{RD}_{text{exit}}(6)$$

in terms of each other. Writing $overrightarrow{RD}$ for this twelve-tuple of sets we can regard the equation system as defining a function $F$ and demanding that:

$$overrightarrow{RD} = F(overrightarrow{RD})$$

To be more specific we can write

$$F(overrightarrow{RD}) (F_text{entry}(1)(overrightarrow{RD}), F_text{exit}(1)(overrightarrow{RD}), dots, F_text{entry}(6)(overrightarrow{RD}), F_text{exit}(6)(overrightarrow{RD}))$$

where e.g.:

$$F_text{entry}(3)(dots, overrightarrow{RD}_text{exit}(2), dots, overrightarrow{RD}_text{exit}(5), dots) = overrightarrow{RD}_text{exit}(2) cup overrightarrow{RD}_text{exit}(5)$$

It should be clear that $F$ operates over twelve-tuples of sets of pairs of variables and labels; this can be written as

$F : (mathcal{P}(mathbf{text{Var}_star times mathbf{text{Lab}_star}))}^{12} to (mathcal{P}(mathbf{text{Var}_star times mathbf{text{Lab}_star}))}^{12}$

where it might be natural to take $mathbf{text{Var}_star} = mathbf{text{Var}}$ and $mathbf{text{Lab}_star} = mathbf{text{Lab}}$. However, it will simplify the presentation in this chapter to let $mathbf{text{Var}_star}$ be afinitesubset of $mathbf{text{Var}}$ that contains the variables occurring in the program $mathbf{S_star}$ of interest and similarly for $mathbf{text{Lab}_star}$. So for the example program we might have $mathbf{text{Var}_star} = { x, y, z }$ and $mathbf{text{Lab}_star} = { 1, dots, 6, ? }$.It is immediate that $(mathcal{P}(mathbf{text{Var}_star times mathbf{text{Lab}_star}))}^{12}$ can be partially ordered by setting

$$overrightarrow{text{RD}} sqsubseteq overrightarrow{text{RD}}^prime text{iff} forall i : text{RD}_i subseteq text{RD}_i^prime$$

where $overrightarrow{text{RD}} = (text{RD}_1, dots, text{RD}_{12})$ and similarly $overrightarrow{text{RD}}^prime = (text{RD}_1^prime, dots, text{RD}_{12}^prime)$. This turns $(mathcal{P}(mathbf{text{Var}_star times mathbf{text{Lab}_star}))}^{12}$ into a complete lattice (see Appendix A) with least element

$$overrightarrow{emptyset} = (emptyset, dots, emptyset)$$

and binary least upper bounds given by:

$$overrightarrow{text{RD}} sqcup overrightarrow{text{RD}}^prime = (text{RD}_1 cup text{RD}_1^prime, dots, text{RD}_{12} cup text{RD}_{12}^prime)$$It is easy to show that $F$ is in fact a monotone function (see Appendix A) meaning that:

$$overrightarrow{text{RD}} sqsubseteq overrightarrow{text{RD}}^prime text{implies} F(overrightarrow{text{RD}}) sqsubseteq F(overrightarrow{text{RD}})^prime$$

This involves calculations like

$$text{RD}_text{exit}(2) subseteq text{RD}_text{exit}^prime(2) text{and} text{RD}_text{exit}(5) subseteq text{RD}_text{exit}^prime(5)$$

imply

$$text{RD}_text{exit}(2) cup text{RD}_text{exit}(5) subseteq text{RD}^prime_text{exit}(2) cup text{RD}_text{exit}^prime(5)$$

and the details are left to the reader.

Appendix A gives the following definition for *monotone function*:

The function $f$ is

monotone(orisotoneororder-preserving) if

$$forall l, l^prime in L_1 : l sqsubseteq_1 l^prime Rightarrow f(l) sqsubseteq_2 f(l^prime)$$

I am trying to do as the author said, and show that $F$ is a monotone function. However, I have so far been unable to make progress. It seems to me that such a proof should proceed by showing that, for some arbitrary element of the set of elements $F(overrightarrow{text{RD}})$, if we use the fact that $overrightarrow{text{RD}} sqsubseteq overrightarrow{text{RD}}^prime$, then we can deduce that said arbitrary element is also an element of the set $F(overrightarrow{text{RD}})^prime$, and so $F(overrightarrow{text{RD}}) sqsubseteq F(overrightarrow{text{RD}})^prime$. However, it seems to me that the textbook is very poorly written, and so it is difficult for me to even understand what said arbitrary elements of the set $F(overrightarrow{text{RD}})^prime$ even are (they seem to be some kind of cartesian product, but I get very confused when trying to figure out precisely what they are). So how is it shown that $F$ is a monotone function?