GroundΒΆ

Let \(\mathcal{T} = (\mathcal{L}, \mathcal{M}, w_{r}, w_{e})\) where \(\mathcal{E} \neq \varnothing\). Given \(\mathcal{T}\), let \(\mathcal{T}' = (\mathcal{L}, \mathcal{M}', w_{r}, w_{e})\) where

\[\mathcal{M}' := \{M'_{1}, \dots, M'_{\sigma(\mathcal{M}')}\}\]

and

\[\tilde{M} \subseteq \tilde{M}'.\]

Now let \(\mathcal{R}' := \{R'_{1}, \dots, R'_{\sigma(\mathcal{R}')}\}\) and \(\mathcal{Q}' := \{Q'_{1}, \dots, Q'_{\sigma(\mathcal{Q}')}\}\) be derived from \(\mathcal{T}'\). By definition, we have the following:

  • \(\forall i, \exists ! j\) such that \(R'_{i} \subseteq R_{j}.\)

  • \(\forall i, \exists ! j\) such that \(Q'_{i} \subseteq Q_{j}.\)

Similarly, let \(\mathcal{V}'\) and \(\mathcal{U}'\) to be derived from \(\mathcal{T}'\) respectively. Since \(\mathcal{V}' \cup \mathcal{U}' = \mathcal{R}'\), we get the following:

  • \(\forall i, \exists ! j\) such that \(V'_{i} \subseteq R_{j}.\)

  • \(\forall i, \exists ! j\) such that \(U'_{i} \subseteq R_{j}.\)

Furthermore, we also have

\[\forall i, \exists ! j ~\text{such that}~ V'_{i} \subseteq V_{j}.\]

Note

This is due to \(\hat{Q}' \subseteq \hat{Q}\). More specifically, for any \(i\), \(V'_{i} \in \mathcal{R}'\) and \(V'_{i} \subseteq \hat{Q}'\). If we let \(V'_{i} = R'_{j}\), there is unique \(R_{k}\) where \(R_{j} \subseteq R_{k}\). By definition of \(V'_{i}\), we have \(R'_{j} \subseteq \hat{Q}'\). It follows

\[R_{k} \cap \hat{Q}' \neq \varnothing \implies R_{k} \cap \hat{Q} \neq \varnothing \implies R_{k} \subseteq \hat{Q}.\]

Hence, \(V_{l} = R_{k}\) for some \(l\) and \(V_{i} \subseteq V_{l}\).

However, it is worthwhile to note that we do not have

\[\forall i, \exists ! j ~\text{such that}~ U'_{i} \subseteq U_{j}.\]

In particular, it is possible to have \(U'_{i} \subseteq V_{j}\) for some \(i\) and \(j\). We denote this by

\[\begin{split}\begin{align} \mathcal{U}' := &~ \{U'_{1}, \dots, U'_{\sigma(\mathcal{U}')}\} \\ = &~ \mathcal{U}'_{\mathcal{V}} \cup \mathcal{U}'_{\mathcal{U}} \end{align}\end{split}\]

where

\[\begin{split}\begin{align} \mathcal{U}'_{\mathcal{V}} := &~ \{U'_{\mathcal{V}, 1}, \dots, U'_{\mathcal{V}, \sigma(\mathcal{U}'_{\mathcal{V}})}\} \\ \mathcal{U}'_{\mathcal{U}} := &~ \{U'_{\mathcal{U}, 1}, \dots, U'_{\mathcal{U}, \sigma(\mathcal{U}'_{\mathcal{V}})}\} \end{align}\end{split}\]

and

\[\begin{split}\begin{align} \mathcal{U}'_{\mathcal{V}} \subseteq &~ \mathcal{V} \\ \mathcal{U}'_{\mathcal{U}} \subseteq &~ \mathcal{U}. \end{align}\end{split}\]

Note

Note redacted.