* Chu et al. (2017c) Shumo Chu, Konstantin Weitz, Alvin Cheung, and Dan Suciu. 2017c.  HoTTSQL: Proving query rewrites with univalent SQL semantics.  _ACM SIGPLAN Notices_ 52, 6 (2017), 510–524.  https://doi.org/10.1145/3062341.3062348
  * Clarke et al. (2004) Edmund Clarke, Daniel Kroening, and Flavio Lerda. 2004\.  A tool for checking ANSI-C programs. In _Tools and Algorithms for the Construction and Analysis of Systems: 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29-April 2, 2004. Proceedings 10_. Springer, 168–176.  https://doi.org/10.1007/978-3-540-24730-2_15
  * Coelho (2013) Fabien Coelho. 2013\.  DataFiller – generate random data from database schema.  https://www.cri.ensmp.fr/people/coelho/datafiller.html.
  * Cordeiro et al. (2018) Lucas Cordeiro, Pascal Kesseli, Daniel Kroening, Peter Schrammel, and Marek Trtik. 2018\.  JBMC: A bounded model checking tool for verifying Java bytecode. In _Computer Aided Verification: 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I_. Springer, 183–190.  https://doi.org/10.1007/978-3-319-96145-3_10
  * Cosette (2018) Cosette. 2018.  Cosette website.  https://cosette.cs.washington.edu/.
  * de Moura and Bjørner (2008) Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008.  Z3: An Efficient SMT Solver. In _Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)_ _(Lecture Notes in Computer Science, Vol. 4963)_. 337–340.  https://doi.org/10.1007/978-3-540-78800-3_24
  * Delaware et al. (2015) Benjamin Delaware, Clément Pit-Claudel, Jason Gross, and Adam Chlipala. 2015.  Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. In _Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL)_. ACM, 689–700.  https://doi.org/10.1145/2676726.2677006
  * Deutsch et al. (2005) Alin Deutsch, Monica Marcus, Liying Sui, Victor Vianu, and Dayou Zhou. 2005.  A Verifier for Interactive, Data-Driven Web Applications. In _Proceedings of the ACM SIGMOD International Conference on Management of Data_. 539–550.  https://doi.org/10.1145/1066157.1066219
  * Deutsch et al. (2007) Alin Deutsch, Liying Sui, and Victor Vianu. 2007.  Specification and verification of data-driven Web applications.  _J. Comput. Syst. Sci._ 73, 3 (2007), 442–474.  https://doi.org/10.1016/j.jcss.2006.10.006
  * Feser et al. (2020) John K. Feser, Sam Madden, Nan Tang, and Armando Solar-Lezama. 2020.  Deductive optimization of relational data storage.  _Proc. ACM Program. Lang._ 4, OOPSLA (2020), 170:1–170:30.  https://doi.org/10.1145/3428238
  * Gligoric and Majumdar (2013) Milos Gligoric and Rupak Majumdar. 2013.  Model checking database applications. In _Tools and Algorithms for the Construction and Analysis of Systems: 19th International Conference, TACAS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings 19_. Springer, 549–564.  https://doi.org/10.1007/978-3-642-36742-7_40
  * Graefe (1995) Goetz Graefe. 1995\.  The cascades framework for query optimization.  _IEEE Data Eng. Bull._ 18, 3 (1995), 19–29.
  * Green (2011) Todd J. Green. 2011\.  Containment of Conjunctive Queries on Annotated Relations.  _Theory Comput. Syst._ 49, 2 (2011), 429–459.  https://doi.org/10.1007/s00224-011-9327-6
  * Guagliardo and Libkin (2017) Paolo Guagliardo and Leonid Libkin. 2017.  A Formal Semantics of SQL Queries, Its Validation, and Applications.  _Proc. VLDB Endow._ 11, 1 (sep 2017), 27–39.  https://doi.org/10.14778/3151113.3151116
  * He et al. (2024) Yang He, Pinhan Zhao, Xinyu Wang, and Yuepeng Wang. 2024\.  Artifact Evaluation VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints.  https://doi.org/10.5281/zenodo.10795614
  * Lal et al. (2012) Akash Lal, Shaz Qadeer, and Shuvendu K Lahiri. 2012.  A solver for reachability modulo theories. In _Computer Aided Verification: 24th International Conference, CAV 2012, Berkeley, CA, USA, July 7-13, 2012 Proceedings 24_. Springer, 427–443.  https://doi.org/10.1007/978-3-642-31424-7_32
  * LeetCode (2023) LeetCode. 2023.  LeetCode website.  https://leetcode.com/.
  * Miao et al. (2019) Zhengjie Miao, Sudeepa Roy, and Jun Yang. 2019.  Explaining wrong queries using small examples. In _Proceedings of the 2019 International Conference on Management of Data (SIGMOD)_. 503–520.  https://doi.org/10.1145/3299869.3319866
  * Necula (2000) George C. Necula. 2000\.  Translation validation for an optimizing compiler. In _Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)_. ACM, 83–94.  https://doi.org/10.1145/349299.349314
  * Negri et al. (1991) Mauro Negri, Giuseppe Pelagatti, and Licia Sbattella. 1991\.  Formal semantics of SQL queries.  _ACM Transactions on Database Systems (TODS)_ 16, 3 (1991), 513–534.  https://doi.org/10.1145/111197.111212
  * Pnueli et al. (1998) Amir Pnueli, Michael Siegel, and Eli Singerman. 1998\.  Translation Validation. In _Proceedings of International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS)_ _(Lecture Notes in Computer Science, Vol. 1384)_. 151–166.  https://doi.org/10.1007/BFb0054170
  * Ricciotti and Cheney (2019) Wilmer Ricciotti and James Cheney. 2019.  Mixing set and bag semantics. In _Proceedings of the ACM SIGPLAN International Symposium on Database Programming Languages (DBPL)_. ACM, 70–73.  https://doi.org/10.1145/3315507.3330202
  * Ricciotti and Cheney (2022) Wilmer Ricciotti and James Cheney. 2022.  A Formalization of SQL with Nulls.  _J. Autom. Reason._ 66, 4 (2022), 989–1030.  https://doi.org/10.1007/s10817-022-09632-4
  * Seshadri et al. (1996) Praveen Seshadri, Hamid Pirahesh, and TY Cliff Leung. 1996\.  Complex query decorrelation. In _Proceedings of the Twelfth International Conference on Data Engineering_. IEEE, 450–458.  https://doi.org/10.1109/ICDE.1996.492194
  * Shah et al. (2011) Shetal Shah, S Sudarshan, Suhas Kajbaje, Sandeep Patidar, Bhanu Pratap Gupta, and Devang Vira. 2011\.  Generating test data for killing SQL mutants: A constraint-based approach. In _2011 IEEE 27th International Conference on Data Engineering_. IEEE, 1175–1186.  https://doi.org/10.1109/ICDE.2011.5767876
  * Sousa and Dillig (2016) Marcelo Sousa and Isil Dillig. 2016.  Cartesian hoare logic for verifying k-safety properties. In _Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)_. ACM, 57–69.  https://doi.org/10.1145/2908080.2908092
  * Stepp et al. (2011) Michael Stepp, Ross Tate, and Sorin Lerner. 2011.  Equality-Based Translation Validator for LLVM. In _Proceedings of the International Conference on Computer Aided Verification (CAV)_ _(Lecture Notes in Computer Science, Vol. 6806)_. 737–742.  https://doi.org/10.1007/978-3-642-22110-1_59
  * Torlak and Bodík (2014) Emina Torlak and Rastislav Bodík. 2014.  A lightweight symbolic virtual machine for solver-aided host languages. In _ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)_. 530–541.  https://doi.org/10.1145/2594291.2594340
  * Tuya et al. (2010) Javier Tuya, María José Suárez-Cabal, and Claudio De La Riva. 2010.  Full predicate coverage for testing SQL database queries.  _Software Testing, Verification and Reliability_ 20, 3 (2010), 237–288.  https://doi.org/10.1002/stvr.424
  * Veanes et al. (2010) Margus Veanes, Nikolai Tillmann, and Jonathan de Halleux. 2010\.  Qex: Symbolic SQL query explorer. In _International Conference on Logic for Programming Artificial Intelligence and Reasoning_. Springer, 425–446.  https://doi.org/10.1007/978-3-642-17511-4_24
  * Wang et al. (2018a) Chenglong Wang, Alvin Cheung, and Rastislav Bodík. 2018a.  Speeding up symbolic reasoning for relational queries.  _Proceedings of the ACM on Programming Languages_ 2, OOPSLA (2018), 1–25.  https://doi.org/10.1145/3276527
  * Wang et al. (2018b) Yuepeng Wang, Isil Dillig, Shuvendu K. Lahiri, and William R. Cook. 2018b.  Verifying Equivalence of Database-Driven Applications.  _Proc. ACM Program. Lang._ 2, POPL, Article 56 (2018), 29 pages.  https://doi.org/10.1145/3158144
  * Wang et al. (2019) Yuepeng Wang, James Dong, Rushi Shah, and Isil Dillig. 2019\.  Synthesizing database programs for schema refactoring. In _Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation_. 286–300.  https://doi.org/10.1145/3314221.3314588
  * Wang et al. (2020) Yuepeng Wang, Rushi Shah, Abby Criswell, Rong Pan, and Isil Dillig. 2020.  Data Migration using Datalog Program Synthesis.  _Proc. VLDB Endow._ 13, 7 (2020), 1006–1019.  https://doi.org/10.14778/3384345.3384350
  * Zaks and Pnueli (2008) Anna Zaks and Amir Pnueli. 2008.  CoVaC: Compiler Validation by Program Analysis of the Cross-Product. In _Proceedings of the International Symposium on Formal Methods (FM)_ _(Lecture Notes in Computer Science, Vol. 5014)_. 35–51.  https://doi.org/10.1007/978-3-540-68237-0_5
  * Zhou et al. (2019) Qi Zhou, Joy Arulraj, Shamkant Navathe, William Harris, and Dong Xu. 2019.  Automated verification of query equivalence using satisfiability modulo theories.  _Proceedings of the VLDB Endowment_ 12, 11 (2019), 1276–1288.  https://doi.org/10.14778/3342263.3342267
  * Zhou et al. (2022) Qi Zhou, Joy Arulraj, Shamkant B Navathe, William Harris, and Jinpeng Wu. 2022.  SPES: A Symbolic Approach to Proving Query Equivalence Under Bag Semantics. In _2022 IEEE 38th International Conference on Data Engineering (ICDE)_. IEEE, 2735–2748.  https://doi.org/10.1109/ICDE53745.2022.00250

##  Appendix A Semantics of Query Language

$\llbracket Q_{r}\rrbracket::\text{Database }\mathcal{D}\to\text{Relation}$

$\begin{array}[]{lcl}\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}})~{}\text{where}\\\
&&\quad\text{MinTuple}(\vec{E},b,xs)=\textsf{foldl}(\lambda x.\lambda
y.\textsf{ite}(\text{Cmp}(\vec{E},b,x,y),y,x),\textsf{head}(xs),xs),\\\
&&\quad\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,\\\
&&\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\quad\textsf{ite}(v(x_{1},E_{i})>v(x_{2},E_{i}),\bot,y)),\top,\vec{E}),\\\
&&\quad v(x,E)=\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{D},[x]}=\text{Null},-\infty,\llbracket
E\rrbracket_{\mathcal{D},[x]})\\\ \end{array}$

$\llbracket Q\rrbracket::\text{Database }\mathcal{D}\to\text{Relation}$

$\begin{array}[]{lcl}\llbracket R\rrbracket_{\mathcal{D}}&=&\mathcal{D}(R)\\\
\llbracket\Pi_{L}(Q)\rrbracket_{\mathcal{D}}&=&\textsf{ite}(\text{hasAgg(L)},[\llbracket
L\rrbracket_{\mathcal{D},\llbracket
Q\rrbracket_{\mathcal{D}}}],\textsf{map}(\llbracket
Q\rrbracket_{\mathcal{D}},\lambda x.\llbracket
L\rrbracket_{\mathcal{D},x}))\\\
\llbracket\sigma_{\phi}(Q)\rrbracket_{\mathcal{D}}&=&\textsf{filter}(\llbracket
Q\rrbracket_{\mathcal{D}},\lambda
x.\llbracket\phi\rrbracket_{\mathcal{D},[x]}=\top)\\\
\llbracket\rho_{R}{(Q)}\rrbracket_{\mathcal{D}}&=&\textsf{map}(\llbracket
Q\rrbracket_{\mathcal{D}},\lambda
x.\textsf{map}(x,\lambda(n,v).(\text{rename}(R,n),v)))\\\ \llbracket Q_{1}\cap
Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{filter}(\llbracket\text{Distinct}(Q_{1})\rrbracket_{\mathcal{D}},\lambda
x.x\in\llbracket Q_{2}\rrbracket_{\mathcal{D}})\\\ \llbracket Q_{1}\cup
Q_{2}\rrbracket_{\mathcal{D}}&=&\llbracket\text{Distinct}(Q_{1}\uplus
Q_{2})\rrbracket_{\mathcal{D}}\\\ \llbracket Q_{1}\setminus
Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{filter}(\llbracket\text{Distinct}(Q_{1})\rrbracket_{\mathcal{D}},\lambda
x.x\not\in\llbracket Q_{2}\rrbracket_{\mathcal{D}})\\\ \llbracket
Q_{1}\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}Q_{2}\rrbracket_{\mathcal{D}}&=&\llbracket
Q_{1}-(Q_{1}-Q_{2})\rrbracket_{\mathcal{D}}\\\ \llbracket Q_{1}\uplus
Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{append}(\llbracket
Q_{1}\rrbracket_{\mathcal{D}},\llbracket Q_{2}\rrbracket_{\mathcal{D}})\\\
\llbracket Q_{1}-Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{foldl}(\lambda
xs.\lambda x.\textsf{ite}(x\in xs,xs-x,xs),\llbracket
Q_{1}\rrbracket_{\mathcal{D}},\llbracket Q_{2}\rrbracket_{\mathcal{D}})\\\
\llbracket\text{Distinct}(Q)\rrbracket_{\mathcal{D}}&=&\textsf{foldr}(\lambda
x.\lambda xs.\textsf{cons}(x,\textsf{filter}(xs,\lambda y.x\neq
y)),[],\llbracket Q\rrbracket_{\mathcal{D}})\\\ \llbracket Q_{1}\times
Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{foldl}(\lambda xs.\lambda
x.\textsf{append}(xs,\textsf{map}(\llbracket
Q_{2}\rrbracket_{\mathcal{D}},\lambda y.\textsf{merge}(x,y))),[],\llbracket
Q_{1}\rrbracket_{\mathcal{D}})\\\ \llbracket
Q_{1}\bowtie_{\phi}Q_{2}\rrbracket_{\mathcal{D}}&=&\llbracket\sigma_{\phi}(Q_{1}\times
Q_{2})\rrbracket_{\mathcal{D}}\\\ \llbracket
Q_{1}\mathbin{\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{foldl}(\lambda
xs.\lambda
x.\textsf{append}(xs,\textsf{ite}(|v_{1}(x)|=0,v_{2}(x),v_{1}(x)),[],\llbracket
Q_{1}\rrbracket_{\mathcal{D}})\\\
&&\quad\text{where}~{}v_{1}(x)=\llbracket[x]\bowtie_{\phi}Q_{2}\rrbracket_{\mathcal{D}}~{}\text{and}~{}v_{2}(x)=[\textsf{merge}(x,T_{\text{Null}})]\\\
\llbracket
Q_{1}\mathbin{\bowtie\mkern-5.8mu\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}}_{\phi}Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{foldl}(\lambda
xs.\lambda
x.\textsf{append}(xs,\textsf{ite}(|v_{1}(x)|=0,v_{2}(x),v_{1}(x)),[],\llbracket
Q_{2}\rrbracket_{\mathcal{D}})\\\ &&\quad\text{where}~{}v_{1}(x)=\llbracket
Q_{1}\bowtie_{\phi}[x]\rrbracket_{\mathcal{D}}~{}\text{and}~{}v_{2}(x)=[\textsf{merge}(T_{\text{Null}},x)]\\\
\llbracket Q_{1}\mathbin{\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}}_{\phi}Q_{2}\rrbracket_{\mathcal{D}}&=&\textsf{append}(\llbracket
Q_{1}\mathbin{\rule[0.58554pt]{2.0pt}{0.6pt}\hbox
to0.0pt{\hss\rule[3.03111pt]{2.0pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q_{2}\rrbracket_{\mathcal{D}},\textsf{map}(v,\lambda
x.\textsf{merge}(T_{\text{Null}},x)))\\\
&&\quad\text{where}~{}v=\textsf{filter}(\llbracket
Q_{2}\rrbracket_{\mathcal{D}},\lambda y.|\llbracket
Q_{1}\bowtie_{\phi}[y]\rrbracket_{\mathcal{D}}|=0)\\\
\llbracket\text{GroupBy}(Q,\vec{E},L,\phi)\rrbracket_{\mathcal{D}}\\!\\!\\!\\!&=&\textsf{map}(\textsf{filter}(Gs,\lambda
xs.\llbracket\phi\rrbracket_{\mathcal{D},xs}=\top),\lambda xs.\llbracket
L\rrbracket_{\mathcal{D},xs})~{}\text{where}\\\ &&\quad
Gs=\textsf{map}(\text{Dedup}(Q,\vec{E}),\lambda y.\textsf{map}(\llbracket
Q\rrbracket_{\mathcal{D}},\lambda z.\text{Eval}(\vec{E},[z])=y)),\\\
&&\quad\text{Dedup}(Q,\vec{E})=\textsf{foldr}(\lambda x.\lambda
xs.\textsf{cons}(x,\textsf{filter}(xs,\lambda y.x\neq y)),[],\\\
&&\quad\qquad\qquad\qquad\qquad\qquad\textsf{map}(\llbracket
Q\rrbracket_{\mathcal{D}},\lambda z.\text{Eval}(\vec{E},[z]))),\\\
&&\quad\text{Eval}(\vec{E},xs)=\textsf{map}(\vec{E},\lambda e.\llbracket
e\rrbracket_{\mathcal{D},xs})\\\
\llbracket\text{With}(\vec{Q},\vec{R},Q)\rrbracket_{\mathcal{D}}&=&\llbracket
Q\rrbracket_{\mathcal{D}^{\prime}}~{}\text{where}~{}\mathcal{D}^{\prime}=\mathcal{D}[R_{i}\mapsto\llbracket
Q_{i}\rrbracket_{\mathcal{D}}~{}|~{}R_{i}\in\vec{R}]\\\ \end{array}$

Figure 16. Formal semantics for queries.

$\llbracket L\rrbracket::\text{Database
}\mathcal{D}\to\text{Relation}\to[(\text{AttributeName},\text{Value})]$

$\begin{array}[]{lcl}\llbracket
L\rrbracket_{\mathcal{D},xs}&=&\textsf{map}(L,\lambda y.\llbracket
y\rrbracket_{\mathcal{D},xs})\\\ \llbracket
id(A)\rrbracket_{\mathcal{D},xs}&=&[(\text{ToString}(A),\llbracket
A\rrbracket_{\mathcal{D},xs})]\\\
\llbracket\rho_{a}(A)\rrbracket_{\mathcal{D},xs}&=&[(a,\llbracket
A\rrbracket_{\mathcal{D},xs})]\\\ \llbracket
L_{1},L_{2}\rrbracket_{\mathcal{D},xs}&=&\textsf{map}(\textsf{append}(L_{1},L_{2}),\lambda
y.\llbracket y\rrbracket_{\mathcal{D},xs})\\\ \end{array}$

$\llbracket E\rrbracket::\text{Database
}\mathcal{D}\to\text{Relation}\to\text{Value}$

$\begin{array}[]{lcl}\llbracket
a\rrbracket_{\mathcal{D},xs}&=&\textsf{lookup}(\textsf{head}(xs),a)\\\
\llbracket v\rrbracket_{\mathcal{D},xs}&=&v\\\ \llbracket E_{1}\diamond
E_{2}\rrbracket_{\mathcal{D},xs}&=&\text{let}~{}v_{1}=\llbracket
E_{1}\rrbracket_{\mathcal{D},xs}~{}\text{and}~{}v_{2}=\llbracket
E_{2}\rrbracket_{\mathcal{D},xs}~{}\text{in}~{}\textsf{ite}(v_{1}=\text{Null}\lor
v_{2}=\text{Null},\text{Null},v_{1}\diamond v_{2})\\\
\llbracket\text{ITE}(\phi,E_{1},E_{2})\rrbracket_{\mathcal{D},xs}&=&\textsf{ite}(\llbracket\phi\rrbracket_{\mathcal{D},xs}=\top,\llbracket
E_{1}\rrbracket_{\mathcal{D},xs},\llbracket
E_{2}\rrbracket_{\mathcal{D},xs})\\\
\llbracket\text{Case}(\vec{\phi},\vec{E},E^{\prime})\rrbracket_{\mathcal{D},xs}&=&\textsf{foldr}(\lambda
y.\lambda(\phi_{i},E_{i}).\llbracket\text{{ite}}(\phi_{i},E_{i},y)\rrbracket_{\mathcal{D},xs},E^{\prime},\textsf{reverse}(zip(\vec{\phi},\vec{E})))~{}\text{where}~{}n=|\vec{\phi}|=|\vec{E}|\\\
\end{array}$

$\llbracket\mathcal{G}(E)\rrbracket::\text{Database
}\mathcal{D}\to\text{Relation}\to\text{Value}$

$\begin{array}[]{lcl}\llbracket\text{Count}(E)\rrbracket_{\mathcal{D},xs}&=&\textsf{ite}(\text{AllNull}(E,\mathcal{D},xs),\text{Null},\textsf{foldl}(+,0,\textsf{map}(xs,\lambda
y.\textsf{ite}(\llbracket E\rrbracket_{\mathcal{D},[y]}=\text{Null},0,1)))\\\
&&\quad\text{where}~{}\text{AllNull}(E,\mathcal{D},xs)=\land_{x\in
xs}\llbracket E\rrbracket_{\mathcal{D},[x]}=\text{Null}\\\
\llbracket\text{Sum}(E)\rrbracket_{\mathcal{D},xs}&=&\textsf{ite}(\text{AllNull}(E,\mathcal{D},xs),\text{Null},\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]})))\\\
\llbracket\text{Avg}(E)\rrbracket_{\mathcal{D},xs}&=&\llbracket\text{Sum}(E)\rrbracket_{\mathcal{D},xs}/\llbracket\text{Count}(E)\rrbracket_{\mathcal{D},xs}\\\
\llbracket\text{Min}(E)\rrbracket_{\mathcal{D},xs}&=&\textsf{ite}(\text{AllNull}(E,\mathcal{D},xs),\text{Null},\textsf{foldl}(\text{min},+\infty,\textsf{map}(xs,\lambda
y.\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{D},[y]}=\text{Null},+\infty,\llbracket
E\rrbracket_{\mathcal{D},[y]}))))\\\
\llbracket\text{Max}(E)\rrbracket_{\mathcal{D},xs}&=&\textsf{ite}(\text{AllNull}(E,\mathcal{D},xs)\text{Null},\textsf{foldl}(\text{max},-\infty,\textsf{map}(xs,\lambda
y.\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{D},[y]}=\text{Null},-\infty,\llbracket
E\rrbracket_{\mathcal{D},[y]}))))\\\ \end{array}$

$\llbracket\phi\rrbracket::\text{Database
}\mathcal{D}\to\text{Relation}\to\text{Bool}\cup{\text{Null}}$

$\begin{array}[]{lcl}\llbracket\top\rrbracket_{\mathcal{D},xs}&=&\top\\\
\llbracket\bot\rrbracket_{\mathcal{D},xs}&=&\bot\\\
\llbracket\text{Null}\rrbracket_{\mathcal{D},xs}&=&\text{Null}\\\ \llbracket
A_{1}\odot A_{2}\rrbracket_{\mathcal{D},xs}&=&\text{let}~{}v_{1}=\llbracket
A_{1}\rrbracket_{\mathcal{D},xs},v_{2}=\llbracket
A_{2}\rrbracket_{\mathcal{D},xs}~{}\text{in}~{}\textsf{ite}(v_{1}=\text{Null}\lor
v_{2}=\text{Null},\bot,v_{1}\odot v_{2})\\\
\llbracket\text{IsNull}(E)\rrbracket_{\mathcal{D},xs}&=&\textsf{ite}(\llbracket
E\rrbracket_{\mathcal{D},xs}=\text{Null},\top,\bot)\\\
\llbracket\vec{E}\in\vec{v}\rrbracket_{\mathcal{D},xs}&=&\lor_{i=1}^{n}\land_{j=1}^{m}\llbracket
E_{j}\rrbracket_{\mathcal{D},xs}=\llbracket
v_{i,j}\rrbracket_{\mathcal{D},xs}~{}\text{where}~{}n=|\vec{v}|~{}\text{and}~{}m=|\vec{E}|=|\vec{v}_{i}|\\\
\llbracket\vec{E}\in Q\rrbracket_{\mathcal{D},xs}&=&\textsf{foldl}(\lambda
ys.\lambda y.ys\lor\llbracket\vec{E}\in
y\rrbracket_{\mathcal{D},xs},\bot,\llbracket Q\rrbracket_{\mathcal{D}})\\\
\llbracket\phi_{1}\land\phi_{2}\rrbracket_{\mathcal{D},xs}&=&\text{let}~{}v_{1}=\llbracket
E_{1}\rrbracket_{\mathcal{D},xs}~{}\text{and}~{}v_{2}=\llbracket
E_{2}\rrbracket_{\mathcal{D},xs}~{}\text{in}{}\\\
&&\quad\textsf{ite}((v_{1}=v_{2}=\text{Null})\lor(v_{1}=\text{Null}\land
v_{2}=\top)\lor(v_{1}=\top\land v_{2}=\text{Null}),\text{Null},v_{1}=\top\land
v_{2}=\top)\\\
\llbracket\phi_{1}\lor\phi_{2}\rrbracket_{\mathcal{D},xs}&=&\text{let}~{}v_{1}=\llbracket
E_{1}\rrbracket_{\mathcal{D},xs}~{}\text{and}~{}v_{2}=\llbracket
E_{2}\rrbracket_{\mathcal{D},xs}~{}\text{in}{}\\\
&&\quad\textsf{ite}((v_{1}=v_{2}=\text{Null})\lor(v_{1}=\text{Null}\land
v_{2}=\top)\lor(v_{1}=\top\land v_{2}=\text{Null}),\text{Null},v_{1}=\top\lor
v_{2}=\top)\\\
\llbracket\neg\phi\rrbracket_{\mathcal{D},xs}&=&\text{let}~{}v=\llbracket\phi\rrbracket_{\mathcal{D},xs}~{}\text{in}~{}\textsf{ite}(v=\text{Null},\text{Null},\neg
v)\\\ \end{array}$

Figure 17. Formal semantics for expressions and predicates.

##  Appendix B Encoding of SQL Queries

$\scriptsize\begin{array}[]{c}\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}R\in\textsf{Dom}(\Gamma)\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash
R\leadsto\top}&\\!\\!\\!\\!\\!\\!\textrm{(E-Rel)}\end{array}\mkern-2.0mu\par\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q\hookrightarrow[t_{1},\ldots,t_{n}]\quad\mathcal{S},\Gamma\vdash
Q\leadsto\Phi_{1}\\\
\Gamma\vdash\rho_{X}(Q)\hookrightarrow[t_{1}^{\prime},\ldots,t_{n}^{\prime}]\quad\Phi_{2}=\land_{i=1}^{n}t_{i}^{\prime}=t_{i}\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash\rho_{X}(Q)\leadsto\Phi_{1}\land\Phi_{2}}&\\!\\!\\!\\!\\!\\!\textrm{(E-Rename)}\end{array}\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\neg\text{hasAgg}(L)\quad\mathcal{S},\Gamma\vdash
Q\leadsto\Phi_{1}\quad\par\Gamma\vdash
Q\hookrightarrow[t_{1},\ldots,t_{n}]\quad\par\mathcal{S}\vdash\Pi_{L}(Q):[a_{1}^{\prime},\ldots,a_{l}^{\prime}]\quad\Gamma\vdash\Pi_{L}(Q)\hookrightarrow[t_{1}^{\prime},\ldots,t_{n}^{\prime}]\\\
\Phi_{2}=\land_{i=1}^{n}(\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}))\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash\Pi_{L}(Q)\leadsto\Phi_{1}\land\Phi_{2}}&\\!\\!\\!\\!\\!\\!\textrm{(E-Proj)}\end{array}\par\par\par\par\par\par\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\text{hasAgg}(L)\quad\mathcal{S},\Gamma\vdash
Q\leadsto\Phi_{1}\quad\Gamma\vdash
Q\hookrightarrow[t_{1},\ldots,t_{n}]\quad\par\mathcal{S}\vdash\Pi_{L}(Q):[a_{1}^{\prime},\ldots,a_{l}^{\prime}]\quad\Gamma\vdash\Pi_{L}(Q)\hookrightarrow[t_{1}^{\prime}]\\\
\Phi_{2}=\land_{j=1}^{l}\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{1}^{\prime}]}=\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{S},\Gamma,\vec{t}}\land{\neg\text{Del}(t_{1}^{\prime})}\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash\Pi_{L}(Q)\leadsto\Phi_{1}\land\Phi_{2}}&\\!\\!\\!\\!\\!\\!\textrm{(E-Agg)}\end{array}\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q\hookrightarrow[t_{1},\ldots,t_{n}]\quad\Gamma\vdash\sigma_{\phi}(Q)\hookrightarrow[t_{1}^{\prime},\ldots,t_{n}^{\prime}]\quad\mathcal{S},\Gamma\vdash
Q\leadsto\Phi_{1}\\\
\Phi_{2}=\land_{i=1}^{n}((\neg\text{Del}(t_{i})\land\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}=\top)\to
t_{i}^{\prime}=t_{i}\land(\text{Del}(t_{i})\lor\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}\neq\top)\to\text{Del}(t_{i}^{\prime}))\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash\sigma_{\phi}(Q)\leadsto\Phi_{1}\land\Phi_{2}}&\\!\\!\\!\\!\\!\\!\textrm{(E-Filter)}\end{array}\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{l}\mathcal{S}\vdash
Q_{1}:[a_{1},\ldots,a_{p}]\quad\Gamma\vdash
Q_{1}\hookrightarrow[t_{1},\ldots,t_{n}]\quad\mathcal{S},\Gamma\vdash
Q_{1}\leadsto\Phi_{1}\\\ \mathcal{S}\vdash
Q_{2}:[a_{1}^{\prime},\ldots,a_{q}^{\prime}]\quad\Gamma\vdash
Q_{2}\hookrightarrow[t_{1}^{\prime},\ldots,t_{m}^{\prime}]\quad\mathcal{S},\Gamma\vdash
Q_{2}\leadsto\Phi_{2}\quad\par\Gamma\vdash Q_{1}\times
Q_{2}\hookrightarrow[t_{1,1}^{\prime\prime},\ldots,t_{nm}^{\prime\prime}]\\\
\Phi=\land_{i=1}^{n}\land_{j=1}^{m}(\neg\text{Del}(t_{i})\land\neg\text{Del}(t_{j}^{\prime}))\to\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}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{i,j}^{\prime\prime}]}=\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{j}^{\prime}]}\land\\\
\qquad(\text{Del}(t_{i})\lor\text{Del}(t_{j}^{\prime}))\to\text{Del}(t_{i,j}^{\prime\prime})\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash Q_{1}\times
Q_{2}\leadsto\Phi_{1}\land\Phi_{2}\land\Phi_{3}}&\\!\\!\\!\\!\\!\\!\textrm{(E-Prod)}\end{array}\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{l}\mathcal{S},\Gamma\vdash\sigma_{\phi}(Q_{1}\times
Q_{2})\leadsto\Phi\\\ \end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash
Q_{1}\bowtie_{\phi}Q_{2}\leadsto\Phi}&\\!\\!\\!\\!\\!\\!\textrm{(E-IJoin)}\end{array}\par\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\mathcal{S}\vdash
Q_{1}:[a_{1},\ldots,a_{p}]\quad\Gamma\vdash
Q_{1}\hookrightarrow[t_{1},\ldots,t_{n}]\quad\mathcal{S}\vdash
Q_{2}:[a_{1}^{\prime},\ldots,a_{q}^{\prime}]\quad\Gamma\vdash
Q_{2}\hookrightarrow[t_{1}^{\prime},\ldots,t_{m}^{\prime}]\\\
\mathcal{S},\Gamma\vdash
Q_{1}\bowtie_{\phi}Q_{2}\leadsto\Phi_{1}\quad\Gamma\vdash
Q_{1}\mathbin{\rule[0.51234pt]{1.75pt}{0.6pt}\hbox
to0.0pt{\hss\rule[2.65222pt]{1.75pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q_{2}\hookrightarrow[t_{1,1}^{\prime\prime},\ldots,t_{n,m}^{\prime\prime},t_{1,m+1}^{\prime\prime},\ldots,t_{n,m+1}^{\prime\prime}]\\\
\Phi_{2}=\land_{i=1}^{n}(\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}]}=\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}))\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash
Q_{1}\mathbin{\rule[0.51234pt]{1.75pt}{0.6pt}\hbox
to0.0pt{\hss\rule[2.65222pt]{1.75pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q_{2}\leadsto\Phi_{1}\land\Phi_{2}}&\\!\\!\\!\\!\\!\\!\textrm{(E-LJoin)}\end{array}\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\mathcal{S}\vdash
Q_{1}:[a_{1},\ldots,a_{p}]\quad\Gamma\vdash
Q_{1}\hookrightarrow[t_{1},\ldots,t_{n}]\quad\mathcal{S}\vdash
Q_{2}:[a_{1}^{\prime},\ldots,a_{q}^{\prime}]\quad\Gamma\vdash
Q_{2}\hookrightarrow[t_{1}^{\prime},\ldots,t_{m}^{\prime}]\\\
\mathcal{S},\Gamma\vdash
Q_{1}\bowtie_{\phi}Q_{2}\leadsto\Phi_{1}\quad\Gamma\vdash
Q_{1}\mathbin{\bowtie\mkern-5.8mu\rule[0.51234pt]{1.75pt}{0.6pt}\hbox
to0.0pt{\hss\rule[2.65222pt]{1.75pt}{0.6pt}}}_{\phi}Q_{2}\hookrightarrow[t_{1,1}^{\prime\prime},\ldots,t_{n,m}^{\prime\prime},t_{n+1,1}^{\prime\prime},\ldots,t_{n+1,m}^{\prime\prime}]\\\
\Phi_{2}=\land_{j=1}^{m}(\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}]}\land(\neg\text{Del}(t_{j}^{\prime})\land\land_{i=1}^{n}\text{Del}(t_{ij}^{\prime\prime})\leftrightarrow\neg\text{Del}(t_{n+1,j}^{\prime\prime})))\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash
Q_{1}\mathbin{\bowtie\mkern-5.8mu\rule[0.51234pt]{1.75pt}{0.6pt}\hbox
to0.0pt{\hss\rule[2.65222pt]{1.75pt}{0.6pt}}}_{\phi}Q_{2}\leadsto\Phi_{1}\land\Phi_{2}}&\\!\\!\\!\\!\\!\\!\textrm{(E-RJoin)}\end{array}\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\mathcal{S}\vdash
Q_{1}:[a_{1},\ldots,a_{p}]\quad\Gamma\vdash
Q_{1}\hookrightarrow[t_{1},\ldots,t_{n}]\quad\mathcal{S}\vdash
Q_{2}:[a_{1}^{\prime},\ldots,a_{q}^{\prime}]\quad\Gamma\vdash
Q_{2}\hookrightarrow[t_{1}^{\prime},\ldots,t_{m}^{\prime}]\\\
\mathcal{S},\Gamma\vdash Q_{1}\mathbin{\rule[0.51234pt]{1.75pt}{0.6pt}\hbox
to0.0pt{\hss\rule[2.65222pt]{1.75pt}{0.6pt}}\mkern-5.8mu\bowtie}_{\phi}Q_{2}\leadsto\Phi\quad\Gamma\vdash
Q_{1}\mathbin{\rule[0.51234pt]{1.75pt}{0.6pt}\hbox
to0.0pt{\hss\rule[2.65222pt]{1.75pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.51234pt]{1.75pt}{0.6pt}\hbox
to0.0pt{\hss\rule[2.65222pt]{1.75pt}{0.6pt}}}_{\phi}Q_{2}\hookrightarrow[t_{1,1}^{\prime\prime},\ldots,t_{n,m}^{\prime\prime},t_{n+1,1}^{\prime\prime},\ldots,t_{n+1,m}^{\prime\prime},t_{1,m+1}^{\prime\prime},\ldots,t_{n,m+1}^{\prime\prime}]\\\
\Phi_{1}=\land_{j=1}^{m}(\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_{ij}^{\prime\prime})\leftrightarrow\neg\text{Del}(t_{n+1,j}^{\prime\prime})))\\\
\end{array}}{\vphantom{,}\Gamma\vdash
Q_{1}\mathbin{\rule[0.51234pt]{1.75pt}{0.6pt}\hbox
to0.0pt{\hss\rule[2.65222pt]{1.75pt}{0.6pt}}\mkern-5.8mu\bowtie\mkern-5.8mu\rule[0.51234pt]{1.75pt}{0.6pt}\hbox
to0.0pt{\hss\rule[2.65222pt]{1.75pt}{0.6pt}}}_{\phi}Q_{2}\leadsto\Phi\land\Phi_{1}}&\\!\\!\\!\\!\\!\\!\textrm{(E-FJoin)}\end{array}\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q\hookrightarrow[t_{1},\ldots,t_{n}]\quad\mathcal{S},\Gamma\vdash
Q\leadsto\Phi_{1}\quad\Gamma\vdash\text{GroupBy}(Q,\vec{E},\phi)\hookrightarrow[t_{1}^{\prime},\ldots,t_{n}^{\prime}]\\\
\Phi_{2}=\land_{i=1}^{n}(\sum_{j=1}^{i}\text{If}(g(t_{i},j),1,0)=\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_{j},j)\land\llbracket\vec{E}\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}=\llbracket\vec{E}\rrbracket_{\mathcal{S},\Gamma,[t_{j}]}))\\\
\Phi_{3}=\land_{i=1}^{n}((g(t_{i},i)\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\\\ \qquad(\neg
g(t_{i},i)\lor\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,g^{-1}(i)}\neq\top\to\text{Del}(t_{i}^{\prime})))\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash\text{GroupBy}(Q,\vec{E},[a_{1}^{\prime},...,a_{l}^{\prime}],\phi)\leadsto\Phi_{1}\land\Phi_{2}\land\Phi_{3}}&\\!\\!\\!\\!\\!\\!\textrm{(E-GroupBy)}\end{array}\par\mkern-2.0mu\\\
\\\ \end{array}$ Figure 18.  Symbolic encoding of SQL queries. The
$\text{Del}(t)$ function represents whether a symbolic tuple $t$ is deleted.
The $g(t,j)$ is an uninterpreted function determining whether the tuple $t$
belongs to the group $j$; and $g^{-1}(j)$ is a reversible function of $g$
which returns the tuples $\vec{t}$ belonging to the group $j$.

Figure 18 and 19 present symbolic encoding for SQL queries in VeriEQL.
Specifically, Figure 18 mainly focuses on formulating JOIN, GROUP BY and ORDER
BY while the set operations are fully encoded in Figure 19. Among these
encoding rules, most of which are straightforward to understand, there are two
interesting operations (i.e., GROUP BY and EXCEPT ALL) on which we further
elaborate.

We decompose GROUP BY into the grouping and reducing procedures. While
grouping, our top priority focuses on the partition over a symbolic table
based on the evaluation of the metrics $\vec{E}$. The tuples with the same
$\vec{E}$ values will be partitioned into a group. Furthermore, a tuple
$t_{i}$ cannot appear in the groups with greater indices, i.e., $\exists
j.1\leq j\leq i\to t_{i}\in G_{j}$. In Figure 20(b), for instance, $t_{1}$ and
$t_{3}$ are partitioned into $G_{1}$ since they share the same grouping
expressions, whereas $t_{2}$ solely constructs $G_{2}$. In the reducing
process, we exploit those groups and their shared information to determine the
existence of new tuples $[t_{1}^{\prime},t_{2}^{\prime},t_{3}^{\prime}]$ and
to compute projected expressions $L$. For instance, $t_{1}^{\prime}$ and
$t_{2}^{\prime}$ exist because $G_{1}$ and $G_{2}$ have at least a non-deleted
tuple, while $t_{3}^{\prime}$ is deleted because no tuple is categorized under
this group $G_{3}$.

$\scriptsize\begin{array}[]{c}\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q\hookrightarrow[t_{1},\ldots,t_{n}]\quad\mathcal{S},\Gamma\vdash
Q\leadsto\Phi_{1}\quad\Gamma\vdash\text{OrderBy}(Q,\vec{E},b)\hookrightarrow[t_{1}^{\prime},\ldots,t_{n}^{\prime}]\\\
\text{fresh }t^{\prime\prime}_{i}\quad 1\leq i\leq
n\quad\Phi_{2}=\text{moveDelToEnd}(\vec{t},\vec{t}^{\prime\prime})\quad\Phi_{3}=\land_{i=1}^{n}t_{i}^{\prime}=t_{\text{find}(i,\vec{E},b)}^{\prime\prime}\par\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash\text{OrderBy}(Q,\vec{E},b)\leadsto\Phi_{1}\land\Phi_{2}\land\Phi_{3}}&\\!\\!\\!\\!\\!\\!\textrm{(E-OrderBy)}\end{array}\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{l}\Gamma\vdash
Q\hookrightarrow[t_{1},\ldots,t_{n}]\quad\mathcal{S},\Gamma\vdash
Q\hookrightarrow\Phi_{1}\quad\Gamma\vdash\text{Distinct}(Q)\hookrightarrow[t_{1}^{\prime},\ldots,t_{n}^{\prime}]\quad\Phi_{2}=\text{Dedup}(\vec{t^{\prime}},\vec{t})\par\par\par\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash\text{Distinct}(Q)\leadsto\Phi_{1}\land\Phi_{2}}&\\!\\!\\!\\!\\!\\!\textrm{(E-Dist)}\end{array}\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{l}\mathcal{S},\Gamma\vdash\text{Distinct}(Q_{1}\uplus
Q_{2})\leadsto\Phi\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash Q_{1}\cup
Q_{2}\leadsto\Phi}&\\!\\!\\!\\!\\!\\!\textrm{(E-Union)}\end{array}\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash
Q_{1}\hookrightarrow[t_{1},\ldots,t_{n}]\quad\mathcal{S},\Gamma\vdash
Q_{1}\leadsto\Phi_{1}\quad\Gamma\vdash
Q_{2}\hookrightarrow[t_{1}^{\prime},\ldots,t_{m}^{\prime}]\quad\mathcal{S},\Gamma\vdash
Q_{2}\leadsto\Phi_{2}\\\ \Gamma\vdash Q_{1}\cup
Q_{2}\hookrightarrow[t_{1}^{\prime\prime},\ldots,t_{n+m}^{\prime\prime}]\quad\Phi_{3}=\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}\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash Q_{1}\uplus
Q_{2}\leadsto\Phi_{1}\land\Phi_{2}\land\Phi_{3}}&\\!\\!\\!\\!\\!\\!\textrm{(E-UnionAll)}\end{array}\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash\text{Distinct}(Q_{1})\hookrightarrow[t_{1},\ldots,t_{n}]\quad\mathcal{S},\Gamma\vdash\text{Distinct}(Q_{1})\leadsto\Phi_{1}\quad\Gamma\vdash
Q_{2}\hookrightarrow[t_{1}^{\prime},\ldots,t_{m}^{\prime}]\quad\mathcal{S},\Gamma\vdash
Q_{2}\leadsto\Phi_{2}\\\ \Gamma\vdash Q_{1}\cap
Q_{2}\hookrightarrow[t_{1}^{\prime\prime},\ldots,t_{n}^{\prime\prime}]\quad\Phi_{3}=\land_{i=1}^{n}(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}))\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash Q_{1}\cap
Q_{2}\leadsto\Phi_{1}\land\Phi_{2}\land\Phi_{3}}&\\!\\!\\!\\!\\!\\!\textrm{(E-Intx)}\end{array}\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{l}\mathcal{S},\Gamma\vdash
Q_{1}-(Q_{1}-Q_{2})\leadsto\Phi\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash
Q_{1}\mathrel{\reflectbox{\rotatebox[origin={c}]{180.0}{$\uplus$}}}Q_{2}\leadsto\Phi}&\\!\\!\\!\\!\\!\\!\textrm{(E-IntxAll)}\end{array}\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{c}\Gamma\vdash\text{Distinct}(Q_{1})\hookrightarrow[t_{1},\ldots,t_{n}]\quad\mathcal{S},\Gamma\vdash\text{Distinct}(Q_{1})\leadsto\Phi_{1}\\\
\Gamma\vdash
Q_{2}\hookrightarrow[t_{1}^{\prime},\ldots,t_{m}^{\prime}]\quad\mathcal{S},\Gamma\vdash
Q_{2}\leadsto\Phi_{2}\\\ \Gamma\vdash Q_{1}\setminus
Q_{2}\hookrightarrow[t_{1}^{\prime\prime},\ldots,t_{n}^{\prime\prime}]\quad\Phi_{3}=\land_{i=1}^{n}(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}))\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash
Q_{1}\setminus
Q_{2}\leadsto\Phi_{1}\land\Phi_{2}\land\Phi_{3}}&\\!\\!\\!\\!\\!\\!\textrm{(E-Ex)}\end{array}\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{l}\Gamma\vdash
Q_{1}\hookrightarrow[t_{1},\ldots,t_{n}]\quad\Gamma\vdash
Q_{2}\hookrightarrow[t_{1}^{\prime},\ldots,t_{m}^{\prime}]\quad\mathcal{S},\Gamma\vdash
Q_{1}\leadsto\Phi_{1}\quad\mathcal{S},\Gamma\vdash Q_{2}\leadsto\Phi_{2}\\\
\mathcal{S}\vdash Q:\mathcal{A}\quad\Gamma\vdash
Q_{1}-Q_{2}\hookrightarrow[t_{1}^{\prime\prime},\ldots,t_{n}^{\prime\prime}]\\\
\Phi_{3}=\texttt{Paired}(1,1)\leftrightarrow\texttt{Eq}(t_{1},t_{1}^{\prime},\mathcal{A})\\\
\Phi_{4}=\land_{j=2}^{m}\texttt{Paired}(1,j)\leftrightarrow(\texttt{Eq}(t_{1},t_{j}^{\prime},\mathcal{A})\land\land_{k=1}^{j-1}\neg\texttt{Paired}(1,k))\\\
\Phi_{5}=\land_{i=2}^{n}\texttt{Paired}(i,1)\leftrightarrow(\texttt{Eq}(t_{i},t_{1}^{\prime},\mathcal{A})\land\land_{k=1}^{i-1}\neg\texttt{Paired}(k,1))\\\
\Phi_{6}=\land_{i=2}^{n}\land_{j=2}^{m}\texttt{Paired}(i,j)=\texttt{Eq}(t_{i},t_{j},\mathcal{A})\land\land_{k=1}^{i-1}\neg\texttt{Paired}(k,j)\land\land_{k=1}^{j-1}\neg\texttt{Paired}(i,k)\\\
\Phi_{7}=\land_{i=1}^{n}(\neg\text{Del}(t_{i})\land\land_{j=1}^{m}\neg\texttt{Paired}(i,j)\to
t_{i}^{\prime\prime}=t_{i}\land\text{Del}(t_{i})\lor\lor_{j=1}^{m}\texttt{Paired}(i,j)\to\text{Del}(t_{i}^{\prime\prime}))\par\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash
Q_{1}-Q_{2}\leadsto\Phi_{1}\land\Phi_{2}\land\Phi_{3}\land\Phi_{4}\land\Phi_{5}\land\Phi_{6}\land\Phi_{7}}&\\!\\!\\!\\!\\!\\!\textrm{(E-ExAll)}\end{array}\mkern-2.0mu\\\
\\\
\mkern-2.0mu\begin{array}[]{ll}\displaystyle\frac{\begin{array}[]{l}\mathcal{S}\vdash
Q:\mathcal{A}_{i}\quad\Gamma\vdash
Q\hookrightarrow\mathcal{T}_{i}\quad\mathcal{S},\Gamma\vdash
Q_{i}\leadsto\Phi_{i}\quad 1\leq i\leq n\quad n=|\vec{Q}|\\\
\mathcal{S}[R_{1}\mapsto\mathcal{A}_{1},\ldots,R_{n}\mapsto\mathcal{A}_{n}],\Gamma[R_{1}\mapsto\mathcal{T}_{1},\ldots,R_{n}\mapsto\mathcal{T}_{n}]\vdash
Q^{\prime}\leadsto\Phi^{\prime}\\\
\end{array}}{\vphantom{,}\mathcal{S},\Gamma\vdash\text{With}(\vec{Q},\vec{R},Q^{\prime})\leadsto\land_{i=1}^{n}\Phi_{i}\land\Phi^{\prime}}&\\!\\!\\!\\!\\!\\!\textrm{(E-With)}\end{array}\mkern-2.0mu\\\
\\\ \end{array}$ Figure 19.  Symbolic encoding of SQL queries. In OrderBy, we
first “remove” those deleted symbolic tuples (i.e., $\text{Del}(t_{i})=\top$)
by moving them to the end of the list s.t. $\exists m.1\leq m\leq
n\land\land_{i=1}^{m}\text{Del}(t_{i})=\bot\land\land_{i=m+1}^{n}\text{Del}(t_{i})=\top$;
and the $\text{find}(i,\vec{E},b)$ function will find the $i$-th
smallest/largest non-deleted tuple $t_{i}^{\prime\prime}$ w.r.t. the
expression list $\vec{E}$ and the ascending order $b$.
$\text{Dedup}(\mathcal{T}^{\prime},\mathcal{T})$ serves as de-duplication on a
set of tuples $\text{Dedup}(\vec{t^{\prime}},\vec{t})=\mathcal{T}$, i.e.,
$t_{1}^{\prime}=t_{1}\land\land_{i=2}^{n}(t_{i}\in\vec{t}_{1:i-1}\to\text{Del}(t_{i}^{\prime})\land
t_{i}\notin\vec{t}_{1:i-1}\to t_{i}^{\prime}=t_{i})$ where
$|\vec{t^{\prime}}|=|\vec{t}|=n$.

Unlike the EXCEPT operation, which rules out all occurrences of duplicate
tuples, EXCEPT ALL only eliminates occurrences of duplicate data with limited
times. We utilize dynamic programming to encode the EXCEPT ALL operation. Let
us define two tuples $t_{i}\in R_{1}$ and $t_{j}^{\prime}\in R_{2}$ are paired
iff they are (1) equal (i.e., $t_{i}$ and $t_{j}^{\prime}$ are not deleted and
share the same values), and (2) not paired with the previous tuples from the
other relation. Formally, paired is defined as follows:

$\texttt{Paired}(i,j)=\left\\{\begin{aligned}
&\texttt{Eq}(t_{i},t_{j}^{\prime},\mathcal{A})&i=1,j=1,\\\
&\texttt{Eq}(t_{i},t_{j}^{\prime},\mathcal{A})\land\land_{k=1}^{j-1}\neg\texttt{Paired}(1,k)&i=1,j\neq
1,\\\
&\texttt{Eq}(t_{i},t_{j}^{\prime},\mathcal{A})\land\land_{k=1}^{i-1}\neg\texttt{Paired}(k,1)&i\neq
1,j=1,\\\
&\texttt{Eq}(t_{i},t_{j}^{\prime},\mathcal{A})\land\land_{k=1}^{i-1}\neg\texttt{Paired}(k,j)\land\land_{k=1}^{j-1}\neg\texttt{Paired}(i,k)&\text{otherwise}.\end{aligned}\right.$

where the $\texttt{Eq}(t_{i},t_{j}^{\prime},\mathcal{A})$ predicate asserts
$t_{i}\in R_{1}$ and $t_{j}^{\prime}\in R_{2}$ are equal, i.e.,
$\texttt{Eq}(t_{i},t_{j}^{\prime},\mathcal{A})\Leftrightarrow\neg\text{Del}(t_{i})\land\neg\text{Del}(t_{j}^{\prime})\land\land_{a\in\mathcal{A}}t_{i}.a=t_{j}^{\prime}.a$.
For instance, $t_{3}$ and $t_{2}^{\prime}$ are paired because they share the
same values and are unable to be paired with other tuples (such as $t_{1}$ or
$t_{1}^{\prime}$), as shown in Figure 20(a).

(a) The paired mechanism of EXCEPT ALL.

(b) The decomposition of GROUP BY.

Figure 20. An illustration on EXCEPT ALL and GROUP BY.

Moreover, Figure 21 encodes rules for evaluating predicates. Note that since
we consider the three-valued logic, the logical operations $\odot$ are able to
return NULL values if the operands have NULL, and the situations for AND and
OR become more complicated. Furthermore, Figure 22 evaluates symbolic
expressions in SQL queries. Due to NULL values, aggregation functions might
also be NULL if the predicate
$\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T})$ holds, and return numeric
values otherwise.

$\begin{array}[]{lcl}\llbracket\top\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\top\\\
\llbracket\bot\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\bot\\\
\llbracket\text{Null}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\text{Null}\\\
\llbracket A_{1}\odot
A_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\text{let}~{}v_{1}=\llbracket
A_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}},v_{2}=\llbracket
A_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}~{}\text{in}~{}\text{ite}(v_{1}=\text{Null}\lor
v_{2}=\text{Null},\text{Null},v_{1}\odot v_{2})\\\
\llbracket\text{IsNull}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\llbracket
E\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\text{Null}\\\
\llbracket\vec{E}\in\vec{v}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\text{let}\\\
&&\quad\vec{v}=[v_{1,1},\ldots,v_{n,m}]\quad\text{where}~{}m=|\vec{E}|=|\vec{v}_{i}|\\\
&&\text{in}~{}\llbracket\lor_{i=1}^{n}\land_{j=1}^{m}E_{j}=v_{i,j}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}\\\
\llbracket\vec{E}\in
Q\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\text{let}{}\\\
&&\quad\mathcal{S}\vdash Q:[a_{1},\ldots,a_{m}],\Gamma\vdash
Q\hookrightarrow[t_{1},\ldots,t_{n}],\mathcal{S},\Gamma\vdash
Q\leadsto\Phi\quad\text{where}~{}m=|\vec{E}|\\\ &&\quad v_{i,j}=\llbracket
a_{j}\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}\quad 1\leq i\leq n,1\leq j\leq
m\\\
&&~{}\text{in}~{}\Phi\land\llbracket\vec{E}\in\vec{v}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}\\\
\llbracket\phi_{1}\land\phi_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\text{let}~{}v_{1}=\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}},v_{2}=\llbracket\phi_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}~{}\text{in}{}\\\
&&\quad\text{ite}((v_{1}=v_{2}=\text{Null})\lor(v_{1}=\text{Null}\land
v_{2}=\top)\lor(v_{1}=\top\land v_{2}=\text{Null}),\text{Null},v_{1}=\top\land
v_{2}=\top)\\\
\llbracket\phi_{1}\lor\phi_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\text{let}~{}v_{1}=\llbracket\phi_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}},v_{2}=\llbracket\phi_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}~{}\text{in}{}\\\
&&\quad\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)\\\
\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)\\\ \end{array}$ Figure 21. Rules for evaluating predicates.
$\begin{array}[]{lcl}\llbracket
a\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&t.a\quad\text{where
}t=\text{First}(\mathcal{T})\\\ \llbracket
v\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&v\\\ \llbracket E_{1}\diamond
E_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\text{let}~{}v_{1}=\llbracket
E_{1}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}},~{}v_{2}=\llbracket
E_{2}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}~{}\text{in}~{}\text{ite}(v_{1}=\text{Null}\lor
v_{2}=\text{Null},\text{Null},v_{1}\diamond v_{2})\\\
\llbracket\text{Count}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\text{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))\\\
\llbracket\text{Sum}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\text{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]}))\\\
\llbracket\text{Avg}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\llbracket\text{Sum}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}/~{}\llbracket\text{Count}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}\\\
\llbracket\text{Min}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\text{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]}))\\\
\llbracket\text{Max}(E)\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\text{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]}))\\\
\llbracket\text{ITE}(\phi,E_{1},E_{2})\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\text{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}})\\\
\llbracket\text{Case}(\vec{\phi},\vec{E},E^{\prime})\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}&=&\llbracket\text{ITE}(\phi_{1},E_{1},\text{ITE}(\phi_{2},E_{2},\text{ITE}(\ldots,\text{ITE}(\phi_{n},E_{n},E^{\prime}))))\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}\text{
where }n=|\vec{\phi}|=|\vec{E}|\\\ \end{array}$
Figure 22. Rules for evaluating expressions. $f$ is an uninterpreted function.
The $\text{First}(\mathcal{T})$ function finds the first tuple from
$\mathcal{T}$. The $\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T})$
predicate asserts the attribute expression $E$ of all non-deleted tuples in
$\mathcal{T}$ is Null, i.e.,
$\text{AllNull}(E,\mathcal{S},\Gamma,\mathcal{T})\leftrightarrow\land_{t\in\mathcal{T}}(\neg\text{Del}(t)\to\llbracket
E\rrbracket_{\mathcal{S},\Gamma,[t]}=\text{Null})$.

##  Appendix C Additional Experimental Results

###  C.1. RQ: Importance of Supporting Rich Integrity Constraints

As mentioned in RQ1 of Section 6.2, one reason that leads to a large number of
“unsupported” benchmarks is due to baselines’ poor support for integrity
constraints. A natural question arises — what if we _do not_ consider
integrity constraints? That is, how important is it to support integrity
constraints? This section aims to address exactly this.

(a) _LeetCode._

(b) _Calcite._

(c) _Literature._

Figure 23. Each sub-figure corresponds to one workload, where it shows the
percentage of benchmarks in each outcome category. A tool name that is
appended with “-RQ2” means the tool is run under RQ2 setup. We also include
VeriEQL-RQ1 in this figure to facilitate an easy comparison of VeriEQL’s
results under two setups. To compare a baseline’s results under two setups,
please also refer to Figure 13.

_Setup._ We use the same setup as in RQ1 except for one difference — we
discard integrity constraints. That is, we drop the integrity constraint
$\mathcal{C}$ associated with a benchmark, regardless of whether or not the
tool supports $\mathcal{C}$. This effectively means we are checking
equivalence with respect to a _superset of inputs_ considered in RQ1 which now
also includes databases that violate $\mathcal{C}$.

In what follows, we report the number of benchmarks in each category under
this new setup, annotated with a suffix “-noIC”. The same setup is used for
VeriEQL and baselines. We will also compare the results with RQ1’s from
Section 6.2.

Take-away: it is critical to support rich integrity constraints in order to
avoid generating spurious counterexamples. For instance, without considering
integrity constraints, the majority of “refuted” benchmarks — many of which
should be equivalent — reported by VeriEQL are mistakenly proved non-
equivalent, due to (spurious) inputs that violate the integrity constraints.

_Results._ Our main results are presented in Figure 23. Let us first focus on
VeriEQL. For LeetCode benchmarks, comparing VeriEQL and VeriEQL-noIC, the most
noticeable change is the _significantly higher_ “refuted” bar — from 14.9%
(with IC) to 47.5% (without IC). Notably, more than 75% of noIC’s “refuted”
benchmarks are caused by _spurious counterexamples_. Some of noIC’s “refuted”
benchmarks were previously “checked” in RQ1 — the “checked” bar lowers from
62.1% to 37% — whereas the rest were previously “unsupported” in RQ1. A very
small number (i.e., 3.3%) of benchmarks previously “unsupported” in RQ1 now
become “checked” in noIC — which suggests that discarding integrity
constraints does _not_ help prove many more benchmarks. For the other two
workloads, we observe a similar trend: “refuted” bars go up (due to spurious
counterexamples) and “checked” bars go down, indicating it is important to
support integrity constraints for Calcite and Literature as well.

Let us now switch gears and briefly go over the baselines’ results. On
LeetCode, all baselines except DataFiller-noIC still have high “unsupported”
percentages, due to their limited support of SQL operations. DataFiller is a
random database generation tool, which does not reply on SQL queries to
generate database instances, so its noIC “unsupported” percentages drop to
zero. However, as shown in Figure 14 of Section 6.3, most of the
counterexamples generated by DataFiller-noIC are spurious. SPES-noIC also has
a high “not-verified” bar: it can now successfully run on 58.5% but 52.8% are
“not-verified”. But unfortunately, there is no easy way to validate its result
in the entirety, as SPES does not provide counterexamples. Among these 52.8%,
VeriEQL can find valid counterexamples for 26.2%. We manually inspected 50
samples from the remaining 26.6%, and believe all of them are equivalent. The
situation for Calcite is similar, where SPES-noIC has the highest “not-
verified” bar (52.9%), though we believe they are false alarms since most
Calcite query pairs (if not all) should be equivalent. Such anecdotal evidence
again indicates the importance of considering integrity constraints. Finally,
for Literature, we also see noticeably higher “refuted” — we confirmed for
Cosette, Qex, and DataFiller, it is due to spurious counterexamples.

_Discussion._ Careful readers may wonder why VeriEQL-noIC’s “unsupported” bar
is still non-zero, given we discard integrity constraints. This is because
VeriEQL currently does not support some SQL features such as correlated
subqueries (i.e., subqueries that use values from the outer query) and window
functions.

###  C.2. Finding Bugs in MySQL

$Q_{1}$ |  |  SELECTDISTINCTpage_id ASrecommended_page
---
FROM(SELECTCASE
WHENuser1_id = 1 THENuser2_id
WHENuser2_id = 1 THENuser1_id
ELSENULL
ENDASuser_id
FROMfriendship) AStb1 JOINlikes AStb2
ONtb1.user_id = tb2.user_id
WHEREpage_id NOTIN(SELECTpage_id
FROMlikes WHEREuser_id = 1)
$Q_{2}$ |  |  SELECTDISTINCTpage_id ASrecommended_page
---
FROM(SELECTb.user_id, b.page_id
FROMfriendship a LEFT JOINlikes b
ON (a.user2_id = b.user_id ORa.user1_id=b.user_id)
AND(a.user1_id = 1 ORa.user2_id = 1)
WHEREb.page_id NOTIN(SELECTDISTINCT(page_id)
FROMlikes WHEREuser_id=1) ) T
(a) Two non-equivalent queries $(Q_{1},Q_{2})$ from LeetCode.

friendship table:
user1_id user2_id 0 1
likes table:
user_id page_id -1 0

(b) Counterexample input database.

page_id
---
NULL
(c) $Q_{2}$’s expected output.

Figure 24. Queries from Figure 24(a), when executed using MySQL on the
database from Figure 24(b), both return the empty table, but they should
return different output tables according to SQL semantics. In particular,
$Q_{1}$ should return the empty table and $Q_{2}$ should return the table in
Figure 24(c).

As mentioned in Section 6.3, for two LeetCode benchmarks, VeriEQL generates
“spurious” counterexamples — that are actually genuine — due to a bug in
MySQL. Figure 24 shows one such
benchmark141414https://leetcode.com/problems/page-recommendations/
$(Q_{1},Q_{2})$ (see Figure 24(a)) and the corresponding counterexample
database $\mathcal{D}$ generated by VeriEQL (see Figure 24(b)). This benchmark
has an integrity constraint $\mathcal{C}$ requiring: (i) (user1_id, user2_id)
is the primary key of the friendship table, (ii) (user_id, page_id) is the
primary key of the likes table, and (iii) the friendship table does not have
any rows with $\texttt{user1\\_id}=\texttt{user2\\_id}$. As we can see,
$\mathcal{D}$ satisfies $\mathcal{C}$. Furthermore, we believe $Q_{1}$’s
output on $\mathcal{D}$ should be the empty table, because the ON predicate
associated with the JOIN operation in $Q_{1}$ is always false. On the other
hand, $Q_{2}$ should return the table shown in Figure 24(c): the LEFT JOIN in
$Q_{2}$ will retain all records from the friendship table in the output, and
the WHERE predicate will be true since b.page_id (i.e., likes.page_id which is
0) will not be in an empty set; therefore, every tuple after the join will be
eventually preserved in $Q_{2}$’s output. However, both queries return the
empty table on MySQL’s latest release version 8.0.32. The MySQL verification
team had confirmed and classified this bug with _serious_ severity.

###  C.3. Detailed Analysis

This section reports detailed performance statistics of VeriEQL.

_Time breakdown._ VeriEQL essentially performs two steps: constraint
generation and constraint solving, where the latter takes 67.7% of the total
time on average across all benchmarks.

_Efficiency at disproving query equivalence._ VeriEQL is very efficient at
disproving query pairs. For example, among the 3,586 non-equivalent LeetCode
benchmarks that VeriEQL can generate counterexamples for in RQ1, 3,108 of them
can be disproved within 1 second, 3,528 can be disproved within 5 seconds, and
the slowest one takes 251 seconds. All Calcite’s non-equivalent benchmarks can
be proved within 2 seconds. Finally, all 29 non-equivalent Literature
benchmarks are identified within 2 minutes where 26 of them took less than 10
seconds.

_Efficiency of bounded verification._ This experiment concerns the number of
benchmarks whose _bounded equivalence_ can be proved by VeriEQL in a given
timeout, with respect to different input bounds. In particular, we vary the
bound from 1 to 10, and for each bound we record the number of benchmarks
whose equivalence can be _completely_ verified using a 10-minute timeout. That
is, if VeriEQL does not terminate on a benchmark within the given timeout, we
do not count this benchmark as “proved” for the given bound. The main result
can be found in Table 1. The key message is that VeriEQL can efficiently prove
most of the benchmarks up to bound 5. While the number drops for larger
bounds, VeriEQL can still prove a significant number of benchmarks quite
efficiently.

Table 1. For each workload, we vary the input database size from 1 to 10 and show the number of benchmarks that can be _completely_ verified by VeriEQL for the given bound using a 10-minute timeout. If VeriEQL does not finish the bounded verification within the timeout, we do not count it as “checked.” We also show the average and median verification times for those benchmarks that terminate.  _bound_ | LeetCode | Calcite | Literature
---|---|---|---
_# proved_ | _mean (sec)_ | _median (sec)_ | _# proved_ | _mean (sec)_ | _median (sec)_ | _# proved_ | _mean (sec)_ | _median (sec)_
1 | 14905 | 0.4 | 0.3 | 261 | 0.7 | 0.7 | 34 | 0.7 | 0.7
2 | 14894 | 0.7 | 0.4 | 261 | 0.4 | 0.3 | 34 | 2.6 | 0.3
3 | 14618 | 16.1 | 0.8 | 261 | 3.1 | 0.4 | 32 | 4.6 | 0.6
4 | 11757 | 24.5 | 1.6 | 242 | 9.7 | 0.6 | 29 | 17.0 | 1.3
5 | 10564 | 73.0 | 5.1 | 224 | 33.6 | 0.7 | 26 | 71.9 | 3.4
6 | 7779 | 63.0 | 4.5 | 193 | 33.0 | 0.8 | 17 | 19.3 | 0.8
7 | 6203 | 41.9 | 6.6 | 162 | 15.5 | 0.8 | 15 | 43.3 | 1.2
8 | 5344 | 34.4 | 7.7 | 153 | 20.0 | 1.0 | 13 | 12.6 | 2.8
9 | 4942 | 53.5 | 12.0 | 144 | 26.5 | 1.3 | 12 | 37.0 | 5.7
10 | 4160 | 49.7 | 4.6 | 134 | 14.4 | 1.7 | 12 | 65.2 | 12.4

##  Appendix D Proof

In this section, we provide the proof of lemmas and theorems in the main
paper.

###### Proof of Theorem 4.2:.

Given a symbolic database $\Gamma$ and an integrity constraint $\mathcal{C}$,
consider a formula $\Phi$ such that
$\Gamma\vdash\mathcal{C}\rightsquigarrow\Phi$. If $\Phi$ is satisfiable, then
the model of $\Phi$ corresponds to a database consistent with $\Gamma$ that
satisfies $\mathcal{C}$. If $\Phi$ is unsatisfiable, then no database
consistent with $\Gamma$ satisfies $\mathcal{C}$. ∎

###### Proof..

By structural induction on $\mathcal{C}$.

  1. (1)

Base case: $\mathcal{C}=\text{PK}(R,\vec{a})$.

Suppose $\Gamma(R)=[t_{1},\ldots,t_{n}]$ and $m=|\vec{a}|$ by Figure 9 and,
for every tuple $t_{i}\in$ $\Gamma(R)$, it has $t_{i}.a_{k}\neq\text{Null}$
where $a_{k}$ denotes the attribute and $1\leq k\leq m$. Also, $\Phi_{2}$ in
Figure 9 ensures no two tuples $t_{i}$ and $t_{j}$ where $t_{i}\in\Gamma(R)$
and $t_{j}\in\Gamma(R)$ such that $\land_{k=1}^{m}t_{i}.a_{k}=t_{j}.a_{k}$ is
true. Therefore, it holds that if $\Phi$ is satisfiable, we have a model of
$\Phi$ corresponds to a database consistent with $\Gamma$ that satisfies
$\text{PK}(R,\vec{a})$ as $\Phi_{1}\land\Phi_{2}$ satisfies $\forall
t_{i}\in\Gamma(R).t_{i}.a\neq\text{Null}\land\forall t_{i}\in\Gamma(R).\forall
t_{j}\in\Gamma(R).i\neq j\to\neg(\land_{k=1}^{m}t_{i}.a_{k}=t_{j}.a_{k})$,
thus ensuring the model conforms to primary key properties that 1) attributes
$\vec{a}$ of every tuple in $\Gamma(R)$ are non-NULL, and 2) there are no two
tuples in $\Gamma(R)$ such that their values of $\vec{a}$ are identical. And
on the contrary, if $\Phi$ is unsatisfiable, then it is necessarily true that
there exists no database consistent with $\Gamma$ that can satisfy
$\text{PK}(R,\vec{a})$.

  2. (2)

Base case: $\mathcal{C}=\text{FK}(R_{1},a_{1},R_{2},a_{2})$.

Suppose $\Gamma(R_{1})=[t_{1},\ldots,t_{n}]$ and
$\Gamma(R_{2})=[t_{1}^{\prime},\ldots,t_{m}^{\prime}]$, by Figure 9, $\Phi$
ensures for any tuple $t_{i}\in\Gamma(R_{1})$,
$t_{i}.a_{1}\in[t_{1}^{\prime}.a_{2},\ldots,t_{m}^{\prime}.a_{2}]$. Therefore,
it holds that if $\Phi$ is satisfiable, we have a model of $\Phi$ corresponds
to a database consistent with $\Gamma$ that satisfies
$\text{FK}(R_{1},a_{1},R_{2},a_{2})$ as $\Phi$ satisfies $\forall
t_{i}\in\Gamma(R_{1}).t_{i}.a_{1}\in[t_{1}^{\prime}.a_{2},\ldots,t_{m}^{\prime}.a_{2}]$
(the value of $a_{1}$ of every tuple in $\Gamma(R_{1})$ references the value
$a_{2}$ of any tuple in $\Gamma(R_{2})$); also, if $\Phi$ is unsatisfiable,
then it is necessarily true that there exists no database consistent with
$\Gamma$ satisfies $\text{FK}(R_{1},a_{1},R_{2},a_{2})$.

  3. (3)

Base case: $\mathcal{C}=\text{NotNull}(R,a)$.

Suppose $\Gamma(R)=[t_{1},\ldots,t_{n}]$, by Figure 9, $\Phi$ ensures for any
tuple $t_{i}$ in $\Gamma(R)$, $t_{i}.a\neq\text{Null}$. Therefore, it holds
that if $\Phi$ is satisfiable, we have a model of $\Phi$ corresponding to a
database consistent with $\Gamma$ where $\forall
t_{i}\in\Gamma(R).t_{i}.a\neq\text{Null}$, which satisfies that the value of
$a$ of every tuple in $\Gamma(R)$ is non-NULL, and also if $\Phi$ is
unsatisfiable, then it is necessarily true that there exists no database
consistent with $\Gamma$ satisfies $\text{NotNull}(R,a)$.

  4. (4)

Base case: $\mathcal{C}=\text{Check}(R,\psi)$.

Suppose $\Gamma(R)=[t_{1},\ldots,t_{n}]$, by Figure 9, $\Phi$ ensures for any
tuple $t_{i}$, the predicate $\llbracket\psi\rrbracket_{t_{i}}$ evaluates to
$\top$. Therefore, it holds that if $\Phi$ is satisfiable, the model of $\Phi$
corresponds to a database consistent with $\Gamma$ that satisfies $\forall
t_{i}\in\Gamma(R).\llbracket\psi\rrbracket_{t_{i}}=\top$ that conforms to the
Check constraint that every tuple in $\Gamma(R)$ satisfies $\psi$, and if
$\Phi$ is unsatisfiable, then it is necessarily true that there exists no
database consistent with $\Gamma$ satisfies $\text{Check}(R,\psi)$.

  5. (5)

Base case: $\mathcal{C}=\text{Inc}(R,a,v)$.

Suppose $\Gamma(R)=[t_{1},\ldots,t_{n}]$, by Figure 9, $\Phi_{2}$ foremost
constrains the attribute $t_{i}.a$ is non-NULL for every tuple
$t_{i}\in\Gamma(R)$. $\Phi_{1}$ then ensures for any tuple $t_{i}$, the
attribute $t_{i}.a=v+i-1$, where $v$ is the initial value. Therefore, it holds
that if $\Phi$ is satisfiable, we have a model of $\Phi$ corresponding to a
database consistent with $\Gamma$ that satisfies $\forall
t_{i}\in\Gamma(R).t_{i}.a\neq\texttt{NULL}\land t_{i}.a=v+i-1$ and hence
ensures the value of $a$ of every tuple in $\Gamma(R)$ is incrementally
increased by 1 from the initial value $v$; if $\Phi$ is unsatisfiable, then it
is necessarily true that there exists no database consistent with $\Gamma$
satisfies $\text{Inc}(R,a,v)$.

  6. (6)

Inductive case:
$\mathcal{C}^{\prime\prime}=\mathcal{C}\land\mathcal{C}^{\prime}$.

By the base cases shown above, the Theorem for the inductive case
$\mathcal{C}^{\prime\prime}=\mathcal{C}\land\mathcal{C}^{\prime}$ can be
proved.

∎

###### Proof of Theorem 4.5:.

Let $\mathcal{D}$ be a database over schema $\mathcal{S}$ and $o_{R}$ be the
output relation of running query $Q$ over $\mathcal{D}$. Consider a symbolic
database $\Gamma$ over $\mathcal{S}$, a symbolic relation $R$ and a formula
$\Phi$ such that $\Gamma\vdash Q\hookrightarrow R$ and
$\mathcal{S},\Gamma\vdash Q\leadsto\Phi$. For any interpretation $\mathcal{I}$
such that $\mathcal{I}(\Gamma)=\mathcal{D}$, there exists an extension
$\mathcal{I}^{\prime}$ of $\mathcal{I}$ such that (1) the result of query $Q$
over $\mathcal{D}$ is $\mathcal{I}^{\prime}(R)$, and (2) the database
$\mathcal{D}$ and $\mathcal{I}^{\prime}$ jointly satisfy $\Phi$, i.e.,

$\begin{array}[]{l}(\Gamma\vdash Q\hookrightarrow
R)\land(\mathcal{S},\Gamma\vdash
Q\leadsto\Phi)\land(\mathcal{I}(\Gamma)=\mathcal{D})\Rightarrow\\\
\qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad\exists\mathcal{I}^{\prime}\sqsupseteq\mathcal{I}.\mathcal{I}^{\prime}(R)=\llbracket
Q\rrbracket_{\mathcal{D}}\land(\mathcal{I}^{\prime},\mathcal{D}[o_{R}\mapsto\mathcal{I}^{\prime}(R)]\models\Phi)\end{array}$

Prove by structural induction on $Q$. 151515To be concise, we widely use a
function ptr in this proof section. The function ptr takes as input an index
$i$ and returns an index $j$ s.t. $\mathcal{I}(t_{j})=x_{i}$ where
$x_{i}\in\llbracket Q\rrbracket_{\mathcal{D}}$ and $t_{j}\in R$.

  1. (1)

Base case: $Q=T$.

$R=\Gamma(T)$ by Figure 11. $\Phi=\top$ by Figure 12.

Take $\mathcal{I}^{\prime}=\mathcal{I}$ and
$\mathcal{D}^{\prime}=\mathcal{D}[o_{R}\mapsto\mathcal{I}(R)]$. Obviously, we
have (a)
$\mathcal{I}^{\prime}(R)=\mathcal{I}(R)=\mathcal{I}(\Gamma(T))=\mathcal{D}(T)=\llbracket
T\rrbracket_{\mathcal{D}}$ because $\llbracket
T\rrbracket_{\mathcal{D}}=\mathcal{D}(T)$ by Figure 18, (b)
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\top$.

Thus, Theorem 4.5 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{D}}=\textsf{ite}(\text{hasAggr}(L),[\llbracket
L\rrbracket_{\mathcal{D},\llbracket
Q\rrbracket_{\mathcal{D}}}],\textsf{map}(\llbracket
Q\rrbracket_{\mathcal{D}},\lambda x.\llbracket L\rrbracket_{\mathcal{D},x}))$
by Figure 17.

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

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, $\llbracket\Pi_{L}(Q)\rrbracket_{\mathcal{D}}=[\llbracket
L\rrbracket_{\mathcal{D},\llbracket Q\rrbracket_{\mathcal{D}}}]$ by Figure 17,
$\mathcal{S},\Gamma\vdash\Pi_{L}(Q)\leadsto\Phi\land\land_{i=1}^{l}\Phi_{i}^{\prime}\land\neg\text{Del}(t_{1}^{\prime})$
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}^{\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_{1}^{\prime})=\bot$ and
$\mathcal{I}^{\prime}(t_{1}^{\prime})=[(\text{ToString}(a_{1}^{\prime}),\llbracket
a_{1}^{\prime}\rrbracket_{\mathcal{D},\mathcal{I}(R)}),\ldots,(\text{ToString}(a_{l}^{\prime}),\llbracket
a_{l}^{\prime}\rrbracket_{\mathcal{D},\mathcal{I}(R)})]$.

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

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

Let
$\mathcal{D}^{\prime}=\mathcal{D}[o_{\Pi_{L}(Q)}\mapsto\llbracket\Pi_{L}(Q)\rrbracket_{\mathcal{D}}]$.
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})}$ and , therefore,
$\mathcal{I},\mathcal{D}\models\llbracket
a^{\prime}\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}=\llbracket
a\rrbracket_{\mathcal{S},\Gamma,\mathcal{T}}\Leftrightarrow\mathcal{I},\mathcal{D}\models\llbracket
a^{\prime}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}=\llbracket
a\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}(\mathcal{T})}$.

$\begin{array}[]{rcl}\mathcal{I}^{\prime},\mathcal{D}^{\prime}&\models&\land_{j=1}^{l}\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{I}(\Gamma),[\mathcal{I}(t_{1}^{\prime})]}=\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}([t_{1},\ldots,t_{n}])}\\\
\mathcal{I}^{\prime},\mathcal{D}^{\prime}&\models&\land_{j=1}^{l}\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{1}^{\prime}]}=\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{1},\ldots,t_{n}]}\\\
\end{array}$

Thus, we have
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi\land\land_{i=1}^{l}\Phi_{i}^{\prime}\land\neg\text{Del}(t_{1}^{\prime})$

    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,
$\llbracket\Pi_{L}(Q)\rrbracket_{\mathcal{D}}=\textsf{map}(\llbracket
Q\rrbracket_{\mathcal{D}},\lambda x.\llbracket L\rrbracket_{\mathcal{D},x})$
by Figure 17,
$\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}^{\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\mathcal{I}(\text{Del})(t_{i})$
and
$\mathcal{I}^{\prime}(t_{i}^{\prime})=[(\text{ToString}(a_{1}^{\prime}),\llbracket
a_{1}^{\prime}\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}),\ldots,(\text{ToString}(a_{l}^{\prime}),\llbracket
a_{l}^{\prime}\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]})]=\llbracket
L\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}$.

Let $x_{i}\in\llbracket Q\rrbracket_{\mathcal{D}}$ where $1\leq i\leq c$ and
$c=|\llbracket Q\rrbracket_{\mathcal{D}}|$, then we know
$x_{i}\in\mathcal{I}(R)$ because $\mathcal{I}(R)=\llbracket
Q\rrbracket_{\mathcal{D}}$, $\mathcal{I}(\text{Del})(x_{i})=\bot$. Further,
for any tuple $x_{i}\in\llbracket Q\rrbracket_{\mathcal{D}}$, we have two
symbolic tuples $t_{\textsf{ptr}(i)}\in Q$ and
$t_{\textsf{ptr}(i)}^{\prime}\in\Pi_{L}(Q)$ s.t.
$\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i)}^{\prime})=\mathcal{I}(\text{Del})(t_{\textsf{ptr}(i)})=\mathcal{I}(\text{Del})(x_{i})=\bot$
and $\llbracket L\rrbracket_{\mathcal{D},[x_{i}]}=\llbracket
L\rrbracket_{\mathcal{D},[\mathcal{I}(t_{\textsf{ptr}(i)})]}=\mathcal{I}^{\prime}(t_{\textsf{ptr}(i)}^{\prime})$.

By the semantics of map, we have

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

Let
$\mathcal{D}^{\prime}=\mathcal{D}[o\mapsto\llbracket\Pi_{\phi}(Q)\rrbracket_{\mathcal{D}}]$.
Since $\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i}^{\prime})]}=\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}\Leftrightarrow\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{i}^{\prime}]}=\llbracket
a_{j}^{\prime}\rrbracket_{\mathcal{S},\Gamma,[t_{i}]}$ and
$\mathcal{I}(\text{Del})(t_{i}^{\prime})=\mathcal{I}(\text{Del})(t_{i})$, we
know $\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi_{i}^{\prime}$ and,
therefore,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi\land\land_{i=1}^{n}\Phi_{i}^{\prime}$.

Hence,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi\land\land_{i=1}^{n}\Phi_{i}^{\prime}$
by 2(a) and 2(b) and Theorem 4.5 for the inductive case
$Q^{\prime}=\Pi_{L}(Q)$ is proved.

  3. (3)

Inductive case: $Q^{\prime}=\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$,
$\mathcal{S},\Gamma\vdash\sigma_{\phi}(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.

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}^{\prime})=\mathcal{I}^{\prime}(t_{i})=\mathcal{I}(t_{i})$
and
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime})\leftrightarrow\mathcal{I}(\text{Del})(t_{i})\lor\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}\neq\top$.

For any tuple $x_{i}\in\llbracket Q\rrbracket_{\mathcal{D}}$, we have a
symbolic tuple $t_{\textsf{ptr}(i)}\in R$ s.t.
$\mathcal{I}(\text{Del})(t_{\textsf{ptr}(i)})=\mathcal{I}(\text{Del})(x_{i})\\\
$ $=\bot$ and $\mathcal{I}(t_{\textsf{ptr}(i)})=\mathcal{I}(x_{i})$. If
$\llbracket\phi\rrbracket_{\mathcal{D},[x_{i}]}=\top$, then
$\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i)}^{\prime})=\mathcal{I}(\text{Del})(t_{\textsf{ptr}(i)})\lor\\\
$
$\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{\textsf{ptr}(i)})]}\neq\top=\bot$
and
$\mathcal{I}^{\prime}(t_{\textsf{ptr}(i)}^{\prime})=\mathcal{I}(t_{\textsf{ptr}(i)})=x_{i}$.
Otherwise,
$\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i)}^{\prime})=\mathcal{I}(\text{Del})(t_{\textsf{ptr}(i)})\lor(\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{\textsf{ptr}(i)})]}\neq\top)=\top$
and
$\mathcal{I}^{\prime}(t_{\textsf{ptr}(i)}^{\prime})=\mathcal{I}(t_{\textsf{ptr}(i)})=x_{i}$.
Therefore, for any
$x_{i}^{\prime\prime}\in\llbracket\sigma_{\phi}(Q)\rrbracket_{\mathcal{D}}$,
we have a symbolic tuple $t_{ptr(i)}^{\prime}\in R^{\prime}$.
$\llbracket\sigma_{\phi}(Q)\rrbracket_{\mathcal{D}}=\mathcal{I}(R^{\prime})$
is proved.

Let
$\mathcal{D}^{\prime}=\mathcal{D}[o_{R^{\prime}}\mapsto\llbracket\sigma_{\phi}(Q)\rrbracket_{\mathcal{D}}]$.
By Lemma D.1, we know
$\mathcal{I}(\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,[x]})=\llbracket\phi\rrbracket_{\mathcal{I}(\Gamma),\mathcal{I}([x])}=\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(x)]}$
and, therefore,
$\mathcal{I},\mathcal{D}\models\llbracket\phi\rrbracket_{\mathcal{S},\Gamma,[x]}\Leftrightarrow\mathcal{I},\mathcal{D}\models\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(x)]}$
and
$\mathcal{I},\mathcal{D}\models\Phi_{i}^{\prime}\Leftrightarrow\mathcal{I},\mathcal{D}\models(\neg\text{Del}(t_{i})\land\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}=\top)\to
t_{i}^{\prime}=t_{i}\land(\text{Del}(t_{i})\lor\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}\neq\top)\to\text{Del}(t_{i}^{\prime})$.

For any $t_{i}\in R$, let us discuss it in two cases.

    1. (a)

If $\mathcal{I}(\text{Del})(t_{i})=\top$, then, by the definition of
$\mathcal{I}^{\prime}$, we have
$\mathcal{I}^{\prime}(\text{Del})(t_{i})=\mathcal{I}(\text{Del})(t_{i})=\top$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime})=\mathcal{I}(\text{Del})(t_{i})\lor(\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}\neq\top)=\top$,
$\mathcal{I}^{\prime}(t_{i}^{\prime})=\mathcal{I}^{\prime}(t_{i})=\mathcal{I}(t_{i})$,

$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models(\neg\text{Del}(t_{i})\land\llbracket\phi\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i})]}=\top)\to
t_{i}^{\prime}=t_{i}$

and

$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models(\text{Del}(t_{i})\lor\llbracket\phi\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i})]}\neq\top)\to\text{Del}(t_{i}^{\prime})$

Thus, $\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi_{i}^{\prime}$.

    2. (b)

If $\mathcal{I}(\text{Del})(t_{i})=\bot$, then, by the definition of
$\mathcal{I}^{\prime}$, we have
$\mathcal{I}^{\prime}(\text{Del})(t_{i})=\mathcal{I}(\text{Del})(t_{i})=\bot$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime})=\mathcal{I}(\text{Del})(t_{i})\lor(\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}\neq\top)=\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}\neq\top$
and
$\mathcal{I}^{\prime}(t_{i}^{\prime})=\mathcal{I}^{\prime}(t_{i})=\mathcal{I}(t_{i})$.

Let us further discuss
$\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}$ in two cases.

      1. (b1)

If $\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}=\top$, then
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime})=\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}\neq\top=\bot$,
we have

$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models(\neg\text{Del}(t_{i})\land\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}=\top)\to
t_{i}^{\prime}=t_{i}$

and

$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models(\text{Del}(t_{i})\lor\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}\neq\top)\to\text{Del}(t_{i}^{\prime})$

      2. (b2)

If $\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}\neq\top$, then
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime})=\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}\neq\top=\top$,
we have

$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models(\neg\text{Del}(t_{i})\land\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}=\top)\to
t_{i}^{\prime}=t_{i}$

and

$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models(\text{Del}(t_{i})\lor\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}\neq\top)\to\text{Del}(t_{i}^{\prime})$

Hence, $\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi_{i}^{\prime}$ by
3((b))(b1) and 3((b))(b2).

Thus,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi\land\land_{i=1}^{n}\Phi_{i}^{\prime}$
by 3(a) and 3(b) and Theorem 4.5 for the inductive case
$Q^{\prime}=\sigma_{\phi}(Q)$ is proved.

  4. (4)

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

Suppose that $\mathcal{S}\vdash Q:[a_{1},\ldots,a_{p}]$ by Figure 10;
$\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.

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}^{\prime})\leftrightarrow\mathcal{I}^{\prime}(\text{Del})(t_{i})\leftrightarrow\mathcal{I}(\text{Del})(t_{i})$,
$\mathcal{I}^{\prime}(t_{i})=\mathcal{I}(t_{i})$, and
$\mathcal{I}^{\prime}(t_{i}^{\prime})=\\\ $
$[(\text{rename}(R,\text{ToString}(a_{1})),\llbracket
a_{1}\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]}),\ldots,(\text{rename}(R,\text{ToString}(a_{p})),\llbracket
a_{p}\rrbracket_{\mathcal{D},[\mathcal{I}(t_{i})]})]$.

Let $x_{i}\in\llbracket Q\rrbracket_{\mathcal{D}}$ where $1\leq i\leq n$, then
we have $t_{\textsf{ptr}(i)}\in\mathcal{I}(R)$ because
$\mathcal{I}(R)=\llbracket Q\rrbracket_{\mathcal{D}}$. Also, by the semantics
of map, we know

$\begin{array}[]{rcl}\llbracket\rho_{T}(Q)\rrbracket_{\mathcal{D}}&=&\textsf{map}(\llbracket
Q\rrbracket_{\mathcal{D}},\lambda
x.\textsf{map}(x,\lambda(n,v).(v,\text{rename}(T,n))))\\\
&=&\textsf{map}([x_{1},\ldots,x_{n}],\lambda
x.\textsf{map}(x,\lambda(n,v).(v,\text{rename}(T,n))))\\\ &=&[\\\
&&\quad[(\text{rename}(T,\text{ToString}(a_{1})),\llbracket
a_{1}\rrbracket_{\mathcal{D},[x_{1}]}),\ldots,\\\
&&\qquad\qquad(\text{rename}(T,\text{ToString}(a_{p})),\llbracket
a_{p}\rrbracket_{\mathcal{D},[x_{1}]})]\\\ &&\quad\ldots,\\\
&&\quad[(\text{rename}(T,\text{ToString}(a_{1})),\llbracket
a_{1}\rrbracket_{\mathcal{D},[x_{n}]}),\ldots,\\\
&&\qquad\qquad(\text{rename}(T,\text{ToString}(a_{p})),\llbracket
a_{p}\rrbracket_{\mathcal{D},[x_{n}]})]\\\ &&]\\\ \end{array}$

By the definition of ptr, we know, for any
$x_{i}^{\prime}\in\llbracket\rho_{T}(Q)\rrbracket_{\mathcal{D}}$, there exists
a symbolic tuple $t_{\textsf{ptr}(i)}^{\prime}\in R^{\prime}$ s.t.
$\mathcal{I}^{\prime}(t_{\textsf{ptr}(i)}^{\prime})=x_{i}^{\prime}$. Further,
$\llbracket\rho_{T}(Q)\rrbracket_{\mathcal{D}}=[x_{1}^{\prime},\ldots,x_{n}^{\prime}]=[\mathcal{I}^{\prime}(t_{\textsf{ptr}(1)}^{\prime}),\ldots,$
$\mathcal{I}^{\prime}(t_{\textsf{ptr}(n)}^{\prime})]=\mathcal{I}^{\prime}([t_{\textsf{ptr}(1)}^{\prime},\ldots,t_{\textsf{ptr}(n)}^{\prime}])=\mathcal{I}^{\prime}(R^{\prime})$.

Let
$\mathcal{D}^{\prime}=\mathcal{D}[T\mapsto\llbracket\rho_{T}(Q)\rrbracket_{\mathcal{D}}]$.
For any symbolic tuple $t_{i}\in R$ and $t_{i}\in R$, we know
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime})=\mathcal{I}(\text{Del})(t_{i})$
and $t_{i}$ is equal to $t_{i}^{\prime}$ in terms of every attribute.
Therefore, $\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models
t_{i}^{\prime}=t_{i}$ and
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi\land\land_{i=1}^{n}t_{i}^{\prime}=t_{i}$.

Thus, Theorem 4.5 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.

By the inductive hypothesis, we have $\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}(\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_{j}^{\prime})\leftrightarrow\mathcal{I}(\text{Del})(t_{j}^{\prime})$,
$\mathcal{I}^{\prime}(t_{j}^{\prime})=\mathcal{I}(t_{j}^{\prime})$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i,j}^{\prime\prime})=\mathcal{I}(\text{Del})(t_{i})\lor\mathcal{I}(\text{Del})(t_{j}^{\prime})$
and
$\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})=\textsf{merge}(\mathcal{I}(t_{i}),\mathcal{I}(t_{j}^{\prime}))$.

Let $x_{i}\in\llbracket Q\rrbracket_{\mathcal{D}}$,
$x_{j}^{\prime}\in\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$ where $1\leq
i\leq c\leq n$, $1\leq j\leq d\leq m$, $c=|\llbracket
Q\rrbracket_{\mathcal{D}}|$ and $d=|\llbracket
Q^{\prime}\rrbracket_{\mathcal{D}}|$, then we have $x_{i}\in\mathcal{I}(R)$
and $x_{j}^{\prime}\in\mathcal{I}(R^{\prime})$ because
$\mathcal{I}(R)=\llbracket Q\rrbracket_{\mathcal{D}}$ and
$\mathcal{I}(R^{\prime})=\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$,
$\mathcal{I}(\text{Del})(x_{i})=\mathcal{I}(\text{Del})(x_{j}^{\prime})=\bot$.
Also, by the semantics of foldl, we know

$\begin{array}[]{rcl}\llbracket Q\times
Q^{\prime}\rrbracket_{\mathcal{D}}&=&\textsf{foldl}(\lambda xs.\lambda
x.\textsf{append}(xs,\textsf{map}(\llbracket
Q^{\prime}\rrbracket_{\mathcal{D}},\lambda
y.\textsf{merge}(x,y))),[],\llbracket Q\rrbracket_{\mathcal{D}})\\\
&=&\textsf{foldl}(\lambda xs.\lambda x.\textsf{append}(xs,\\\
&&\qquad[\textsf{merge}(x,x_{1}^{\prime}),\ldots,\textsf{merge}(x,x_{q}^{\prime})]),[],\llbracket
Q\rrbracket_{\mathcal{D}})\\\ &=&[\\\
&&\qquad[\textsf{merge}(x_{1},x_{1}^{\prime}),\ldots,\textsf{merge}(x_{1},x_{q}^{\prime})],\\\
&&\qquad\ldots,\\\
&&\qquad[\textsf{merge}(x_{p},x_{1}^{\prime}),\ldots,\textsf{merge}(x_{p},x_{q}^{\prime})]\\\
&&]\\\ &=&[[x_{1,1},\ldots,x_{1,d}],\ldots,[x_{c,1},\ldots,x_{c,d}]]\\\
&=&\mathcal{I}^{\prime}([[x_{1,1},\ldots,x_{1,d}],\ldots,[x_{c,1},\ldots,x_{c,d}]])\\\
\end{array}$

By the definition of ptr, we know, for any
$x_{i,j}^{\prime\prime}\in\llbracket Q\times
Q^{\prime}\rrbracket_{\mathcal{D}}$, there exists a symbolic tuple
$t_{\textsf{ptr}(i),\textsf{ptr}(j)}^{\prime\prime}\in R^{\prime\prime}$ as
$x_{i,j}$ is a concatenation of $x_{i}\in Q$ and $x_{j}\in Q^{\prime}$.
Conversely, for any symbolic tuple $t_{i,j}^{\prime\prime}\in
R^{\prime\prime}-\llbracket Q\times Q^{\prime}\rrbracket_{\mathcal{D}}$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i,j}^{\prime\prime})=\bot$ because
$\mathcal{I}(\text{Del})(t_{i})\lor\mathcal{I}(\text{Del})(t_{j}^{\prime})=\bot$.
Therefore, $\mathcal{I}^{\prime}(R^{\prime\prime})=\llbracket Q\times
Q^{\prime}\rrbracket_{\mathcal{D}}$.

Let $\mathcal{D}^{\prime}=\mathcal{D}[o_{Q^{\prime\prime}}\mapsto\llbracket
Q\times Q^{\prime}\rrbracket_{\mathcal{D}}]$. For any $t_{i}\in R$ and
$t_{j}^{\prime}\in R^{\prime}$, let us discuss them in four cases.

    1. (a)

If
$\mathcal{I}(\text{Del})(t_{i})=\mathcal{I}(\text{Del})(t_{j}^{\prime})=\top$,
then, by the definition of $\mathcal{I}^{\prime}$, we have
$\mathcal{I}^{\prime}(\text{Del})(t_{i})=\mathcal{I}(\text{Del})(t_{i})=\top$
and
$\mathcal{I}^{\prime}(\text{Del})(t_{j}^{\prime})=\mathcal{I}(\text{Del})(t_{j}^{\prime})=\top$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i,j}^{\prime\prime})=\mathcal{I}(\text{Del})(t_{i})\lor\mathcal{I}(\text{Del})(t_{j}^{\prime})\\\
$$=\top$, $\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}(t_{i})]}$ and $\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}(t_{j}^{\prime})]}$,

$\begin{array}[]{rcl}\mathcal{I}^{\prime},\mathcal{D}^{\prime}&\models&(\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{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i})]}\\\
&&\qquad\land\land_{k=1}^{q}\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{j}^{\prime})]})\end{array}$

and

$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\text{Del}(t_{i})\lor\text{Del}(t_{j}^{\prime})\to\text{Del}(t_{i,j}^{\prime\prime})$

Thus,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi_{i,j}^{\prime\prime}$.

    2. (b)

If $\mathcal{I}(\text{Del})(t_{i})=\bot$ and
$\mathcal{I}(\text{Del})(t_{j}^{\prime})=\top$, then, by the definition of
$\mathcal{I}^{\prime}$, we have
$\mathcal{I}^{\prime}(\text{Del})(t_{i})=\mathcal{I}(\text{Del})(t_{i})=\bot$
and
$\mathcal{I}^{\prime}(\text{Del})(t_{j}^{\prime})=\mathcal{I}(\text{Del})(t_{j}^{\prime})=\top$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i,j}^{\prime\prime})=\mathcal{I}(\text{Del})(t_{i})\lor\mathcal{I}(\text{Del})(t_{j}^{\prime})\\\
$$=\top$, $\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}(t_{i})]}$ and $\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}(t_{j}^{\prime})]}$,

$\begin{array}[]{rcl}\mathcal{I}^{\prime},\mathcal{D}^{\prime}&\models&(\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{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i})]}\\\
&&\qquad\land\land_{k=1}^{q}\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{j}^{\prime})]})\end{array}$

and

$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\text{Del}(t_{i})\lor\text{Del}(t_{j}^{\prime})\to\text{Del}(t_{i,j}^{\prime\prime})$

Thus,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi_{i,j}^{\prime\prime}$.

    3. (c)

If $\mathcal{I}(\text{Del})(t_{i})=\top$ and
$\mathcal{I}(\text{Del})(t_{j}^{\prime})=\bot$, then, by the definition of
$\mathcal{I}^{\prime}$, we have
$\mathcal{I}^{\prime}(\text{Del})(t_{i})=\mathcal{I}(\text{Del})(t_{i})=\top$
and
$\mathcal{I}^{\prime}(\text{Del})(t_{j}^{\prime})=\mathcal{I}(\text{Del})(t_{j}^{\prime})=\bot$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i,j}^{\prime\prime})=\mathcal{I}(\text{Del})(t_{i})\lor\mathcal{I}(\text{Del})(t_{j}^{\prime})\\\
$$=\top$, $\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}(t_{i})]}$ and $\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}(t_{j}^{\prime})]}$,

$\begin{array}[]{rcl}\mathcal{I}^{\prime},\mathcal{D}^{\prime}&\models&(\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{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i})]}\\\
&&\qquad\land\land_{k=1}^{q}\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{j}^{\prime})]})\end{array}$

and

$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\text{Del}(t_{i})\lor\text{Del}(t_{j}^{\prime})\to\text{Del}(t_{i,j}^{\prime\prime})$

Thus,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi_{i,j}^{\prime\prime}$.

    4. (d)

If $\mathcal{I}(\text{Del})(t_{i})=\bot$ and
$\mathcal{I}(\text{Del})(t_{j}^{\prime})=\bot$, then, by the definition of
$\mathcal{I}^{\prime}$, we have
$\mathcal{I}^{\prime}(\text{Del})(t_{i})=\mathcal{I}(\text{Del})(t_{i})=\bot$
and
$\mathcal{I}^{\prime}(\text{Del})(t_{j}^{\prime})=\mathcal{I}(\text{Del})(t_{j}^{\prime})=\bot$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i,j}^{\prime\prime})=\mathcal{I}(\text{Del})(t_{i})\lor\mathcal{I}(\text{Del})(t_{j}^{\prime})\\\
$$=\bot$, $\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}(t_{i})]}$ and $\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}(t_{j}^{\prime})]}$,

$\begin{array}[]{rcl}\mathcal{I}^{\prime},\mathcal{D}^{\prime}&\models&(\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{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i})]}\\\
&&\qquad\land\land_{k=1}^{q}\llbracket
a_{k}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}=\llbracket
a_{k}^{\prime}\rrbracket_{\mathcal{D}^{\prime},[\mathcal{I}^{\prime}(t_{j}^{\prime})]})\end{array}$

and

$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\text{Del}(t_{i})\lor\text{Del}(t_{j}^{\prime})\to\text{Del}(t_{i,j}^{\prime\prime})$

Thus,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi_{i,j}^{\prime\prime}$.

Thus,
$\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}$
and Theorem 4.5 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}]$ 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.

By the inductive hypothesis, we have $\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$.

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_{j}^{\prime})\leftrightarrow\mathcal{I}(\text{Del})(t_{j}^{\prime})$,
$\mathcal{I}^{\prime}(t_{j}^{\prime})=\mathcal{I}(t_{j}^{\prime})$,
$\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})=\textsf{merge}(t_{i},t_{j}^{\prime})$
for $1\leq i\leq n$ and $1\leq j\leq m$,
$\mathcal{I}^{\prime}(t_{i,m+1}^{\prime\prime})=\textsf{merge}(t_{i},T_{\text{Null}})$
for $1\leq i\leq n$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i,j}^{\prime\prime})=\mathcal{I}(\text{Del})(t_{i})\lor\mathcal{I}(\text{Del})(t_{j}^{\prime})\lor\llbracket\phi\rrbracket_{\mathcal{D},[\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})]}$
for $1\leq i\leq n$ and
$\mathcal{I}^{\prime}(\text{Del})(t_{i,m+1}^{\prime\prime})=\mathcal{I}^{\prime}(\text{Del})(t_{i})\lor\neg\land_{j=1}^{m}\mathcal{I}^{\prime}(\text{Del})(t_{i,j}^{\prime\prime})$
for $1\leq i\leq n$.

Let $x_{i}\in\llbracket Q\rrbracket_{\mathcal{D}}$,
$x_{j}^{\prime}\in\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$ where $1\leq
i\leq c\leq n$, $1\leq j\leq d\leq m$, $c=|\llbracket
Q\rrbracket_{\mathcal{D}}|$ and $d=|\llbracket
Q^{\prime}\rrbracket_{\mathcal{D}}|$, then
$\mathcal{I}(\text{Del})(x_{i})=\mathcal{I}(\text{Del})(x_{j}^{\prime})=\bot$.
Also, by the semantics of foldl and append, we know

$\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{D}}&=&\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{D}}))\\\ &=&\textsf{foldl}(\lambda xs.\lambda
x.\textsf{append}(xs,\textsf{ite}(|v_{1}(x)|=0,v_{2}(x),v_{1}(x)),[],\vec{x}_{1:c}))\\\
&=&\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}(x_{1})|=0,v_{2}(x_{1}),v_{1}(x_{1}))],\vec{x}_{2:c}))\\\
&=&\ldots\\\ &=&[\\\
&&\quad\textsf{ite}(|v_{1}(x_{1})|=0,v_{2}(x_{1}),v_{1}(x_{1}))\\\
&&\quad\ldots\\\
&&\quad\textsf{ite}(|v_{1}(x_{c})|=0,v_{2}(x_{c}),v_{1}(x_{c}))\\\
&&]\end{array}$

For any entry
$\textsf{ite}(|v_{1}(x_{i})|=0,v_{2}(x_{i}),v_{1}(x_{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}(x_{i})|=0$ in two cases.

    1. (a)

If $|v_{1}(x_{i})|=0$ is true, then
$|\llbracket[x_{i}]\bowtie_{\phi}Q^{\prime}\rrbracket_{\mathcal{D}}|=0$ and
$\textsf{ite}(|v_{1}(x_{i})|=0,v_{2}(x_{i}),v_{1}(x_{i}))=v_{2}(x_{i})=[\textsf{merge}(x_{i},T_{\text{Null}})]$.
By the inductive case $Q^{\prime\prime}=Q\times Q^{\prime}$, we know
$\llbracket[x_{i}]\bowtie_{\phi}Q^{\prime}\rrbracket_{\mathcal{D}}=\sigma_{\phi}(\llbracket[x_{i}]\times
Q^{\prime}\rrbracket_{\mathcal{D}})=\sigma_{\phi}(\llbracket[x_{i}]\times[x_{1}^{\prime},\ldots,x_{d}^{\prime}]\rrbracket_{\mathcal{D}})=\sigma_{\phi}([x_{i,1}^{\prime\prime},\ldots,x_{i,d}^{\prime\prime}])$
where
$\mathcal{I}(\text{Del})(x_{i})=\mathcal{I}(\text{Del})(x_{j}^{\prime})=\bot$.
Therefore, for any $1\leq j\leq d$,
$|\llbracket[x_{i}]\bowtie_{\phi}Q^{\prime}\rrbracket_{\mathcal{D}}|=0\Leftrightarrow\llbracket\phi\rrbracket_{\mathcal{D},[x_{i,j}^{\prime\prime}]}\neq\top$
by Lemma D.1, $\mathcal{I}^{\prime}(\text{Del})(x_{i,j}^{\prime\prime})=\top$
and $\mathcal{I}^{\prime}(\text{Del})(x_{i,c+1}^{\prime\prime})=\bot$,
Further, for $x_{i}\in\llbracket Q\rrbracket_{\mathcal{D}}$ and
$x_{j}^{\prime}\in\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$, there exist
two symbolic tuples $t_{\textsf{ptr}(i)}\in R$ and
$t_{\textsf{ptr}(j)}^{\prime}\in R^{\prime}$ s.t.
$\mathcal{I}(t_{\textsf{ptr}(i)})=x_{i}$,
$\mathcal{I}(t_{\textsf{ptr}(j)}^{\prime})=x_{j}^{\prime}$ and
$\mathcal{I}(\text{Del})(x_{i})=\mathcal{I}(\text{Del})(t_{\textsf{ptr}(i)})=\mathcal{I}(\text{Del})(x_{j}^{\prime})=\mathcal{I}(\text{Del})(t_{\textsf{ptr}(j)}^{\prime})=\bot$.
Therefore,
$\mathcal{I}^{\prime}(t_{\textsf{ptr}(i),m+1}^{\prime\prime})=\textsf{merge}(x_{i},T_{\text{Null}})$
and all tuples $t_{\textsf{ptr}(i),j}^{\prime\prime}$ are deleted where $1\leq
j\leq m$, i.e.,
$\land_{j=1}^{m}\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i),j}^{\prime\prime})=\top$
and
$\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i),m+1}^{\prime\prime})=\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i)})\lor\neg\land_{j=1}^{m}\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i),j}^{\prime\prime})=\bot$.

    2. (b)

If $|v_{1}(x_{i})|=0$ is false, then
$|\llbracket[x_{i}]\bowtie_{\phi}Q^{\prime}\rrbracket_{\mathcal{D}}|\neq 0$
and
$\textsf{ite}(|v_{1}(x_{i})|=0,v_{2}(x_{i}),v_{1}(x_{i}))=v_{2}(x_{i})=[[x_{i,1}^{\prime\prime},\ldots,x_{i,c}^{\prime\prime}]]$.
By the inductive case $Q^{\prime\prime}=Q\times Q^{\prime}$, we know
$\llbracket[x_{i}]\bowtie_{\phi}Q^{\prime}\rrbracket_{\mathcal{D}}=\sigma_{\phi}(\llbracket[x_{i}]\times
Q^{\prime}\rrbracket_{\mathcal{D}})=\sigma_{\phi}([x_{i,1}^{\prime\prime},\ldots,x_{i,d}^{\prime\prime}])$.
Therefore,
$|\llbracket[x_{i}]\bowtie_{\phi}Q^{\prime}\rrbracket_{\mathcal{D}}|\neq
0\Leftrightarrow\llbracket\phi\rrbracket_{\mathcal{D},[x_{i,j}^{\prime\prime}]}=\top$
for some $1\leq j\leq d$ by Lemma D.1,
$\mathcal{I}^{\prime}(\text{Del})(x_{i,c+1}^{\prime\prime})=\top$. Further,
for $x_{i}\in\mathcal{I}(R)$ and $x_{j}^{\prime}\in\mathcal{I}(R^{\prime})$,
there exist two symbolic tuples $t_{\textsf{ptr}(i)}\in R$ and
$t_{\textsf{ptr}(j)}^{\prime}\in R^{\prime}$ s.t.
$\mathcal{I}(t_{\textsf{ptr}(i)})=x_{i}$,
$\mathcal{I}(t_{\textsf{ptr}(j)}^{\prime})=x_{j}^{\prime}$ and
$\mathcal{I}(\text{Del})(t_{\textsf{ptr}(i)})=\mathcal{I}(\text{Del})(x_{i})=\mathcal{I}(\text{Del})(t_{\textsf{ptr}(j)}^{\prime})=\mathcal{I}(\text{Del})(x_{j}^{\prime})=\bot$.
Therefore, we have
$\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i),m+1}^{\prime\prime})=\top$
and some tuples $t_{\textsf{ptr}(i),j}^{\prime\prime}$ remain alive, i.e.,
$\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i),\textsf{ptr}(j)}^{\prime\prime})=\bot$
for some $1\leq j\leq m$ and
$\mathcal{I}^{\prime}(t_{\textsf{ptr}(i),\textsf{ptr}(j)}^{\prime\prime})=x_{i,j}^{\prime\prime}$.

Besides 7(a) and 7(b), we know, for any tuple $t\in
R^{\prime\prime}-\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{D}}$,
$\mathcal{I}^{\prime}(\text{Del})(t)=\top$. Thus,
$\mathcal{I}^{\prime}(R^{\prime\prime})=\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{D}}$.

Let $\mathcal{D}^{\prime}=\mathcal{D}[o_{Q^{\prime\prime}}\mapsto\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{D}}]$.
$T_{\text{Null}}(A)$ denote a tuple that has the attributes from $A$ but all
their values are Null. For instance, assume $A=[\text{"a"},\text{"b"}]$, then
$T_{\text{Null}}(A)=[(\text{"a"},\text{Null}),$ $(\text{"b"},\text{Null})]$.
By the semantics of merge and the definition of $T_{\text{Null}}$,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi_{j}^{\prime}$ and,
therefore,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi\land\land_{j=1}^{m}\Phi_{j}^{\prime}$

Hence, Theorem 4.5 for the inductive case
$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 can find a $\mathcal{I}^{\prime}$ s.t.
$\mathcal{I}^{\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})=\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{D}}$
and a $\mathcal{D}^{\prime}$ s.t.
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi$.

  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$ has symbolic tuples
$[t_{1,1}^{\prime\prime},\ldots,t_{n,m}^{\prime\prime},t_{n+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.

By the inductive hypothesis, we have $\mathcal{I},\mathcal{D}\models\Phi$,
$\mathcal{I}(R)=\llbracket Q\rrbracket_{\mathcal{D}}$,
$\mathcal{I}(R^{\prime})=\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$,
$\mathcal{I}([t_{1,1}^{\prime\prime},\ldots,$
$t_{n,m}^{\prime\prime},t_{n+1,1}^{\prime\prime},\ldots,t_{n+1,m}^{\prime\prime}])=\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{D}}$.

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_{j}^{\prime})\leftrightarrow\mathcal{I}(\text{Del})(t_{j}^{\prime})$,
$\mathcal{I}^{\prime}(t_{i})=\mathcal{I}(t_{i})$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i,j}^{\prime\prime})\leftrightarrow\mathcal{I}(\text{Del})(t_{i,j}^{\prime\prime})$
for $1\leq i\leq n$ and $1\leq j\leq m+1$,
$\mathcal{I}^{\prime}(t_{i,j}^{\prime\prime})=\mathcal{I}(t_{i,j}^{\prime\prime})$
for $1\leq i\leq n$ and $1\leq j\leq m+1$,
$\mathcal{I}^{\prime}(\text{Del})(t_{n+1,j}^{\prime\prime})\leftrightarrow(\mathcal{I}(\text{Del})(t_{j}^{\prime})\lor\neg\land_{i=1}^{n}\mathcal{I}(\text{Del})(t_{i,j}^{\prime\prime}))$
for $1\leq j\leq m$,
$\mathcal{I}^{\prime}(t_{n+1,j}^{\prime\prime})=\textsf{merge}(T_{\text{Null}},t_{j}^{\prime})$
for $1\leq j\leq m$.

Let $x_{j}^{\prime}\in\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$ where
$1\leq j\leq c\leq m$ and $c=|\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}|$,
then we have $x_{j}^{\prime}\in\mathcal{I}(Q^{\prime})$ because
$\mathcal{I}(R^{\prime})=\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$,
$\mathcal{I}(\text{Del})(x_{j}^{\prime})=\bot$. For any tuple
$x_{j}^{\prime}\in\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$, we have a
symbolic tuple $t_{\textsf{ptr}(j)}^{\prime}$ s.t.
$\mathcal{I}(t_{\textsf{ptr}(j)}^{\prime})=\mathcal{I}(x_{j}^{\prime})$ and
$\mathcal{I}(\text{Del})(t_{\textsf{ptr}(j)}^{\prime})=\bot$ by the definition
of $\mathcal{I}^{\prime}$. By the semantics of filter, we know
$|v|\leq|\llbracket Q\rrbracket_{\mathcal{D}}|$. Also, for any tuple
$x_{j}^{\prime}\in\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$,
$\textsf{merge}(T_{\text{Null}},x_{j}^{\prime})$ exists iff $|\llbracket
Q\bowtie_{\phi}[x_{j}^{\prime}]\rrbracket_{\mathcal{D}}|=0$. Therefore,
$\textsf{map}(v,\lambda
x.\textsf{merge}(T_{\text{Null}},x))=\mathcal{I}^{\prime}([t_{n+1,1}^{\prime\prime},\ldots,t_{n+1,m}^{\prime\prime}])$
by Figure 18. Furthermore, 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\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{D}}&=&\textsf{append}(\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{D}},\textsf{map}(v,\lambda
x.\textsf{merge}(T_{\text{Null}},x)))\\\
&=&\textsf{append}(\mathcal{I}^{\prime}([t_{1,1}^{\prime\prime},\ldots,t_{n,m+1}^{\prime\prime}]),\mathcal{I}^{\prime}([t_{n+1,1}^{\prime\prime},\ldots,t_{n+1,m}^{\prime\prime}]))\\\
&=&\mathcal{I}^{\prime}(R^{\prime\prime})\end{array}$

by the semantics of map.

Let $\mathcal{D}^{\prime}=\mathcal{D}[o_{Q^{\prime\prime}}\mapsto\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{D}}]$.
By the semantics of merge and the definition of $T_{\text{Null}}$,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi_{j}^{\prime}$ and,
therefore,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi\land\land_{j=1}^{m}\Phi_{j}^{\prime}$

Hence, Theorem 4.5 for the inductive case
$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
$\mathcal{I}(R)=\llbracket Q\rrbracket_{\mathcal{D}}$.

Take $\mathcal{I}^{\prime}$ s.t.
$\mathcal{I}^{\prime}(\text{Del})(t_{i})\leftrightarrow\mathcal{I}^{\prime}(\text{Del})(t_{i})$,
$\mathcal{I}^{\prime}(t_{i})=\mathcal{I}^{\prime}(t_{i})$,
$\mathcal{I}^{\prime}(\text{Del})(t_{1})\leftrightarrow\mathcal{I}^{\prime}(\text{Del})(t_{1})$,
$\mathcal{I}^{\prime}(\text{Del})\\\
$$(t_{i}^{\prime})\leftrightarrow\land_{j=1}^{i-1}(\mathcal{I}(t_{i})=\mathcal{I}(t_{j})\land\neg\mathcal{I}(\text{Del})(t_{j}))$
for $2\leq j\leq i$,
$\mathcal{I}^{\prime}(t_{i}^{\prime})=\mathcal{I}(t_{i})$.

For any tuples $x_{i}^{\prime}$ and $x_{j}^{\prime}$ in
$\llbracket\text{Distinct}(Q)\rrbracket_{\mathcal{D}}$ s.t.
$x_{i}^{\prime}\neq x_{j}^{\prime}$, we have two symbolic tuples
$t_{\textsf{ptr}(i)}^{\prime}$ and $t_{\textsf{ptr}(j)}^{\prime}$ in $R$ s.t.
$x_{i}^{\prime}=\mathcal{I}(t_{\textsf{ptr}(i)}^{\prime})$ and
$\mathcal{I}(\text{Del})(t_{\textsf{ptr}(i)}^{\prime})=\bot$,
$x_{j}^{\prime}=\mathcal{I}(t_{\textsf{ptr}(j)}^{\prime})$ and
$\mathcal{I}(\text{Del})(t_{\textsf{ptr}(j)}^{\prime})=\bot$. Moreover, if
$t_{i}$ is a unique symbolic tuple in $R$, then
$\mathcal{I}^{\prime}(t_{i}^{\prime})=\mathcal{I}(t_{i})$ and
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime})=\mathcal{I}(\text{Del})(t_{i})=\bot$
where $t_{i}^{\prime}\in R^{\prime}$ by the definition of
$\mathcal{I}^{\prime}$; otherwise, there exist some tuples
$[t_{i_{1}},\ldots,t_{i_{l}}]$ s.t. $\mathcal{I}(\text{Del})(t_{i_{j}})=\bot$
and $t_{i_{j}}\in R$ for $1\leq j\leq k$, and
$\mathcal{I}(t_{i_{j}})=\mathcal{I}(t_{i_{k}})$ for $1\leq j\neq k\leq k$.
Further, by the definition of
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime})=\land_{j=1}^{i}\mathcal{I}(t_{i})=\mathcal{I}(t_{j})$,
only the first symbolic tuple $t_{i_{1}}$ will be retained in $R^{\prime}$ and
the other tuples $[t_{i_{2}},\ldots,t_{i_{l}}]$ will be removed, i.e.,
$\mathcal{I}^{\prime}(t_{i_{1}})=\top$ and
$\mathcal{I}^{\prime}(t_{i_{j}})=\top$ for $2\leq j\leq l$. Therefore,
$\mathcal{I}^{\prime}(R^{\prime})=\llbracket\text{Distinct}(Q)\rrbracket_{\mathcal{D}}$.

Let
$\mathcal{D}^{\prime}=\mathcal{D}[o_{Q^{\prime}}\mapsto\text{Distinct}(Q)]$.
By the definition of $\mathcal{I}^{\prime}$, we know
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models
t_{1}^{\prime}=t_{1}\land\land_{i=2}^{n}(t_{i}\in\vec{t}_{1:i-1}\to\text{Del}(t_{i}^{\prime})\land
t_{i}\not\in\vec{t}_{1:i-1}\to t_{i}^{\prime}=t_{i})$ and, therefore,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi\land\Phi^{\prime}$.

Hence, Theorem 4.5 for the inductive case $\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\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
$\mathcal{I},\mathcal{D}\models\Phi\land\Phi^{\prime}$,
$\mathcal{I}(R)=\llbracket\text{Distinct}(Q)\rrbracket_{\mathcal{D}}$ and
$\mathcal{I}(R^{\prime})=\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$.

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}^{\prime}(t_{j})$,
$\mathcal{I}^{\prime}(\text{Del})(t_{j}^{\prime})\leftrightarrow\mathcal{I}^{\prime}(\text{Del})(t_{j})$,
$\mathcal{I}^{\prime}(t_{i}^{\prime\prime})=\mathcal{I}(t_{i})$ and
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime\prime})\leftrightarrow\mathcal{I}(\text{Del})(t_{i})\lor\neg\lor_{j=1}^{m}(\mathcal{I}(t_{i})=\mathcal{I}(t_{j}^{\prime})\land\neg\mathcal{I}(\text{Del})(t_{j}^{\prime}))$.

For any tuple $x_{i}\in\llbracket\text{Distinct}(Q)\rrbracket_{\mathcal{D}}$,
let us discuss $x_{i}\in\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$ in two
cases.

    1. (a)

If $x_{i}\in\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$ is true, then we
can find at least one tuple $x_{j}^{\prime}\in\llbracket
Q^{\prime}\rrbracket_{\mathcal{D}}$ and its corresponding symbolic tuple
$t_{\textsf{ptr}(j)}^{\prime}\in R^{\prime}$ s.t.
$\mathcal{I}(\text{Del})(x_{i})=\mathcal{I}(\text{Del})(x_{j}^{\prime})=\mathcal{I}(\text{Del})(t_{\textsf{ptr}(j)}^{\prime})=\bot$
and
$\mathcal{I}(x_{i})=\mathcal{I}(x_{j}^{\prime})=\mathcal{I}(t_{\textsf{ptr}(j)}^{\prime})$.
By the definition of $\mathcal{I}^{\prime}$ and the semantics of filter, we
know there exist two symbolic tuples $t_{\textsf{ptr}(i)}^{\prime\prime}\in
R^{\prime\prime}$ and $t_{\textsf{ptr}(i)}\in R$ s.t.
$\mathcal{I}(\text{Del})(t_{\textsf{ptr}(i)})=\bot$,
$\mathcal{I}^{\prime}(t_{\textsf{ptr}(i)}^{\prime\prime})=\mathcal{I}(t_{\textsf{ptr}(i)})=\mathcal{I}(x_{i})$,
$\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i)}^{\prime\prime})=\mathcal{I}(\text{Del})(t_{\textsf{ptr}(i)})\lor\neg\lor_{j=1}^{m}(\mathcal{I}(t_{\textsf{ptr}(i)})=\mathcal{I}(t_{j}^{\prime})\land\neg\mathcal{I}(\text{Del})(t_{j}^{\prime}))=\bot$.

    2. (b)

If $x_{i}\in\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$ is false, then
$x_{i}$ will be removed by the semantics of filter. Assume the symbolic tuple
$t_{\textsf{ptr}(i)}\in R$ is corresponding to $x_{i}$, i.e.,
$\mathcal{I}(t_{\textsf{ptr}(i)})=\mathcal{I}(x_{i})$ and
$\mathcal{I}(\text{Del})(t_{\textsf{ptr}(i)})=\mathcal{I}(\text{Del})(x_{i})=\bot$,
then
$\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i)}^{\prime\prime})=\mathcal{I}(\text{Del})(t_{i})\lor\neg\lor_{j=1}^{m}(\mathcal{I}(t_{\textsf{ptr}(i)})=\mathcal{I}(t_{j}^{\prime})\land\neg\mathcal{I}(\text{Del})\\\
$$(t_{j}^{\prime}))=\top$.

By 11(a) and 11(b), we have two symbolic tuples $t_{\textsf{ptr}(i)}\in R$ and
$t_{\textsf{ptr}(i)}^{\prime\prime}\in R^{\prime\prime}$ for any tuple
$x_{i}\in\llbracket Q\cap Q^{\prime}\rrbracket_{\mathcal{D}}$ s.t.
$\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i)}^{\prime\prime})=\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i)})=\bot$
and
$\mathcal{I}^{\prime}(t_{\textsf{ptr}(i)}^{\prime\prime})=\mathcal{I}^{\prime}(t_{\textsf{ptr}(i)})$
iff
$\mathcal{I}(\text{Del})(t_{\textsf{ptr}(i)})\lor\neg\lor_{j=1}^{m}(\mathcal{I}(t_{a})=\mathcal{I}(t_{j}^{\prime})\land\neg\mathcal{I}(\text{Del})(t_{j}^{\prime}))$
is false. For the other tuple $t^{\prime\prime}\in R^{\prime\prime}-\llbracket
Q\cap Q^{\prime}\rrbracket_{\mathcal{D}}$,
$\mathcal{I}^{\prime}(\text{Del})(t^{\prime\prime})=\top$ because
$\mathcal{I}^{\prime}(\text{Del})(t)=\top$ or
$\mathcal{I}^{\prime}(t)\not\in\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$.
Therefore, $\mathcal{I}^{\prime}(R^{\prime\prime})=\llbracket Q\cap
Q^{\prime}\rrbracket_{\mathcal{D}}$.

Let $\mathcal{D}^{\prime}=\mathcal{D}[o_{Q^{\prime\prime}}\mapsto\llbracket
Q\cap Q^{\prime}\rrbracket_{\mathcal{D}}]$. By the definition of
$\mathcal{I}^{\prime}$, $\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models
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})$ and,
therefore,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi\land\Phi^{\prime}\land\land_{i=1}^{n}\Phi^{\prime\prime}_{i}$

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

  12. (12)

Inductive case: $Q^{\prime\prime}=Q\setminus 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\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\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
$\mathcal{I}(R)=\llbracket\text{Distinct}(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}^{\prime}(t_{j})$,
$\mathcal{I}^{\prime}(\text{Del})(t_{j}^{\prime})\leftrightarrow\mathcal{I}^{\prime}(\text{Del})(t_{j})$,
$\mathcal{I}^{\prime}(t_{i}^{\prime\prime})=\mathcal{I}(t_{i})$ and
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime\prime})\leftrightarrow\mathcal{I}(\text{Del})(t_{i})\lor\lor_{j=1}^{m}(\mathcal{I}(t_{i})=\mathcal{I}(t_{j}^{\prime})\land\neg\mathcal{I}(\text{Del})\\\
$$(t_{j}^{\prime}))$

For any tuple $x_{i}\in\llbracket\text{Distinct}(Q)\rrbracket_{\mathcal{D}}$,
let us discuss the predicate $x_{i}\in\llbracket
Q^{\prime}\rrbracket_{\mathcal{D}}$ in two cases.

    1. (a)

If the predicate $x_{i}\in\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$ is
true, then we can find at least one tuple $x_{j}^{\prime}\in\llbracket
Q^{\prime}\rrbracket_{\mathcal{D}}$ and its corresponding symbolic tuple
$t_{\textsf{ptr}(j)}^{\prime}$ s.t.
$\mathcal{I}(\text{Del})(x_{i})=\mathcal{I}(\text{Del})(x_{j}^{\prime})=\mathcal{I}(\text{Del})(x_{\textsf{ptr}(j)}^{\prime})=\bot$
and $x_{i}=x_{j}^{\prime}=\mathcal{I}(t_{\textsf{ptr}(j)}^{\prime})$. By the
definition of $\mathcal{I}^{\prime}$ and the semantics of filter, we have the
symbolic tuples $t_{\textsf{ptr}(i)}^{\prime\prime}\in R^{\prime\prime}$ and
$t_{\textsf{ptr}(i)}\in R$ s.t.
$\mathcal{I}(\text{Del})(t_{\textsf{ptr}(i)})=\bot$,
$\mathcal{I}^{\prime}(t_{\textsf{ptr}(i)}^{\prime\prime})=\mathcal{I}(t_{\textsf{ptr}(i)})=x_{i}$,
$\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i)}^{\prime\prime})=\mathcal{I}(\text{Del})(t_{\textsf{ptr}(i)})\lor\lor_{j=1}^{m}(\mathcal{I}(t_{\textsf{ptr}(i)})=\mathcal{I}(t_{j}^{\prime})\land\neg\mathcal{I}(\text{Del})(t_{j}^{\prime}))=\top$.

    2. (b)

If the predicate $x_{i}\in\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$ is
false, then $x_{i}$ will be retained by the semantics of filter. Assume the
symbolic tuple $t_{\textsf{ptr}(i)}\in R$ is corresponding to $x_{i}$, i.e.,
$\mathcal{I}(t_{\textsf{ptr}(i)})=\mathcal{I}(x_{i})$ and
$\mathcal{I}(\text{Del})(t_{a})=\mathcal{I}(\text{Del})(x_{i})$, then
$\mathcal{I}^{\prime}(t_{\textsf{ptr}(i)}^{\prime\prime})=\neg\mathcal{I}(t_{i})\land\neg\lor_{j=1}^{m}(\mathcal{I}(t_{\textsf{ptr}(i)})=\mathcal{I}(t_{j}^{\prime})\land\neg\mathcal{I}(\text{Del})(t_{j}^{\prime}))=\bot$.

By 12(a) and 12(b), we have two symbolic tuples $t_{i}\in R$ and
$t_{i}^{\prime\prime}\in R^{\prime\prime}$ for any tuple $x\in\llbracket
Q\setminus Q^{\prime}\rrbracket_{\mathcal{D}}$ s.t.
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime\prime})=\mathcal{I}^{\prime}(\text{Del})(t_{i})=\bot$
and $\mathcal{I}^{\prime}(t_{i}^{\prime\prime})=\mathcal{I}^{\prime}(t_{i})$
iff
$\mathcal{I}(\text{Del})(t_{i})\lor\lor_{j=1}^{m}(\mathcal{I}(t_{i})=\mathcal{I}(t_{j}^{\prime})\land\neg\mathcal{I}(\text{Del})(t_{j}^{\prime}))$
is false. For the other tuple $t^{\prime\prime}\in
R^{\prime\prime}\setminus\llbracket Q\setminus
Q^{\prime}\rrbracket_{\mathcal{D}}$,
$\mathcal{I}^{\prime}(\text{Del})(t^{\prime\prime})=\top$ because
$\mathcal{I}^{\prime}(\text{Del})(t)=\top$ or
$\mathcal{I}^{\prime}(t)\in\llbracket Q^{\prime}\rrbracket_{\mathcal{D}}$.
Therefore, $\mathcal{I}^{\prime}(R^{\prime\prime})=\llbracket Q\setminus
Q^{\prime}\rrbracket_{\mathcal{D}}$.

Let $\mathcal{D}^{\prime}=\mathcal{D}[o_{Q^{\prime\prime}}\mapsto\llbracket
Q\setminus Q^{\prime}\rrbracket_{\mathcal{D}}]$. By the definition of
$\mathcal{I}^{\prime}$, $\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models
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})$ and, therefore,
$\mathcal{I}^{\prime},\mathcal{D}^{\prime}\models\Phi\land\Phi^{\prime}\land\land_{i=1}^{n}\Phi^{\prime\prime}_{i}$

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

  13. (13)

Inductive case: $Q^{\prime\prime}=Q-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-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.

Let the Paired function only register in $\mathcal{I}$. 161616We slightly
abuse interpretation here since the Paired function only works in this case.
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})$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime\prime})\leftrightarrow\mathcal{I}(\text{Del})(t_{i})\lor\lor_{j=1}^{m}\mathcal{I}^{\prime}(\text{Paired}(i,j))$.

By definition of $\llbracket Q-Q^{\prime}\rrbracket_{\mathcal{D}}$, let
$xs_{k}=\textsf{ite}(x^{\prime}\in xs_{k-1},xs_{k-1}-x,xs_{k-1})$ and
$xs_{0}=\llbracket Q\rrbracket_{\mathcal{D}}$. Obviously, the value of
$xs_{k}$ will be updated iff $x_{j}^{\prime}\in xs_{k-1}$. Let us discuss the
predicate $x_{j}^{\prime}\in xs_{k-1}$ in two cases.

    1. (a)

If the predicate $x_{j}^{\prime}\in xs_{k-1}$ is true, then we have two
corresponding symbolic tuples $t_{i}\in R$ and
$t_{\textsf{ptr}(j)}^{\prime}\in R^{\prime}$ s.t.
$\mathcal{I}(t_{i})=\mathcal{I}(t_{\textsf{ptr}(j)}^{\prime})=x_{j}^{\prime}\in
xs_{k-1}$ and
$\mathcal{I}(\text{Del})(t_{i})=\mathcal{I}(\text{Del})(t_{\textsf{ptr}(j)}^{\prime})=\mathcal{I}(\text{Del})(x_{j}^{\prime})=\bot$.
Therefore, $\text{Paired}(i,j)=\top$ and
$\text{Paired}(i,l)=\text{Paired}(k,j)=\bot$ for any $1\leq k\neq i\leq n$ and
$1\leq l\neq j\leq m$ to follow the semantics of EXCEPT ALL. Further, we know
$xs_{k}=xs_{k-1}-x$ and
$\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i)}^{\prime\prime})=\top$.

    2. (b)

If the predicate $x_{j}^{\prime}\in xs_{k-1}$ is false, then we have a
corresponding symbolic tuple $t_{\textsf{ptr}(j)}^{\prime}\in R^{\prime}$ s.t.
$\mathcal{I}(t_{\textsf{ptr}(j)}^{\prime})=x_{j}^{\prime}\not\in xs_{k-1}$,
$\mathcal{I}(\text{Del})(t_{\textsf{ptr}(j)}^{\prime})=\mathcal{I}(\text{Del})(x_{j})=\bot$.
Also, by the definition of the Paired function, we know
$\text{Paired}(i,{\textsf{ptr}(j)})=\bot$ where $1\leq i\leq n$ because
$t_{\textsf{ptr}(j)}^{\prime}$ is never paired with previously paired tuples
in $R$ and $\mathcal{I}(x_{i})\neq\mathcal{I}(t_{\textsf{ptr}(j)}^{\prime})$.
Therefore, we have $xs_{k}=xs_{k-1}$.

Let $xs^{\prime}=[x_{i_{1}},\ldots,x_{i_{l}}]$ be the deleted tuples from
$\llbracket Q\rrbracket_{\mathcal{D}}$, $i_{k}$ the real index in $\llbracket
Q\rrbracket_{\mathcal{D}}$ and $1\leq k\leq l$. By 13(a) and 13(b), we have
corresponding symbolic tuples $t_{\textsf{ptr}(i_{k})}^{\prime\prime}\in
R^{\prime\prime}$ s.t.
$\mathcal{I}^{\prime}(\text{Del})(t_{\textsf{ptr}(i_{k})}^{\prime\prime})=\top$.
Further, for any symbolic tuple $t_{i}\in\llbracket
Q\rrbracket_{\mathcal{D}}-xs^{\prime}$,
$\mathcal{I}^{\prime}(\text{Del})(t_{i}^{\prime\prime})=\bot$ and
$\mathcal{I}^{\prime}(t_{i}^{\prime\prime})=\mathcal{I}(t_{i})$; for the
resting symbolic tuples $t\in R^{\prime}-\llbracket
Q\rrbracket_{\mathcal{D}}$,
$\mathcal{I}^{\prime}(\text{Del})(t^{\prime\prime})=\top$ because
$t\not\in\llbracket Q\rrbracket_{\mathcal{D}}$. Therefore,
$\mathcal{I}^{\prime}(R^{\prime\prime})=\llbracket
Q-Q^{\prime}\rrbracket_{\mathcal{D}}$.

Let $\mathcal{D}^{\prime}=\mathcal{D}[o_{Q^{\prime\prime}}\mapsto\llbracket
Q-Q^{\prime}\rrbracket_{\mathcal{D}}]$ For any tuple $xs_{i}^{\prime}\in