The Dynamic Cut

In the following definitions, the notion of $DynamicCut$ is introduced. This refers to nodes in the mother $M$ after the grammar rule is completed, and mother $M$ is ready to be inserted in the chart as an edge $\widehat{M}$.

Definition 6.6   For a mother $M$ and a daughter $D$ that are unifiable before parsing, the dynamic cut $DynamicCut(\widehat{M},D)$ is defined as the largest subset of $\{\widehat{x}\in Q^{\widehat{M}}\}$ such that:

1. $\exists x\in [\widehat{x}]^{-1}$, $x\notin StaticCut(M,D)$,
2. $\forall y\in Q_D$, if $\exists x\in [\widehat{x}]^{-1} \textrm{ . } x\bowtie y$, then $\forall s\sqsupseteq \theta(\widehat{x}), \forall t\sqsupseteq \theta(y) , s \sqcup t \downarrow$.

Note: If condition 2 in Definition 6.6 is not satisfied, the newly created edge from mother $\widehat{M}$ may no longer unify with daughter $D$.

Definition 6.7   $\widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}}= \langle Q',\overline{Q'}, \theta,\delta \rangle$ is the Dynamically Cut typed feature structure of a mother $M=\langle Q,\overline{q}, \theta, \delta\rangle$ with respect to a daughter $D$ iff

• $M$'s rule represented as an MRS is $R=\langle \dots, M\rangle$, and $\widehat{M}=M^{\widehat{n}}$ is the mother of the same rule after the rule is completed: $R^{\widehat{n}}=\langle \dots, M^{\widehat{n}}\rangle$ (where $n$ is the length of $R$),
• $Q'$ is the largest set of nodes $\{\widehat{x} \in (Q_{\widehat{M}} \setminus DynamicCut(\widehat{M},D)) \vert \forall x\in ([\widehat{x}]^{-1}\cap Q), x\notin StaticCut(M,D)\}$.

Before stating the main proposition about the Dynamic Cut, some elementary propositions are necessary for establishing correctness. The shorter notations $\widehat{M}$ and $\widehat{D}$ will be used here to symbolize $Q_{\widehat{M}}$ and $Q_{\widehat{D}}$, while $M$ and $D$ symbolize $Q_M$ and $Q_D$.

Proposition 6.2   $\forall \widehat{x} \in \widehat{M}$ such that $\widehat{x}\notin \widehat{M}^{\textrm{\Cutleft}_D}$, if there exists $x\in M$ such that $x\mapsto \widehat{x}$ and $x\in RigidCut(M,D)$, then $[\widehat{x}]^{-1}=\{x\}$.

Proof. By Definition 6.2, there are no externally shared nodes on any path leading to $x$. Therefore, all paths in $\widehat{M}$ leading to $\widehat{x}$ exists also in $M$ and lead to $x$. $\qedsymbol$

Corollary 6.1   If $\widehat{x}\in \widehat{M} \cup \widehat{D}$ and $\vert[\widehat{x}]_{\bowtie}\vert > 1$, then $[[\widehat{x}]_{\bowtie}]^{-1} \cap RigidCut(M,D) = \emptyset$.

Corollary 6.2   $\forall \widehat{x} \in \widehat{M}$ such that $\widehat{x}\notin \widehat{M}^{\textrm{\Cutleft}_D}$, if $\{x_1, x_2\} \subseteq [\widehat{x}]^{-1}$, $x_1\ne x_2$, then $x_1, x_2 \in VariableCut(M,D)$.

Proposition 6.3   If $\widehat{x} \in \widehat{M}$ and $\vert[\widehat{x}]_{\bowtie} \cap \widehat{M}\vert = 1$ ($\bowtie$ with respect to $\widehat{M}\sqcup \widehat{D}$), then $\forall \widehat{y} \in [\widehat{x}]_{\bowtie} \cap \widehat{D}$, $\exists x\in [\widehat{x}]^{-1}$, $\exists y\in[\widehat{y}]^{-1}$ such that $x\bowtie y$ ($\bowtie$ with respect to $M\sqcup D$). Similarly, if $\widehat{y} \in \widehat{D}$ and $\vert[\widehat{y}]_{\bowtie} \cap \widehat{D}\vert = 1$ ($\bowtie$ with respect to $\widehat{M}\sqcup \widehat{D}$), then $\forall{\widehat{x}} \in [\widehat{y}]_{\bowtie} \cap \widehat{M}$, $\exists y\in[\widehat{y}]^{-1}$, $\exists x\in [\widehat{x}]^{-1}$ such that $y\bowtie x$ ($\bowtie$ with respect to $M\sqcup D$).

Proof. $\forall \widehat{y}, \widehat{y'} \in [\widehat{x}]_{\bowtie}\cap \widehat{D} (\widehat{y} \neq \widehat{y'})$, there is no path in $\widehat{D}$ leading to both $\widehat{y}$ and $\widehat{y'}$ (otherwise $\widehat{y}=\widehat{y'}$). Thus, $\widehat{y} \bowtie \widehat{y'}$ because of the transitivity of $\bowtie$ ($\bowtie$ with respect to $\widehat{M}\sqcup \widehat{D}$). Therefore, since $\vert[\widehat{x}]_{\bowtie} \cap \widehat{M}\vert = 1$, for any $\widehat{y}\in [\widehat{x}]_{\bowtie}\cap \widehat{D}$ there is at least one path $\pi$ leading to $\widehat{x}$ in $\widehat{M}$ and to $\widehat{y}$ in $\widehat{D}$. Therefore, according to the definition of $\mapsto$, $\exists x\in [\widehat{x}]^{-1}, y\in [\widehat{y}]^{-1}$ such that $x\bowtie y$ ($\bowtie$ with respect to $M\sqcup D$). $\qedsymbol$

Figure 6.2 presents an example of a situation where this Proposition holds. As can be seen in the figure, $[\widehat{x}]^{-1}=\{x_1,x_2\}$, $[\widehat{y}]^{-1}=\{y_1\}$, $[\widehat{y}']^{-1}=\{y_2,y_3\}$, $[\widehat{x}]_{\bowtie}\cap \widehat{M}=\{\widehat{x}\}$, and $[\widehat{x}]_{\bowtie}\cap \widehat{D}=\{\widehat{y},\widehat{y}'\}$. Proposition 6.3 states that for both $\widehat{y}$ and $\widehat{y}'$ there is at least one node in $D$ mappable to them which is equivalent to at least one node in $M$ that maps to $\widehat{x}$. Indeed, for $\widehat{y}$ it is $y_1\in[\widehat{y}]^{-1}$ that is equivalent to $x_1\in [\widehat{x}]^{-1}$ ( $x_1\bowtie y_1$), and for $\widehat{y}'$ it is $y_2\in[\widehat{y}']^{-1}$ that is equivalent to $x_2\in [\widehat{x}]^{-1}$ ( $x_2 \bowtie y_2$).

Figure 6.2: An example of the applicability of Proposition 6.3.

It should be noted that in the above proposition, $[\widehat{x}]_{\bowtie} \cap \widehat{M}$ is restricted to a single element, and thus, the proposition states the existence of $y\in[\widehat{y}]^{-1}$ equivalent to $x \in [\widehat{x}]^{-1}$ and not to $x \in [[\widehat{x}]_{\bowtie}]^{-1}$. Figure 6.3 presents an example where $[\widehat{x_1}]_{\bowtie} \cap \widehat{M} =\{\widehat{x_1},\widehat{x_2}\}$ and $[\widehat{x_1}]_{\bowtie} \cap \widehat{D}=\{\widehat{y_1},\widehat{y_2},\widehat{y_4}\}$. $\widehat{x_1}\bowtie \widehat{y_4}$, $[\widehat{y_4}]^{-1}=\{y_4\}$, and $[\widehat{x_1}]^{-1}=\{x_1,x_2\}$; however neither $x_1$ nor $x_2$ are equivalent to $y_4$.

Figure: An example of Proposition 6.3 limitation to $\vert[\widehat{x}]_{\bowtie} \cap \widehat{M}\vert = 1$.

Proposition 6.4   If $x\in M, x\in RigidCut(M,D), y\in D$ such that $x\bowtie y$ and $x\mapsto \widehat{x}, y\mapsto \widehat{y}$, then $\theta(\widehat{x})=\theta(x)$ and $\theta(\widehat{y})=\theta(y)$.

Proof. By Definition 6.2, there are no externally shared nodes on any path leading to $x$ or $y$. Therefore, during parsing, no types of any of $x$ or $y$'s ancestor nodes is promoted, and thus, $\theta(\widehat{x})=\theta(x)$ and $\theta(\widehat{y})=\theta(y)$. $\qedsymbol$

Proposition 6.5   If $t_0, t_1, \dots, t_n \in Type$ such that $\forall t_0'\sqsupseteq t_0, \forall i\in (1,\dots,n)$, $t_0' \sqcup t_i \downarrow$, then $\exists t\sqsupseteq t_0$ such that $\forall i\in (1,\dots,n)$, $t\sqsupseteq t_i$.

Proof. By induction on $n$ ($n\geq 1$).

Base case ($n=1$):

$\forall t_0'\sqsupseteq t_0, t_0'\sqcup t_1\downarrow \textrm{\mbox{$=\!\!\!>$... ...box{$=\!\!\!>$}} \exists t\sqsupseteq t_0 \textrm{ such that } t\sqsupseteq t_1$.

Induction ($n>1$):

Assume the proposition holds for $n-1$: $\exists t'\sqsupseteq t_0 \textrm{ such that } \forall i \in (1,\dots,n-1), t'\sqsupseteq t_i$. If $\forall t_0'\sqsupseteq t_0, t_0'\sqcup t_n\downarrow$, then also $t'\sqcup t_n\downarrow$. Therefore, $\exists t\sqsupseteq t'$ such that $t\sqsupseteq t_n$ and thus, $\exists t\sqsupseteq t_0$ such that $\forall i\in (1,\dots,n), t\sqsupseteq t_i$.

$\qedsymbol$

Proposition 6.6   For a mother $M$ and a daughter $D$, if $M\sqcup D\downarrow$ before parsing, and $\widehat{M}$ and $\widehat{D}$ exist (after completion), then after completion:

1. $\widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}} \sqcup \widehat{D}\downarrow \textrm{\mbox{$=\!\!\!>$}}\widehat{M}\sqcup \widehat{D}\downarrow$,
2. $\widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}} \sqcup \widehat{D}\uparrow \textrm{\mbox{$=\!\!\!>$}}\widehat{M}\sqcup \widehat{D}\uparrow$.

Proof. The first part of the proposition, if $\widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}}\sqcup \widehat{D}\downarrow$, then $\widehat{M}\sqcup \widehat{D}\downarrow$ will be proven by showing that $\forall \widehat{z}\in \widehat{M} \cup \widehat{D}$, $\theta^{\bowtie}([\widehat{z}]_{\bowtie})\downarrow$. The shorter notations $\widehat{M}$ and $\widehat{D}$ will be used here to symbolize $Q_{\widehat{M}}$ and $Q_{\widehat{D}}$.

Part 1 Four cases can be identified:

Case A:

$\vert[\widehat{z}]_{\bowtie} \cap \widehat{M}\vert = 1$ and $\vert[\widehat{z}]_{\bowtie} \cap \widehat{D}\vert = 1$,

Case B:

$\vert[\widehat{z}]_{\bowtie} \cap \widehat{M}\vert = 1$ and $\vert[\widehat{z}]_{\bowtie} \cap \widehat{D}\vert > 1$,

Case C:

$\vert[\widehat{z}]_{\bowtie} \cap \widehat{M}\vert > 1$ and $\vert[\widehat{z}]_{\bowtie} \cap \widehat{D}\vert = 1$,

Case D:

$\vert[\widehat{z}]_{\bowtie} \cap \widehat{M}\vert > 1$ and $\vert[\widehat{z}]_{\bowtie} \cap \widehat{D}\vert > 1$,

Case E:

$\vert[\widehat{z}]_{\bowtie} \cap \widehat{M}\vert = 0$ or $\vert[\widehat{z}]_{\bowtie} \cap \widehat{D}\vert = 0$,

Both of the cases A and B can have four subcases, based on where the node $\widehat{x}$ ( $\{\widehat{x}\}=[\widehat{z}]_{\bowtie} \cap \widehat{M}$) belongs to:

Case i:

$\widehat{x} \in \widehat{M}$, $\widehat{x}\notin \widehat{M}^{\textrm{\Cutleft}_D}$, and $([[\widehat{x}]_{\bowtie}]^{-1} \cap M) \subseteq RigidCut(M,D)$,

Case ii:

$\widehat{x} \in \widehat{M}$, $\widehat{x}\notin \widehat{M}^{\textrm{\Cutleft}_D}$, and $([[\widehat{x}]_{\bowtie}]^{-1} \cap M) \subseteq VariableCut(M,D)$,

Case iii:

$\widehat{x} \in \widehat{M}$, $\widehat{x} \in \widehat{M}^{\textrm{\Cutleft}_D}$, $\widehat{x}\notin \widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}}$ and $\widehat{x} \in DynamicCut(\widehat{M},D)$,

Case iv:

$\widehat{x} \in \widehat{M}$, $\widehat{x} \in \widehat{M}^{\textrm{\Cutleft}_D}$, $\widehat{x}\in \widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}}$.

For cases C and D, the above subcase i is not possible (according to Corollary 6.1), and subcases ii - iv will be treated as a single, unified, subcase ( $\widehat{z} \in \widehat{M}$).

Case A. It will be shown that $\theta^{\bowtie}([\widehat{z}]_{\bowtie})\downarrow$ by showing that $\theta(\widehat{x})\sqcup\theta(\widehat{y}) \downarrow$, where $\{\widehat{x}\}=[\widehat{z}]_{\bowtie} \cap \widehat{M}$ and $\{\widehat{y}\} = [\widehat{z}]_{\bowtie} \cap \widehat{D}$.

Case A.i. $[\widehat{x}]^{-1}\subseteq RigidCut(M,D)$. Proposition 6.3 states that $\exists x\in [\widehat{x}]^{-1}, \exists y\in [\widehat{y}]^{-1}$ such that $x\bowtie y$. Thus, since $M\sqcup D\downarrow$, $\theta(x) \sqcup \theta(y) \downarrow$. Therefore, according to Proposition 6.4, $\theta(\widehat{x})\sqcup\theta(\widehat{y}) \downarrow$.

Case A.ii. $[\widehat{x}]^{-1}\subseteq VariableCut(M,D)$. According to Proposition 6.3, $\exists x\in [\widehat{x}]^{-1}, \exists y\in [\widehat{y}]^{-1}$ such that $x\bowtie y$. But Proposition 4.1 states that $\theta(\widehat{x}) \sqsupseteq \theta(x)$ and $\theta(\widehat{y}) \sqsupseteq \theta(y)$. Therefore, according to Condition 2 of Definition 6.3, $\theta(\widehat{x})\sqcup\theta(\widehat{y}) \downarrow$.

Case A.iii. $\widehat{x} \in DynamicCut(\widehat{M},D)$. According to Proposition 6.3, $\exists x\in [\widehat{x}]^{-1}, \exists y\in [\widehat{y}]^{-1}$ such that $x\bowtie y$. But Proposition 4.1 states that $\theta(\widehat{y}) \sqsupseteq \theta(y)$. Therefore, according to Condition 2 of Definition 6.6, $\theta(\widehat{x})\sqcup\theta(\widehat{y}) \downarrow$.

Case A.iv. According to Proposition 6.3, $\exists x\in [\widehat{x}]^{-1}, \exists y\in [\widehat{y}]^{-1}$ such that $x\bowtie y$. Since $\widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}}\sqcup \widehat{D}\downarrow$ and based on Proposition 2.1 ( $\bowtie = \blacktriangleright\!\!\blacktriangleleft$), $\theta(\widehat{x})\sqcup\theta(\widehat{y}) \downarrow$.

Case B. It will be shown that $\exists t\in Type$ such that $\forall \widehat{y} \in [\widehat{z}]_{\bowtie} \cap \widehat{D}$ and for $\{\widehat{x}\}=[\widehat{z}]_{\bowtie} \cap \widehat{M}$, $t \sqsupseteq \theta(\widehat{y})$ and $t \sqsupseteq \theta(\widehat{x})$.

Case B.i. According to Corollary 6.1, this case is not possible.

Case B.ii. $\forall \widehat{y} \in [\widehat{z}]_{\bowtie} \cap \widehat{D}$, $\widehat{y} \bowtie \widehat{x}$, and according to Proposition 6.3, $\exists y\in [\widehat{y}]^{-1}, \exists x \in [\widehat{x}]^{-1}$ such that $y\bowtie x$. Thus, according to Condition 2 of Definition 6.3, $\forall s\sqsupseteq \theta(y), \forall t\sqsupseteq \theta(x)$, $s\sqcup t\downarrow$. But according to Proposition 4.1, $\theta(\widehat{y}) \sqsupseteq \theta(y)$ and $\theta(\widehat{x}) \sqsupseteq \theta(x)$. Therefore, $\forall \widehat{y} \in [\widehat{z}]_{\bowtie} \cap \widehat{D}$, $\forall s\sqsupseteq \theta(\widehat{y})$, $\forall t\sqsupseteq \theta(\widehat{x})$, $s\sqcup t\downarrow$, and hence, $\forall \widehat{y} \in [\widehat{z}]_{\bowtie} \cap \widehat{D}, \forall t\sqsupseteq \theta(\widehat{x}), t\sqcup \theta(\widehat{y})\downarrow$. Thus, according to Proposition 6.5, $\exists t\sqsupseteq \theta(\widehat{x}), \forall \widehat{y} \in [\widehat{z}]_{\bowtie} \cap \widehat{D}$, $t \sqsupseteq \theta(\widehat{y})$.

Case B.iii. $\forall \widehat{y} \in [\widehat{z}]_{\bowtie} \cap \widehat{D}$, $\widehat{y} \bowtie \widehat{x}$, and according to Proposition 6.3, $\exists y\in [\widehat{y}]^{-1}, \exists x \in [\widehat{x}]^{-1}$ such that $y\bowtie x$. Thus, according to Condition 2 of Definition 6.6, $\forall s\sqsupseteq \theta(y), \forall t\sqsupseteq \theta(\widehat{x})$, $s\sqcup t\downarrow$. But according to Proposition 4.1, $\theta(\widehat{y}) \sqsupseteq \theta(y)$. Therefore, $\forall \widehat{y} \in [\widehat{z}]_{\bowtie} \cap \widehat{D}$, $\forall s\sqsupseteq \theta(\widehat{y})$, $\forall t\sqsupseteq \theta(\widehat{x})$, $s\sqcup t\downarrow$, and hence, $\forall \widehat{y} \in [\widehat{z}]_{\bowtie} \cap \widehat{D}, \forall t\sqsupseteq \theta(\widehat{x}), t\sqcup \theta(\widehat{y})\downarrow$. Thus, according to Proposition 6.5, $\exists t\sqsupseteq \theta(\widehat{x}), \forall \widehat{y} \in [\widehat{z}]_{\bowtie} \cap \widehat{D}$, $t \sqsupseteq \theta(\widehat{y})$.

Case B.iv. Since $\widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}}\sqcup \widehat{D}\downarrow$, $\exists t\sqsupseteq \theta(\widehat{x})$ such that $\forall \widehat{y} \in [\widehat{z}]_{\bowtie} \cap \widehat{D}$, $t \sqsupseteq \theta(\widehat{y})$.

Case C. It will be shown that $\exists t\in Type$ such that $\forall \widehat{x} \in [\widehat{z}]_{\bowtie}$, $t \sqsupseteq \theta(\widehat{x})$.

Case C.i. According to Corollary 6.1, this case is not possible.

Cases C.ii-iv. Let $\{\widehat{y}\} = [\widehat{z}]_{\bowtie} \cap \widehat{D}$. The set $[\widehat{z}]_{\bowtie} \cap \widehat{M}$ can be divided into three subsets, similar to the subcases ii-iv: a set $S_{iv}=\{\widehat{x} \in [\widehat{z}]_{\bowtie} \cap \widehat{M} \vert \widehat{x}\in \widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}} \}$, a set $S_{iii}=\{\widehat{x} \in [\widehat{z}]_{\bowtie} \cap \widehat{M} \vert \wide... ..._{\textrm{\Cutleft}} \textrm{, and } \widehat{x}\in DynamicCut(\widehat{M},D)\}$, and a set $S_{ii}=\{\widehat{x} \in [\widehat{z}]_{\bowtie} \cap \widehat{M} \vert \wideh... ...t}_D} \textrm{, and } ([\widehat{x}]^{-1} \cap M) \subseteq VariableCut(M,D) \}$. It will be shown that:

1. $\exists t \sqsupseteq \theta(\widehat{y})$ such that $\forall \widehat{x}\in S_{iv}$, $t \sqsupseteq \theta(\widehat{x})$,
2. $\exists t'\sqsupseteq t$ such that $\forall \widehat{x}\in S_{iii}$, $t'\sqsupseteq \theta(\widehat{x})$,
3. $\exists t''\sqsupseteq t'$ such that $\forall \widehat{x}\in S_{ii}$, $t''\sqsupseteq \theta(\widehat{x})$.

By proving the above claims, it is demonstrated that $\exists t''$ such that $\forall \widehat{x} \in [\widehat{z}]_{\bowtie}$, $t''\sqsupseteq \theta(\widehat{x})$. An example of nodes in Case C is presented in Figure 6.4.

Figure 6.4: An example of nodes in Case C of the proof for Proposition 6.6. Given $\theta(x_1)=t_1, \theta(x_2)=t_2, \theta(x_3)=t_3, \theta(x_4)=t_3, \theta(y_1... ...2, \theta(\widehat{x_3})=t_3, \theta(\widehat{x_4})=t_4, \theta(\widehat{y})=t4$, $\widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}}\sqcup \widehat{D}\downarrow$, and also $\widehat{M}\sqcup \widehat{D}\downarrow$.

1. Since $S_{iv} \subseteq \widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}}$ and since $\widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}}\sqcup \widehat{D}\downarrow$,
   $$\exists t \sqsupseteq \theta(\widehat{y}) \textrm{ such that } \forall \widehat{x} \in S_{iv}, t \sqsupseteq \theta(\widehat{x}). \tag{*}$$

2. $\forall \widehat{x}\in S_{iii}$, $\widehat{x} \bowtie \widehat{y}$ and therefore, according to Proposition 6.3, $\exists x\in [\widehat{x}]^{-1}, \exists y \in [\widehat{y}]^{-1} \textrm{ such that } x\bowtie y$. Thus, according to Condition 2 of Definition 6.6 and to Proposition 4.1, $\forall s_1\sqsupseteq \theta(\widehat{x}), \forall s_2 \sqsupseteq \theta(\widehat{y}), s_1\sqcup s_2 \downarrow$. More than this, since $t \sqsupseteq \theta(\widehat{y})$ (for the type $t$ from (*)), $\forall s_1\sqsupseteq \theta(\widehat{x}), \forall s_2' \sqsupseteq t, s_1\sqcup s_2' \downarrow$, and hence, $\forall s_2'\sqsupseteq t, s_2' \sqcup \theta(\widehat{x}) \downarrow$. Therefore, according to Proposition 6.5 and to (*),
   $$\exists t'\sqsupseteq t \sqsupseteq \theta(\widehat{y}) \textrm{ ... ...} \forall \widehat{x} \in S_{iii}, t'\sqsupseteq \theta(\widehat{x}). \tag{**}$$

3. $\forall \widehat{x}\in S_{ii}$, $\widehat{x} \bowtie \widehat{y}$ and therefore, according to Proposition 6.3, $\exists x\in [\widehat{x}]^{-1}, \exists y \in [\widehat{y}]^{-1} \textrm{ such that } x\bowtie y$. Thus, since $x\in VariableCut(M,D)$, Condition 2 of Definition 6.3 holds, and therefore, according to Proposition 4.1, $\forall s_1\sqsupseteq \theta(\widehat{x}), \forall s_2 \sqsupseteq \theta(\widehat{y}), s_1\sqcup s_2 \downarrow$. More than this, since $t'\sqsupseteq \theta(\widehat{y})$ (for the type $t'$ from (**)), $\forall s_1\sqsupseteq \theta(\widehat{x}), \forall s_2' \sqsupseteq t', s_1\sqcup s_2' \downarrow$, and hence, $\forall s_2'\sqsupseteq t', s_2' \sqcup \theta(\widehat{x}) \downarrow$. Therefore, according to Proposition 6.5 and to (**),
   $$\exists t''\sqsupseteq t'\sqsupseteq t \sqsupseteq \theta(\wideha... ...h that } \forall \widehat{x} \in S_{ii}, t''\sqsupseteq \theta(\widehat{x}).$$

Case D. According to Corollary 6.1, Case D.i is not possible, while Cases D.ii. - D.iv. are a generalization of cases B.ii-iv and C.ii-iv.

Case E. If $\vert[\widehat{z}]_{\bowtie} \cap \widehat{M}\vert = 0$, then $[\widehat{z}]_{\bowtie} \subseteq \widehat{D}$. Since $\widehat{D}$ exists, $\exists t\in Type$ such that $\forall \widehat{y}\in [\widehat{z}]_{\bowtie}$, $t \sqsupseteq \theta(\widehat{y})$.

If $\vert[\widehat{z}]_{\bowtie} \cap \widehat{D}\vert = 0$, then $[\widehat{z}]_{\bowtie} \subseteq \widehat{M}$ and $\forall \widehat{x} \in [\widehat{z}]_{\bowtie}$, $\forall \widehat{y}\in \widehat{D}$, $\neg (\widehat{x}\bowtie \widehat{y})$. Therefore, since $\widehat{M}$ exists, $\exists t\in Type$ such that $\forall \widehat{x} \in [\widehat{z}]_{\bowtie}$, $t \sqsupseteq \theta(\widehat{x})$.

Part 2 ( $\widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}} \sqcup \widehat{D}\uparrow \textrm{\mbox{$=\!\!\!>$}}\widehat{M}\sqcup \widehat{D}\uparrow$.) If $\widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}} \sqcup \widehat{D}\uparrow$, then $\exists \widehat{z}\in \widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}} \cup \widehat{D}$ such that $\neg \exists t\in Type$ for which $\forall \widehat{x}\in [\widehat{z}]_{\bowtie}, t\sqsupseteq \theta(\widehat{x})$. Since $\widehat{M}^{\textrm{\Cutleft}_D}_{\textrm{\Cutleft}} \subseteq \widehat{M}$, $\exists \widehat{z}\in \widehat{M} \cup \widehat{D}$ such that $\neg \exists t\in Type$ for which $\forall \widehat{x}\in [\widehat{z}]_{\bowtie}, t\sqsupseteq \theta(\widehat{x})$, and therefore, $\widehat{M} \sqcup \widehat{D} \uparrow$.

$\qedsymbol$