This question is related to this recent question. The difference is that this question relates to a different proof of a different claim by the authors. Specifically, this question presents an attempted proof of $F^n(\overrightarrow{\emptyset}) \sqsubseteq F^{n + 1}(\overrightarrow{\emptyset})$.
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 a finite subset 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.
Consider the sequence $(F^n(\overrightarrow{\emptyset}))_n$ and note that $\overrightarrow{\emptyset} \sqsubseteq F(\overrightarrow{\emptyset})$. Since $F$ is monotone, a straightforward mathematical induction (see Appendix B) gives that $F^n(\overrightarrow{\emptyset}) \sqsubseteq F^{n + 1}(\overrightarrow{\emptyset})$ for all $n$. All the elements of the sequence will be in $(\mathcal{P}(\mathbf{\text{Var}_\star \times \mathbf{\text{Lab}_\star}))}^{12}$ and since this is a finite set it cannot be the case that all elements of the sequence are distinct so there must be some $n$ such that: $$F^{n+1}(\overrightarrow{\emptyset}) = F^n(\overrightarrow{\emptyset})$$
I have attempted to use mathematical induction to prove this part:
Consider the sequence $(F^n(\overrightarrow{\emptyset}))_n$ and note that $\overrightarrow{\emptyset} \sqsubseteq F(\overrightarrow{\emptyset})$. Since $F$ is monotone, a straightforward mathematical induction (see Appendix B) gives that $F^n(\overrightarrow{\emptyset}) \sqsubseteq F^{n + 1}(\overrightarrow{\emptyset})$ for all $n$.
Appendix A gives the following definition for monotone function:
The function $f$ is monotone (or isotone or order-preserving) if $$\forall l, l^\prime \in L_1 : l \sqsubseteq_1 l^\prime \Rightarrow f(l) \sqsubseteq_2 f(l^\prime)$$
I use this definition in the proof below.
For the base case $n = 0$, we get
$$F^0(\overrightarrow{\emptyset}) \sqsubseteq F^1(\overrightarrow{\emptyset}) \\ \Rightarrow \overrightarrow{\emptyset} \sqsubseteq F(\overrightarrow{\emptyset}),$$
which is true, since the empty set is a subset of all sets.
We want to show that
$$F^n(\overrightarrow{\emptyset}) \sqsubseteq F^{n + 1}(\overrightarrow{\emptyset})$$
So we can proceed as follows:
$$F^{n - 1}(\overrightarrow{\emptyset}) \sqsubseteq F^n(\overrightarrow{\emptyset}) \\ \Rightarrow F(F^{n - 1}(\overrightarrow{\emptyset})) \sqsubseteq F(F^n(\overrightarrow{\emptyset})) \ \ \ \text{(Since $F$ is monotone.)} \\ \Rightarrow F^{n}(\overrightarrow{\emptyset}) \sqsubseteq F^{n + 1}(\overrightarrow{\emptyset}) \ \ \ \text{(Since $F^n$ denotes iterated composition, right?)}$$
Is this correct? If not, then what is the correct proof using mathematical induction?
And as an aside, the full formula for the function $F$ is
$$\begin{align*} \newcommand{\ent}{\mathsf{RD}_{\mathit{entry}}} \newcommand{\ext}{\mathsf{RD}_{\mathit{exit}}} \newcommand{\Lab}{\mathbf{Lab}} \newcommand{\bx}{\mathbf{x}} \newcommand{\by}{\mathbf{y}} \newcommand{\bz}{\mathbf{z}} &F(\ent(1),\ldots,\ent(6),\ext(1),\ldots,\ext(6)) = \\ (&\{(\bx,?),(\by,?),(\bz,?)\}, \ext(1), \ext(2) \cup \ext(5), \ext(3), \ext(4), \ext(3), \\ &(\ent(1) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,1)\}, \\ &(\ent(2) \setminus \{(\bz,\ell) \mid \ell \in \Lab\}) \cup \{(z,2)\}, \\ &\ent(3), \\ &(\ent(4) \setminus \{(\bz,\ell) \mid \ell \in \Lab\}) \cup \{(z,4)\}, \\ &(\ent(5) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,5)\}, \\ &(\ent(6) \setminus \{(\by,\ell) \mid \ell \in \Lab\}) \cup \{(y,6)\}). \end{align*}$$