xs^{\prime}$, there exist symbolic tuples $t_{a}\in R$ and $t_{b}^{\prime}\in
R^{\prime}$ s.t.
$\mathcal{I}(xs_{i}^{\prime})=\mathcal{I}(t_{a})=\mathcal{I}(t_{b}^{\prime})$,
$\mathcal{I}(\text{Del})(xs_{i}^{\prime})=\mathcal{I}(\text{Del})(t_{a})=\mathcal{I}(\text{Del})(t_{b}^{\prime})=\bot$
and $\text{Paired}(a,b)=\top$. Also, by the definition of the Paired function,
we know $\text{Paired}(a,j)=\bot$ for any $j\neq b$ and
$\text{Paired}(i,b)=\bot$ for any $i\neq a$. Therefore,
$\mathcal{I}^{\prime},\mathcal{D}\models\neg\text{Del}(t_{a})\land\land_{j=1}^{m}\neg\text{Paired}(a,j)\to
t_{a}^{\prime\prime}=t_{a}\land\text{Del}(t_{a})\lor\lor_{j=1}^{m}\neg\text{Paired}(a,j)\to\text{Del}(t_{a}^{\prime\prime})$
and
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi\land\Phi^{\prime}\land\land_{i=1}^{n}\land_{j=1}^{m}\Phi_{i,j}^{\prime\prime}$

Hence, Theorem 4.5 for the inductive case $Q^{\prime\prime}=Q-Q^{\prime}$ is
proved.

  14. (14)

Inductive case: $Q^{\prime\prime}=Q\cup Q^{\prime}$.

Since $Q\cup
Q^{\prime}\Leftrightarrow\text{Distinct}(Q\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}Q^{\prime})$,
this case can be proved by the inductive cases
$Q^{\prime\prime}=Q\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}Q^{\prime}$
and
$Q^{\prime}=\text{Distinct}(Q\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}Q^{\prime})$.

  15. (15)

Inductive case: $Q^{\prime\prime}=Q\uplus Q^{\prime}$.

Suppose that $\mathcal{S}\vdash Q\hookrightarrow R$ where $R$ has symbolic
tuples $[t_{1},\ldots,t_{n}]$, $\mathcal{S}\vdash Q^{\prime}\hookrightarrow
R^{\prime}$ where $R^{\prime}$ has symbolic tuples
$[t_{1}^{\prime},\ldots,t_{m}^{\prime}]$, $\mathcal{S}\vdash Q\uplus
Q^{\prime}\hookrightarrow R^{\prime\prime}$ where $R^{\prime\prime}$ has
symbolic tuples $[t_{1}^{\prime\prime},\ldots,t_{n+m}^{\prime\prime}]$ by
Figure 11; $\mathcal{S},\Gamma\vdash Q\leadsto\Phi$, $\mathcal{S},\Gamma\vdash
Q^{\prime}\leadsto\Phi^{\prime}$, $\mathcal{S},\Gamma\vdash Q\uplus
Q^{\prime}\leadsto\Phi\land\Phi^{\prime}\land\Phi^{\prime\prime}$ where
$\Phi^{\prime\prime}=\land_{i=1}^{n}t_{i}^{\prime\prime}=t_{i}\land\land_{j=n+1}^{n+m}t_{j}^{\prime\prime}=t_{j-n}^{\prime}$
by Figure 18.

By the inductive hypothesis, we know $\mathcal{I}(R)=\llbracket
Q\rrbracket_{\mathcal{D}}$, $\mathcal{I}(R^{\prime})=\llbracket
Q^{\prime}\rrbracket_{\mathcal{D}}$ and
$\mathcal{I},\mathcal{D}\models\Phi\land\Phi^{\prime}$.

Take $\mathcal{I}^{\prime}$ s.t.
$\mathcal{I}^{\prime}(t_{i})=\mathcal{I}(t_{i})$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i})\leftrightarrow\mathcal{I}(\text{Del})(t_{i})$,
$\mathcal{I}^{\prime}(t_{j}^{\prime})=\mathcal{I}(t_{j}^{\prime})$,
$\mathcal{I}^{\prime}(\text{Del})(t_{j}^{\prime})\leftrightarrow\mathcal{I}(\text{Del})(t_{j}^{\prime})$,
$\mathcal{I}^{\prime}(t_{i}^{\prime\prime})=\mathcal{I}(t_{i})$ and
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime\prime})\leftrightarrow\mathcal{I}^{\prime}(\text{Del})(t_{i})$
for $1\leq i\leq n$,
$\mathcal{I}^{\prime}(t_{j}^{\prime\prime})=\mathcal{I}(t_{j-n}^{\prime})$ and
$\mathcal{I}^{\prime}(\text{Del})(t_{j}^{\prime\prime})\leftrightarrow\mathcal{I}^{\prime}(\text{Del})(t_{j}^{\prime})$
for $n+1\leq i\leq n+m$.

Further, since $\mathcal{I}(R)=\llbracket Q\rrbracket_{\mathcal{D}}$ and
$\mathcal{I}(R^{\prime})=\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$,

$\begin{array}[]{rcl}\llbracket Q\uplus
Q^{\prime}\rrbracket_{\mathcal{D}}&=&\textsf{append}(\llbracket
Q\rrbracket_{\mathcal{D}},\llbracket Q^{\prime}\rrbracket_{\mathcal{D}})\\\
&=&\textsf{append}(\mathcal{I}(R),\mathcal{I}(R^{\prime}))\\\
&=&\textsf{append}(\mathcal{I}([t_{1},\ldots,t_{n}]),\mathcal{I}([t_{1}^{\prime},\ldots,t_{m}^{\prime}]))\\\
&=&\textsf{append}([\mathcal{I}(t_{1}),\ldots,\mathcal{I}(t_{n})],[\mathcal{I}(t_{1}^{\prime}),\ldots,\mathcal{I}(t_{m}^{\prime})])\\\
&=&[\mathcal{I}(t_{1}),\ldots,\mathcal{I}(t_{n}),\mathcal{I}(t_{1}^{\prime}),\ldots,\mathcal{I}(t_{m}^{\prime})]\\\
&=&[\mathcal{I}^{\prime}(t_{1}^{\prime\prime}),\ldots,\mathcal{I}^{\prime}(t_{n}^{\prime\prime}),\mathcal{I}^{\prime}(t_{n+1}^{\prime\prime}),\ldots,\mathcal{I}^{\prime}(t_{n+m}^{\prime\prime})]\\\
&=&\mathcal{I}^{\prime}([t_{1}^{\prime\prime},\ldots,t_{n}^{\prime\prime},t_{n+1}^{\prime\prime},\ldots,t_{n+m}^{\prime\prime}])\\\
&=&\mathcal{I}^{\prime}(R^{\prime\prime})\end{array}$

Let $\mathcal{D}^{\prime}=\mathcal{D}[o_{Q^{\prime\prime}}\mapsto\llbracket
Q\uplus Q^{\prime}\rrbracket_{\mathcal{D}}]$. By the definition of
$\mathcal{I}^{\prime}$, we have
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\land_{i=1}^{n}t_{i}^{\prime\prime}=t_{i}\land\land_{j=n+1}^{n+m}t_{j}^{\prime\prime}=t_{j-n}^{\prime}$
and, therefore,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi\land\Phi^{\prime}\land\Phi^{\prime\prime}$.

Hence, Theorem 4.5 for the inductive case $Q^{\prime\prime}=Q\uplus
Q^{\prime}$ is proved.

  16. (16)

Inductive case:
$Q^{\prime\prime}=Q\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}Q^{\prime}$.

Since
$Q\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}Q^{\prime}\Leftrightarrow
Q-(Q-Q^{\prime})$, this case can be proved by the inductive case
$Q^{\prime\prime}=Q-Q^{\prime}$.

  17. (17)

Inductive case: $Q^{\prime}=\text{GroupBy}(Q,\vec{E},L,\phi)$.

Suppose that $\Gamma\vdash Q\hookrightarrow R$ where $R$ has symbolic tuples
$[t_{1},\ldots,t_{n}]$,
$\Gamma\vdash\text{GroupBy}(Q,\vec{E},L,\phi)\hookrightarrow R$ where $R$ has
symbolic tuples $[t_{1}^{\prime},\ldots,t_{n}^{\prime}]$ by Figure 11;
$\mathcal{S},\Gamma\vdash Q\leadsto\Phi$,
$\mathcal{S},\Gamma\vdash\text{GroupBy}(Q,\vec{E},$
$L,\phi)\leadsto\Phi\land\land_{i=1}^{n}\Phi_{i}^{\prime}\land\land_{i=1}^{n}\Phi_{i}^{\prime\prime}$
where
$\Phi_{i}^{\prime}=\Sigma_{j=1}^{n}\text{If}(g(t_{i},j),0,1)=\text{If}(\text{Del}(t_{i}),0,1)\land\land_{j=1}^{i-1}g(t_{i},j)=(\neg\text{Del}(t_{i})\land
g(t_{i},j)\land\llbracket\vec{E}\rrbracket)_{\mathcal{S},\Gamma,[t_{i}]}=\llbracket\vec{E}\rrbracket)_{\mathcal{S},\Gamma,[t_{i}j}$
and
$\Phi_{i}^{\prime\prime}=(g(t_{i},j)\land\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,g^{-1}(i)}=\top\to\neg\text{Del}(t_{i}^{\prime})\land\land_{k=1}^{l}\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{i}^{\prime}]}=\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{S},\Gamma,g^{-1}(i)})\land(\neg
g(t_{i},j)\lor\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,g^{-1}(i)}\neq\top\to\text{Del}(t_{i}^{\prime}))$
by Figure 18; $L=[a_{1},\ldots a_{l}]$.

By the inductive hypothesis, we have $\mathcal{I}(R)=\llbracket
Q\rrbracket_{\mathcal{D}}$ and $\mathcal{I},\mathcal{D}\models\Phi$.

Take $\mathcal{I}^{\prime}$ s.t.
$\mathcal{I}^{\prime}(\text{Del})(t_{i})\leftrightarrow\mathcal{I}(\text{Del})(t_{i})$,
$\mathcal{I}^{\prime}(t_{i})=\mathcal{I}(t_{i})$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime})\leftrightarrow\neg
g(t_{i},i)$, $\mathcal{I}^{\prime}(t_{i})=\llbracket
L\rrbracket_{\mathcal{D},[g^{-1}(i)]}$ where $g$ checks whether $t_{i}$ is
partitioned into the $i$-th group, and $g^{-1}(i)$ finds symbolic tuples from
the $i$-th group.

For any tuple $x_{i}\in\llbracket Q\rrbracket_{\mathcal{D}}$, we have a
symbolic tuple $t_{\textsf{ptr}(i)}^{\prime}\in R$ s.t.
$\mathcal{I}(\text{Del})(t_{\textsf{ptr}(i)}^{\prime})=\mathcal{I}(\text{Del})(x_{i})\\\
$$=\bot$ and $\mathcal{I}(t_{\textsf{ptr}(i)}^{\prime})=\mathcal{I}(x_{i})$.
By the definition of foldl, we know $\text{Dedup}(Q,\vec{E})=\\\
$$\text{Distinct}([\llbracket\vec{E}\rrbracket_{\mathcal{D},[x_{1}]},\ldots,\llbracket\vec{E}\rrbracket_{\mathcal{D},[x_{c}]}])$
where $c=|\llbracket Q\rrbracket_{\mathcal{D}}|\leq n$. Assuming that
$\text{Dedup}(Q,\vec{E})=[\llbracket\vec{E}\rrbracket_{\mathcal{D},[x_{f(1)}]},\ldots,\llbracket\vec{E}\rrbracket_{\mathcal{D},[x_{f(d)}]}]$
after executing Distinct operation where $d=|\text{Dedup}(Q,\vec{E})|$ $\leq
c$ and the function $f(i)$ is the original index for the $i$-th entry in
$\text{Dedup}(Q,\vec{E})$. Furthermore, by the definition of
$ys=\textsf{map}(\text{Dedup}(Q,\vec{E}),\lambda y.\textsf{map}(\llbracket
Q\rrbracket_{\mathcal{D}},\lambda z.\text{Eval}(\vec{E},[z])=y))$, we have a
set of tuples $G_{i}$ sharing the same values over $\vec{E}$ for any entry
$e_{f(i)}\in\text{Dedup}(Q,\vec{E})$.

On the other hand, the definition of $g(t_{i},j)$ guarantees two properties.
The first property states that, for any existing symbolic tuple $t_{i}$, it
only can be partitioned into one symbolic group $G_{j}^{\prime}$ whose group
index $j$ cannot be greater than $i$, i.e.,
$\sum_{j=1}^{i}\text{If}(g(t_{i},j),1,0)=\text{If}(\text{Del}(t_{i}),0,1)$;
otherwise, this deleted symbolic tuple $t_{i}$ never belongs to any group. The
second one ensures the symbolic tuple $t_{i}$ is partitioned into a previous
symbolic group $G_{j}^{\prime}$ iff $t_{i}$ and $t_{j}\in G_{j}^{\prime}$
shares the same values over $\vec{E}$, i.e.,
$\land_{j=1}^{i-1}g(t_{i},j)=(\neg\text{Del}(t_{i})\land
g(t_{i},j)\land\llbracket\vec{E}\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}=\llbracket\vec{E}\rrbracket_{\mathcal{S},\Gamma,[t_{j}]})$.
Therefore, we have symbolic groups $[G_{1}^{\prime},\ldots,G_{n}^{\prime}]$ as
every tuple might be not deleted and unique over $\vec{E}$.

Let us discuss the tuple $x_{i}\in\llbracket Q\rrbracket_{\mathcal{D}}$ in the
two cases.

    1. (a)

If no other tuple $x_{j}\in\llbracket Q\rrbracket_{\mathcal{D}}$ shares the
same values over $\vec{E}$ with $x_{i}$, then only $x_{i}$ will be partitioned
into a group $G_{i}$. Similarly, the symbolic tuple $t_{\textsf{ptr}(i)}$ is
separated into the symbolic group $G_{i}^{\prime}$ because
$g(t_{\textsf{ptr}(i)},i)=\top$ and $g(t_{\textsf{ptr}(i)},j)=\top$ where
$1\leq j\leq i-1$.

    2. (b)

If there exist some tuples in $\llbracket Q\rrbracket_{\mathcal{D}}$ share the
same values over $\vec{E}$ with $x_{i}$. Let $x_{j}$ be the first tuple in the
group $G_{j}$, then we have $\llbracket
E\rrbracket_{\mathcal{D},t_{j}}=\llbracket E\rrbracket_{\mathcal{D},t_{i}}$
where $j<i$ and $G_{j}=\textsf{append}(G_{j},t_{i})$. In symbolic setting, we
have $g(t_{\textsf{ptr}(i)},t_{\textsf{ptr}(j)})=\top$ because
$g(t_{j},j)=\top$ and
$\llbracket\vec{E}\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}=\llbracket\vec{E}\rrbracket_{\mathcal{S},\Gamma,[t_{j}]}$
is true.

By 17(a) and 17(b), we know if $\llbracket Q\rrbracket_{\mathcal{D}}$ is
partitioned into $[G_{1},\ldots,G_{m}]$ where $1\leq m\leq|\llbracket
Q\rrbracket_{\mathcal{D}}|$, there exists a symbolic group list s.t.
$[G_{\textsf{ptr}(1)}^{\prime},\ldots,G_{\textsf{ptr}(m)}^{\prime}]$ and
$G_{i}=\mathcal{I}(G_{\textsf{ptr}(i)}^{\prime})$ for $1\leq i\leq m$ because
$\llbracket Q\rrbracket_{\mathcal{D}}=\mathcal{I}(R)$. For any other group
$G_{j}^{\prime}\in[G_{1}^{\prime},\ldots,G_{n}^{\prime}]-[G_{\textsf{ptr}(1)}^{\prime},\ldots,G_{\textsf{ptr}(m)}^{\prime}]$,
there is no symbolic tuple inside, i.e., $\mathcal{I}(g^{-1}(j))=[]$ by the
definition of the function $g(t_{i},j)$. Therefore,
$[G_{1},\ldots,G_{m}]=\mathcal{I}([G_{\textsf{ptr}(1)}^{\prime},\ldots,G_{\textsf{ptr}(m)}^{\prime}])$.
Furthermore, since we will perform the same operations (e.g., $\sigma_{\phi}$
and $\Pi$) over $[G_{1},\ldots,G_{m}]$ and
$[G_{\textsf{ptr}(1)}^{\prime},\ldots,G_{\textsf{ptr}(m)}^{\prime}]$,

$\begin{array}[]{rcl}\llbracket\text{GroupBy}(Q,\vec{E},L,\phi)\rrbracket_{\mathcal{D}}&=&\textsf{map}(\textsf{filter}([G_{1},\ldots,G_{m}],\lambda
xs.\llbracket\phi\rrbracket_{\mathcal{D},xs}=\top),\lambda xs.\llbracket
L\rrbracket_{\mathcal{D},xs})\\\
&=&\textsf{map}(\textsf{filter}(\mathcal{I}([G_{\textsf{ptr}(1)}^{\prime},\ldots,G_{\textsf{ptr}(m)}^{\prime}]),\lambda
xs.\llbracket\phi\rrbracket_{\mathcal{D},xs}=\top),\lambda xs.\llbracket
L\rrbracket_{\mathcal{D},xs})\\\
&=&\mathcal{I}(\textsf{map}(\textsf{filter}([G_{\textsf{ptr}(1)}^{\prime},\ldots,G_{\textsf{ptr}(m)}^{\prime}],\lambda
xs.\llbracket\phi\rrbracket_{\mathcal{D},xs}=\top),\lambda xs.\llbracket
L\rrbracket_{\mathcal{D},xs}))\\\
&=&\mathcal{I}(\text{GroupBy}(Q,\vec{E},L,\phi))\\\ \end{array}$

Let
$\mathcal{D}^{\prime}=\mathcal{D}[Q^{\prime}\mapsto\llbracket\text{GroupBy}(Q,\vec{E},L,\phi)\rrbracket_{\mathcal{D}}]$,
then we know $x_{i}^{\prime}=\textsf{map}(\textsf{filter}([G_{i}],\lambda
xs.\llbracket\phi\rrbracket_{\mathcal{D},xs}$ $=\top),\lambda xs.\llbracket
L\rrbracket_{\mathcal{D},xs})$ and $\mathcal{I}(\text{Del})(x_{i})$ $=\bot$
for any tuple
$x_{i}^{\prime}\in\llbracket\text{GroupBy}(Q,\vec{E},L,\phi)\rrbracket_{\mathcal{D}}$.

If $x_{i}$ is the first tuple of $G_{i}$, then $t_{\textsf{ptr}(i)}$ is the
first symbolic tuple of $G_{\textsf{ptr}(i)}^{\prime}$, and
$g^{-1}(\textsf{ptr}(i))=G_{\textsf{ptr}(i)}^{\prime}$. Since
$ys\in[G_{1},\ldots,G_{m}]$, let us discuss the predicate
$\llbracket\phi\rrbracket_{\mathcal{D},G_{i}}$ in two cases.

    1. (a)

If $\llbracket\phi\rrbracket_{\mathcal{D},G_{i}}\neq\top$ is true, then the
group $G_{i}$ will be removed and the tuple
$\textsf{map}(\textsf{filter}([G_{i}],$ $\lambda
xs.\llbracket\phi\rrbracket_{\mathcal{D},xs}=\top),\lambda xs.\llbracket
L\rrbracket_{\mathcal{D},xs})$ does not exist,
$\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i)}^{\prime})=\top$,
$\llbracket\phi\rrbracket_{\mathcal{D},\mathcal{I}(G_{\textsf{ptr}(i)}^{\prime})}=\llbracket\phi\rrbracket_{\mathcal{D},\mathcal{I}(g^{-1}(\textsf{ptr}(i)))}\neq\top$.
As $g(t_{\textsf{ptr}(i)},i)$ always holds for $G_{i}$, we know
$g(t_{\textsf{ptr}(i)},i)\land\\\
$$\llbracket\phi\rrbracket_{\mathcal{D},\mathcal{I}(g^{-1}(\textsf{ptr}(i)))}=\top$
is false and $\neg
g(t_{\textsf{ptr}(i)},i)\lor\llbracket\phi\rrbracket_{\mathcal{D},\mathcal{I}(g^{-1}(\textsf{ptr}(i)))}\neq\top$
is true. Therefore,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi_{\textsf{ptr}(i)}^{\prime\prime}$.

    2. (b)

If $\llbracket\phi\rrbracket_{\mathcal{D},G_{i}}\neq\top$ is false, then the
group $G_{i}$ will projected out and the tuple
$\textsf{map}(\textsf{filter}([G_{i}],$ $\lambda
xs.\llbracket\phi\rrbracket_{\mathcal{D},xs}=\top),\lambda xs.\llbracket
L\rrbracket_{\mathcal{D},xs})$ does exist,
$\llbracket\phi\rrbracket_{\mathcal{D},\mathcal{I}(G_{\textsf{ptr}(i)}^{\prime})}=\llbracket\phi\rrbracket_{\mathcal{D},\mathcal{I}(g^{-1}(\textsf{ptr}(i)))}=\top$,
$\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i)}^{\prime})=\bot$. As
$g(t_{\textsf{ptr}(i)},i)$ always holds for $G_{i}$, we know
$g(t_{\textsf{ptr}(i)},i)\land\\\
$$\llbracket\phi\rrbracket_{\mathcal{D},\mathcal{I}(g^{-1}(\textsf{ptr}(i)))}=\top$
is true and $\neg
g(t_{\textsf{ptr}(i)},i)\lor\llbracket\phi\rrbracket_{\mathcal{D},\mathcal{I}(g^{-1}(\textsf{ptr}(i)))}\neq\top$
is false. Therefore,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi_{\textsf{ptr}(i)}^{\prime\prime}$.

Also, by the definition of the function $g$, we know
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\land_{i=1}^{n}\Phi_{i}^{\prime}$.

Hence,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi\land\land_{i=1}^{n}\Phi_{i}^{\prime}\land\land_{i=1}^{n}\Phi_{i}^{\prime\prime}$
and Theorem 4.5 for the inductive case $Q^{\prime}=\text{GroupBy}(Q,$
$\vec{E},L,\phi)$ is proved.

  18. (18)

Inductive case: $Q^{\prime\prime}=\text{With}(\vec{Q},\vec{T},Q^{\prime})$.

Suppose that $\mathcal{S}\vdash Q_{i}:\mathcal{A}_{i}$ by Figure 10;
$\Gamma\vdash Q_{i}\hookrightarrow R_{i}$ by Figure 11;
$\mathcal{S},\Gamma\vdash Q_{i}\leadsto\Phi_{i}$ by Figure 18.

By the inductive hypothesis, we have $\mathcal{I}(R_{i})=\llbracket
Q_{i}\rrbracket_{\mathcal{D}}$ where $1\leq i\leq n$ and
$n=|\vec{Q}|=|\vec{T}|$; $\Gamma^{\prime}\vdash Q^{\prime}\hookrightarrow
R^{\prime}$, $\mathcal{S}^{\prime},\Gamma^{\prime}\vdash
Q^{\prime}\leadsto\Phi^{\prime}$, $\mathcal{I}(R^{\prime})=\llbracket
Q^{\prime}\rrbracket_{\mathcal{D}_{n}}$ where
$\mathcal{S}^{\prime}=\mathcal{S}[T_{1}\mapsto\mathcal{A}_{1},\ldots,T_{n}\mapsto\mathcal{A}_{n}]$
and
$\Gamma^{\prime}=\Gamma[T_{1}\mapsto\mathcal{T}_{1},\ldots,T_{n}\mapsto\mathcal{T}_{n}]$.
Also, by Figure 17, we know
$\mathcal{D}^{\prime}=\mathcal{D}[R_{i}\mapsto\llbracket
Q\rrbracket_{\mathcal{D}}~{}|~{}R_{i}\in R]=[R_{1}\mapsto\llbracket
Q_{1}\rrbracket_{\mathcal{D}},\ldots,R_{n}\mapsto\llbracket
Q_{n}\rrbracket_{\mathcal{D}}]$.

Let $\mathcal{I}^{\prime}=\mathcal{I}$,
$\mathcal{D}^{\prime\prime}=\mathcal{D}^{\prime}[o_{Q^{\prime}}\mapsto\llbracket
Q^{\prime}\rrbracket_{\mathcal{D}}]$. Obviously, we have
$\llbracket\text{With}(\vec{Q},\vec{T},Q^{\prime})\rrbracket_{\mathcal{D}^{\prime\prime}}=\llbracket
Q^{\prime}\rrbracket_{\mathcal{D}^{\prime\prime}}=\mathcal{I}(R^{\prime})$ and
$\mathcal{I}^{\prime},\mathcal{D}^{\prime\prime}\models\land_{i=1}^{n}\Phi_{i}\land\Phi^{\prime}$.

Hence, Theorem 4.5 for the inductive case
$Q^{\prime\prime}=\text{With}(\vec{Q},\vec{T},Q^{\prime})$ is proved.

  19. (19)

Inductive case: $Q^{\prime}=\text{OrderBy}(Q,\vec{E},b)$.

Suppose that $\Gamma\vdash Q\hookrightarrow R$ where $R$ has symbolic tuples
$[t_{1},\ldots,t_{n}]$,
$\Gamma\vdash\text{OrderBy}(Q,\vec{E},b)\hookrightarrow R^{\prime}$ where
$R^{\prime}$ has symbolic tuples $[t_{1}^{\prime},\ldots,t_{n}^{\prime}]$
Figure 11; $\mathcal{S},\Gamma\vdash Q\leadsto\Phi$ by Figure 19;

By the inductive hypothesis, we have $\mathcal{I}(R)=\llbracket
Q\rrbracket_{\mathcal{D}}$ and $\mathcal{I},\mathcal{D}\models\Phi$.

We create a fresh symbolic table $R^{\prime\prime}$ where $R^{\prime\prime}$
has symbolic tuples $[t_{1}^{\prime\prime},\ldots,t_{n}^{\prime\prime}]$, and
the function $\text{moveDelToEnd}(R,R^{\prime\prime})$ can ”remove” deleted
symbolic tuples in $R$ by moving them to the end of a list $R$ and return the
sorted list to $R^{\prime\prime}$. Further,
$\text{moveDelToEnd}(\vec{t},\vec{t}^{\prime\prime})$ guarantees that there
exists $m$ symbolic tuples s.t. $\forall i\leq m.\text{Del}(t_{i})=\bot$ and
$\forall m<i.\text{Del}(t_{i})=\top$ and, for each tuple
$t_{i}^{\prime\prime}\in R^{\prime\prime}$, we can find its corresponding
tuple $t_{\text{indexOf}(\vec{t},i)}$ in $R$ where the $\text{indexOf}(R,i)$
function take as input a symbolic tuple list $R$ and an index $i$, and returns
the corresponding index $\text{indexOf}(R,i)$ s.t.
$\mathcal{I}(t_{i}^{\prime\prime})=\mathcal{I}(t_{\text{indexOf}(\vec{t},i)})$
and
$\mathcal{I}(\text{Del})(t_{i}^{\prime\prime})=\mathcal{I}(\text{Del})(t_{\text{indexOf}(\vec{t},i)})$
because $t_{i}^{\prime\prime}=t_{\text{indexOf}(\vec{t},i)}$.

Take $\mathcal{I}^{\prime}$ s.t.
$\mathcal{I}^{\prime}(\text{Del})(t_{i})\leftrightarrow\mathcal{I}(\text{Del})(t_{i})$,
$\mathcal{I}^{\prime}(t_{i})=\mathcal{I}(t_{i})$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime\prime})=\mathcal{I}(\text{Del})(t_{i}^{\prime\prime})$,
$\mathcal{I}^{\prime}(t_{i}^{\prime\prime})=\mathcal{I}(t_{\text{indexOf}(\vec{t},i)})$,
$\mathcal{I}^{\prime}(t_{i}^{\prime})=\mathcal{I}(t_{\text{find}(i,\vec{E},b)}^{\prime\prime})$
and
$\mathcal{I}(\text{Del})(t_{i}^{\prime})\leftrightarrow\mathcal{I}(\text{Del})(t_{\text{find}(i,\vec{E},b)}^{\prime\prime})$
where the find function seeks out the $i$-th smallest symbolic tuple
$t_{\text{find}(i,\vec{E},b)^{\prime\prime}}\in R^{\prime\prime}$ w.r.t. the
expression list $\vec{E}$ and the ascending flag $b$. Additionally, for those
deleted tuples $[t_{m+1},\ldots t_{n}]$ in $R^{\prime\prime}$, the find
function will not consider them because they are ”deleted”. Hence, for any
tuple
$t_{i}^{\prime\prime}\in[t_{1}^{\prime\prime},\ldots,t_{m}^{\prime\prime}]$,
we always can find a tuple $t_{\text{find}(i,\vec{E},b)}^{\prime\prime}$ s.t.
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime})=\mathcal{I}(\text{Del})(t_{\text{find}(i,\vec{E},b)}^{\prime\prime})=\mathcal{I}(\text{Del})(t_{\text{find}(\text{indexOf}(\vec{t},i),\vec{E},b)}^{\prime\prime})=\bot$
and
$\mathcal{I}^{\prime}(t_{i}^{\prime})=\mathcal{I}(t_{\text{find}(i,\vec{E},b)}^{\prime\prime})=\mathcal{I}(t_{\text{find}(\text{indexOf}(\vec{t},i)}^{\prime\prime},\vec{E},b))$.

To compare two tuples (e.g., $x_{1}$ and $x_{2}$) w.r.t. the expression list
$\vec{E}$ and the ascending flag $b$, let us discuss the value of
$\text{Cmp}(\vec{E},b,x_{1},x_{2})$ in three cases.

    1. (a)

If $v(x_{1},E_{i})<v(x_{2},E_{i})$, then
$\text{Cmp}(\vec{E},b,x_{1},x_{2})=b\neq\top$ by the semantics of foldr.
Furthermore, if $b=\top$ (i.e., in ascending order), then
$\text{Cmp}(\vec{E},b,x_{1},x_{2})=\bot$ and vice versa.

    2. (b)

If $v(x_{1},E_{i})>v(x_{2},E_{i})$, then
$\text{Cmp}(\vec{E},b,x_{1},x_{2})=b\neq\bot$ by the semantics of foldr.
Furthermore, if $b=\top$ (i.e., in ascending order), then
$\text{Cmp}(\vec{E},b,x_{1},x_{2})=\top$ and vice versa.

    3. (c)

If $v(x_{1},E_{i})=v(x_{2},E_{i})$, then
$\text{Cmp}(\vec{E},b,x_{1},x_{2})=b\neq\textsf{foldr}(\lambda E_{i}.\lambda
y.\textsf{ite}(v(x_{1},E_{i})<v(x_{2},E_{i}),\\\
$$\top,\textsf{ite}(v(x_{1},E_{i})>v(x_{2},E_{i}),\bot,y)),\top,\vec{E}_{i+1:m})$
where $m=|\vec{E}|$, $y$ denotes the accumulator of foldr and
$\text{Cmp}(\vec{E},b,x_{1},x_{2})$ will be determined by the following
expressions $[E_{i+1},\ldots,E_{m}]$. Also, we initialize the accumulator $y$
to $\top$ which aims to find the first smallest (last biggest) tuple if
$x_{1}$ and $x_{2}$ are equal w.r.t. $\vec{E}$ and b.

Further, by the semantics of foldl and the value of
$\text{Cmp}(\vec{E},b,x_{1},x_{2})$, we know $\text{MinTuple}(\vec{E},b,$
$xs)$ is to find the first smallest (last biggest) tuple from $xs$ w.r.t.
$\vec{E}$ and $b$.

$\begin{array}[]{rcl}\text{MinTuple}(\vec{E},b,xs)&=&\textsf{foldl}(\lambda
x.\lambda
y.\textsf{ite}(\text{Cmp}(\vec{E},b,x_{1},x_{2}),y,x),\textsf{head}(xs),xs)\\\
&=&\textsf{foldl}(\lambda x.\lambda
y.\textsf{ite}(\text{Cmp}(\vec{E},b,x_{1},x_{2}),y,x),\\\
&&\qquad\textsf{ite}(\text{Cmp}(\vec{E},b,xs_{1},xs_{1}),xs_{1},xs_{1}),xs_{2:n})\\\
&=&\textsf{foldl}(\lambda x.\lambda
y.\textsf{ite}(\text{Cmp}(\vec{E},b,x_{1},x_{2}),y,x),xs_{1},xs_{2:n})\\\
\end{array}$

Let us discuss $\text{MinTuple}(\vec{E},b,xs)$ in two cases.

    1. (a)

If $\text{Cmp}(\vec{E},b,x_{1},x_{2})$ is true, the accumulator (i.e., the
smallest or biggest tuple of $xs$) in $\text{MinTuple}(\vec{E},b,xs)$ will be
updated.

    2. (b)

If $\text{Cmp}(\vec{E},b,x_{1},x_{2})$ is false, the accumulator (i.e., the
smallest or biggest tuple of $xs$) in $\text{MinTuple}(\vec{E},b,xs)$ remains
constant.

Therefore, $\text{MinTuple}(\vec{E},b,\llbracket
Q\rrbracket_{\mathcal{D}}-xs)$ seeks out the smallest (biggest) tuple from
$\llbracket Q\rrbracket_{\mathcal{D}}-xs$. Let $a_{i}$ denote the $i$-th
smallest (biggest) tuple from $\llbracket Q\rrbracket_{\mathcal{D}}-xs$ (i.e.,
$a_{i}=\text{MinTuple}(\vec{E},b,\llbracket Q\rrbracket_{\mathcal{D}}-xs)$
where $xs=[a_{i},\ldots,a_{i-1}]$) and $\vec{t}_{1:p}=\llbracket
Q\rrbracket_{\mathcal{D}}$, then

$\begin{array}[]{rcl}\llbracket\text{OrderBy}(Q,\vec{E},b)\rrbracket_{\mathcal{D}}&=&\textsf{foldl}(\lambda
xs.\lambda\\_.(\textsf{append}(xs,\text{MinTuple}(\vec{E},b,\llbracket
Q\rrbracket_{\mathcal{D}}-xs))),[],\llbracket Q\rrbracket_{\mathcal{D}})\\\
&=&\textsf{foldl}(\lambda
xs.\lambda\\_.(\textsf{append}(xs,\text{MinTuple}(\vec{E},b,\llbracket
Q\rrbracket_{\mathcal{D}}-xs))),[],\vec{t}_{1:p})\\\ &=&\textsf{foldl}(\lambda
xs.\lambda\\_.(\textsf{append}(xs,\text{MinTuple}(\vec{E},b,\llbracket
Q\rrbracket_{\mathcal{D}}-xs))),[a_{1}],\vec{t}_{2:p})\\\ &&\ldots\\\
&=&[a_{1},\ldots,a_{p}]\\\ \end{array}$

Since (i) $t_{\text{find}(i,\vec{E},b)}^{\prime\prime}$ and $a_{i}$ are the
$i$-th smallest (biggest) tuples from $\mathcal{I}(R^{\prime\prime})$ and
$\llbracket Q\rrbracket_{\mathcal{D}}$, respectively, (ii)
$\mathcal{I}(R^{\prime\prime})=\llbracket Q\rrbracket_{\mathcal{D}}$, we have,
for any $1\leq i\leq p$,
$\mathcal{I}(t_{\text{find}(i,\vec{E},b)}^{\prime\prime})=\mathcal{I}(a_{i})$
and
$\mathcal{I}(\text{Del})(t_{\text{find}(i,\vec{E},b)}^{\prime\prime})=\mathcal{I}(\text{Del})(a_{i})=\bot$;
and, for any $p\leq i\leq n$,
$\mathcal{I}(\text{Del})(t_{\text{find}(i,\vec{E},b)}^{\prime\prime})=\top$.
Also by the definition of $\mathcal{I}^{\prime}$, we have
$t_{i}^{\prime}=t_{\text{find}(i,\vec{E},b)}^{\prime\prime}$,
$\mathcal{I}(t_{i}^{\prime})=\mathcal{I}(a_{i})$ and
$\mathcal{I}(\text{Del})(t_{i}^{\prime})=\mathcal{I}(\text{Del})(a_{i})=\bot$
where $1\leq i\leq p$. Thus,
$\mathcal{I}^{\prime}(\text{OrderBy}(Q,\vec{E},b))=\llbracket\text{OrderBy}(Q,\vec{E},b)\rrbracket_{\mathcal{D}}$.

Let
$\mathcal{D}^{\prime}=\mathcal{D}[o_{\text{OrderBy}(Q,\vec{E},b)}\mapsto\llbracket\text{OrderBy}(Q,\vec{E},b)\rrbracket_{\mathcal{D}}]$.
Obviously,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi\land\Phi^{\prime}\land\Phi^{\prime\prime}$
where $\Phi^{\prime}=\text{moveDelToEnd}(\vec{t},\vec{t}^{\prime\prime})$ and
$\Phi^{\prime\prime}=\land_{i=1}^{n}t_{i}^{\prime}=t_{\text{find}(i,\vec{E},b)}^{\prime\prime}$
hold because
$\mathcal{I}^{\prime}(t_{i}^{\prime})=\mathcal{I}^{\prime}(t_{\text{find}(i,\vec{E},b)}^{\prime\prime})=\mathcal{I}^{\prime}(t_{\text{find}(\text{indexOf}(\vec{t},i),\vec{E},b)})$
and
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime})=\mathcal{I}^{\prime}(\text{Del})(t_{\text{find}(i,\vec{E},b)})=\mathcal{I}^{\prime}(\text{Del})$
$(t_{\text{find}(\text{indexOf}(\vec{t},i),\vec{E},b)})$.

Hence, Theorem 4.5 for the inductive case
$Q^{\prime}=\text{OrderBy}(Q,\vec{E},b)$ is proved.

∎

###### Proof of Theorem 4.6:.

Let $\Gamma$ be a symbolic database over schema $\mathcal{S}$ and $Q$ be a
query. Consider a symbolic relation $R$ and a formula $\Phi$ such that
$\Gamma\vdash Q\hookrightarrow R$ and $\mathcal{S},\Gamma,\vdash
Q\leadsto\Phi$. If $\Phi$ is satisfiable, then for any satisfying
interpretation $\mathcal{I}$ of $\Phi$, running $Q$ over the concrete database
$\mathcal{I}(\Gamma)$ yields the relation $\mathcal{I}(R)$, i.e.,

$(\Gamma\vdash Q\hookrightarrow R)\land(\mathcal{S},\Gamma\vdash
Q\leadsto\Phi)\land(\mathcal{I}\models\Phi)\Rightarrow\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$

∎

###### Proof..

By structural induction on $Q$.

  1. (1)

Base case: $Q=T$.

$R=\Gamma(T)$ by Figure 11. $\llbracket
T\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(\Gamma)(T)$ by Figure 17.
Therefore, $\llbracket
T\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(\Gamma)(T)=\mathcal{I}(\Gamma(T))=\mathcal{I}(R)$.

Thus, Theorem 4.6 for the inductive case $Q=T$ is proved.

  2. (2)

Inductive case: $Q^{\prime}=\Pi_{L}(Q)$.

Suppose that $\mathcal{S}\vdash Q:[a_{1},\ldots,a_{m}]$ by Figure 10;
$\mathcal{S}\vdash\sigma_{L}(Q):[a_{1}^{\prime},\ldots,a_{l}^{\prime}]$ where
$l=|L|$ by Figure 10; $\Gamma\vdash Q\hookrightarrow R$ where $R$ has symbolic
tuples $[t_{1},\ldots,t_{n}]$ by Figure 11; $\mathcal{S},\Gamma\vdash
Q\leadsto\Phi$ by Figure 18;
$\llbracket\Pi_{L}(Q)\rrbracket_{\mathcal{I}(\Gamma)}=\textsf{ite}(\text{hasAggr}(L),[\llbracket
L\rrbracket_{\mathcal{I}(\Gamma),\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}}],\textsf{map}(\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)},\lambda x.\llbracket
L\rrbracket_{\mathcal{I}(\Gamma),x}))$ by Figure 17.

Let us discuss $\text{hasAggr}(L)$ in two cases.

    1. (a)

If $\text{hasAggr}(L)$ is true, then $\Gamma\vdash\Pi_{L}(Q)\hookrightarrow
R^{\prime}$ where $R^{\prime}$ only has one symbolic tuple $[t_{1}^{\prime}]$
by Figure 11,
$\mathcal{S},\Gamma\vdash\Pi_{L}(Q)\leadsto\Phi\land\land_{i=1}^{l}\Phi_{i}^{\prime}\land(\text{Del}(t_{1}^{\prime})\leftrightarrow\land_{i=1}^{n}\text{Del}(t_{i}))$
where $\Phi_{i}^{\prime}=\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{1}^{\prime}]}=\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{S},\Gamma,\vec{t}}$ by Figure 12.

Take $\mathcal{I}$ s.t.
$\mathcal{I}\models\Phi\land\land_{i=1}^{l}\Phi_{i}^{\prime}\land\neg\text{Del}(t_{1}^{\prime})$.

By Lemma D.5, we know $\mathcal{I}(\llbracket
A\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\llbracket
A\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$. Also, by Figure
17, we have

$\begin{array}[]{rcl}\llbracket\Pi_{L}(Q)\rrbracket_{\mathcal{I}(\Gamma)}&=&[\llbracket
L\rrbracket_{\mathcal{I}(\Gamma),\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}}]=[\llbracket
L\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}([t_{1},\ldots,t_{n}])}]\\\
&=&[(\text{ToString}(a_{1}^{\prime}),\llbracket
a_{1}^{\prime}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}([t_{1},\ldots,t_{n}])}),\ldots,(\text{ToString}(a_{l}^{\prime}),\llbracket
a_{l}^{\prime}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}([t_{1},\ldots,t_{n}])})]\\\
&=&[(\text{ToString}(a_{1}^{\prime}),\llbracket
a_{1}^{\prime}\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(t_{1}^{\prime})]}),\ldots,(\text{ToString}(a_{l}^{\prime}),\llbracket
a_{l}^{\prime}\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(t_{1}^{\prime})]})]\\\
&=&[\llbracket
L\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(t_{1}^{\prime})]}]=\mathcal{I}(R^{\prime})\end{array}$

    2. (b)

If $\text{hasAggr}(L)$ is false, then $\Gamma\vdash\Pi_{L}(Q)\hookrightarrow
R^{\prime}$ where $R^{\prime}$ has symbolic tuples
$[t_{1}^{\prime},\ldots,t_{n}^{\prime}]$ by Figure 11,
$\mathcal{S},\Gamma\vdash\Pi_{L}(Q)\leadsto\Phi\land\land_{i=1}^{n}\Phi_{i}^{\prime}$
where $\Phi_{i}^{\prime}=\land_{j=1}^{l}\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{i}^{\prime}]}=\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}\land\text{Del}(t_{i}^{\prime})\leftrightarrow\text{Del}(t_{i})$
by Figure 12.

Take $\mathcal{I}$ s.t.
$\mathcal{I}\models\Phi\land\land_{i=1}^{n}\Phi_{i}^{\prime}$.

By Figure 17, we have

$\begin{array}[]{rcl}\llbracket\Pi_{L}(Q)\rrbracket_{\mathcal{I}(\Gamma)}&=&\textsf{map}(\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)},\lambda x.\llbracket
L\rrbracket_{\mathcal{I}(\Gamma),x})\\\
&=&\textsf{map}(\mathcal{I}([t_{1},\ldots,t_{n}]),\lambda x.\llbracket
L\rrbracket_{\mathcal{I}(\Gamma),x})\\\ &=&[\llbracket
L\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(t_{1})]},\ldots,\llbracket
L\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(t_{n})]}]\\\ &=&[\llbracket
L\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(t_{1}^{\prime})]},\ldots,\llbracket
L\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(t_{n}^{\prime})]}]\\\
&=&\mathcal{I}(R^{\prime})\end{array}$

Thus, $\llbracket\Pi_{L}(Q)\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$ by
2(a) and 2(b) and Theorem 4.6 for the inductive case $Q^{\prime}=\Pi_{L}(Q)$
is proved.

  3. (3)

Inductive case: $Q=\sigma_{\phi}(Q)$.

Suppose that $\Gamma\vdash Q\hookrightarrow R$ where $R$ has symbolic tuples
$[t_{1},\ldots,t_{n}]$, $\Gamma\vdash\sigma_{\phi}(Q)\hookrightarrow
R^{\prime}$ where $R^{\prime}$ has symbolic tuples
$[t_{1}^{\prime},\ldots,t_{n}^{\prime}]$ by Figure 11;
$\mathcal{S},\Gamma\vdash Q\leadsto\Phi\land\land_{i=1}^{n}\Phi_{i}^{\prime}$
where
$\Phi_{i}^{\prime}=(\neg\text{Del}(t_{i})\land\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}=\top)\to
t_{i}^{\prime}=t\land(\text{Del}(t_{i})\lor\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}\neq\top)\to\text{Del}(t_{i}^{\prime})$
by Figure 18.

Take $\mathcal{I}$ s.t.
$\mathcal{I}\models\Phi\land\land_{i=1}^{n}\Phi_{i}^{\prime}$.

By Lemma D.1, we know
$\mathcal{I}(\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,[x]})=\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}([x])}$
and, therefore,

$\begin{array}[]{rcl}\llbracket\sigma_{\phi}(Q)\rrbracket_{\mathcal{I}(\Gamma)}&=&\textsf{filter}(\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)},\lambda
x.\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[x]}=\top)\\\
&=&\textsf{filter}(\mathcal{I}([t_{1},\ldots,t_{n}]),\lambda
x.\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[x]}=\top)\\\ \end{array}$

For any tuple $t_{i}\in R$, let us discuss $\text{Del}(t_{i})$ in two cases.

    1. (a)

If $\mathcal{I}(\text{Del})(t_{i})=\top$, then we know
$\textsf{filter}([\mathcal{I}(t_{i})],\lambda
x.\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[x]}=\top)$ is deleted because
of the semantics of filter, and $\mathcal{I}(\text{Del})(t_{i}^{\prime})=\top$
because of
$\text{Del}(t_{i}^{\prime})\leftrightarrow\text{Del}(t_{i})\lor\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(t_{i})]}$.

    2. (b)

If $\mathcal{I}(\text{Del})(t_{i})=\bot$, then we know the existence of
$\textsf{filter}([\mathcal{I}(t_{i})],\lambda
x.\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[x]}=\top)$ depends on
$\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(t_{i})]}=\top$.
Let us discuss
$\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(t_{i})]}$ in two
cases.

      1. (b1)

If $\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(t_{i})]}=\top$
is true, then $\textsf{filter}([\mathcal{I}(t_{i})],\lambda
x.\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[x]}=\top)$ exists and
$\mathcal{I}(\text{Del})(t_{i}^{\prime})=\bot$ because
$\text{Del}(t_{i})\lor\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}=\top\to\text{Del}(t_{i}^{\prime})$.
Therefore, $\textsf{filter}([\mathcal{I}(t_{i})],$ $\lambda
x.\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[x]}$
$=\top)=[\mathcal{I}(t_{i}^{\prime})]$.

      2. (b2)

If $\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(t_{i})]}=\top$
is false, then $\textsf{filter}([\mathcal{I}(t_{i})],\lambda
x.\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[x]}=\top)$ is deleted and
$\mathcal{I}(\text{Del})$ $(t_{i}^{\prime})=\top$ because
$\text{Del}(t_{i})\lor\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}=\top\to\text{Del}(t_{i}^{\prime})$.
Therefore, $\textsf{filter}([\mathcal{I}(t_{i})],$ $\lambda
x.\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[x]}=\top)=[\mathcal{I}(t_{i}^{\prime})]$.

Thus,
$\llbracket\sigma_{\phi}(Q)\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$ by
3(a) and 3(b) and Theorem 4.6 for the inductive case
$Q^{\prime}=\sigma_{\phi}(Q)$ is proved.

  4. (4)

Inductive case: $Q^{\prime}=\rho_{T}(Q)$.

Suppose that $\Gamma\vdash Q\hookrightarrow R$ where $R$ has symbolic tuples
$[t_{1},\ldots,t_{n}]$, $\Gamma\vdash\rho_{T}(Q)\hookrightarrow R^{\prime}$
where $R^{\prime}$ has symbolic tuples
$[t_{1}^{\prime},\ldots,t_{n}^{\prime}]$ by Figure 11;
$\mathcal{S},\Gamma\vdash Q\leadsto\Phi$,
$\mathcal{S},\Gamma\vdash\Phi\land\land_{i=1}^{n}t_{i}^{\prime}=t_{i}$ by
Figure 18.

Take $\mathcal{I}$ s.t.
$\mathcal{I}\models\Phi\land\land_{i=1}^{n}t_{i}^{\prime}=t_{i}$.

$\llbracket\rho_{T}(Q)\rrbracket_{\mathcal{I}(\Gamma)}=\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)[T\mapsto\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}]}=\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}([t_{1},\ldots,t_{n}])=\mathcal{I}(R)$.

Thus, Theorem 4.6 for the inductive case $Q^{\prime}=\rho_{T}(Q)$ is proved.

  5. (5)

Inductive case: $Q^{\prime\prime}=Q\times Q^{\prime}$.

Suppose that $\mathcal{S}\vdash Q:[a_{1},\ldots,a_{p}]$, $\mathcal{S}\vdash
Q^{\prime}:[a_{1}^{\prime},\ldots,a_{q}^{\prime}]$ by Figure 10; $\Gamma\vdash
Q\hookrightarrow R$ where $R$ has symbolic tuples $[t_{1},\ldots,t_{n}]$,
$\Gamma\vdash Q^{\prime}\hookrightarrow R^{\prime}$ where $R^{\prime}$ has
symbolic tuples $[t_{1}^{\prime},\ldots,t_{m}^{\prime}]$, $\Gamma\vdash
Q\times Q^{\prime}\hookrightarrow R^{\prime\prime}$ where $R^{\prime\prime}$
has symbolic tuples $[t_{1,1}^{\prime\prime},\ldots,t_{n,m}^{\prime\prime}]$
by Figure 11; $\mathcal{S},\Gamma\vdash Q\leadsto\Phi$,
$\mathcal{S},\Gamma\vdash Q^{\prime}\leadsto\Phi^{\prime}$,
$\mathcal{S},\Gamma\vdash Q\times
Q^{\prime}\leadsto\Phi\land\Phi^{\prime}\land\land_{i=1}^{n}\land_{j=1}^{m}\Phi^{\prime\prime}_{i,j}$
where
$\Phi^{\prime\prime}_{i,j}=(\neg\text{Del}(t_{i})\land\neg\text{Del}(t_{j}^{\prime}))\to(\neg\text{Del}(t_{i,j}^{\prime\prime})\land\land_{k=1}^{p}\llbracket
a_{k}\rrbracket_{\mathcal{S},\Gamma,[t_{i,j}^{\prime\prime}]}=\llbracket
a_{k}\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}\land\land_{k=1}^{q}\llbracket
a_{k}\rrbracket_{\mathcal{S},\Gamma,[t_{i,j}^{\prime\prime}]}=\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{j}^{\prime}]})\land(\text{Del}(t_{i})\lor\text{Del}(t_{j}^{\prime})\to\text{Del}(t_{i,j}^{\prime\prime}))$
by Figure 18.

Take $\mathcal{I}$ s.t.
$\mathcal{I}\models\Phi\land\Phi^{\prime}\land\land_{i=1}^{n}\land_{j=1}^{m}\Phi^{\prime\prime}_{i,j}$.

By Figure 17, we have

$\begin{array}[]{rcl}\llbracket Q\times
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}&=&\textsf{foldl}(\lambda xs.\lambda
x.\textsf{append}(xs,\textsf{map}(\llbracket
Q_{2}\rrbracket_{\mathcal{I}(\Gamma)},\lambda
y.\textsf{merge}(x,y))),[],\llbracket
Q_{1}\rrbracket_{\mathcal{I}(\Gamma)})\\\ &=&[\\\
&&\quad[\textsf{merge}(\mathcal{I}(t_{1}),\mathcal{I}(t_{1}^{\prime})),\ldots,\textsf{merge}(\mathcal{I}(t_{1}),\mathcal{I}(t_{m}^{\prime}))]\\\
&&\quad\ldots\\\
&&\quad[\textsf{merge}(\mathcal{I}(t_{n}),\mathcal{I}(t_{1}^{\prime})),\ldots,\textsf{merge}(\mathcal{I}(t_{n}),\mathcal{I}(t_{m}^{\prime}))]\\\
&&]\\\ \end{array}$

For any tuples $t_{i}\in R$ and $t_{j}^{\prime}\in R^{\prime}$, let us discuss
$\mathcal{I}(\text{Del})(t_{i})\lor\mathcal{I}(\text{Del})(t_{j}^{\prime})$ in
two cases.

    1. (a)

If
$\mathcal{I}(\text{Del})(t_{i})\lor\mathcal{I}(\text{Del})(t_{j}^{\prime})=\top$,
then we know $\textsf{merge}(\mathcal{I}(t_{i}),\mathcal{I}(t_{j}^{\prime}))$
is deleted by the semantics of merge and
$\mathcal{I}(\text{Del})(t_{i,j}^{\prime\prime})=\top$ because of
$\text{Del}(t_{i})\lor\text{Del}(t_{j}^{\prime})\to\text{Del}(t_{i,j}^{\prime\prime})$.
Therefore,
$\textsf{merge}(\mathcal{I}(t_{i}),\mathcal{I}(t_{j}^{\prime}))=\mathcal{I}(t_{i,j}^{\prime\prime})$.

    2. (b)

If
$\mathcal{I}(\text{Del})(t_{i})\lor\mathcal{I}(\text{Del})(t_{j}^{\prime})=\bot$,
then we know
$\textsf{merge}(\mathcal{I}(t_{i}),\mathcal{I}(t_{j}^{\prime}))=\mathcal{I}(t_{i,j}^{\prime\prime})$
by the semantics of merge and
$\mathcal{I}(\text{Del})(t_{i,j}^{\prime\prime})=\top$ because of
$\Phi_{i,j}^{\prime\prime}$.

Hence, $\llbracket Q\times
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$ by 5(a) and 5(b)
and Theorem 4.6 for the inductive case $Q^{\prime\prime}=Q\times Q^{\prime}$
is proved.

  6. (6)

Inductive case: $Q^{\prime\prime}=Q\bowtie_{\phi}Q^{\prime}$.

This case can be proved by the inductive cases $Q^{\prime\prime}=Q\times
Q^{\prime}$ and $Q^{\prime}=\sigma_{\phi}(Q)$.

  7. (7)

Inductive case:
$Q^{\prime\prime}=Q\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q^{\prime}$.

Suppose that $\mathcal{S}\vdash Q:[a_{1},\ldots,a_{p}]$, $\mathcal{S}\vdash
Q^{\prime}:[a_{1}^{\prime},\ldots,a_{q}^{\prime}]$ by Figure 10;
$\mathcal{S}\vdash Q\hookrightarrow R$ where $R$ has symbolic tuples
$[t_{1},\ldots,t_{n}]$, $\mathcal{S}\vdash Q^{\prime}\hookrightarrow
R^{\prime}$ where $R^{\prime}$ has symbolic tuples
$[t_{1}^{\prime},\ldots,t_{m}^{\prime}]$, $\mathcal{S}\vdash
Q\bowtie_{\phi}Q^{\prime}\hookrightarrow R$ where $R^{\prime\prime}$ has
symbolic tuples
$[t_{1,1}^{\prime\prime},\ldots,t_{n,m}^{\prime\prime},t_{1,m+1}^{\prime\prime},\ldots,t_{n,m+1}^{\prime\prime}]$
by Figure 10; $\mathcal{S},\Gamma\vdash
Q\bowtie_{\phi}Q^{\prime}\leadsto\Phi$, $\mathcal{S},\Gamma\vdash
Q\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q^{\prime}\leadsto\Phi\land\land_{i=1}^{n}\Phi_{i}^{\prime}$
where $\Phi_{i}^{\prime}=\land_{k=1}^{p}\llbracket
a_{k}\rrbracket_{\mathcal{S},\Gamma,[t_{i,m+1}^{\prime\prime}]}=\llbracket
a_{k}\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}\land\land_{k=1}^{q}\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{i,m+1}^{\prime\prime}]}=\text{Null}\land(\neg\text{Del}(t_{i})\land\land_{j=1}^{m}\text{Del}(t_{i,j}^{\prime\prime})\leftrightarrow\neg\text{Del}(t_{i,m+1}^{\prime\prime}))$
by Figure 18.

Take $\mathcal{I}$ s.t.
$\mathcal{I}\models\Phi\land\land_{i=1}^{n}\Phi_{i}^{\prime}$.

By Figure 17, we have

$\begin{array}[]{rcl}\llbracket Q\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}&=&\textsf{foldl}(\lambda
xs.\lambda
x.\textsf{append}(xs,\textsf{ite}(|v_{1}(x)|=0,v_{2}(x),v_{1}(x)),[],\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}))\\\ &=&\textsf{foldl}(\lambda xs.\lambda
x.\textsf{append}(xs,\textsf{ite}(|v_{1}(x)|=0,v_{2}(x),v_{1}(x)),[],\mathcal{I}(\vec{t}_{1:n})))\\\
&=&\textsf{foldl}(\lambda xs.\lambda
x.\textsf{append}(xs,\textsf{ite}(|v_{1}(x)|=0,v_{2}(x),v_{1}(x)),\\\
&&\quad[\textsf{ite}(|v_{1}(\mathcal{I}(t_{1}))|=0,v_{2}(\mathcal{I}(t_{1})),v_{1}(\mathcal{I}(t_{1})))],\mathcal{I}(\vec{t}_{2:n})))\\\
&=&\ldots\\\ &=&[\\\
&&\quad\textsf{ite}(|v_{1}(\mathcal{I}(t_{1}))|=0,v_{2}(\mathcal{I}(t_{1})),v_{1}(\mathcal{I}(t_{1})))\\\
&&\quad\ldots\\\
&&\quad\textsf{ite}(|v_{1}(\mathcal{I}(t_{n}))|=0,v_{2}(\mathcal{I}(t_{n})),v_{1}(\mathcal{I}(t_{n})))\\\
&&]\end{array}$

For any entry
$\textsf{ite}(|v_{1}(\mathcal{I}(t_{i}))|=0,v_{2}(\mathcal{I}(t_{i})),v_{1}(\mathcal{I}(t_{i})))\in\llbracket
Q\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q^{\prime}\rrbracket$,
let us discuss $|v_{1}(\mathcal{I}(t_{i}))|=0$ in two cases.

    1. (a)

If $|v_{1}(\mathcal{I}(t_{i}))|=0$ is true, then
$|\llbracket[\mathcal{I}(t_{i})]\bowtie_{\phi}Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}|=0$
and $\textsf{ite}(|v_{1}(\mathcal{I}(t_{i}))|=0,v_{2}(\mathcal{I}(t_{i})),\\\
$$v_{1}(\mathcal{I}(t_{i})))=v_{2}(\mathcal{I}(t_{i}))=[\textsf{merge}(\mathcal{I}(t_{i}),T_{\text{Null}})]$.

Further, if $\mathcal{I}(\text{Del})(t_{i})=\top$, then
$\textsf{ite}(|v_{1}(\mathcal{I}(t_{i}))|=0,v_{2}(\mathcal{I}(t_{i})),v_{1}(\mathcal{I}(t_{i})))=\textsf{merge}$
$(\mathcal{I}(t_{i}),\\\ $$T_{\text{Null}})$ is deleted by the semantics of
merge. Meanwhile,
$\mathcal{I}([t_{i,1}^{\prime\prime},\ldots,t_{i,m}^{\prime\prime},t_{i,m+1}^{\prime\prime}])$
are all deleted because of
$\text{Del}(t_{i,j}^{\prime\prime})\leftrightarrow\text{Del}(t_{i})\lor\text{Del}(t_{j}^{\prime})\lor\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(\textsf{merge}(t_{i},t_{j}^{\prime}))]}\neq\top$
for $1\leq j\leq m$ and
$\text{Del}(t_{i,m+1}^{\prime\prime})\leftrightarrow\text{Del}(t_{i})\lor\neg\land_{j=1}^{m}\text{Del}(t_{i,j}^{\prime\prime})$.
Therefore,
$\textsf{ite}(|v_{1}(\mathcal{I}(t_{i}))|=0,v_{2}(\mathcal{I}(t_{i})),\\\
$$v_{1}(\mathcal{I}(t_{i})))=\mathcal{I}$
$([t_{i,1}^{\prime\prime},\ldots,t_{i,m}^{\prime\prime},t_{i,m+1}^{\prime\prime}])$.

Otherwise, if $\mathcal{I}(\text{Del})(t_{i})=\bot$, then
$\textsf{merge}(\mathcal{I}(t_{i}),T_{\text{Null}})=\mathcal{I}(t_{i,m+1}^{\prime\prime})$.
Also, since $\sigma_{\phi}(\mathcal{I}($
$[\textsf{merge}(t_{i},t_{1}^{\prime}),\ldots,\textsf{merge}(t_{i},t_{m}^{\prime})]))$
and $\mathcal{I}([t_{i,1}^{\prime\prime},\ldots,t_{i,m}^{\prime\prime}])$ are
deleted, $\textsf{ite}(|v_{1}(\mathcal{I}(t_{i}))|=0,\\\
$$v_{2}(\mathcal{I}(t_{i})),v_{1}(\mathcal{I}(t_{i})))=[\textsf{merge}(\mathcal{I}(t_{i}),T_{\text{Null}})]=[\mathcal{I}(t_{i,m+1}^{\prime\prime})]$.

    2. (b)

If $|v_{1}(\mathcal{I}(t_{i}))|=0$ is false, then
$|\llbracket[\mathcal{I}(t_{i})]\bowtie_{\phi}Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}|\neq
0$ and
$\textsf{ite}(|v_{1}(\mathcal{I}(t_{i}))|=0,v_{2}(\mathcal{I}(t_{i})),\\\
$$v_{1}(\mathcal{I}(t_{i})))=v_{1}(\mathcal{I}(t_{i}))=\llbracket[\mathcal{I}(t_{i})]\bowtie_{\phi}Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}=\sigma_{\phi}(\mathcal{I}([\textsf{merge}(t_{i},t_{j}^{\prime}),$
$\ldots,\textsf{merge}(t_{i},t_{j}^{\prime})]))$.

Further, if $\mathcal{I}(\text{Del})(t_{i})=\top$, then
$\mathcal{I}(\sigma_{\phi}([\textsf{merge}(t_{i},t_{j}^{\prime}),\ldots,\textsf{merge}(t_{i},t_{j}^{\prime})]))$
are deleted by the semantics of merge. Meanwhile,
$\mathcal{I}([t_{i,1}^{\prime\prime},\ldots,t_{i,m}^{\prime\prime},t_{i,m+1}^{\prime\prime}])$
are all deleted because of
$\text{Del}(t_{i,j}^{\prime\prime})\leftrightarrow\text{Del}(t_{i})\lor\text{Del}(t_{j}^{\prime})\lor\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(\textsf{merge}(t_{i},t_{j}^{\prime}))]}\neq\top$
for $1\leq j\leq m$ and
$\text{Del}(t_{i,m+1}^{\prime\prime})\leftrightarrow\text{Del}(t_{i})\lor\neg\land_{j=1}^{m}\text{Del}(t_{i,j}^{\prime\prime})$.
Therefore,
$\textsf{ite}(|v_{1}(\mathcal{I}(t_{i}))|=0,v_{2}(\mathcal{I}(t_{i})),$
$v_{1}(\mathcal{I}(t_{i})))=\\\ $$\mathcal{I}$
$([t_{i,1}^{\prime\prime},\ldots,t_{i,m}^{\prime\prime},t_{i,m+1}^{\prime\prime}])$.

Otherwise, if $\mathcal{I}(\text{Del})(t_{i})=\bot$,
$\mathcal{I}(\text{Del})(t_{k}^{\prime})=\bot$ and
$\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(\textsf{merge}(t_{i},t_{k}^{\prime}))]}=\top$
where $1\leq k\leq m$, then
$\mathcal{I}(t_{i,k}^{\prime\prime})=\mathcal{I}(\textsf{merge}(t_{i},t_{k}^{\prime}))$
and
$\mathcal{I}(\text{Del})(t_{i,k}^{\prime\prime})=\mathcal{I}(\text{Del})(\textsf{merge}(t_{i},t_{k}^{\prime}))=\bot$.

Hence, $\llbracket Q\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$
by 7(a) and 7(b) and Theorem 4.6 for the inductive case
$Q^{\prime\prime}=Q\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q^{\prime}$
is proved.

  8. (8)

Inductive case:
$Q^{\prime\prime}=Q\mathbin{\bowtie\mkern-5.8mu\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}}_{\phi}Q^{\prime}$.

Following a similar method in the inductive case
$Q^{\prime\prime}=Q\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q^{\prime}$,
we prove $\llbracket
Q\mathbin{\bowtie\mkern-5.8mu\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}}_{\phi}Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$.

  9. (9)

Inductive case:
$Q^{\prime\prime}=Q\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}}_{\phi}Q^{\prime}$.

Suppose that by $\mathcal{S}\vdash Q:[a_{1},\ldots,a_{p}]$, $\mathcal{S}\vdash
Q:[a_{1}^{\prime},\ldots,a_{q}^{\prime}]$ by Figure 10; $\mathcal{S}\vdash
Q\hookrightarrow R$ where $R$ has symbolic tuples $[t_{1},\ldots,t_{n}]$,
$\mathcal{S}\vdash Q^{\prime}\hookrightarrow R^{\prime}$ where $R^{\prime}$
has symbolic tuples $[t_{1}^{\prime},\ldots,t_{m}^{\prime}]$,
$\mathcal{S}\vdash Q\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}}_{\phi}Q^{\prime}\hookrightarrow
R^{\prime\prime}$ where $R^{\prime\prime}$ has symbolic tuples
$[t_{1,1}^{\prime\prime},\ldots,t_{n+1,m}^{\prime\prime},t_{1,m+1}^{\prime\prime},\ldots,t_{n,m+1}^{\prime\prime}]$,
by Figure 11; $\mathcal{S},\Gamma\vdash
Q\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q^{\prime}\leadsto\Phi$,
$\mathcal{S},\Gamma\vdash Q\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}}_{\phi}Q^{\prime}\leadsto\Phi\land\land_{j=1}^{m}\Phi_{j}^{\prime}$
where $\Phi_{j}^{\prime}=\land_{k=1}^{p}\llbracket
a_{k}\rrbracket_{\mathcal{S},\Gamma,[t_{n+1,j}^{\prime\prime}]}=\text{Null}\land\land_{k=1}^{q}\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{n+1,j}^{\prime\prime}]}=\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{j}^{\prime}]}\land(\neg\text{Del}(t_{j}^{\prime})\land\land_{i=1}^{n}\text{Del}(t_{i,j}^{\prime\prime})\leftrightarrow\neg\text{Del}(t_{n+1,j}^{\prime\prime}))$
by Figure 18.

Take $\mathcal{I}$ s.t.
$\mathcal{I}\models\Phi\land\land_{j=1}^{m}\Phi_{j}^{\prime}$.

By the inductive hypothesis, we know $\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$, $\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R^{\prime})$ and
$\llbracket Q\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}([t_{1,1}^{\prime\prime},\ldots,t_{n,m+1}^{\prime\prime}])$.

For any tuple $t_{j}^{\prime}\in\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}$, if
$\mathcal{I}(\text{Del})(t_{j}^{\prime})=\top$, then $|\llbracket
Q\bowtie_{\phi}[t_{j}^{\prime}]\rrbracket_{\mathcal{I}(\Gamma)}|=0$ is true
and, therefore, $\textsf{filter}([\mathcal{I}(t_{j}^{\prime})],\lambda
y.|\llbracket Q\bowtie_{\phi}[y]\rrbracket_{\mathcal{I}(\Gamma)}|=0)$ is
deleted because of the semantics of filter and
$\mathcal{I}(\text{Del})(t_{n+1,j}^{\prime\prime})=\top$ because of
$\neg\text{Del}(t_{j}^{\prime})\land\land_{i=1}^{n}\text{Del}(t_{i,j}^{\prime\prime})\leftrightarrow\neg\text{Del}(t_{n+1,j}^{\prime\prime})$.
Otherwise, $\mathcal{I}(\text{Del})(t_{j}^{\prime})=\bot$ and then let us
discuss $|\llbracket
Q\bowtie_{\phi}[t_{j}^{\prime}]\rrbracket_{\mathcal{I}(\Gamma)}|=0$ in two
cases.

    1. (a)

If $|\llbracket
Q\bowtie_{\phi}[t_{j}^{\prime}]\rrbracket_{\mathcal{I}(\Gamma)}|=0$ is true,
then $\textsf{map}(\textsf{filter}([\mathcal{I}(t_{j}^{\prime})],\lambda
y.|\llbracket Q\bowtie_{\phi}[y]\rrbracket_{\mathcal{I}(\Gamma)}|=0),\\\
$$\lambda x.\textsf{merge}(T_{\text{Null}},x))=[\textsf{merge}$
$(T_{\text{Null}},\mathcal{I}(t_{j}^{\prime}))]$,
$\mathcal{I}(\text{Del})(t_{i,j}^{\prime\prime})=\top$ for $1\leq i\leq n$,
$\mathcal{I}(\text{Del})(t_{n+1,j}^{\prime\prime})\\\ $$=\bot$ and
$\mathcal{I}(t_{n+1,j}^{\prime\prime})=\textsf{merge}(T_{\text{Null}},\mathcal{I}(t_{j}^{\prime}))$
because of $\Phi_{j}^{\prime}$ and the semantics of merge.

    2. (b)

If $|\llbracket Q\bowtie_{\phi}[t_{i}]\rrbracket_{\mathcal{I}(\Gamma)}|=0$ is
false, then $\textsf{map}(\textsf{filter}([\mathcal{I}(t_{i})],\lambda
y.|\llbracket Q\bowtie_{\phi}[y]\rrbracket_{\mathcal{I}(\Gamma)}|=0),\lambda
x.$ $\textsf{merge}(T_{\text{Null}},x))$ is deleted and
$\mathcal{I}(\text{Del})(t_{n+1,j}^{\prime})=\top$.

Hence, $\llbracket Q\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}}_{\phi}Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R^{\prime\prime})$
by 10(a) and 10(b) and Theorem 4.6 for the inductive case
$Q^{\prime\prime}=Q\mathbin{\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.73193pt]{2.5pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.7889pt]{2.5pt}{0.6pt}}}_{\phi}Q^{\prime}$ is proved.

  10. (10)

Inductive case: $Q^{\prime}=\text{Distinct}(Q)$.

Suppose that $\mathcal{S},\Gamma\vdash Q\hookrightarrow R$ where $R$ has
symbolic tuples $[t_{1},\ldots,t_{n}]$,
$\mathcal{S},\Gamma\vdash\text{Distinct}(Q)\hookrightarrow R^{\prime}$ where
$R^{\prime}$ has symbolic tuples $[t_{1}^{\prime},\ldots,t_{n}^{\prime}]$ by
Figure 11; $\mathcal{S},\Gamma\vdash Q\leadsto\Phi$, $\mathcal{S},\Gamma\vdash
Q\leadsto\Phi\land\Phi^{\prime}$ where
$\Phi^{\prime}=\text{Dedup}(\vec{t},\vec{t^{\prime}})$ by Figure 18.

By the inductive hypothesis, we have $\mathcal{I},\mathcal{D}\models\Phi$ and
$\llbracket Q\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$.

Take $\mathcal{I}$ s.t. $\mathcal{I}\models\Phi\land\Phi^{\prime}$.

For any tuple $t_{i}\in\llbracket Q\rrbracket_{\mathcal{I}(\Gamma)}$, if
$\mathcal{I}(\text{Del})(t_{i})=\top$, then
$\mathcal{I}(\text{Del})(t_{i}^{\prime})=\top$. On the other hand, for any
existing tuples $t_{i}$ and $t_{j}$ in $\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}$ s.t.
$\mathcal{I}(\text{Del})(t_{i})=\mathcal{I}(\text{Del})(t_{i})=\bot$ and
$i\leq j$, let us discuss $\mathcal{I}(t_{i})=\mathcal{I}(t_{j})$ in two
cases.

    1. (a)

If $\mathcal{I}(t_{i})=\mathcal{I}(t_{j})$ is true, then
$\mathcal{I}(t_{i}^{\prime})=\mathcal{I}(t_{i})$ and
$\mathcal{I}(\text{Del})(t_{i}^{\prime})=\mathcal{I}(\text{Del})(t_{i})=\bot$,
and $\textsf{filter}(\mathcal{I}(t_{j}),\lambda y.\mathcal{I}(t_{i})=y)$ is
deleted and $\mathcal{I}(\text{Del})(t_{j}^{\prime})=\top$ by the semantics of
filter.

    2. (b)

If $\mathcal{I}(t_{i})=\mathcal{I}(t_{j})$ is false, then
$\mathcal{I}(t_{i}^{\prime})=\mathcal{I}(t_{i})$ and
$\mathcal{I}(\text{Del})(t_{i}^{\prime})=\mathcal{I}(\text{Del})(t_{i})=\bot$,
and $\mathcal{I}(t_{j}^{\prime})=\mathcal{I}(t_{j})$ and
$\mathcal{I}(\text{Del})(t_{j}^{\prime})=\mathcal{I}(\text{Del})(t_{j})=\bot$
by the semantics of filter.

Hence,
$\llbracket\text{Distinct}(Q)\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R^{\prime\prime})$
by 10(a) and 10(b) and Theorem 4.6 for the inductive case
$Q^{\prime}=\text{Distinct}(Q)$ is proved.

  11. (11)

Inductive case: $Q^{\prime\prime}=Q\cap Q^{\prime}$.

Suppose that $\mathcal{S}\vdash\text{Distinct}(Q)\hookrightarrow R$ where $R$
ash symbolic tuples $[t_{1},\ldots,t_{n}]$, $\mathcal{S}\vdash
Q^{\prime}\hookrightarrow R^{\prime}$ where $R^{\prime}$ ash symbolic tuples
$[t_{1}^{\prime},\ldots,t_{m}^{\prime}]$, $\mathcal{S}\vdash Q\cap
Q^{\prime}\hookrightarrow R^{\prime\prime}$ where $R^{\prime\prime}$ ash
symbolic tuples $[t_{1}^{\prime\prime},\ldots,t_{n}^{\prime\prime}]$ by Figure
11; $\mathcal{S},\Gamma\vdash\text{Distinct}(Q)\leadsto\Phi$,
$\mathcal{S},\Gamma\vdash Q^{\prime}\leadsto\Phi^{\prime}$ ,
$\mathcal{S},\Gamma\vdash Q\cap
Q^{\prime}\leadsto\Phi\land\Phi^{\prime}\land\land_{i=1}^{n}\Phi_{i}^{\prime\prime}$
where $\Phi_{i}^{\prime\prime}=t_{i}\in\vec{t^{\prime}}\to
t_{i}^{\prime\prime}=t_{i}\land
t_{i}\not\in\vec{t^{\prime}}\to\text{Del}(t_{i}^{\prime\prime})$ by Figure 18.

By the inductive hypothesis, we know
$\llbracket\text{Distinct}(Q)\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$
and $\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R^{\prime})$.

Take $\mathcal{I}$ s.t.
$\mathcal{I}\models\Phi\land\Phi^{\prime}\land\land_{i=1}^{n}\land_{j=1}^{m}\Phi_{i,j}^{\prime\prime}$.

For any tuple
$\mathcal{I}(t_{i})\in\llbracket\text{Distinct}(Q)\rrbracket_{\mathcal{I}(\Gamma)}$,
if $\mathcal{I}(\text{Del})(t_{i})=\top$, then
$\mathcal{I}(\text{Del})(t_{i}^{\prime})=\top$ because of
$t_{i}\not\in\vec{t^{\prime}}\to\text{Del}(t_{i}^{\prime\prime})$; otherwise,
let us discuss $\mathcal{I}(t_{i})\in\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}$ in two cases.

    1. (a)

If $\mathcal{I}(\text{Del})(t_{i})=\bot$ and $\mathcal{I}(t_{i})\in\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}$ is true, then
$\mathcal{I}(t_{i})=\mathcal{I}(t_{i}^{\prime})$ and
$\mathcal{I}(\text{Del})(t_{i})=\mathcal{I}(\text{Del})(t_{i}^{\prime})=\bot$
by the semantics of filter.

    2. (b)

If $\mathcal{I}(\text{Del})(t_{i})=\bot$ and $\mathcal{I}(t_{i})\in\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}$ is false, then
$\textsf{filter}([t_{i}],\lambda x.x\in\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)})$ is deleted by the semantics of
filter and $\mathcal{I}(\text{Del})(t_{i}^{\prime})=\top$ because of
$t_{i}\not\in\vec{t^{\prime}}\to\text{Del}(t_{i}^{\prime\prime})$.

Hence, $\llbracket Q\cap
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R^{\prime\prime})$ by
11(a) and 11(b) and Theorem 4.6 for the inductive case $Q^{\prime\prime}=Q\cap
Q^{\prime}$ is proved.

  12. (12)

Inductive case: $Q=Q_{1}\setminus Q_{2}$.

Suppose that $\mathcal{S}\vdash\text{Distinct}(Q)\hookrightarrow R$ where $R$
ash symbolic tuples $[t_{1},\ldots,t_{n}]$, $\mathcal{S}\vdash
Q^{\prime}\hookrightarrow R^{\prime}$ where $R^{\prime}$ ash symbolic tuples
$[t_{1}^{\prime},\ldots,t_{m}^{\prime}]$, $\mathcal{S}\vdash Q\setminus
Q^{\prime}\hookrightarrow R^{\prime\prime}$ where $R^{\prime\prime}$ ash
symbolic tuples $[t_{1}^{\prime\prime},\ldots,t_{n}^{\prime\prime}]$ by Figure
11; $\mathcal{S},\Gamma\vdash\text{Distinct}(Q)\leadsto\Phi$,
$\mathcal{S},\Gamma\vdash Q^{\prime}\leadsto\Phi^{\prime}$ ,
$\mathcal{S},\Gamma\vdash Q\setminus
Q^{\prime}\leadsto\Phi\land\Phi^{\prime}\land\land_{i=1}^{n}\Phi_{i}^{\prime\prime}$
where $\Phi_{i}^{\prime\prime}=t_{i}\not\in\vec{t^{\prime}}\to
t_{i}^{\prime\prime}=t_{i}\land
t_{i}\in\vec{t^{\prime}}\to\text{Del}(t_{i}^{\prime\prime})$ by Figure 18.

By the inductive hypothesis, we know
$\llbracket\text{Distinct}(Q)\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$
and $\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R^{\prime})$.

Take $\mathcal{I}$ s.t.
$\mathcal{I}\models\Phi\land\Phi^{\prime}\land\land_{i=1}^{n}\land_{j=1}^{m}\Phi_{i,j}^{\prime\prime}$.

For any tuple
$\mathcal{I}(t_{i})\in\llbracket\text{Distinct}(Q)\rrbracket_{\mathcal{I}(\Gamma)}$,
if $\mathcal{I}(\text{Del})(t_{i})=\top$, then
$\mathcal{I}(\text{Del})(t_{i}^{\prime})=\top$ because of
$t_{i}\in\vec{t^{\prime}}\to t_{i}^{\prime\prime}=t_{i}$; otherwise, let us
discuss $\mathcal{I}(t_{i})\in\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}$ in two cases.

    1. (a)

If $\mathcal{I}(\text{Del})(t_{i})=\bot$ and $\mathcal{I}(t_{i})\in\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}$ is true, then
$\textsf{filter}([t_{i}],\lambda x.x\not\in\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)})$ is deleted by the semantics of
filter and $\mathcal{I}(\text{Del})(t_{i}^{\prime})=\top$ because of
$t_{i}\in\vec{t^{\prime}}\to\text{Del}(t_{i}^{\prime\prime})$.

    2. (b)

If $\mathcal{I}(\text{Del})(t_{i})=\bot$ and $\mathcal{I}(t_{i})\in\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}$ is false, then
$\mathcal{I}(t_{i})=\mathcal{I}(t_{i}^{\prime})$ and
$\mathcal{I}(\text{Del})(t_{i})=\mathcal{I}(\text{Del})(t_{i}^{\prime})=\bot$
by the semantics of filter.

Hence, $\llbracket Q\setminus
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R^{\prime\prime})$ by
12(a) and 12(b) and Theorem 4.6 for the inductive case
$Q^{\prime\prime}=Q\setminus Q^{\prime}$ is proved.

  13. (13)

Inductive case: $Q=Q_{1}-Q_{2}$.

Suppose that $\mathcal{S}\vdash Q\hookrightarrow R$ where $R$ has symbolic
tuples $[t_{1},\ldots,t_{n}]$, $\mathcal{S}\vdash Q^{\prime}\hookrightarrow
R^{\prime}$ where $R^{\prime}$ has symbolic tuples
$[t_{1}^{\prime},\ldots,t_{m}^{\prime}]$, $\mathcal{S}\vdash
Q-Q^{\prime}\hookrightarrow R^{\prime\prime}$ where $R^{\prime\prime}$ has
symbolic tuples $[t_{1}^{\prime\prime},\ldots,t_{n}^{\prime\prime}]$ by Figure
11; $\mathcal{S},\Gamma\vdash Q\leadsto\Phi$, $\mathcal{S},\Gamma\vdash
Q^{\prime}\leadsto\Phi^{\prime}$, $\mathcal{S},\Gamma\vdash
Q-Q^{\prime}\leadsto\Phi\land\Phi^{\prime}\land\land_{i=1}^{n}\land_{j=1}^{m}\Phi_{i,j}^{\prime\prime}$
where
$\Phi_{i,j}^{\prime\prime}=\neg\text{Del}(t_{i})\land\neg\text{Paired}(i,j)\to
t_{i}^{\prime\prime}=t_{i}\land\text{Del}(t_{i})\lor\text{Paired}(i,j)\to\text{Del}(t_{i}^{\prime\prime})$
by Figure 19.

By the inductive hypothesis, we know $\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$ and $\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R^{\prime})$.

Take $\mathcal{I}$ s.t.
$\mathcal{I}\models\Phi\land\Phi^{\prime}\land\land_{i=1}^{n}\land_{j=1}^{m}\Phi_{i,j}^{\prime\prime}$.

  14. (14)

Inductive case: $Q^{\prime\prime}=Q\cup Q^{\prime}$.

Since $Q\cup
Q^{\prime}\Leftrightarrow\text{Distinct}(Q\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}Q^{\prime})$,
this case can be proved by the inductive cases
$Q^{\prime\prime}=Q\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}Q^{\prime}$
and
$Q^{\prime}=\text{Distinct}(Q\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}Q^{\prime})$.

  15. (15)

Inductive case: $Q^{\prime\prime}=Q\uplus Q^{\prime}$.

Suppose that $\mathcal{S}\vdash Q\hookrightarrow R$ where $R$ has symbolic
tuples $[t_{1},\ldots,t_{n}]$, $\mathcal{S}\vdash Q^{\prime}\hookrightarrow
R^{\prime}$ where $R^{\prime}$ has symbolic tuples
$[t_{1}^{\prime},\ldots,t_{m}^{\prime}]$, $\mathcal{S}\vdash Q\uplus
Q^{\prime}\hookrightarrow R^{\prime\prime}$ where $R^{\prime\prime}$ has
symbolic tuples $[t_{1}^{\prime\prime},\ldots,t_{n+m}^{\prime\prime}]$ by
Figure 11; $\mathcal{S},\Gamma\vdash Q\leadsto\Phi$, $\mathcal{S},\Gamma\vdash
Q^{\prime}\leadsto\Phi^{\prime}$, $\mathcal{S},\Gamma\vdash Q\uplus
Q^{\prime}\leadsto\Phi\land\Phi^{\prime}\land\Phi^{\prime\prime}$ where
$\Phi^{\prime\prime}=\land_{i=1}^{n}t_{i}^{\prime\prime}=t_{i}\land\land_{j=n+1}^{n+m}t_{j}^{\prime\prime}=t_{j-n}^{\prime}$
by Figure 18.

By the inductive hypothesis, we know $\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$ and $\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R^{\prime})$.

Take $\mathcal{I}$ s.t.
$\mathcal{I}\models\Phi\land\Phi^{\prime}\land\Phi^{\prime\prime}$.

Further, since $t_{i}^{\prime\prime}=t_{i}$ for $1\leq i\leq n$ and
$t_{j}^{\prime\prime}=t_{j}$ for $n+1\leq j\leq n+m$, we have

$\begin{array}[]{rcl}\llbracket Q\uplus
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)}&=&\textsf{append}(\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)},\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma)})\\\
&=&\textsf{append}(\mathcal{I}(R),\mathcal{I}(R^{\prime}))\\\
&=&\textsf{append}([\mathcal{I}(t_{1}),\ldots,\mathcal{I}(t_{n})],[\mathcal{I}(t_{1}^{\prime}),\ldots,\mathcal{I}(t_{m}^{\prime})])\\\
&=&[\mathcal{I}(t_{1}),\ldots,\mathcal{I}(t_{n}),\mathcal{I}(t_{1}^{\prime}),\ldots,\mathcal{I}(t_{m}^{\prime})]\\\
&=&\mathcal{I}(R^{\prime\prime})\\\ \end{array}$

Hence, Theorem 4.6 for the inductive case $Q^{\prime\prime}=Q\uplus
Q^{\prime}$ is proved.

  16. (16)

Inductive case:
$Q^{\prime\prime}=Q\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}Q^{\prime}$.

Since
$Q\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}Q^{\prime}\Leftrightarrow
Q-(Q-Q^{\prime})$, this case can be proved by the inductive case
$Q^{\prime\prime}=Q-Q^{\prime}$.

  17. (17)

Inductive case: $Q^{\prime}=\text{GroupBy}(Q,\vec{E},L,\phi)$.

Suppose that $\Gamma\vdash Q\hookrightarrow R$ where $R$ has symbolic tuples
$[t_{1},\ldots,t_{n}]$,
$\Gamma\vdash\text{GroupBy}(Q,\vec{E},L,\phi)\hookrightarrow R$ where $R$ has
symbolic tuples $[t_{1}^{\prime},\ldots,t_{n}^{\prime}]$ by Figure 11;
$\mathcal{S},\Gamma\vdash Q\leadsto\Phi$,
$\mathcal{S},\Gamma\vdash\text{GroupBy}(Q,\vec{E},$
$L,\phi)\leadsto\Phi\land\land_{i=1}^{n}\Phi_{i}^{\prime}\land\land_{i=1}^{n}\Phi_{i}^{\prime\prime}$
where
$\Phi_{i}^{\prime}=\Sigma_{j=1}^{n}\text{If}(g(t_{i},j),0,1)=\text{If}(\text{Del}(t_{i}),0,1)\land\land_{j=1}^{i-1}g(t_{i},j)=(\neg\text{Del}(t_{i})\land
g(t_{i},j)\land\llbracket\vec{E}\rrbracket)_{\mathcal{S},\Gamma,[t_{i}]}=\llbracket\vec{E}\rrbracket)_{\mathcal{S},\Gamma,[t_{i}j}$
and
$\Phi_{i}^{\prime\prime}=(g(t_{i},j)\land\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,g^{-1}(i)}=\top\to\neg\text{Del}(t_{i}^{\prime})\land\land_{k=1}^{l}\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{i}^{\prime}]}=\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{S},\Gamma,g^{-1}(i)})\land(\neg
g(t_{i},j)\lor\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,g^{-1}(i)}\neq\top\to\text{Del}(t_{i}^{\prime}))$
by Figure 18; $L=[a_{1},\ldots a_{l}]$.

By the inductive hypothesis, we have $\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$.

Take $\mathcal{I}$ s.t.
$\mathcal{I}\models\Phi\land\land_{i=1}^{n}\Phi_{i}^{\prime}\land\land_{i=1}^{n}\Phi_{i}^{\prime\prime}$.

Let $G_{i}$ be the $i$-th group of $\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}$ and $g^{-1}(i)$ be the function takes the
index of the group $G_{i}$ and returns the tuples of the group $G_{i}$. Assume
there are $m$ non-empty groups in $\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}$ s.t. $m\leq n$ and the other $n-m$ empty
groups are deleted because of no non-deleted tuple. Therefore, we know that
for each group $G_{i}$, (i) it must have at least one non-deleted tuple, (ii)
all tuples $g^{-1}(i)$ in $G_{i}$ must share the same values over $\vec{E}$
and (iii)
$\llbracket\vec{E}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(g^{-1}(i))}$ is
unique among those groups because of Figure 18.

Further, by the semantics of filter and $\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}=\mathcal{I}(R)$, we know
$\text{Dedup}(Q,\vec{E})$ denotes $m$ unique values over $\vec{E}$. Therefore,
$Gs$ in
$\llbracket\text{GroupBy}(Q,\vec{E},L,\phi)\rrbracket_{\mathcal{I}(\Gamma)}$
is equivalent to the groups $\mathcal{I}([G_{1},\ldots,G_{m}])$ in the formula
$\Phi_{i}^{\prime\prime}$ and $\mathcal{I}(\text{Del})(t_{i})=\top$ since
$G_{i}$ is empty group for $m<i\leq n$.

$\begin{array}[]{rcl}\llbracket\text{GroupBy}(Q,\vec{E},L,\phi)\rrbracket_{\mathcal{I}(\Gamma)}&=&\textsf{map}(\textsf{filter}(Gs,\lambda
xs.\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),xs}=\top),\lambda
xs.\llbracket L\rrbracket_{\mathcal{I}(\Gamma),xs})\\\
&=&\textsf{map}(\textsf{filter}([G_{1},\ldots,G_{m}],\lambda
xs.\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),xs}=\top),\lambda
xs.\llbracket L\rrbracket_{\mathcal{I}(\Gamma),xs})\\\
&=&[\mathcal{I}(t_{1}^{\prime}),\ldots,\mathcal{I}(t_{m}^{\prime})]\\\
&=&\textsf{append}([\mathcal{I}(t_{1}^{\prime}),\ldots,\mathcal{I}(t_{m}^{\prime})],[\mathcal{I}(t_{m+1}),\ldots,\mathcal{I}(t_{n})])\\\
&=&[\mathcal{I}(t_{1}^{\prime}),\ldots,\mathcal{I}(t_{m}^{\prime}),\mathcal{I}(t_{m+1}^{\prime}),\ldots,\mathcal{I}(t_{n}^{\prime})]\\\
&=&\mathcal{I}(R^{\prime})\end{array}$

Hence, Theorem 4.6 for the inductive case
$Q^{\prime}=\text{GroupBy}(Q,\vec{E},L,\phi)$ is proved.

  18. (18)

Inductive case: $Q^{\prime\prime}=\text{With}(\vec{Q},\vec{T},Q^{\prime})$.

Suppose that $\mathcal{S}\vdash Q_{i}:\mathcal{A}_{i}$ by Figure 10;
$\Gamma\vdash Q_{i}\hookrightarrow R_{i}$ by Figure 11;
$\mathcal{S},\Gamma\vdash Q_{i}\leadsto\Phi_{i}$ by Figure 18.

By the inductive hypothesis, we have $\mathcal{I}(R_{i})=\llbracket
Q_{i}\rrbracket_{\mathcal{I}(\Gamma)}$ where $1\leq i\leq n$ and
$n=|\vec{Q}|=|\vec{T}|$; $\Gamma^{\prime}\vdash Q^{\prime}\hookrightarrow
R^{\prime}$, $\mathcal{S}^{\prime},\Gamma^{\prime}\vdash
Q^{\prime}\leadsto\Phi^{\prime}$, $\mathcal{I}(R^{\prime})=\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma^{\prime})}$ where
$\mathcal{S}^{\prime}=\mathcal{S}[T_{1}\mapsto\mathcal{A}_{1},\ldots,T_{n}\mapsto\mathcal{A}_{n}]$
and
$\Gamma^{\prime}=\Gamma[T_{1}\mapsto\mathcal{T}_{1},\ldots,T_{n}\mapsto\mathcal{T}_{n}]$.

Take $\mathcal{I}$ s.t.
$\mathcal{I}\models\land_{i=1}^{n}\Phi_{i}\land\Phi^{\prime}$.

By Figure 17, we know
$\llbracket\text{With}(\vec{Q},\vec{T},Q^{\prime})\rrbracket_{\mathcal{I}(\Gamma^{\prime})}=\llbracket
Q^{\prime}\rrbracket_{\mathcal{I}(\Gamma^{\prime})}=\mathcal{I}(R^{\prime})$.

Hence, Theorem 4.6 for the inductive case
$Q^{\prime\prime}=\text{With}(\vec{Q},\vec{T},Q^{\prime})$ is proved.

  19. (19)

Inductive case: $Q^{\prime}=\text{OrderBy}(Q,\vec{E},b)$.

Suppose that $\Gamma\vdash Q\hookrightarrow R$ where $R$ has symbolic tuples
$[t_{1},\ldots,t_{n}]$,
$\Gamma\vdash\text{OrderBy}(Q,\vec{E},b)\hookrightarrow R^{\prime}$ where
$R^{\prime}$ has symbolic tuples $[t_{1}^{\prime},\ldots,t_{n}^{\prime}]$ by
Figure 11; $\mathcal{S},\Gamma\vdash Q\leadsto\Phi$,
$\mathcal{S},\Gamma\vdash$
$\text{OrderBy}(Q,\vec{E},b)\leadsto\Phi\land\Phi^{\prime}\land\land_{i=1}^{n}\Phi_{i}^{\prime\prime}$
where $\Phi^{\prime}=\text{moveDelToEnd}(\vec{t},\vec{t^{\prime\prime}})$ and
$\Phi_{i}^{\prime\prime}=t_{i}^{\prime}=t_{\text{find}(i,\vec{E},b)}^{\prime\prime}$
by Figure 19; $R^{\prime\prime}$ is the fresh symbolic table where
$R^{\prime\prime}$ has the symbolic tuples
$[t_{1}^{\prime\prime},\ldots,t_{n}^{\prime\prime}]$ and
$t_{\text{indexOf}(\vec{t},i)}=t_{i}^{\prime\prime}$ for any tuple
$t_{i}^{\prime\prime}\in R^{\prime\prime}$.

By the inductive hypothesis, we have $\mathcal{I}(R)=\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}$. Also, by the semantics of the moveDelToEnd
function,
$\mathcal{I}(\text{Del})(t_{\text{indexOf}(\vec{t},i)})=\mathcal{I}(\text{Del})(t_{i}^{\prime\prime})$
and
$\mathcal{I}(t_{\text{indexOf}(\vec{t},i)})=\mathcal{I}(t_{i}^{\prime\prime})$.

Take $\mathcal{I}$ s.t.
$\mathcal{I}\models\Phi\land\Phi^{\prime}\land\land_{i=1}^{n}\Phi_{i}^{\prime\prime}$.

Assume there are $m$ non-deleted symbolic tuples in $R$ where $m\leq n$, then
we have, for any tuple
$t_{i}^{\prime\prime}\in[t_{1}^{\prime\prime},\ldots,t_{m}^{\prime\prime}]$,
$\mathcal{I}(t_{i})=\mathcal{I}(t_{\text{indexOf}(\vec{t},i)}^{\prime\prime})$
and
$\mathcal{I}(del)(t_{i})=\mathcal{I}(del)(t_{\text{indexOf}(\vec{t},i)}^{\prime\prime})=\bot$
and the other tuples $[t_{m+1}^{\prime\prime},\ldots,t_{n}^{\prime\prime}]$
are deleted (i.e., $\mathcal{I}(\text{Del})(t_{i})=\top$ where $m<i\leq n$) by
the semantics of the moveDelToEnd function. Let $a_{i}$ denote the $i$-th
smallest (biggest) tuple from $\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}-xs$ (i.e.,
$a_{i}=\text{MinTuple}(\vec{E},b,$ $\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}-xs)$ where $xs=[a_{i},\ldots,a_{i-1}]$),
then

$\begin{array}[]{rcl}\llbracket\text{OrderBy}(Q,\vec{E},b)\rrbracket_{\mathcal{I}(\Gamma)}&=&\textsf{foldl}(\lambda
xs.\lambda\\_.(\textsf{append}(xs,[\text{MinTuple}(\vec{E},b,\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}-xs)])),\\\ &&\quad[],\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)})\\\ &=&\textsf{foldl}(\lambda
xs.\lambda\\_.(\textsf{append}(xs,[\text{MinTuple}(\vec{E},b,\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}-xs)])),\\\ &&\quad[],\mathcal{I}(R))\\\
&&\ldots\\\ &=&[\mathcal{I}(a_{1}),\ldots,\mathcal{I}(a_{m})]\\\
&=&\mathcal{I}([a_{1},\ldots,a_{m}])\\\ \end{array}$

Furthermore, let $t_{\text{indexOf}(\vec{t},i)}$ be the corresponding tuple of
$a_{i}\in\llbracket Q\rrbracket_{\mathcal{I}(\Gamma)}$,

$\begin{array}[]{rcl}\llbracket\text{OrderBy}$
$(Q,\vec{E},b)\rrbracket_{\mathcal{I}(\Gamma)}&=&\mathcal{I}([a_{1},\ldots,a_{m}])\\\
&=&\mathcal{I}([t_{\text{indexOf}(\vec{t},i)},\ldots,t_{\text{indexOf}(\vec{t},i)}])\\\
&=&\mathcal{I}([t_{1}^{\prime\prime},\ldots,t_{m}^{\prime\prime}])\\\
&=&\mathcal{I}([t_{1}^{\prime\prime},\ldots,t_{m}^{\prime\prime}])+\mathcal{I}([t_{m+1}^{\prime\prime},\ldots,t_{n}^{\prime\prime}])\\\
&=&\mathcal{I}([t_{1}^{\prime\prime},\ldots,t_{n}^{\prime\prime}])\\\
&=&\mathcal{I}([t_{\text{find}(1,\vec{E},b)}^{\prime\prime},\ldots,t_{\text{find}(n,\vec{E},b)}^{\prime\prime}])\\\
&=&\mathcal{I}([t_{1}^{\prime},\ldots,t_{n}^{\prime}])\\\
&=&\mathcal{I}(R^{\prime})\\\ \end{array}$

Hence, Theorem 4.6 for the inductive case
$Q^{\prime}=\text{OrderBy}(Q,\vec{E},b)$ is proved.

∎

###### Lemma D.1.

Let $\mathcal{D}$ be a database over schema $\mathcal{S}$ and $xs$ be a tuple
list which formulates a predicate $\phi$. Consider a symbolic database
$\Gamma$ over $\mathcal{S}$ and a list of symbolic tuples $\mathcal{T}$ such
that $\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$ is valid. For
any interpretation $\mathcal{I}$ such that
$\mathcal{I}(\Gamma)=\mathcal{D}\land\mathcal{I}(\mathcal{T})=xs$, evaluating
$\phi$ over the concrete database $\mathcal{I}(\Gamma)$ and the concrete tuple
list $\mathcal{I}(\mathcal{T})$ yields the value of
$\mathcal{I}(\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$,
i.e.,

$\mathcal{I}(\Gamma)=\mathcal{D}\land\mathcal{I}(\mathcal{T})=xs\Rightarrow\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$

###### Lemma D.2.

Suppose $\llbracket\phi\rrbracket_{\mathcal{D},xs}$ is valid, then
$\mathcal{I}(\Gamma)=\mathcal{D}\land\mathcal{I}(\mathcal{T})=xs\Rightarrow\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$
holds.

###### Proof..

By structural induction on $\phi$.

  1. (1)

Base case: $\phi=\top$.

$\llbracket\top\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\top$ by Figure 21.
Also,
$\llbracket\top\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\top$
by Figure 17. Therefore,
$\mathcal{I}(\llbracket\top\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\mathcal{I}(\top)=\top=\llbracket\top\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$.

  2. (2)

Base case: $\phi=\bot$.

$\llbracket\bot\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\bot$ by Figure 21.
Also,
$\llbracket\bot\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\bot$
by Figure 17. Therefore,
$\mathcal{I}(\llbracket\bot\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\mathcal{I}(\bot)=\bot=\llbracket\bot\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$.

  3. (3)

Base case: $\phi=\text{Null}$.

$\llbracket\text{Null}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\text{Null}$
by Figure 21. Also,
$\llbracket\text{Null}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\text{Null}$
by Figure 17. Therefore,
$\mathcal{I}(\llbracket\text{Null}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\mathcal{I}(\text{Null})=\text{Null}=\llbracket\text{Null}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$.

  4. (4)

Base case: $\phi=A_{1}\odot A_{2}$.

$\llbracket A_{1}\odot
A_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\textsf{ite}(v_{1}=\text{Null}\lor
v_{2}=\text{Null},\bot,v_{1}\odot v_{2})$ where $v_{1}=\llbracket
A_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$ and $v_{2}=\llbracket
A_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$ by Figure 21. $\llbracket
A_{1}\odot
A_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\textsf{ite}(v_{1}^{\prime}=\text{Null}\lor
v_{2}^{\prime}=\text{Null},\bot,v_{1}^{\prime}\odot v_{2}^{\prime})$ where
$v_{1}^{\prime}=\llbracket
A_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$ and
$v_{2}^{\prime}=\llbracket
A_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$ by Figure 17.
By Lemma D.3, we have $\llbracket
A_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
A_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$ and $\llbracket
A_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
A_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$. Also since
$\mathcal{I}(v_{1})=\mathcal{I}(\llbracket
A_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\\\ $$\llbracket
A_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$
$=v_{1}^{\prime}$ and $\mathcal{I}(v_{2})=v_{2}^{\prime}$,

$\begin{array}[]{rcl}\mathcal{I}(\llbracket A_{1}\odot
A_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\mathcal{I}(\textsf{ite}(v_{1}=\text{Null}\lor
v_{2}=\text{Null},\bot,v_{1}\odot v_{2}))\\\
&=&\textsf{ite}(\mathcal{I}(v_{1})=\text{Null}\lor\mathcal{I}(v_{2})=\text{Null},\bot,\mathcal{I}(v_{1})\odot\mathcal{I}(v_{2}))\\\
&=&\textsf{ite}(v_{1}^{\prime}=\text{Null}\lor
v_{2}^{\prime}=\text{Null},\bot,v_{1}^{\prime}\odot v_{2}^{\prime})\\\
&=&\llbracket A_{1}\odot
A_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\\\ \end{array}$

  5. (5)

Base case: $\phi=\text{IsNull}(E)$.

$\llbracket\text{IsNull}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\text{Null},\top,\bot)$ by Figure
21.
$\llbracket\text{IsNull}(E)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\textsf{ite}($
$\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\text{Null},\top,\bot)$
by Figure 17. By Lemma D.3, we have $\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$.

$\begin{array}[]{rcl}\mathcal{I}(\llbracket\text{IsNull}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\mathcal{I}(\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\text{Null},\top,\bot))\\\
&=&\textsf{ite}(\mathcal{I}(\llbracket
E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\text{Null},\top,\bot)\\\
&=&\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\text{Null},\top,\bot)\\\
&=&\llbracket\text{IsNull}(E)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\end{array}$

  6. (6)

Base case: $\phi=\vec{E}\in\vec{v}$.
$\llbracket\vec{E}\in\vec{v}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\llbracket\lor_{i=1}^{n}\land_{j=1}^{m}E_{j}=v_{i,j}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$
where $\vec{v}=[v_{1,1},\ldots,v_{n,m}]$ and $m=|\vec{E}|$ by Figure 21.
$\llbracket\vec{E}\in\vec{v}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\lor_{i=1}^{n}\llbracket\vec{E}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\llbracket
v_{i}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$ by Figure 17.
By Lemma D.3, we have $\llbracket
E_{j}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
E_{j}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$ and $\llbracket
v_{i,j}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
v_{i,j}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$.

$\begin{array}[]{rcl}\mathcal{I}(\llbracket\vec{E}\in\vec{v}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\mathcal{I}(\llbracket\lor_{i=1}^{n}\land_{j=1}^{m}E_{j}=v_{i,j}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})\\\
&=&\lor_{i=1}^{n}\land_{j=1}^{m}\mathcal{I}(\llbracket
E_{j}=v_{i,j}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})\\\
&=&\lor_{i=1}^{n}\land_{j=1}^{m}\mathcal{I}(\llbracket
E_{j}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\mathcal{I}(\llbracket
v_{i,j}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})\\\
&=&\lor_{i=1}^{n}\land_{j=1}^{m}\llbracket
E_{j}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\llbracket
v_{i,j}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\\\
&=&\llbracket\vec{E}\in\vec{v}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\\\
\end{array}$

  7. (7)

Base case: $\phi=\vec{E}\in Q$.

Suppose that $\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}=\vec{v}=[v_{1,1},\ldots,v_{n,m}]$ by .

  8. (8)

Inductive case: $\phi=\phi_{1}\land\phi_{2}$.

$\llbracket\phi_{1}\land\phi_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\text{ite}((v_{1}=v_{2}=\text{Null})\land(v_{1}=\text{Null}\land
v_{2}=\bot)\land(v_{1}=\bot\land
v_{2}=\text{Null}),\text{Null},v_{1}=\top\land v_{2}=\top)$ where
$v_{1}=\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$ and
$v_{2}=\llbracket\phi_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$ by
Figure 21.
$\llbracket\phi_{1}\land\phi_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\text{ite}((v_{1}^{\prime}=v_{2}^{\prime}=\text{Null})\land(v_{1}^{\prime}=\text{Null}\land
v_{2}^{\prime}=\bot)\land(v_{1}^{\prime}=\bot\land
v_{2}^{\prime}=\text{Null}),\text{Null},v_{1}^{\prime}=\top\land
v_{2}^{\prime}=\top)$ where
$v_{1}^{\prime}=\llbracket\phi_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$
and
$v_{2}^{\prime}=\llbracket\phi_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$
by Figure 17. By Lemma D.1, we have
$\llbracket\phi_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$
and
$\llbracket\phi_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket\phi_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$.
Also since
$\mathcal{I}(v_{1})=\mathcal{I}(\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\llbracket\phi_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=v_{1}^{\prime}$
and $\mathcal{I}(v_{2})=v_{2}^{\prime}$,

$\begin{array}[]{rcl}\mathcal{I}(\llbracket\phi_{1}\land\phi_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\mathcal{I}(\text{ite}((v_{1}=\text{Null}\land
v_{2}=\text{Null})\land(v_{1}=\text{Null}\land v_{2}=\bot)\\\
&&\qquad\land(v_{1}=\bot\land v_{2}=\text{Null}),\text{Null},v_{1}=\top\land
v_{2}=\top))\\\
&=&\text{ite}((\mathcal{I}(v_{1})=\text{Null}\land\mathcal{I}(v_{2})=\text{Null})\land(\mathcal{I}(v_{1})=\text{Null}\land\mathcal{I}(v_{2})=\bot)\\\
&&\qquad\land(\mathcal{I}(v_{1})=\bot\land\mathcal{I}(v_{2})=\text{Null}),\text{Null},\mathcal{I}(v_{1})=\top\land\mathcal{I}(v_{2})=\top)\\\
&=&\text{ite}((v_{1}^{\prime}=\text{Null}\land
v_{2}^{\prime}=\text{Null})\land(v_{1}^{\prime}=\text{Null}\land
v_{2}^{\prime}=\bot)\\\ &&\qquad\land(v_{1}^{\prime}=\bot\land
v_{2}^{\prime}=\text{Null}),\text{Null},v_{1}^{\prime}=\top\land
v_{2}^{\prime}=\top)\\\
&=&\llbracket\phi_{1}\land\phi_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\end{array}$

  9. (9)

Inductive case: $\phi=\phi_{1}\lor\phi_{2}$.

$\llbracket\phi_{1}\lor\phi_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\text{ite}((v_{1}=v_{2}=\text{Null})\lor(v_{1}=\text{Null}\land
v_{2}=\bot)\lor(v_{1}=\bot\land v_{2}=\text{Null}),\text{Null},v_{1}=\top\lor
v_{2}=\top)$ where
$v_{1}=\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$ and
$v_{2}=\llbracket\phi_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$ by
Figure 21.
$\llbracket\phi_{1}\lor\phi_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\text{ite}((v_{1}^{\prime}=v_{2}^{\prime}=\text{Null})\lor(v_{1}^{\prime}=\text{Null}\land
v_{2}^{\prime}=\bot)\lor(v_{1}^{\prime}=\bot\land
v_{2}^{\prime}=\text{Null}),\text{Null},v_{1}^{\prime}=\top\lor
v_{2}^{\prime}=\top)$ where
$v_{1}^{\prime}=\llbracket\phi_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$
and
$v_{2}^{\prime}=\llbracket\phi_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$
by Figure 17. By Lemma D.1, we have
$\llbracket\phi_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$
and
$\llbracket\phi_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket\phi_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$.
Also since
$\mathcal{I}(v_{1})=\mathcal{I}(\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\llbracket\phi_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=v_{1}^{\prime}$
and $\mathcal{I}(v_{2})=v_{2}^{\prime}$,

$\begin{array}[]{rcl}\mathcal{I}(\llbracket\phi_{1}\lor\phi_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\mathcal{I}(\text{ite}((v_{1}=\text{Null}\lor
v_{2}=\text{Null})\lor(v_{1}=\text{Null}\land v_{2}=\bot)\\\
&&\qquad\lor(v_{1}=\bot\land v_{2}=\text{Null}),\text{Null},v_{1}=\top\lor
v_{2}=\top))\\\
&=&\text{ite}((\mathcal{I}(v_{1})=\text{Null}\lor\mathcal{I}(v_{2})=\text{Null})\lor(\mathcal{I}(v_{1})=\text{Null}\land\mathcal{I}(v_{2})=\bot)\\\
&&\qquad\lor(\mathcal{I}(v_{1})=\bot\land\mathcal{I}(v_{2})=\text{Null}),\text{Null},\mathcal{I}(v_{1})=\top\lor\mathcal{I}(v_{2})=\top)\\\
&=&\text{ite}((v_{1}^{\prime}=\text{Null}\lor
v_{2}^{\prime}=\text{Null})\lor(v_{1}^{\prime}=\text{Null}\land
v_{2}^{\prime}=\bot)\\\ &&\qquad\lor(v_{1}^{\prime}=\bot\land
v_{2}^{\prime}=\text{Null}),\text{Null},v_{1}^{\prime}=\top\lor
v_{2}^{\prime}=\top)\\\
&=&\llbracket\phi_{1}\lor\phi_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\end{array}$

  10. (10)

Inductive case: $\phi=\neg\phi_{1}$.

$\llbracket\neg\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\textsf{ite}(\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\text{Null},\text{Null},\neg\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$
because
$\llbracket\neg\phi\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\text{let}~{}v=\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}\\\
$$~{}\text{in}~{}\text{ite}(v=\text{Null},\text{Null},\neg v)$ by Figure 21.
$\llbracket\neg\phi_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\textsf{ite}(\llbracket\phi_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\text{Null},\text{Null},\\\
$$\neg\llbracket\phi_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})})$
because
$\llbracket\neg\phi\rrbracket_{\mathcal{D},xs}=\text{let}~{}v=\llbracket\phi\rrbracket_{\mathcal{D},xs}~{}\text{in}~{}\text{ite}(v=\text{Null},\text{Null},\neg
v)$ by Figure 17. By Lemma D.1, we have
$\llbracket\phi_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$.
Therefore,

$\begin{array}[]{rcl}\mathcal{I}(\llbracket\neg\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\textsf{ite}(\mathcal{I}(\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\text{Null})=\text{Null},\mathcal{I}(\neg\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}))\\\
&=&\textsf{ite}(\mathcal{I}(\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\text{Null},\text{Null},\neg\mathcal{I}(\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}))\\\
&=&\textsf{ite}(\llbracket\phi_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\text{Null},\text{Null},\neg\llbracket\phi_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})})\\\
&=&\llbracket\neg\phi_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\end{array}$

∎

###### Lemma D.3.

Let $\mathcal{D}$ be a database over schema $\mathcal{S}$ and $xs$ be a tuple
list which formulates an expression $E$. Consider a symbolic database $\Gamma$
over $\mathcal{S}$ and a list of symbolic tuples $\mathcal{T}$ such that
$\llbracket E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$. For any
interpretation $\mathcal{I}$ such that
$\mathcal{I}(\Gamma)=\mathcal{D}\land\mathcal{I}(\mathcal{T})=xs$, evaluating
$E$ over the concrete database $\mathcal{I}(\Gamma)$ and the concrete tuple
list $\mathcal{I}(\mathcal{T})$ yields the value of $\mathcal{I}(\llbracket
E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$, i.e.,

$\mathcal{I}(\Gamma)=\mathcal{D}\land\mathcal{I}(\mathcal{T})=xs\Rightarrow\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$

###### Lemma D.4.

Suppose $\llbracket E\rrbracket_{\mathcal{D},xs}=v$, then
$\mathcal{I}(\Gamma)=\mathcal{D}\land\mathcal{I}(\mathcal{T})=xs\Rightarrow\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$ is true iff $\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=v$ and
$\mathcal{I}(\llbracket E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=v$.

###### Proof..

By structural induction on $E$.

  1. (1)

Base case: $E=a$.

$\llbracket
a\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\textsf{head}(\mathcal{T}).a$ by
Figure 22. $\llbracket
a\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=lookup(\textsf{head}(\mathcal{I}(\mathcal{T})),a)$
by Figure 17. Therefore,

$\begin{array}[]{rcl}\mathcal{I}(\llbracket
a\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\mathcal{I}(\textsf{head}(\mathcal{T}).a)=\mathcal{I}(lookup(\textsf{head}(\mathcal{T}),a))\\\
&=&lookup(\textsf{head}(\mathcal{I}(\mathcal{T})),a)=lookup(\textsf{head}(xs),a)\\\
&=&\llbracket
a\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\end{array}$

  2. (2)

Base case: $E=v$.

$\llbracket v\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=v$ by Figure 22.
$\llbracket v\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=v$ by
Figure 17. Therefore, $\mathcal{I}(\llbracket
v\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\mathcal{I}(v)=v=\llbracket
v\rrbracket_{\mathcal{D},xs}$.

  3. (3)

Inductive case: $E=E_{1}\diamond E_{2}$.

$\llbracket E_{1}\diamond
E_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\textsf{ite}(v_{1}=\text{Null}\lor
v_{2}=\text{Null},\text{Null},v_{1}\diamond v_{2})$ where $v_{1}=\llbracket
E_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$ and $v_{2}=\llbracket
E_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$ by Figure 22. $\llbracket
E_{1}\diamond
E_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\textsf{ite}(v_{1}^{\prime}=\text{Null}\lor
v_{2}^{\prime}=\text{Null},\text{Null},v_{1}^{\prime}\diamond v_{2}^{\prime})$
where $v_{1}^{\prime}=\llbracket
E_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$ and
$v_{2}^{\prime}=\llbracket
E_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$ by Figure 17.
By inductive hypothesis, we have $\llbracket
E_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
E_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$ and $\llbracket
E_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
E_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$. Also since
$\mathcal{I}(v_{1})=\mathcal{I}(\llbracket
E_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\llbracket
E_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=v_{1}^{\prime}$
and $\mathcal{I}(v_{2})=v_{2}^{\prime}$,

$\begin{array}[]{rcl}\mathcal{I}(\llbracket E_{1}\diamond
E_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\mathcal{I}(\textsf{ite}(v_{1}=\text{Null}\lor
v_{2}=\text{Null},\text{Null},v_{1}\diamond v_{2}))\\\
&=&\textsf{ite}(\mathcal{I}(v_{1})=\text{Null}\lor\mathcal{I}(v_{2})=\text{Null},\text{Null},\mathcal{I}(v_{1})\diamond\mathcal{I}(v_{2}))\\\
&=&\textsf{ite}(v_{1}^{\prime}=\text{Null}\lor
v_{2}^{\prime}=\text{Null},\text{Null},v_{1}^{\prime}\diamond
v_{2}^{\prime})\\\ &=&\llbracket E_{1}\diamond
E_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\\\ \end{array}$

  4. (4)

Inductive case: $E=\text{ITE}(\phi,E_{1},E_{2})$.

$\llbracket\text{ITE}(\phi,E_{1},E_{2})\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\textsf{ite}(\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\top,\llbracket
E_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}},\llbracket
E_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$ by Figure 22.
$\llbracket\text{ITE}(\phi,E_{1},$
$E_{2})\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\textsf{ite}(\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\top,\llbracket
E_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})},\llbracket
E_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})})$ by Figure 17.
By inductive hypothesis, we have
$\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$,
$\llbracket
E_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
E_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$ and $\llbracket
E_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
E_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$. Therefore,

$\begin{array}[]{rcl}\mathcal{I}(\llbracket\text{ITE}(\phi,E_{1},E_{2})\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\mathcal{I}(\textsf{ite}(\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\top,\llbracket
E_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}},\llbracket
E_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}))\\\
&=&\textsf{ite}(\mathcal{I}(\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\top,\mathcal{I}(\llbracket
E_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}),\mathcal{I}(\llbracket
E_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}))\\\
&=&\textsf{ite}(\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\top,\llbracket
E_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})},\llbracket
E_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})})\\\
&=&\llbracket\text{ITE}(\phi,E_{1},E_{2})\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\\\
\end{array}$

  5. (5)

Inductive case: $E=\text{Case}(\vec{\phi},\vec{E_{1}},E_{2})$.

$\llbracket\text{Case}(\vec{\phi},\vec{E_{1}},E_{2})\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\llbracket\text{ITE}(\phi_{1},E_{1}^{1},\text{ITE}(\ldots,\text{ITE}(\phi_{n},E_{1}^{n},E_{2})))\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$
where $E_{1}^{i}\in\vec{E_{1}}$ and $n=|\vec{\phi}|=|\vec{E}|$ by Figure 22.
$\llbracket\text{Case}(\vec{\phi},\vec{E_{1}},E_{2})\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\textsf{foldr}(\lambda
y.\lambda(\phi_{i},E_{1}^{i}).\llbracket\text{ite}(\phi_{i},E_{1}^{i},y)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})},$
$E_{2},reverse(zip(\vec{\phi},\vec{E_{1}})))$ by Figure 17. By inductive
hypothesis, we have
$\llbracket\phi_{i}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket\phi_{i}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$,
$\llbracket
E_{1}^{i}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
E_{1}^{i}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$ and $\llbracket
E_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
E_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$.

∎

###### Lemma D.5.

Let $\mathcal{D}$ be a database over schema $\mathcal{S}$ and $xs$ be a tuple
list which formulates an attribute $A$. Consider a symbolic database $\Gamma$
over $\mathcal{S}$ and a list of symbolic tuples $\mathcal{T}$ such that
$\llbracket A\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}$. For any
interpretation $\mathcal{I}$ such that
$\mathcal{I}(\Gamma)=\mathcal{D}\land\mathcal{I}(\mathcal{T})=xs$, evaluating
$A$ over the concrete database $\mathcal{I}(\Gamma)$ and the concrete tuple
list $\mathcal{I}(\mathcal{T})$ yields the value of $\mathcal{I}(\llbracket
A\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$, i.e.,

$\mathcal{I}(\Gamma)=\mathcal{D}\land\mathcal{I}(\mathcal{T})=xs\Rightarrow\llbracket
A\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
A\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$

###### Proof..

By structural induction on $A$.

  1. (1)

Inductive case: $A=\text{Cast}(\phi)$.

By the definition of the Cast function, we know
$\text{Cast}(\phi)=\text{Null}$ iff $\phi=\text{Null}$, $\text{Cast}(\phi)=1$
iff $\phi$ is true; otherwise it returns 0. Furthermore, by Lemma D.3, we know
$\mathcal{I}(\llbracket
A\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\mathcal{I}(\llbracket\text{Cast}(\phi)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\llbracket\text{Cast}(\phi)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\llbracket
v\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\llbracket
A\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$ where
$v\in\\{0,1\\}$ if $\phi\in\\{\top,\bot\\}$; and by Lemma D.2
$\mathcal{I}(\llbracket
A\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\mathcal{I}(\llbracket\text{Cast}(\text{Null})\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\llbracket\text{Cast}(\text{Null})\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\llbracket\text{Null}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\llbracket
A\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$ if
$\phi=\text{Null}$.

  2. (2)

Inductive case: $A=E$.

By Lemma D.3, we know $\mathcal{I}(\llbracket
A\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\mathcal{I}(\llbracket
E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\llbracket
A\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$.

  3. (3)

Inductive case: $A=\text{Count}(E)$.

$\llbracket\text{Count}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\textsf{ite}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T}),\text{Null},\Sigma_{t\in\mathcal{T}}\text{ite}(\text{Del}(t)\lor\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}=\text{Null},0,1))$ by Figure 22.
$\llbracket\text{Count}(E)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\textsf{ite}(\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})),\text{Null},\textsf{foldl}(+,0,\textsf{map}(xs,\lambda
y.$ $\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]}=\text{Null},0,1))))$ by Figure 17. By
Lemma D.3, we have $\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\\\
$$\mathcal{I}(\llbracket E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$. By
the definition of $\mathcal{I}$, $\mathcal{I}(\text{Del})(t)=\top$ for the
symbolic tuple $t\in\mathcal{T}\land t\not\in xs$; similarly
$\mathcal{I}(\text{Del})(t)=\bot$ for the symbolic tuple $t\in\mathcal{T}\land
t\in xs$.

$\begin{array}[]{rcl}\mathcal{I}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T}))&=&\mathcal{I}(\land_{t\in\mathcal{T}}(\neg\text{Del}(t)\to\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}=\text{Null}))\\\
&=&\land_{t\in\mathcal{I}(\mathcal{T})}(\neg\mathcal{I}(\text{Del})(t)\to\mathcal{I}(\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]})=\text{Null})\\\
&=&\land_{t\in\mathcal{I}(\mathcal{T})}(\neg\bot\to\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}([t])}=\text{Null})\\\
&=&\land_{t\in\mathcal{I}(\mathcal{T})}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}([t])}=\text{Null})\\\
&=&\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T}))\end{array}$

By the definition of foldl and map,
$\textsf{foldl}(+,0,\textsf{map}(xs,\lambda y.\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{D},[y]}=\text{Null},0,1)))=\\\
\Sigma_{x\in\mathcal{I}(\mathcal{T})}\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{D},[x]}=\text{Null},0,1)$.

$\begin{array}[]{rcl}\mathcal{I}(\llbracket\text{Count}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\mathcal{I}(\textsf{ite}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T}),\text{Null},\\\
&&\qquad\Sigma_{t\in\mathcal{T}}\text{ite}(\text{Del}(t)\lor\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}=\text{Null},0,1)))\\\
&=&\textsf{ite}(\mathcal{I}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T})),\text{Null},\\\
&&\qquad\mathcal{I}(\Sigma_{t\in\mathcal{T}}\text{ite}(\text{Del}(t)\lor\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}=\text{Null},0,1)))\\\
&=&\textsf{ite}(\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})),\text{Null},\\\
&&\qquad\Sigma_{t\in\mathcal{I}(\mathcal{T})}\text{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[t]}=\text{Null},0,1))\\\
&=&\textsf{ite}(\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})),\text{Null},\\\
&&\qquad\textsf{foldl}(+,0,\textsf{map}(\mathcal{I}(\mathcal{T}),\lambda
y.\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]}=\text{Null},0,1)))\\\
&=&\llbracket\text{Count}(E)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\end{array}$

  4. (4)

Inductive case: $A=\text{Sum}(E)$.

$\llbracket\text{Sum}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\textsf{ite}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T}),\text{Null},\Sigma_{t\in\mathcal{T}}\text{ite}(\text{Del}(t)\lor\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}=\text{Null},0,\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}))$ by Figure 22.
$\llbracket\text{Sum}(E)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\textsf{ite}(\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})),\text{Null},\textsf{foldl}(+,0,\textsf{map}(xs,\lambda
y.$ $\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]}=\text{Null},0,\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]}))))$ by Figure 17. By Lemma D.3, we have
$\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$. By the definition of
$\mathcal{I}$, we know
$\mathcal{I}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T}))=\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T}))$.
By the definition of foldl and map,
$\textsf{foldl}(+,0,\textsf{map}(xs,\lambda y.\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{D},[y]}=\text{Null},0,\llbracket
E\rrbracket_{\mathcal{D},[y]})))=\Sigma_{x\in\mathcal{I}(\mathcal{T})}\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{D},[x]}=\text{Null},0,\llbracket
E\rrbracket_{\mathcal{D},[x]})$.

$\begin{array}[]{rcl}\mathcal{I}(\llbracket\text{Sum}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\mathcal{I}(\textsf{ite}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T}),\text{Null},\\\
&&\qquad\Sigma_{t\in\mathcal{T}}\text{ite}(\text{Del}(t)\lor\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}=\text{Null},0,\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]})))\\\
&=&\textsf{ite}(\mathcal{I}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T})),\text{Null},\\\
&&\qquad\mathcal{I}(\Sigma_{t\in\mathcal{T}}\text{ite}(\text{Del}(t)\lor\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}=\text{Null},0,\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]})))\\\
&=&\textsf{ite}(\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})),\text{Null},\\\
&&\qquad\Sigma_{t\in\mathcal{I}(\mathcal{T})}\text{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[t]}=\text{Null},0,\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[t]}))\\\
&=&\textsf{ite}(\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})),\text{Null},\textsf{foldl}(+,0,\\\
&&\qquad\textsf{map}(\mathcal{I}(\mathcal{T}),\lambda
y.\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]}=\text{Null},0,\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]})))\\\
&=&\llbracket\text{Sum}(E)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\end{array}$

  5. (5)

Inductive case: $A=\text{Avg}(E)$. By the semantics of $\text{Avg}(E)$, we
have

$\begin{array}[]{rcl}\mathcal{I}(\llbracket\text{Avg}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\mathcal{I}(\llbracket\text{Sum}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})/\mathcal{I}(\llbracket\text{Count}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})\\\
&=&\llbracket\text{Sum}(E)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}/\llbracket\text{Count}(E)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\\\
&=&\llbracket\text{Avg}(E)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\end{array}$

  6. (6)

Inductive case: $A=\text{Min}(E)$.

$\llbracket\text{Min}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\textsf{ite}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T}),\text{Null},\text{min}_{t\in\mathcal{T}}\text{ite}(\text{Del}(t)\lor\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}=\text{Null},+\infty,\\\ $ $\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}))$ by Figure 22.
$\llbracket\text{Min}(E)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\textsf{ite}(\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})),\text{Null},\textsf{foldl}(\text{min},$
$+\infty,\textsf{map}(xs,\lambda y.$ $\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]}=\text{Null},+\infty,\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]}))))$ by Figure 17. By Lemma D.3, we have
$\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$. By the definition of
$\mathcal{I}$, we know
$\mathcal{I}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T}))=\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T}))$.
By the definition of foldl and map,
$\textsf{foldl}(\text{min},+\infty,\textsf{map}(xs,\lambda y.\textsf{ite}($
$\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]}=\text{Null},+\infty,\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]})))\\\ =\text{min}_{x\in
xs}(\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[x]}=\text{Null},+\infty,\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[x]}))$.

$\begin{array}[]{rcl}\mathcal{I}(\llbracket\text{Min}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\mathcal{I}(\textsf{ite}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T}),\text{Null},\\\
&&\qquad\text{min}_{t\in\mathcal{T}}\text{ite}(\text{Del}(t)\lor\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}=\text{Null},+\infty,\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]})))\\\
&=&\textsf{ite}(\mathcal{I}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T})),\text{Null},\\\
&&\qquad\mathcal{I}(\text{min}_{t\in\mathcal{T}}\text{ite}(\text{Del}(t)\lor\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}=\text{Null},+\infty,\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]})))\\\
&=&\textsf{ite}(\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})),\text{Null},\\\
&&\qquad\Sigma_{t\in\mathcal{I}(\mathcal{T})}\text{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[t]}=\text{Null},+\infty,\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}))\\\
&=&\textsf{ite}(\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})),\text{Null},\textsf{foldl}(\text{min},+\infty,\\\
&&\qquad\textsf{map}(\mathcal{I}(\mathcal{T}),\lambda
y.\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]}=\text{Null},+\infty,\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[y]})))\\\
&=&\llbracket\text{Min}(E)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\end{array}$

  7. (7)

Inductive case: $A=\text{Max}(E)$.

$\llbracket\text{Max}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\textsf{ite}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T}),\text{Null},\text{max}_{t\in\mathcal{T}}\text{ite}(\text{Del}(t)\lor\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}=\text{Null},-\infty,$ $\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}))$ by Figure 22.
$\llbracket\text{Max}(E)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\textsf{ite}(\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})),\text{Null},\textsf{foldl}(\text{max},$
$-\infty,\textsf{map}(xs,\lambda y.$ $\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]}=\text{Null},-\infty,\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]}))))$ by Figure 17. By Lemma D.3, we have
$\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\mathcal{I}(\llbracket
E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})$. By the definition of
$\mathcal{I}$, we know
$\mathcal{I}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T}))=\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T}))$.
By the definition of foldl and map,
$\textsf{foldl}(\text{max},-\infty,\textsf{map}(xs,\lambda y.\textsf{ite}($
$\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]}=\text{Null},-\infty,\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]})))=\text{max}_{x\in
xs}(\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[x]}=\text{Null},-\infty,\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[x]}))$.

$\begin{array}[]{rcl}\mathcal{I}(\llbracket\text{Max}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\mathcal{I}(\textsf{ite}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T}),\text{Null},\\\
&&\qquad\text{max}_{t\in\mathcal{T}}\text{ite}(\text{Del}(t)\lor\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}=\text{Null},-\infty,\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]})))\\\
&=&\textsf{ite}(\mathcal{I}(\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T})),\text{Null},\\\
&&\qquad\mathcal{I}(\text{max}_{t\in\mathcal{T}}\text{ite}(\text{Del}(t)\lor\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}=\text{Null},-\infty,\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]})))\\\
&=&\textsf{ite}(\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})),\text{Null},\\\
&&\qquad\Sigma_{t\in\mathcal{I}(\mathcal{T})}\text{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[t]}=\text{Null},-\infty,\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}))\\\
&=&\textsf{ite}(\text{AllNull}(E,\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})),\text{Null},\textsf{foldl}(\text{max},-\infty,\\\
&&\qquad\textsf{map}(\mathcal{I}(\mathcal{T}),\lambda
y.\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{I}(\Gamma),[y]}=\text{Null},-\infty,\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[y]})))\\\
&=&\llbracket\text{Max}(E)\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\end{array}$

  8. (8)

Inductive case: $A=A_{1}\diamond A_{2}$.

By the inductive hypothesis, we have $\mathcal{I}(\llbracket
A_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\llbracket
A_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$ and
$\mathcal{I}(\llbracket
A_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})=\llbracket
A_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$. Therefore,

$\begin{array}[]{rcl}\mathcal{I}(\llbracket A_{1}\diamond
A_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})&=&\mathcal{I}(\llbracket
A_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})\diamond\mathcal{I}(\llbracket
A_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}})\\\ &=&\llbracket
A_{1}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\diamond\llbracket
A_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\\\
&=&\llbracket A_{1}\diamond
A_{2}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}\end{array}$

∎

###### Proof of Theorem 4.7:.

Given two relations $R_{1}=[t_{1},\ldots,t_{n}]$ and
$R_{2}=[r_{1},\ldots,r_{m}]$, if the formula
$(\ref{eq:bag1})\land(\ref{eq:bag2})$ is valid, then $R_{1}$ is equal to
$R_{2}$ under bag semantics. If the formula
$(\ref{eq:list1})\land(\ref{eq:list2})$ is valid, then $R_{1}$ is equal to
$R_{2}$ under list semantics. ∎

###### Proof..

Let us prove this Theorem under bag and list semantics.

  1. (1)

Under bag semantics.

By the formula $(\ref{eq:bag1})$, we assume there exist $a$ non-deleted tuples
in $R_{1}$ and $R_{2}$ where $a\leq\text{min}\\{n,m\\}$. Let
$[x_{1},\ldots,x_{b}]$ be the distinct tuples of those non-deleted tuples in
$R_{1}$ or $R_{2}$. To ensure the formula $(\ref{eq:bag2})$ holds, for any
tuple $x_{i}$, it has the same multiplicity in $R_{1}$ and $R_{2}$ (i.e.,
$M(x_{i},R_{1})=M(x_{i},R_{2})$) where the function $M$ takes as input a non-
delete tuple and the symbolic table, and returns the multiplicity of the
tuple. Therefore, the sum of all distinct tuples’ multiplicity is equal to the
number of non-deleted tuples, i.e.,
$a=\Sigma_{i=1}^{b}M(x_{i},R_{1})=\Sigma_{i=1}^{b}M(x_{i},R_{2})$, and the
formula $(\ref{eq:bag2})$ holds for those non-deleted tuples.

Moreover, we know, for any deleted tuples $t_{i}\in R_{1}$ and $r_{i}\in
R_{2}$ where $\text{Del}(t_{i})=\text{Del}(r_{i})=\top$, their multiplicities
in $R_{1}$ and $R_{2}$ are always $0$ and, therefore, the formula
$(\ref{eq:bag2})$ holds for them.

Thus, Theorem 4.7 holds under the bag semantics.

  2. (2)

Under list semantics.

Let us discuss the value of $\text{min}\\{n,m\\}$ in three cases.

    1. (a)

If $n<m$, then $\text{min}\\{n,m\\}=n$ and $\text{Del}(r_{i})=\top$ for any
$n<i\leq m$ because of the formula $(\ref{eq:list1})$. Furthermore, as we know
$t_{i}=r_{i}$ for any $1\leq i\leq n$, then
$R_{1}=[t_{1},\ldots,t_{n}]=[r_{1},\ldots,r_{n}]=\textsf{append}([r_{1},\ldots,r_{n}],[r_{n+1},\ldots,r_{m}])=[r_{1},\ldots,r_{m}]=R_{2}$.

    2. (b)

If $n=m$, then, apparently, we know $\text{min}\\{n,m\\}=n=m$ and
$R_{1}=R_{2}$ by the formula $(\ref{eq:list2})$.

    3. (c)

If $n>m$, then $\text{min}\\{n,m\\}=m$ and $\text{Del}(t_{i})=\top$ for any
$m<i\leq n$ because of the formula $(\ref{eq:list1})$. Furthermore, as we know
$t_{i}=r_{i}$ for any $1\leq i\leq m$, then
$R_{2}=[r_{1},\ldots,r_{m}]=[t_{1},\ldots,t_{m}]=\textsf{append}([t_{1},\ldots,t_{m}],[t_{n+1},\ldots,t_{m}])=[t_{1},\ldots,t_{m}]=R_{1}$.

By the above cases, we can prove that Theorem 4.7 holds under the list
semantics.

Hence, Theorem 4.7 is proved by the aforementioned cases. ∎

###### Proof of Theorem 4.8:.

Given two queries $Q_{1},Q_{2}$ under schema $\mathcal{S}$, an integrity
constraint $\mathcal{C}$, a bound $N$, if
$\textsc{Verify}(Q_{1},Q_{2},\mathcal{S},\mathcal{C},N)$ returns $\top$, then
$Q_{1}\simeq_{\mathcal{S},\mathcal{C},N}Q_{2}$. Otherwise, if
$\textsc{Verify}(Q_{1},Q_{2},\mathcal{S},$ $\mathcal{C},N)$ returns a database
$\mathcal{D}$, then $\mathcal{D}::\mathcal{S}\land\llbracket
Q_{1}\rrbracket_{\mathcal{D}}\neq\llbracket Q_{2}\rrbracket_{\mathcal{D}}$. ∎

###### Proof..

Let us prove Theorem 4.8 in two cases.

  1. (1)

If $\textsc{Verify}(Q_{1},Q_{2},\mathcal{S},\mathcal{C},N)$ returns $\top$,
then we cannot find two symbolic relations $R_{1}$ and $R_{2}$ s.t. $R_{1}\neq
R_{2}$ by Theorem 4.7. Let $\mathcal{I}$ be an interpretation s.t.
$\mathcal{D}=\mathcal{I}(\Gamma)$. By the soundness of
$\textsc{BuildSymbolicDB}(\mathcal{S},N)$ (line 2) of Algorithm 1, we know
$\mathcal{D}::\mathcal{S}$ and $\forall R\in\mathcal{D}.|R|\leq N$ holds for
any database $\mathcal{D}$ instantiated from $\Gamma$. By Theorem 4.2, we know
$\mathcal{C}(\mathcal{D})$ holds for any database $\mathcal{D}$ instantiated
from $\Gamma$. Further, by Theorem 4.5 and 4.6, $\llbracket
Q\rrbracket_{\mathcal{I}(\Gamma)}=\llbracket
Q\rrbracket_{\mathcal{D}}=\mathcal{I}(R)$ where $R$ is a symbolic relation
from $\Phi_{R},R\leftarrow\textsc{EncodeQuey}(\mathcal{S},\Gamma,Q)$.
Therefore,
$R_{1}=R_{2}\Leftrightarrow\mathcal{I}(R_{1})=\mathcal{I}(R_{2})\Leftrightarrow\llbracket
Q_{1}\rrbracket_{\mathcal{D}}=\llbracket Q_{2}\rrbracket_{\mathcal{D}}$ where
$\mathcal{D}$ is instantiated from $\Gamma$, and
$Q_{1}\simeq_{\mathcal{S},\mathcal{C},N}Q_{2}$ holds.

  2. (2)

If $\textsc{Verify}(Q_{1},Q_{2},\mathcal{S},\mathcal{C},N)$ returns a database
$\mathcal{D}$, we know that there exists a database $\mathcal{D}$ s.t.
$\Phi=\Phi_{\mathcal{C}}\land\Phi_{R_{1}}\land\Phi_{R_{2}}\land\neg\textsc{Equal}(R_{1},R_{2})$.
By the soundness of $\text{BuildExample}(\mathcal{S},\text{Model}(\Phi))$,
$\mathcal{D}::\mathcal{S}$ is also true. Further,
$\Phi_{\mathcal{C}}\land\Phi_{R_{1}}\land\Phi_{R_{2}}\land\neg\textsc{Equal}(R_{1},R_{2})=\top\Rightarrow\neg\textsc{Equal}(R_{1},R_{2})=\top$
$\Leftrightarrow\textsc{Equal}(R_{1},R_{2})=\bot$. By Theorem 4.5 and 4.6,
there exists an $\mathcal{I}$ s.t. $\mathcal{I}(R)=\llbracket
Q\rrbracket_{\mathcal{I}(R)}=\llbracket Q\rrbracket_{\mathcal{D}}$; and, by
Theorem 4.7, $\textsc{Equal}(R_{1},R_{2})=\bot\Leftrightarrow\llbracket
Q_{1}\rrbracket_{\mathcal{I}(R_{1})}\neq\llbracket
Q_{2}\rrbracket_{\mathcal{I}(R_{2})}\Leftrightarrow\llbracket
Q_{1}\rrbracket_{\mathcal{D}}\neq\llbracket Q_{2}\rrbracket_{\mathcal{D}}$.

Hence, Theorem 4.8 is proved by the aforementioned cases. ∎