* Kobayashi and Ong (2009) Naoki Kobayashi and C.-H. Luke Ong. 2009.  A Type System Equivalent to the Modal Mu-Calculus Model Checking of Higher-Order Recursion Schemes. In _Logic in Computer Science, LICS 2009_. IEEE Computer Society, 179–188.
  * Miller and Nadathur (2012) Dale Miller and Gopalan Nadathur. 2012.  _Programming with Higher-Order Logic_.  Cambridge University Press.  https://doi.org/10.1017/CBO9781139021326
  * Miller et al. (1991) Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. 1991.  Uniform proofs as a foundation for logic programming.  _Annals of Pure and Applied Logic_ 51, 1 (1991), 125–157.  https://doi.org/10.1016/0168-0072(91)90068-W
  * Mokhov et al. (2019) Andrey Mokhov, Georgy Lukyanov, Simon Marlow, and Jeremie Dimino. 2019.  Selective applicative functors.  _Proceedings of the ACM on Programming Languages_ 3, ICFP (2019), 1–29.
  * Muller and Schupp (1987) David E. Muller and Paul E. Schupp. 1987.  Alternating automata on infinite trees.  _Theoretical Computer Science_ 54, 2 (1987), 267–276.  https://doi.org/10.1016/0304-3975(87)90133-2
  * Nagaya and Toyama (2002) Takashi Nagaya and Yoshihito Toyama. 2002.  Decidability for Left-Linear Growing Term Rewriting Systems.  _Information and Computation_ 178, 2 (2002), 499–514.  https://doi.org/10.1006/inco.2002.3157
  * Neatherway et al. (2012) Robin P. Neatherway, Steven J. Ramsay, and C.-H. Luke Ong. 2012\.  A Traversal-Based Algorithm for Higher-Order Model Checking.  _SIGPLAN Not._ 47, 9 (Sep 2012), 353–364.  https://doi.org/10.1145/2398856.2364578
  * Nielson et al. (2002) Flemming Nielson, Hanne Riis Nielson, and Helmut Seidl. 2002\.  Normalizable Horn clauses, strongly recognizable relations, and Spi. In _International Static Analysis Symposium_. Springer, 20–35.
  * Ong (2006) C.-H. Luke Ong. 2006\.  On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In _21th IEEE Symposium on Logic in Computer Science (LICS 2006), 12-15 August 2006, Seattle, WA, USA, Proceedings_. 81–90.  https://doi.org/10.1109/LICS.2006.38
  * Ong and Wagner (2019) C.-H. Luke Ong and Dominik Wagner. 2019.  HoCHC: A Refutationally Complete and Semantically Invariant System of Higher-order Logic Modulo Theories. In _2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)_. 1–14.  https://doi.org/10.1109/LICS.2019.8785784
  * Ramsay (2014) Steven J. Ramsay. 2014\.  _Intersection types and higher-order model checking_.  Ph.D. Dissertation. Oxford University, UK.
  * Ramsay et al. (2014) Steven J. Ramsay, Robin P. Neatherway, and C.-H. Luke Ong. 2014\.  A Type-Directed Abstraction Refinement Approach to Higher-Order Model Checking. In _Principles of Programming Languages, POPL’14_. ACM, 61–72.
  * Rehof and Urzyczyn (2011) Jakob Rehof and Paweł Urzyczyn. 2011.  Finite Combinatory Logic with Intersection Types. In _Typed Lambda Calculi and Applications_ , C.-H. Luke Ong (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 169–183.
  * Rondon et al. (2008) Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala. 2008\.  Liquid types. In _Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008_. 159–169.
  * Salvati and Walukiewicz (2016) Sylvain Salvati and Igor Walukiewicz. 2016.  Simply typed fixpoint calculus and collapsible pushdown automata.  _Math. Struct. Comput. Sci._ 26, 7 (2016), 1304–1350.  https://doi.org/10.1017/S0960129514000590
  * Terao and Kobayashi (2014) Taku Terao and Naoki Kobayashi. 2014.  A ZDD-based efficient higher-order model checking algorithm. In _Asian Symposium on Programming Languages and Systems_. Springer, 354–371.
  * Terauchi (2010) Tachio Terauchi. 2010\.  Dependent types from counterexamples. In _Proceedings of the 37th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2010, Madrid, Spain, January 17-23, 2010_. 119–130.
  * Teucke and Weidenbach (2017) Andreas Teucke and Christoph Weidenbach. 2017.  Decidability of the Monadic Shallow Linear First-Order Fragment with Straight Dismatching Constraints. In _Automated Deduction – CADE 26_ , Leonardo de Moura (Ed.). Springer International Publishing, Cham, 202–219.
  * Unno and Kobayashi (2009) Hiroshi Unno and Naoki Kobayashi. 2009.  Dependent type inference with interpolants. In _Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7-9, 2009, Coimbra, Portugal_. 277–288.
  * Vazou et al. (2015) Niki Vazou, Alexander Bakst, and Ranjit Jhala. 2015\.  Bounded refinement types. In _Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, Vancouver, BC, Canada, September 1-3, 2015_. 48–61.
  * Vazou et al. (2013) Niki Vazou, Patrick Maxim Rondon, and Ranjit Jhala. 2013\.  Abstract Refinement Types. In _Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings_. 209–228.
  * Viswanathan and Viswanathan (2004) Mahesh Viswanathan and Ramesh Viswanathan. 2004.  A Higher Order Modal Fixed Point Logic. In _CONCUR 2004 - Concurrency Theory_ , Philippa Gardner and Nobuko Yoshida (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 512–528.
  * Weidenbach (1999) Christoph Weidenbach. 1999\.  Towards an Automatic Analysis of Security Protocols in First-Order Logic. In _Automated Deduction — CADE-16_. Springer Berlin Heidelberg, Berlin, Heidelberg, 314–328.
  * Zhu and Jagannathan (2013) He Zhu and Suresh Jagannathan. 2013.  Compositional and Lightweight Dependent Type Inference for ML. In _Verification, Model Checking, and Abstract Interpretation, 14th International Conference, VMCAI 2013, Rome, Italy, January 20-22, 2013. Proceedings_. 295–314.

##  Appendix A Semantics

Our fragments use the standard semantics of HOL. An explicit denotational
semantics is provided below.

##### Interpretation of types.

Let $\Sigma$ be a constructor signature. A $\Sigma$-_structure_ $\mathcal{A}$
assigns a non-empty set $A_{\iota}$ to the semantic domain of $\iota$ and an
element $c^{a}\in\llbracket\gamma\rrbracket$ to each constructor
$a:\gamma\in\Sigma$, with types interpreted as:

$\llbracket\iota\rrbracket:=A_{\iota}\qquad\llbracket
o\rrbracket:=\mathbb{B}\qquad\llbracket\sigma_{1}\to\sigma_{2}\rrbracket:=\left[\llbracket\sigma_{1}\rrbracket\to\llbracket\sigma_{2}\rrbracket\right]$

where $\mathbb{B}$ denotes the boolean lattice and
$\left[\llbracket\sigma_{1}\rrbracket\to\llbracket\sigma_{2}\rrbracket\right]$
denotes the full function space between $\llbracket\sigma_{1}\rrbracket$ and
$\llbracket\sigma_{2}\rrbracket$, as dictated by the standard semantics of
HOL.

##### Interpretation of terms and goal formulas.

Let $\Pi^{\prime}$ consist of predicate signature $\Pi$ and a variable
environment $\Delta$. A $\Pi^{\prime}$-_valuation_ (typically $\alpha$) is a
function such that $\alpha(x)\in\llbracket\sigma\rrbracket$, for all
$x:\sigma\in\Pi^{\prime}$ (taking the liberty to write $x$ for both variables
and predicates in $\Pi^{\prime}$.)

By some abuse, we consider goal formulas as goal _terms_ , treating logical
symbols as constants with their usual interpretations from HOL:

$\displaystyle\llbracket x:\sigma\rrbracket(\alpha)$ $\displaystyle=\alpha(x)$
$\displaystyle\llbracket a:\gamma\rrbracket(\alpha)$ $\displaystyle=c^{a}$
$\displaystyle\llbracket\mathsf{true}:o\rrbracket(\alpha)$ $\displaystyle=1$
$\displaystyle\llbracket s\,t:\sigma_{2}\rrbracket(\alpha)$
$\displaystyle=\llbracket
s:\sigma_{1}\to\sigma_{2}\rrbracket(\alpha)(\llbracket
t:\sigma_{1}\rrbracket(\alpha))$ $\displaystyle\llbracket\lambda
x:\sigma_{1}.\,t:\sigma_{2}\rrbracket(\alpha)$ $\displaystyle=\lambda
s\in\llbracket\sigma_{1}\rrbracket.\,\llbracket
t:\sigma_{2}\rrbracket(\alpha[x\mapsto s])$
$\displaystyle\llbracket\wedge:o\to o\to o\rrbracket(\alpha)$
$\displaystyle=\lambda b_{1}\,b_{2}.\,\min\\{b_{1},b_{2}\\}$
$\displaystyle\llbracket\exists_{\sigma}:(\sigma\to o)\to o\rrbracket(\alpha)$
$\displaystyle=\lambda r.\,\max\\{r\,s\mid s\in\llbracket\sigma\rrbracket\\}$

where $\sigma$ is either a constructor type $\gamma$ or predicate type $\rho$,
and the $\Sigma$-structure $\mathcal{A}$ and environment $\Pi^{\prime}$ are
left implicit.

##### Interpretation of clauses.

Interpreting clauses requires additional constants, again with their standard
semantics. Since the types are clear, we omit them.

$\displaystyle\llbracket\vee\rrbracket(\alpha)$ $\displaystyle=\lambda
b_{1}\,b_{2}.\,\max\\{b_{1},b_{2}\\}$
$\displaystyle\llbracket\neg\rrbracket(\alpha)$ $\displaystyle=\lambda
b.\,1-b$ $\displaystyle\llbracket{\Rightarrow}\rrbracket(\alpha)$
$\displaystyle=\lambda
b_{1}\,b_{2}.\,\llbracket\lor\rrbracket\,(\llbracket\neg\rrbracket\,b_{1})\,b_{2}$
$\displaystyle\llbracket\forall_{\sigma}\rrbracket(\alpha)$
$\displaystyle=\lambda r.\,\min\\{r\,s\mid s\in\llbracket\sigma\rrbracket\\}$

We have allowed some redundancy in the logical symbols for convenience: the
semantics of $\forall_{\sigma}$ can equivalently be formulated in terms of
$\neg$ and $\exists_{\sigma}$, and $\lor$ in terms of $\neg$ and $\land$.

The above determines the semantics of clauses-treated-as-terms. This behaves
as expected, with the semantics
$\llbracket\forall\overline{{y}}.\,G\Rightarrow A\rrbracket(\alpha)$ of
definite clause $\forall\overline{{y}}.\,G\Rightarrow A$ given by:

$\displaystyle\min\left\\{\max\\{\llbracket
A\rrbracket(\alpha[\overline{{y}}\mapsto\overline{{s}}]),1-\llbracket
G\rrbracket(\alpha[\overline{{y}}\mapsto\overline{{s}}])\\}\;\middle|\;\vphantom{\bigcup}\forall
y_{i}\in\overline{{y}}.\,s_{i}\in\llbracket\sigma_{i}\rrbracket\right\\}$

I.e. a clause valuates to $0$ iff there exists a valuation of the top-level
universal variables such that the body valuates to $1$ and the head to $0$.

##### Satisfaction.

A model of $D$ over $\Sigma$ and $\Pi$ consists of a $\Sigma$-structure
$\mathcal{A}$ and a $\Pi$-valuation $\alpha$ such that $\llbracket
D\rrbracket(\alpha)=1$. We say $D\vDash G$ just if $\llbracket
G\rrbracket(\alpha)=1$ for all models of $D$.

###  A.1. Completeness of the proof system

This section demonstrates soundness and completeness of the Figure 2 proof
system with respect to the standard semantics of HOL.

See 2.4

Soundness follows from each rule being clearly admissible in HOL.

For completeness, suppose $D\models G$ over constructor signature $\Sigma$ and
predicate signature $\Pi$. We assume $D$ contains a universal clause
$(\forall\overline{{y}}.\,\mathsf{true}\Rightarrow\mathsf{Univ}_{\rho}\,\overline{{y}})$
for every type $\rho$ occurring in $D$ or $G$. We refer to
$\mathsf{Univ}_{\rho}$ as a _universal relation_.

We construct an no-instance of the HOCHC satisfiability problem over the
equational theory of first-order trees as background. The instance is
constructed by defunctionalising the higher-order constructors and simulating
both pattern-matching clause heads and the higher-order typing discipline on
first-order trees with equational constraints.

##### The HOCHC signature.

Types $\tau$ are transformed to HOCHC types $\langle\\!|\tau|\\!\rangle$:

$\langle\\!|\gamma|\\!\rangle:=\iota\qquad\langle\\!|o|\\!\rangle:=o\qquad\langle\\!|\sigma\to\rho|\\!\rangle:=\langle\\!|\sigma|\\!\rangle\to\langle\\!|\rho|\\!\rangle$

We flatten our constructors to first-order, where the only non-nullary
constructor is binary application, written $\\_\cdot{}\\_$. A family of new
unary predicate symbols $T_{\gamma}$ is axiomatised so as to restrict
$x:\gamma$ to represent a well-formed tree of type $\gamma$ under the original
higher-order signature $\Sigma$.

Let $\mathsf{sorts}_{\exists}(D\land G)$ contain all types of existential
variables in $D\land G$, so we can define first-order signature
$\Sigma_{\mathsf{FO}}$ and set of predicates $\Delta$.

$\displaystyle\Sigma_{\mathsf{FO}}$ $\displaystyle:=\\{f:\iota\mid
f:\gamma\in\Sigma\\}\cup\\{\\_\cdot{}\\_:\iota\to\iota\to\iota\\}$
$\displaystyle\Delta$ $\displaystyle:=\Pi\cup\\{T_{\gamma}:\iota\to
o\mid\gamma\in\mathsf{sorts}_{\exists}(D\land
G)\lor(f:\gamma_{1}\to\dots\to\gamma_{n}\in\Sigma\land\gamma\in\\{\gamma_{1},\dots,\gamma_{n}\\})\\}$

##### The transformation.

We define a term transformation $\langle\\!|t|\\!\rangle$ by:

$\langle\\!|x|\\!\rangle:=x\qquad\langle\\!|c|\\!\rangle:=c\qquad\langle\\!|P|\\!\rangle:=P\qquad\langle\\!|s\,t|\\!\rangle:=\left\\{\begin{array}[]{ll}\langle\\!|s|\\!\rangle\cdot\langle\\!|t|\\!\rangle&\text{if
}s\,t:\gamma\\\
\langle\\!|s|\\!\rangle\,\langle\\!|t|\\!\rangle&\text{o/w}\end{array}\right.$

We extend this to goal formulas $\langle\\!|G|\\!\rangle$ by:

$\displaystyle\langle\\!|\mathsf{true}|\\!\rangle$
$\displaystyle:=\mathsf{true}$ $\displaystyle\qquad\quad\langle\\!|\exists
x:\rho.\,G|\\!\rangle$ $\displaystyle:=\exists
x:\langle\\!|\rho|\\!\rangle.\,\langle\\!|G|\\!\rangle$
$\displaystyle\langle\\!|G\wedge H|\\!\rangle$
$\displaystyle:=\langle\\!|G|\\!\rangle\wedge\langle\\!|H|\\!\rangle$
$\displaystyle\qquad\quad\langle\\!|\exists x:\gamma.\,G|\\!\rangle$
$\displaystyle:=\exists x:\iota.\,T_{\gamma}\,x\land\langle\\!|G|\\!\rangle$

We extend to definite formulas $\langle\\!|C|\\!\rangle$ by:

$\displaystyle\langle\\!|\mathsf{true}|\\!\rangle$
$\displaystyle:=\mathsf{true}$
$\displaystyle\qquad\quad\langle\\!|\forall\overline{{y}}.\,G\Rightarrow
P\,\overline{{y}}|\\!\rangle$
$\displaystyle:=\forall\overline{{y}}.\,\langle\\!|G|\\!\rangle\Rightarrow
P\,\overline{{y}}$ $\displaystyle\langle\\!|C\wedge D|\\!\rangle$
$\displaystyle:=\langle\\!|C|\\!\rangle\wedge\langle\\!|D|\\!\rangle$
$\displaystyle\qquad\quad\langle\\!|\forall\overline{{y}}.\,G\Rightarrow
P\,(c\,\overline{{y}})|\\!\rangle$ $\displaystyle:=\forall
z.\,\langle\\!|G|\\!\rangle_{z=c\overline{{y}}}\Rightarrow P\,z$

where

$\langle\\!|G|\\!\rangle_{z=c\overline{{y}}}:=\exists\overline{{y}}.\,z=\langle\\!|c\,\overline{{y}}|\\!\rangle\land\bigwedge_{y_{i}:\gamma_{i}\in\overline{{y}}}T_{\gamma_{i}}\,y_{i}\land\langle\\!|G|\\!\rangle$

Finally, we define an equi-satisfiable HOCHC instance over the first-order
equational theory of trees with signature $\Sigma_{\mathsf{FO}}$ and
predicates $\Delta$:

$\displaystyle D_{\mathit{Th}}$
$\displaystyle:=\langle\\!|D|\\!\rangle\land\\{\forall
x.\,\langle\\!|\mathsf{true}|\\!\rangle_{x=fy_{1}\dots y_{n}}\Rightarrow
T_{\gamma}\,x\mid f:\gamma_{1}\to\dots\to\gamma_{n}\to\gamma\in\Sigma\\}$
$\displaystyle G_{\mathit{Th}}$ $\displaystyle:=\langle\\!|G|\\!\rangle$

The transformation $\langle\\!|\\_|\\!\rangle$ has a straightforward inverse
$\langle\\!|\\_|\\!\rangle^{-1}$ on existential-free goal formulas.

Note that all universal variables are guarded by a $T_{\gamma}$ of the
appropriate type. Since universal variables do not occur in goal formulas,
those do not need to be guarded.

##### The HOCHC proof system.

Ong and Wagner (2019) propose a simple, sound and refutationally complete
resolution proof system for HOCHC (under the standard semantics of HOL) that
we shall call the _HOCHC proof system_. Any resolution proof for our HOCHC
instance requires only two of their three proof rules, due to the lack of
internal $\lambda$s and the fact that the HOCHC proof system does not
introduce those. In the terminology of our paper, these two proof rules are:

$\begin{array}[]{cc}\\!\prftree[l]{\textsf{\small{(OW${}_{\top}$)}}}{\textstyle\exists\overline{{y}}.\bigwedge_{i\in[1..n]}\varphi_{i}\land\exists\overline{{x}}.\bigwedge_{j\in[1..m]}x_{k_{j}}\,\overline{{M_{j}}}}{\top}\par\;\,\par\prftree[l,r]{\\!\\!\\!\\!$(\forall\overline{
{y} }.\,G' \Rightarrow P\,\overline{ {y} }) \in
D_{\mathit{Th}}$}{\textsf{\small{(OW${}_{\text{R}}$)}}}{\exists\overline{{z}}.\,G\land
P\,\overline{{M}}}{\exists\overline{{z}}.\,G\land
G^{\prime}[\overline{{M}}/\overline{{y}}]}\end{array}$

where $\varphi_{1},\dots,\varphi_{n}$ are constraints from the equational
theory of trees for which there exists a satisfying assignment $\alpha$ (i.e.
$\alpha\vDash\varphi_{1}\land\dots\land\varphi_{n}$ such that $\alpha(y)$ is a
finite tree over $\Sigma_{\mathsf{FO}}$, for all $y\in\overline{{y}}$). Note
that $\overline{{x}}$ in (OW⊤) are higher-order and $\overline{{y}}$ first-
order existentials. Proof rule (OW⊤) implicitly assigns universal relations to
$\overline{{x}}$; these are part of the semantic domain and guaranteed to
satisfy the formula.

We write $D_{\mathit{Th}}\vdash G^{\prime}\twoheadrightarrow G^{\prime\prime}$
to denote $G^{\prime}$ as a premise for $G^{\prime\prime}$ in the HOCHC proof
system, with $D_{\mathit{Th}}\vdash
G^{\prime}\twoheadrightarrow^{*}G^{\prime\prime}$ its reflexive, transitive
closure.

###### Notation 0.

Every HOCHC goal formula $G^{\prime}$ can be written as
$\exists\overline{{y}}_{\mathsf{FO}}\,\overline{{x}}_{\mathsf{HO}}.\,G_{\varphi}\land
G_{\mathsf{var}}\land G_{A}$ where:

  * •

$G_{\varphi}$ is existential-free and contains the constraints and atoms
headed by $T_{\gamma}$,

  * •

$G_{\mathsf{var}}$ is existential-free and contains the atoms headed by
$x\in\overline{{x}}_{\mathsf{HO}}$, and

  * •

$G_{A}$ is existential-free and contains the remaining atoms.

We may write $G_{\neg\varphi}$ for $G_{\mathsf{var}}\land G_{A}$.

##### HOCHC semantics.

Recall that $D\vDash G$ means “every model of $D$ satisfies $G$”, much like
$D_{\mathit{Th}}\vDash G_{\mathit{Th}}$ means “every model of
$D_{\mathit{Th}}$ satisfies $G_{\mathit{Th}}$”. Note, however, that a HOCHC
instance has a fixed background theory from which it inherits
$\llbracket\iota\rrbracket$ and interpretations of the constants in $\Sigma$.
Intuitively, our quantifier ranges over all $\Pi$-valuations and
$\Sigma$-structures, while the HOCHC quantifier only ranges over
$\Pi$-valuations that extend the background theory.

Consequently, we can choose our $\Sigma$-structure in the HOCHC case to match
the background theory of trees, and it is not difficult to see that $D\vDash
G$ implies $D_{\mathit{Th}}\vDash G_{\mathit{Th}}$.

##### Proof outline.

By refutation completeness of the HOCHC proof system, there exists a HOCHC
proof $D_{\mathit{Th}}\vdash G_{\mathit{Th}}\twoheadrightarrow^{*}\top$ with
satisfying assignment $\alpha$ to the first-order existentials.

We replay this HOCHC proof in our Figure 2 proof system starting from $G$.
Since all existential variables are guarded by typing predicates $T_{\gamma}$
and all elements of the universe of the theory of (finite) trees are
representable by terms, the satisfying assignment can be explicitly
constructed and implemented using (Ex). Furthermore, the presence of universal
clauses allow us to prove existential-headed atoms using (Ex) as
well777Although the type of a HOCHC existential may not match the
corresponding original existential, the existence of the appropriate universal
clause in $D$ is guaranteed.. Hence $D\vdash G$.

##### From constraints to type-respecting substitutions.

The purpose of our equality constraints and $T_{\gamma}$ predicates is to
restrict the domain of HOCHC variable $y:\iota$ to well-formed trees of type
$\gamma$ under the original higher-order signature; they guarantee that every
satisfying assignment $\alpha$ from an application of (OW⊤) respects the
original higher-order types.

We say that an assignment $\alpha$ to $\overline{{y}}$ is _type-respecting_
just if, for all $y\in\overline{{y}}$, there exists a closed tree $t:\gamma$
over $\Sigma$ such that $\alpha(y)=\langle\\!|t|\\!\rangle$ and $\gamma$ is
the original type of $y$.

###### Lemma A.1.

If $D_{\mathit{Th}}\vdash\exists
y.\,T_{\gamma}\,y\twoheadrightarrow^{*}H\twoheadrightarrow\top$ with
satisfying assignment $\alpha$, then $\alpha$ is type-respecting.

###### Proof.

Ong and Wagner (2019) leave existential quantifiers implicit in the HOCHC
proof system. For convenience, we do the same here. We use a straightforward
induction on length $k$ in $D_{\mathit{Th}}\vdash
T_{\gamma}\,y\twoheadrightarrow^{k}H\twoheadrightarrow\top$.

Clearly, $k$ cannot be zero, so suppose $k=1$. This first proof step must be
(OW${}_{\text{R}}$) with a side condition $(\forall
x.\,x=\langle\\!|f|\\!\rangle\Rightarrow T_{\gamma}\,x)\in D_{\mathit{Th}}$
with $f:\gamma\in\Sigma$, so $H=(y=\langle\\!|f|\\!\rangle)$. This means that
$y$ equals $\langle\\!|f|\\!\rangle$ under $\alpha$, so
$\alpha(y)=\langle\\!|f|\\!\rangle$ witnesses that $\alpha$ is type-
respecting.

Suppose $k>1$ with side condition $(\forall
x.\,\exists\overline{{z}}.\,x=\langle\\!|f\,\overline{{z}}|\\!\rangle\land\bigwedge_{j\in[1..m]}T_{\gamma_{j}}\,z_{j}\Rightarrow
T_{\gamma}\,x)\in D_{\mathit{Th}}$ with
$f:\gamma_{1}\to\dots\to\gamma_{m}\to\gamma\in\Sigma$. The result of this
first step is
$G^{\prime\prime}=(y=\langle\\!|f\,\overline{{z}}|\\!\rangle)\land\bigwedge_{j\in[1..m]}T_{\gamma_{j}}\,z_{j}$,
still omitting quantifiers.

For all $j\in[1..m]$, $\alpha$ is a satisfying assignment for some
$D_{\mathit{Th}}\vdash T_{\gamma_{j}}\,z_{j}\twoheadrightarrow^{k_{j}}\bot$
with $k_{j}<k$. By the IH, $\alpha(z_{j})=\langle\\!|t_{j}|\\!\rangle$ for
closed tree $t_{j}:\gamma_{j}$ over $\Sigma$.

Now, $\alpha$ satisfies $H$ and, by soundness of the HOCHC proof system, also
$G^{\prime\prime}$. In particular, this means $y$ equals
$\langle\\!|f\,\overline{{z}}|\\!\rangle$ under $\alpha$, so $\alpha(y)$
equals $\langle\\!|f\,\overline{{t}}|\\!\rangle$ for closed tree
$f\,\overline{{t}}:\gamma$ over $\Sigma$, as required. ∎

Observe from the transformation $\langle\\!|\\_|\\!\rangle$ that all first-
order existentials occurring in a HOCHC proof of a
$\langle\\!|G^{\prime}|\\!\rangle$ are guarded by the appropriate
$T_{\gamma}$. It is easy to see that the above lemma generalises to
$D_{\mathit{Th}}\vdash\exists\overline{{y}}_{\mathsf{FO}}\,\overline{{x}}_{\mathsf{HO}}.\,\bigwedge_{y_{i}:\gamma_{i}\in\overline{{y}}_{\mathsf{FO}}}T_{\gamma_{i}}\,y_{i}\land
G^{0}\twoheadrightarrow^{*}H\twoheadrightarrow\top$ with existential-free
$G^{0}$. Since every $\langle\\!|G^{\prime}|\\!\rangle$ can be written in this
shape, the following holds.

###### Lemma A.2.

If
$D_{\mathit{Th}}\vdash\langle\\!|G^{\prime}|\\!\rangle\twoheadrightarrow^{*}\top$
with satisfying assignment $\alpha$, then $\alpha$ is type-respecting.

Note that any satisfying assignment $\alpha$ to
$D_{\mathit{Th}}\vdash\exists\overline{{y}}_{\mathsf{FO}}\,\overline{{x}}_{\mathsf{HO}}.\,G_{\varphi}\land
G_{\neg\varphi}\twoheadrightarrow^{*}\top$ is also a satisfying assignment to
$D_{\mathit{Th}}\vdash\exists\overline{{y}}_{\mathsf{FO}}\,\overline{{x}}_{\mathsf{HO}}.\,G_{\neg\varphi}\twoheadrightarrow^{*}\top$.
We know that $\alpha$ respects original types, so
$[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}]$
is a well-defined substitution in our original program, giving rise to the
following lemma that allows us to replay a HOCHC proof in our Figure 2 proof
system.

###### Lemma A.3 (Replay lemma).

If
$D_{\mathit{Th}}\vdash\exists\overline{{y}}_{\mathsf{FO}}\,\overline{{x}}_{\mathsf{HO}}.\,G_{\varphi}\land
G_{\neg\varphi}\twoheadrightarrow^{*}\top$ with satisfying assignment
$\alpha$, then

$D\vdash\langle\\!|G_{\neg\varphi}|\\!\rangle^{-1}[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}}]$

###### Proof.

Suppose $D_{\mathit{Th}}\vdash
G^{\prime}\twoheadrightarrow^{*}H\twoheadrightarrow\top$ with satisfying
assignment $\alpha$. Because (OW${}_{\text{R}}$) is a local rule and (OW⊤) a
global one, and $T_{\gamma}$-clauses only have other
$T_{\gamma^{\prime}}$-predicates in their bodies, we may assume WLOG that all
$T_{\gamma}$-headed resolutions in a HOCHC proof are performed last.

Suppose our HOCHC proof has shape $D_{\mathit{Th}}\vdash
G^{\prime}\twoheadrightarrow^{k}G^{\prime\prime}\twoheadrightarrow^{\ell}H\twoheadrightarrow\top$
for a $G^{\prime\prime}$ where the first $k$ steps do not use
$T_{\gamma}$-headed clauses, followed by $\ell$ steps that (exclusively) do.
We use induction on $k$.

  * •

If $k=0$, then let
$G^{\prime}=G^{\prime\prime}=\exists\overline{{y}}_{\mathsf{FO}}\,\overline{{x}}_{\mathsf{HO}}.\,G_{\varphi}\land
G_{\mathsf{var}}$ with
$\overline{{x}}_{\mathsf{HO}}:\langle\\!|\overline{{\rho}}|\\!\rangle$. Let
$G_{\mathsf{var}}=\bigwedge_{j\in[1..m]}x_{i_{j}}\,\overline{{M_{j}}}$ with
$x_{i_{1}},\dots,x_{i_{m}}\in\overline{{x}}_{\mathsf{HO}}$. We prove
$D\vdash\langle\\!|G_{\mathsf{var}}|\\!\rangle^{-1}[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}}]$
where $\overline{{\mathsf{Univ}}}:\overline{{\rho}}$:

$\prftree[l]{\textsf{\small{(And)}}^{*}}{\forall
j\in[1..m].\\!\\!\\!\\!}{\prftree[l]{\textsf{\small{(Res)}}}{\prftree[l]{\textsf{\small{(T)}}}{D_{\mathit{Th}}\vdash\mathsf{true}}}{D_{\mathit{Th}}\vdash\mathsf{Univ}_{i_{j}}\,\langle\\!|\overline{{M_{j}}}|\\!\rangle^{-1}[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}}]}}{D_{\mathit{Th}}\vdash\bigwedge_{j\in[1..m]}\mathsf{Univ}_{i_{j}}\,\langle\\!|\overline{{M_{j}}}|\\!\rangle^{-1}[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}}]}$

  * •

If $k>0$, then let
$G^{\prime}=\exists\overline{{y}}_{\mathsf{FO}}\,\overline{{x}}_{\mathsf{HO}}.\,G_{\varphi}\land
G_{\neg\varphi}\land P\,\overline{{s}}$ such that the first step is
(OW${}_{\text{R}}$) on $P\,\overline{{s}}$. Suppose
$\overline{{x}}_{\mathsf{HO}}$ and $\overline{{\mathsf{Univ}}}$ with $\rho$ as
in the previous case, and $\overline{{x}}_{\mathsf{HO}}^{0}$ and
$\overline{{\mathsf{Univ}^{0}}}$ with $\rho^{0}$ analogous.

We shall abbreviate
$[\langle\\!|\alpha_{|{\overline{{x_{1}}}}}|\\!\rangle^{-1}/\overline{{x_{1}}},\dots,\langle\\!|\alpha_{|{\overline{{x_{n}}}}}|\\!\rangle^{-1}/\overline{{x_{n}}}]$
to
$[\langle\\!|\alpha_{|{\overline{{x_{1}}}\dots\overline{{x_{n}}}}}|\\!\rangle^{-1}/\overline{{x_{1}}}\dots\overline{{x_{n}}}]$.

    * –

Suppose the side condition is
$(\forall\overline{{z}}.\,\langle\\!|\exists\overline{{y}}_{\mathsf{FO}}^{0}\,\overline{{x}}_{\mathsf{HO}}^{0}.\,G^{0}|\\!\rangle\Rightarrow
P\,\overline{{z}})\in D_{\mathit{Th}}$ with existential-free $G^{0}$ from some
$(\forall\overline{{z}}.\,\exists\overline{{y}}_{\mathsf{FO}}^{0}\,\overline{{x}}_{\mathsf{HO}}^{0}.\,G^{0}\Rightarrow
P\,\overline{{z}})\in D$. In this case,
$\langle\\!|\exists\overline{{y}}_{\mathsf{FO}}^{0}\,\overline{{x}}_{\mathsf{HO}}^{0}.\,G^{0}|\\!\rangle$
equals some
$\exists\overline{{y}}_{\mathsf{FO}}^{0}\,\overline{{x}}_{\mathsf{HO}}^{0}.\,\bigwedge_{y_{j}^{0}\in\overline{{y}}_{\mathsf{FO}}^{0}}T_{\gamma_{j}^{0}}\,y_{j}^{0}\land\langle\\!|G^{0}|\\!\rangle$.
This gives us:

$G^{\prime\prime}=\exists\overline{{y}}_{\mathsf{FO}}\,\overline{{y}}_{\mathsf{FO}}^{0}\,\overline{{x}}_{\mathsf{HO}}\,\overline{{x}}_{\mathsf{HO}}^{0}.\,G_{\varphi}\land
G_{\neg\varphi}\land\bigwedge_{y_{j}^{0}\in\overline{{y}}_{\mathsf{FO}}^{0}}T_{\gamma_{j}^{0}}\,y_{j}^{0}\land\langle\\!|G^{0}|\\!\rangle[\overline{{s}}/\overline{{z}}]$

We aim to show $D\vdash\langle\\!|G_{\neg\varphi}\land
P\,\overline{{s}}|\\!\rangle^{-1}[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}}]$,
which holds if both of these claims hold:

(C1) $\displaystyle D$
$\displaystyle\vdash\langle\\!|G_{\neg\varphi}|\\!\rangle^{-1}[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}}]$
(C2) $\displaystyle D$ $\displaystyle\vdash
P\,\langle\\!|\overline{{s}}|\\!\rangle^{-1}[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}}]$

Note
$D\vdash\langle\\!|G_{\neg\varphi}\land\langle\\!|G^{0}|\\!\rangle[\overline{{s}}/\overline{{z}}]|\\!\rangle^{-1}[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}\overline{{y}}_{\mathsf{FO}}^{0}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}\,\overline{{y}}_{\mathsf{FO}}^{0}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}},\overline{{\mathsf{Univ}^{0}}}/\overline{{x}}_{\mathsf{HO}}^{0}]$,
i.e. $D\vdash(\langle\\!|G_{\neg\varphi}|\\!\rangle^{-1}\land
G^{0}[\langle\\!|\overline{{s}}|\\!\rangle^{-1}/\overline{{z}}])[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}\overline{{y}}_{\mathsf{FO}}^{0}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}\,\overline{{y}}_{\mathsf{FO}}^{0}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}},\overline{{\mathsf{Univ}^{0}}}/\overline{{x}}_{\mathsf{HO}}^{0}]$,
by the IH on $G^{\prime\prime}$. This implies the following, by (And):

(IH1) $\displaystyle D$
$\displaystyle\vdash\langle\\!|G_{\neg\varphi}|\\!\rangle^{-1}[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}\overline{{y}}_{\mathsf{FO}}^{0}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}\,\overline{{y}}_{\mathsf{FO}}^{0}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}},\overline{{\mathsf{Univ}^{0}}}/\overline{{x}}_{\mathsf{HO}}^{0}]$
(IH2) $\displaystyle D$ $\displaystyle\vdash
G^{0}[\langle\\!|\overline{{s}}|\\!\rangle^{-1}/\overline{{z}}][\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}\overline{{y}}_{\mathsf{FO}}^{0}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}\,\overline{{y}}_{\mathsf{FO}}^{0}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}},\overline{{\mathsf{Univ}^{0}}}/\overline{{x}}_{\mathsf{HO}}^{0}]$

Since $\langle\\!|G_{\neg\varphi}|\\!\rangle^{-1}$ does not contain
$\overline{{y}}_{\mathsf{FO}}^{0}$ or $\overline{{x}}_{\mathsf{HO}}^{0}$, IH1
gives us C1 immediately.

We apply (Ex) to IH2 for
$D\vdash\exists\overline{{y}}_{\mathsf{FO}}^{0}\,\overline{{x}}_{\mathsf{HO}}^{0}.\,G^{0}[\langle\\!|\overline{{s}}|\\!\rangle^{-1}/\overline{{z}}][\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}},\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}}]$.
This is now an instance of the body of the original definite clause
$(\forall\overline{{z}}.\,\exists\overline{{y}}_{\mathsf{FO}}^{0}\,\overline{{x}}_{\mathsf{HO}}^{0}.\,G^{0}\Rightarrow
P\,\overline{{z}})\in D$, so we apply (Res) to obtain C2.

    * –

Suppose the side condition is $(\forall
v.\,\langle\\!|\exists\overline{{y}}_{\mathsf{FO}}^{0}\,\overline{{x}}_{\mathsf{HO}}^{0}.\,G^{0}|\\!\rangle_{f\,\overline{{z}}}\Rightarrow
P\,v)\in D_{\mathit{Th}}$ with existential-free $G^{0}$ from some
$(\forall\overline{{z}}.\,\exists\overline{{y}}_{\mathsf{FO}}^{0}\,\overline{{x}}_{\mathsf{HO}}^{0}.\,G^{0}\Rightarrow
P\,(f\,\overline{{z}}))\in D$. Then,
$\langle\\!|\exists\overline{{y}}_{\mathsf{FO}}^{0}\,\overline{{x}}_{\mathsf{HO}}^{0}.\,G^{0}|\\!\rangle_{f\,\overline{{z}}}$
equals some
$\exists\overline{{y}}_{\mathsf{FO}}^{0}\,\overline{{z}}\,\overline{{x}}_{\mathsf{HO}}^{0}.\,\bigwedge_{y_{j}^{0}:\gamma^{0}_{j}\in\overline{{y}}}T_{\gamma^{0}_{j}}\,y_{j}^{0}\land(v=\langle\\!|f\,\overline{{z}}|\\!\rangle)\land\bigwedge_{z_{i}:\gamma^{1}_{i}\in\overline{{z}}}T_{\gamma^{1}_{i}}\,z_{i}\land\langle\\!|G^{0}|\\!\rangle$.

This gives us:

$\displaystyle
G^{\prime\prime}=\exists\overline{{y}}_{\mathsf{FO}}\,\overline{{y}}_{\mathsf{FO}}^{0}\,\overline{{z}}\,\overline{{x}}_{\mathsf{HO}}\,\overline{{x}}_{\mathsf{HO}}^{0}.\,$
$\displaystyle G_{\varphi}\land
G_{\neg\varphi}\land\bigwedge_{y_{j}^{0}:\gamma^{0}_{j}\in\overline{{y}}}T_{\gamma^{0}_{j}}\,y_{j}^{0}\land(s_{1}=\langle\\!|f\,\overline{{z}}|\\!\rangle)$
$\displaystyle\land\;\bigwedge_{z_{i}:\gamma^{1}_{i}\in\overline{{z}}}T_{\gamma^{1}_{i}}\,z_{i}\land\langle\\!|G^{0}|\\!\rangle[s_{1}/v]$

By the IH,
$D\vdash\langle\\!|G_{\neg\varphi}\land\langle\\!|G^{0}|\\!\rangle[s_{1}/v]|\\!\rangle^{-1}[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}\overline{{y}}_{\mathsf{FO}}^{0}\overline{{z}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}\,\overline{{y}}_{\mathsf{FO}}^{0}\,\overline{{z}}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}},\overline{{\mathsf{Univ}^{0}}}/\overline{{x}}_{\mathsf{HO}}^{0}]$.
However, $v$ does not occur in $\langle\\!|G^{0}|\\!\rangle$, so
$\langle\\!|G^{0}|\\!\rangle[s_{1}/v]=\langle\\!|G^{0}|\\!\rangle$, which
yields:

$D\vdash(\langle\\!|G_{\neg\varphi}|\\!\rangle^{-1}\land
G^{0})[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}\overline{{y}}_{\mathsf{FO}}^{0}\overline{{z}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}\,\overline{{y}}_{\mathsf{FO}}^{0}\,\overline{{z}}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}},\overline{{\mathsf{Univ}^{0}}}/\overline{{x}}_{\mathsf{HO}}^{0}]$

Compared with the IH in the previous case, only the substitution to
$\overline{{z}}$ is different; instead of $\overline{{z}}$ first being
partially instantiated with $\langle\\!|\overline{{s}}|\\!\rangle^{-1}$ (in
the previous case), $\overline{{z}}$ is directly fully instantiated by
$\alpha$.

We know from Lemma A.2 that $\alpha$ assigns each $z_{i}\in\overline{{z}}$ a
closed term $\langle\\!|t^{\prime}_{i}|\\!\rangle$ such that
$t^{\prime}_{i}:\gamma^{1}_{i}$. Furthermore, $\alpha$ satisfies $H$ and, by
soundness of the HOCHC proof system, also $G^{\prime\prime}$. In particular,
this means $s_{1}$ equals $\langle\\!|f\,\overline{{z}}|\\!\rangle$ under
$\alpha$, and
$\langle\\!|s_{1}|\\!\rangle^{-1}[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}]$
equals $f\,\overline{{t^{\prime}}}$.

Since we set out to prove $D\vdash\langle\\!|G_{\neg\varphi}\land
P\,s_{1}|\\!\rangle^{-1}[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}}]$,
it suffices to show

$D\vdash\langle\\!|G_{\neg\varphi}|\\!\rangle^{-1}[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}}]\land
P\,(f\,\overline{{t^{\prime}}})$

We now proceed as in the previous case.

∎

###### Proof of Theorem 2.4.

Since $G_{\mathit{Th}}=\langle\\!|G|\\!\rangle$, it remains to show
$D_{\mathit{Th}}\vdash\langle\\!|G|\\!\rangle\twoheadrightarrow^{*}\top$
implies $D\vdash G$.

Let
$G=\exists\overline{{y}}_{\mathsf{FO}}\,\overline{{x}}_{\mathsf{HO}}.\,G_{\mathsf{var}}\land
G_{A}$, so
$G_{\mathit{Th}}=\langle\\!|G|\\!\rangle=\exists\overline{{y}}_{\mathsf{FO}}\,\overline{{x}}_{\mathsf{HO}}.\,G_{\varphi}\land\langle\\!|G_{\mathsf{var}}\land
G_{A}|\\!\rangle$. This gives us
$D_{\mathit{Th}}\vdash\exists\overline{{y}}_{\mathsf{FO}}\,\overline{{x}}_{\mathsf{HO}}.\,G_{\varphi}\land\langle\\!|G_{\mathsf{var}}\land
G_{A}|\\!\rangle\twoheadrightarrow^{*}\top$ for a $G_{\varphi}$ and
satisfying, type-respecting assignment $\alpha$.

By Replay Lemma A.3, $D\vdash\langle\\!|\langle\\!|G_{\mathsf{var}}\land
G_{A}|\\!\rangle|\\!\rangle^{-1}[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}}]$,
which is:

$D\vdash(G_{\mathsf{var}}\land
G_{A})[\langle\\!|\alpha_{|{\overline{{y}}_{\mathsf{FO}}}}|\\!\rangle^{-1}/\overline{{y}}_{\mathsf{FO}}][\overline{{\mathsf{Univ}}}/\overline{{x}}_{\mathsf{HO}}]$

Finally, we prove $Ds\vdash G$ with (Ex) and conclude that the Figure 2 proof
system is complete with respect to the standard semantics of HOL. ∎

###  A.2. Elimination of predicate-type existentials

###### Corollary A.4.

Predicate-type existentials do not add expressive power to HOMSL($\omega$).

###### Proof.

We prove that $D\vdash\exists x_{0}:\rho.\,G$ if, and only if, $D\vdash
G[\mho_{\rho}/x_{0}]$, relying on the reduction of provability in
HOMSL($\omega$) to provability in HOCHC with a decidable equational theory of
first-order trees (see Theorem 2.4, soundness and completeness of the proof
system).

Direction $\Leftarrow$ is immediate from (Ex), so suppose $D\vdash\exists
x_{0}:\rho.\,G$. There exists a HOCHC proof:

$\textstyle D_{\mathit{Th}}\vdash\exists
x_{0}:\langle\\!|\rho|\\!\rangle.\,\langle\\!|G|\\!\rangle\twoheadrightarrow^{*}\exists
x_{0}\,\overline{{x}}\,\overline{{y}}.\,\bigwedge_{i\in[1..n]}\varphi_{i}\bigwedge_{j\in[1..m]}x_{k_{j}}\,\overline{{M_{j}}}\twoheadrightarrow\top$

with a satisfying assignment $\alpha$ to the existentials $\overline{{y}}$
with constructor types. The existentials $x_{0}$ and $\overline{{x}}$ with
predicate types are implicitly assigned the maximal element in the semantic
domain of their respective types, which is captured by
$\mho_{\langle\\!|\rho^{\prime}|\\!\rangle}$ for type
$\langle\\!|\rho^{\prime}|\\!\rangle$.

This means there is a proof
$D_{\mathit{Th}}\vdash\langle\\!|G|\\!\rangle[\mho_{\langle\\!|\rho|\\!\rangle}/x_{0}]\twoheadrightarrow^{*}\top$.
Because
$\langle\\!|G|\\!\rangle[\mho_{\langle\\!|\rho|\\!\rangle}/x_{0}]=\langle\\!|G[\mho_{\rho}/x_{0}]|\\!\rangle$,
the final part of the proof of Theorem 2.4 gives us $D\vdash
G[\mho_{\rho}/x_{0}]$.

We conclude that preprocessing HOMSL($\omega$) can eliminate predicate-type
existentials by instantiating them with universal relations. ∎

##  Appendix B Supporting Material for Section 3

###  B.1. Elimination of higher-order predicates

Note that the transformation on goal formulas has a straightforward retraction
$(\\!|\\_|\\!)^{-1}$ which removes occurrences of $\mathsf{T}$ and the $\\#$.

###### Lemma B.1.

$D\vdash_{\omega}G$ implies $(\\!|D|\\!)\vdash_{1}(\\!|G|\\!)$

###### Proof.

The proof is by induction on the proof object in the antecedent.

(T):

Clear by definition.

(Res):

In this case, $G$ is of the form $A[\overline{{s}}/\overline{{y}}]$ and there
is a clause $(\forall\overline{{y}}.\,H\Rightarrow A)\in D$. By induction, we
may assume that
$(\\!|D|\\!)\vdash_{1}(\\!|H[\overline{{s}}/\overline{{y}}]|\\!)$. Note that,
by definition,
$(\\!|H[\overline{{s}}/\overline{{y}}]|\\!)=(\\!|H|\\!)[(\\!|\overline{{s}}|\\!)/\overline{{y}}]$
and
$(\\!|A[\overline{{s}}/\overline{{y}}]|\\!)=(\\!|A|\\!)[(\\!|\overline{{s}}|\\!)/\overline{{y}}]$.
We consider two cases for $A$.

  * •:

If $A$ is of shape $P\,(c\,\overline{{y}})$, then
$(\\!|A|\\!)=\mathsf{T}\,(p^{\\#}\,(c\,\overline{{y}}))$ and we prove
$(\\!|A|\\!)[(\\!|\overline{{s}}|\\!)/\overline{{y}}]=\mathsf{T}\,(p^{\\#}\,(c\,(\\!|\overline{{s}}|\\!)))$
by two applications of (Res). The first uses the reflection clause from
$(\\!|D|\\!)$ to unwrap the $\mathsf{T}$ predicate, obtaining
$P\,(c\,(\\!|\overline{{s}}|\\!))$, and the second uses the transformed copy
of the side premise to obtain
$(\\!|H|\\!)[(\\!|\overline{{s}}|\\!)/\overline{{y}}]$, which is provable by
the induction hypothesis.

  * •:

Otherwise, $A$ is of the form $P\,\overline{{y}}$ and
$(\\!|A|\\!)=\mathsf{T}\,(p^{\\#}\,\overline{{y}})$. We can prove
$(\\!|A|\\!)[\overline{{(\\!|s|\\!)}}/\overline{{y}}]$ by (Res) directly using
the transformed copy of the side premise and the induction hypothesis.

(Ex):

In this case, $G$ is of the form $\exists x.\,H$ and $(\\!|G|\\!)=\exists
x.\,(\\!|H|\\!)$. By induction, we may assume $(\\!|H[t/x]|\\!)$, which is
synonymous with $(\\!|H|\\!)[(\\!|t|\\!)/x]$, is already provable. Therefore,
the proof can be concluded using (Ex).

(And):

Follows immediately from the induction hypotheses.

∎

We need to generalise a little bit in the converse direction.

###### Lemma B.2.

$(\\!|D|\\!)\vdash_{1}G$ implies $D\vdash_{\omega}(\\!|G|\\!)^{-1}$

###### Proof.

The proof is by induction.

(T):

Clear by definition.

(Res):

In this case, $G$ has the form $A[\overline{{s}}/\overline{{y}}]$ and there is
a clause $(\forall\overline{{y}}.\,H\Rightarrow A)\in(\\!|D|\\!)$. We
distinguish cases on the form of $A$ and the provenance of the side premise.

  * •:

If $A$ is of the form $P\,(c\,\overline{{y}})$, then there is a clause
$(\forall\overline{{y}}.\,(\\!|H|\\!)^{-1}\Rightarrow
P\,(c\,\overline{{y}}))\in D$ from which the side premise originates. From the
induction hypothesis, we can assume that
$D\vdash_{\omega}(\\!|H[\overline{{s}}/\overline{{y}}]|\\!)^{-1}$, which is,
by definition,
$D\vdash_{\omega}(\\!|H|\\!)^{-1}[(\\!|\overline{{s}}|\\!)^{-1}/\overline{{y]}}]$.
Hence, we can conclude $(\\!|G|\\!)^{-1}$, namely
$P\,(c\,(\\!|\overline{{s}}|\\!)^{-1})$, directly by (Res).

  * •:

If $A$ is of the form $\mathsf{T}\,(p^{\\#}\,\overline{{y}})$ and the side
premise is not a reflection, then there is a clause
$(\forall\overline{{y}}.\,(\\!|H|\\!)^{-1}\Rightarrow P\,\overline{{y}})\in
D$. From the induction hypothesis we can assume
$D\vdash_{\omega}(\\!|H[\overline{{s}}/\overline{{y}}]|\\!)^{-1}$, which is,
by definition,
$D\vdash_{\omega}(\\!|H|\\!)^{-1}[(\\!|\overline{{s}}|\\!)^{-1}/\overline{{y}}]$.
We can conclude $(\\!|G|\\!)^{-1}$, namely $P\,(\\!|\overline{{s}}|\\!)^{-1}$,
directly by (Res).

  * •:

Otherwise the side premise is a reflection, has shape $\forall
y.\,P\,y\Rightarrow\mathsf{T}\,(p^{\\#}\,y)$, and $A$ is of the form
$\mathsf{T}\,(p^{\\#}\,y)$. We may assume, by the induction hypothesis, that
$D\vdash_{\omega}(\\!|P\,s|\\!)^{-1}$, which is
$D\vdash_{\omega}P\,(\\!|s|\\!)^{-1}$ by definition. But this is already
$D\vdash_{\omega}(\\!|G|\\!)^{-1}$, so we are done.

(Ex):

In this case, $G$ has the form $\exists x.\,H$ and it follows from the
induction hypothesis that there is some $t$ such that
$D\vdash_{\omega}(\\!|H[t/x]|\\!)^{-1}$. By definition, this means we have
$D\vdash_{\omega}(\\!|H|\\!)^{-1}[(\\!|t|\\!)^{-1}/x]$ and so we can conclude
$D\vdash_{\omega}(\\!|G|\\!)^{-1}$, being $\exists x.\,(\\!|H|\\!)^{-1}$,
immediately by (Ex).

(And):

This case follows directly from the induction hypotheses.

∎

It now follows immediately from these lemmas that $D\vdash_{\omega}G$ iff
$(\\!|D|\\!)\vdash_{1}(\\!|G|\\!)$, proving Theorem 3.1.

###  B.2. Elimination of existentials

###### Lemma B.3.

For all terms $\exists_{\gamma}\,s$ over signatures
${\Sigma}_{\mathsf{\not\exists}}$ and ${\Pi}_{\mathsf{\not\exists}}$,
${D}_{\mathsf{\not\exists}}\vdash\exists_{\gamma}\,s$ if, and only if,
${D}_{\mathsf{\not\exists}}\vdash s\,t$ for a closed $t:\gamma$.

###### Proof.

For $\Rightarrow$, let $\mathcal{T}$ be an underlying proof tree of
${D}_{\mathsf{\not\exists}}\vdash\exists_{\gamma}\,s$. We prove $\mathcal{T}$
contains ${D}_{\mathsf{\not\exists}}\vdash s\,t$ for a closed $t:\gamma$, by
induction on the number $m$ of proof steps headed by any
$\exists_{\gamma^{\prime}}$ external to $s$.

  * •

If $m=1$, then, by our assumption of adequate signatures, there exists
$c:\gamma\in\Sigma$ such that a $\mathcal{T}$ has shape:

$\prftree[l]{\textsf{\small{(Res)}}}{\prftree[l]{\textsf{\small{(Res)}}}{{D}_{\mathsf{\not\exists}}\vdash
s\,c}{{D}_{\mathsf{\not\exists}}\vdash\mathsf{Comp}_{c}^{0,0}\,s}}{{D}_{\mathsf{\not\exists}}\vdash\exists_{\gamma}\,s}$

  * •

If $m>1$, then
$\mathcal{T}(1)={D}_{\mathsf{\not\exists}}\vdash\mathsf{Comp}^{0,k}_{f}\,s$
for a $k>0$ and constructor $f:\gamma_{1}\to\dots\to\gamma_{k}\to\gamma$. We
apply the IH to the subproof rooted at node $111$ (which clearly has
$m^{\prime}_{1}<m$).

Now, if $k=1$, then we use (Res) with $\forall
v\,x_{1}.\,v\,(f\,x_{1})\Rightarrow\mathsf{Comp}_{f}^{1,1}\,v\,x_{1}$ to give
us ${D}_{\mathsf{\not\exists}}\vdash s\,(f\,t_{1})$, as required. Otherwise,
we use (Res) with $\forall
v\,x_{1}.\,\exists_{\gamma_{2}}\,(\mathsf{Comp}^{2,k}\,v\,x_{1})\Rightarrow\mathsf{Comp}^{1,k}_{f}\,v\,x_{1}$
to give us
${D}_{\mathsf{\not\exists}}\vdash\exists_{\gamma_{2}}\,(\mathsf{Comp}^{2,k}_{f}\,s\,t_{1})$
to which we apply the IH again.

We use the IH a total of $k$ times, once for each $\gamma_{i}$, for a proof
tree of the following shape:

$\prftree[l]{\textsf{\small{(Res)}}}{\prftree[l]{\textsf{\small{(Res)}}}{\prftree[l]{\textsf{\small{(IH)}}}{\prftree{\prftree{\prftree[l]{\textsf{\small{(Res)}}}{{D}_{\mathsf{\not\exists}}\vdash
s\ (f\ t_{1}\dots
t_{k})}{{D}_{\mathsf{\not\exists}}\vdash\mathsf{Comp}_{f}^{k,k}\ s\ t_{1}\
\cdots\
t_{k}}}{\vdots}}{{D}_{\mathsf{\not\exists}}\vdash\mathsf{Comp}^{1,k}_{f}\,s\,t_{1}}}{{D}_{\mathsf{\not\exists}}\vdash\exists_{\gamma_{1}}\,(\mathsf{Comp}^{1,k}_{f}\,s)}}{{D}_{\mathsf{\not\exists}}\vdash\mathsf{Comp}^{0,k}_{f}\,s}}{{D}_{\mathsf{\not\exists}}\vdash\exists_{\gamma}\,s}$

The direction $\Leftarrow$ is a straightforward inverse of hereof, using
induction on the number of symbols in $t$. ∎

###### Lemma B.4.

For all closed subformulas $G$ of the original clauses, $D\vdash G$ if and
only if ${D}_{\mathsf{\not\exists}}\vdash\Lbag G\Rbag$.

###### Proof.

In the forwards direction, we prove the following for all subformulas $G$ of
the original clauses with free variables $\overline{{z}}$:

$D\vdash
G[\overline{{t/z}}]\quad\text{implies}\quad{D}_{\mathsf{\not\exists}}\vdash\Lbag
G\Rbag[\overline{{t/z}}]$

The proof is by induction on $D\vdash G$.

(T):

Immediate.

(And):

Immediate from the induction hypothesis and the definition of the mapping.

(Ex):

In this case $G[\overline{{t/z}}]$ is of shape $\exists
x:\gamma.\,G^{\prime}[\overline{{t/z}}]$ and $\Lbag
G\Rbag=\exists_{\gamma}\,(\Lambda_{\gamma,\,G^{\prime}}\,\overline{{z}})$. It
follows from the induction hypothesis that
${D}_{\mathsf{\not\exists}}\vdash\Lbag G^{\prime}\Rbag[\overline{{t/z}}][u/x]$
for some closed $u$. Hence, it follows from (Res) that
${D}_{\mathsf{\not\exists}}\vdash\Lambda_{\gamma,G^{\prime}}\,\overline{{t}}\,u$.
Then, from Lemma B.3, we obtain
${D}_{\mathsf{\not\exists}}\vdash\exists_{\gamma}\,(\Lambda_{\gamma,G^{\prime}}\,\overline{{t}})$,
which is just ${D}_{\mathsf{\not\exists}}\vdash\Lbag G\Rbag[\overline{{t/z}}]$
as required.

(Res):

In this case $G[\overline{{t/z}}]$ is of shape $A[\overline{{s/y}}]$ and there
is a clause $\forall\overline{{y}}.\ G^{\prime}\Rightarrow A$ in $D$. Then
there is a clause $\forall\overline{{y}}.\ \Lbag G^{\prime}\Rbag\Rightarrow A$
in ${D}_{\mathsf{\not\exists}}$. It follows from the induction hypothesis that
${D}_{\mathsf{\not\exists}}\vdash\Lbag G^{\prime}\Rbag[\overline{{s/y}}]$.
Therefore, by (Res), we get ${D}_{\mathsf{\not\exists}}\vdash
A[\overline{{s/y}}]$. Since $G[\overline{{t/z}}]=A[\overline{{s/y}}]$ with $A$
the head of a clause, we have that $\Lbag G\Rbag=G$ and hence our conclusion
is already in the desired form.

For the backward direction, we prove the following for all subformulas
$H^{\prime}$ of the original clauses with free variables $\overline{{z}}$:

${D}_{\mathsf{\not\exists}}\vdash H\quad\text{and}\quad H=\Lbag
H^{\prime}\Rbag[\overline{{t/z}}]\quad\text{and}\quad\mathsf{FV}(H^{\prime})=\overline{{z}}\quad\text{implies}\quad
D\vdash H^{\prime}[\overline{{t/z}}]$

The proof is by strong induction on ${D}_{\mathsf{\not\exists}}\vdash H$:

(T):

Immediate.

(And):

Immediate from the induction hypothesis and the definition of the mapping.

(Ex):

In this case, $H$ is of shape $\exists x\mathord{:}\gamma.\ G$, but there is
no $G^{\prime}$ such that $\exists x\mathord{:}\gamma.\ G=\Lbag
G^{\prime}\Rbag[\overline{{t/z}}]$. So the result is vacuously true.

(Res):

In this case, $H$ is of shape $A[\overline{{s/y}}]$ and we have
$\forall\overline{{y}}.\ G\Rightarrow A\in{D}_{\mathsf{\not\exists}}$. We
analyse cases on the predicate that heads $A[\overline{{s/y}}]$ (which is just
the predicate that heads $A$). As in the previous case, this predicate cannot
be $\Lambda_{\gamma,K}$ or $\mathsf{Comp}_{f}^{i,j}$ since neither of those
heads a formula in the image of $\Lbag-\Rbag$.

  * •:

If the predicate is $\exists_{\gamma}$, we reason as follows. In this case,
since $A$ heads a clause in ${D}_{\mathsf{\not\exists}}$, it must be that $A$
is $\exists_{\gamma}\,y$ for some variable $y$. Therefore, $\overline{{s}}$ is
a singleton $s$. Suppose $A[\overline{{s/y}}]=\Lbag
H^{\prime}\Rbag[\overline{{t/z}}]$ for some $H^{\prime}$. Since there are no
existential quantifiers in $A[\overline{{s/y}}]$ and $A$ is headed by
$\exists_{\gamma}$, $\Lbag H^{\prime}\Rbag$ must be of shape
$\exists_{\gamma}\,(\Lambda_{\gamma,\,K}\,\overline{{z}})$ for some $K$ and
$\overline{{z}}=\mathsf{FV}(K)$. Hence,
$s=(\Lambda_{\gamma,\,K}\,\overline{{z}})$ with
$\overline{{z}}=\mathsf{FV}(K)$. Thus
$A[\overline{{t/z}}]=\exists_{\gamma}\,(\Lambda_{\gamma,\,K}\,\overline{{t}})$
and, since we know this is provable in the context
${D}_{\mathsf{\not\exists}}$, it follows from the proof of from Lemma B.3
(although we did not state the lemma this way) that there is a closed term $u$
and there is actually a subproof concluding
${D}_{\mathsf{\not\exists}}\vdash(\Lambda_{\gamma,\,K}\,\overline{{z}})\,u$.
This subproof must be concluded using the rule (Res) with premise
${D}_{\mathsf{\not\exists}}\vdash\Lbag K\Rbag[\overline{{t/z}}][u/x]$. Since
this is a strict subproof of the original, we can apply the induction
hypothesis to obtain $D\vdash K[\overline{{t/z}}][u/x]$. Then it follows from
(Ex) that $D\vdash(\exists x:\gamma.\ K)[\overline{{t/z}}]$, as required.

  * •:

Otherwise the predicate is some $P$ from $\Pi$ (the old signature). In this
case, the side premise comes from $\Lbag D\Rbag$ and $G$ of the side premise
must be of shape $\Lbag G^{\prime}\Rbag$ for some $G^{\prime}$ from the
original clauses with $\mathsf{FV}(G^{\prime})=\overline{{y}}$. Then, the
induction hypothesis applies to ${D}_{\mathsf{\not\exists}}\vdash\Lbag
G^{\prime}\Rbag[\overline{{s/y}}]$, so we can deduce $D\vdash
G^{\prime}[\overline{{s/y}}]$. Then, by (Res), we obtain
$A[\overline{{s/y}}]$. Now, suppose that $A[\overline{{s/y}}]=\Lbag
H^{\prime}\Rbag[\overline{{t/z}}]$ as required by the statement. Since $A$ is
a head with predicate $P$, it can only be that $\Lbag
H^{\prime}\Rbag=H^{\prime}$ and so what we obtained is already in the correct
form.

∎

##  Appendix C Supporting Material for Section 4

###### Lemma C.1 (Reflexivity of implication).

$V,\,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
U)\triangleright^{*}\mathsf{true}$

###### Lemma C.2 (Progress).

If $V,\,\overline{{z}}\vdash G[\overline{{u}}/\overline{{y}}]\triangleright H$
then there is $K$ and $U$ such that:

$\textit{(a)}\quad V,\,\overline{{y}}\overline{{z}}\vdash
G\triangleright^{*}K\wedge U$

and we can split $H$ as $H_{1}\wedge H_{2}$ so that both the following hold:

$\textit{(b)}\quad V,\,\overline{{z}}\vdash
U[\overline{{u}}/\overline{{y}}]\triangleright^{*}H_{1}\qquad\qquad\textit{(c)}\quad
K[\overline{{u}}/\overline{{y}}]=H_{2}$

and, moreover, $\mathsf{FV}(U)\subseteq\overline{{y}}$.

###### Proof.

By induction on the rewrite $V,\,\overline{{z}}\vdash
G[\overline{{u}}/\overline{{y}}]\triangleright H$.

(Refl):

In this case, $H$ is $\mathsf{true}$ and $G[\overline{{u}}/\overline{{y}}]$ is
some $P\,x\in V$. Take $K=H_{1}=H_{2}=\mathsf{true}$ and (c) follows
immediately. It must be that $G=P\,v$ for some variable $v$. We distinguish
cases on $v$:

  * •:

If $v\in\overline{{y}}$ then take $U$ to be $P\ v$. Then (a) follows in 0
rewrite steps and (b) follows by (Refl) because
$U[\overline{{u}}/\overline{{y}}]=P\ x$.

  * •:

Otherwise, take $U$ to be $\mathsf{true}$. Then (a) follows by (Refl) and (b)
is immediate.

(Step):

In this case, $G[\overline{{u}}/\overline{{y}}]=P\ (f\ \overline{{s}})$,
$H=U^{\prime}[\overline{{s}}/\overline{{x}}]$ and there is a clause
$(\forall\overline{{x}}.\,U^{\prime}\Rightarrow P\ (f\ \overline{{x}}))\in V$.
In general, $G$ has shape $P\,s$ and so we distinguish cases on $s$:

  * •:

If the head symbol of $s$ is a variable $y\in\overline{{y}}$, it must be that
$s$ is of shape $y\ \overline{{v}}$,
$y[\overline{{u}}/\overline{{y}}]=f\,\overline{{s_{1}}}$,
$\overline{{v}}[\overline{{u}}/\overline{{y}}]=\overline{{s_{2}}}$ and
$\overline{{s_{1}s_{2}}}=\overline{{s}}$ and we may split $\overline{{x}}$ as
$\overline{{x_{1}}}\overline{{x_{2}}}$ (i.e.
$|\overline{{v}}|=|\overline{{s_{2}}}|=|\overline{{x_{2}}}|$). First observe
that $H=U^{\prime}[\overline{{s}}/\overline{{x}}]$ can also be written as
$U^{\prime}_{|{\overline{{x_{1}}}}}[\overline{{s}}/\overline{{x_{1}}}]\wedge
U^{\prime}_{|{\overline{{x_{2}}}}}[\overline{{v}}/\overline{{x_{2}}}][\overline{{u}}/\overline{{y}}]$.
Take $H_{1}$ as the former and $H_{2}$ as the latter conjunct. Take $K$ to be
$U^{\prime}_{|{\overline{{x_{2}}}}}[\overline{{v}}/\overline{{x_{2}}}]$ and
$U$ to be
$\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
P\,(y\ \overline{{x_{2}}})$. Thus (c) holds immediately. Then (a) follows by
(Assm):

$V,\,\overline{{y}}\overline{{z}}\vdash P(y\ \overline{{v}})\triangleright
U^{\prime}_{|{\overline{{x_{2}}}}}[\overline{{v}}/\overline{{x_{2}}}]\wedge(\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
P\,(y\ \overline{{x_{2}}}))$

For (b), observe that $U[\overline{{u}}/\overline{{y}}]$ is
$\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow P\
(f\,\overline{{s_{1}}}\overline{{x_{2}}})$. By (Imp) and (Step), (ImpAnd), and
(Scope) respectively, we have:

$\displaystyle
V,\overline{{z}}\vdash\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
P\ (f\,\overline{{s_{1}}}\overline{{x_{2}}})$
$\displaystyle\triangleright\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
U^{\prime}[\overline{{s_{1}}}\overline{{x_{2}}}/\overline{{x}}]$
$\displaystyle\triangleright^{*}(\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
U^{\prime}_{|{\overline{{x_{1}}}}}[\overline{{s_{1}}}/\overline{{x_{1}}}])\wedge(\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
U^{\prime}_{|{\overline{{x_{2}}}}})$
$\displaystyle\triangleright^{*}U^{\prime}_{|{\overline{{x_{1}}}}}[\overline{{s_{1}}}/\overline{{x_{1}}}]\wedge(\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
U^{\prime}_{|{\overline{{x_{2}}}}})$

with the latter conjunct rewriting to $\mathsf{true}$ by the reflexivity of
implication, leaving $H_{1}$.

  * •:

Otherwise, $s$ is of shape $f\ \overline{{w}}$ and
$\overline{{w}}[\overline{{u}}/\overline{{y}}]=\overline{{s}}$. Then take
$K:=U^{\prime}[\overline{{w}}/\overline{{x}}]$, $H_{2}:=H$, and
$U:=\mathsf{true}$ and $H_{1}:=\mathsf{true}$. Now (a) follows by (Step), (b)
is trivial, and (c) from
$K[\overline{{u}}/\overline{{y}}]=U^{\prime}[\overline{{w}}/\overline{{x}}][\overline{{u}}/\overline{{y}}]=H_{2}$.

(Assm):

In this case, $G[\overline{{u}}/\overline{{y}}]$ has shape
$P\,(z\,\overline{{s}})$ and $H$ has shape
$U^{\prime}[\overline{{s}}/\overline{{x}}]\land(\forall\overline{{x}}.\,U^{\prime}\Rightarrow
P\,(z\,\overline{{x}}))$ with $z\in\overline{{z}}$. In general, $G$ has shape
$P\,s$ and so we distinguish cases on $s$:

  * •:

This case is similar to the corresponding (Step) case. If the head symbol of
$s$ is a variable $y\in\overline{{y}}$, it must be that $s$ is of shape $y\
\overline{{v}}$, $y[\overline{{u}}/\overline{{y}}]=z\,\overline{{s_{1}}}$,
$\overline{{v}}[\overline{{u}}/\overline{{y}}]=\overline{{s_{2}}}$ and
$\overline{{s_{1}s_{2}}}=\overline{{s}}$ and we may split $\overline{{x}}$ as
$\overline{{x_{1}}}\overline{{x_{2}}}$ (i.e.
$|\overline{{v}}|=|\overline{{s_{2}}}|=|\overline{{x_{2}}}|$). First observe
that
$H=U^{\prime}[\overline{{s}}/\overline{{x}}]\land(\forall\overline{{x}}.\,U^{\prime}\Rightarrow
P\,(z\,\overline{{x}}))$ can also be written as
$U^{\prime}_{|{\overline{{x_{1}}}}}[\overline{{s}}/\overline{{x_{1}}}]\land(\forall\overline{{x}}.\,U^{\prime}\Rightarrow
P\,(z\,\overline{{x}}))\land
U^{\prime}_{|{\overline{{x_{2}}}}}[\overline{{v}}/\overline{{x_{2}}}][\overline{{u}}/\overline{{y}}]$.
Take $H_{1}$ as the first two conjuncts and $H_{2}$ as the third conjunct.
Take $K$ to be
$U^{\prime}_{|{\overline{{x_{2}}}}}[\overline{{v}}/\overline{{x_{2}}}]$ and
$U$ to be
$\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
P\,(y\ \overline{{x_{2}}})$. Thus (c) holds immediately. Then (a) follows by
(Assm):

$V,\,\overline{{y}}\overline{{z}}\vdash P(y\ \overline{{v}})\triangleright
U^{\prime}_{|{\overline{{x_{2}}}}}[\overline{{v}}/\overline{{x_{2}}}]\wedge(\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
P\,(y\ \overline{{x_{2}}}))$

For (b), observe that $U[\overline{{u}}/\overline{{y}}]$ is
$\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow P\
(z\,\overline{{s_{1}}}\overline{{x_{2}}})$. This rewrites with (Assm) (with
(Imp)) followed by (ImpAnd):

$\displaystyle V,\overline{{z}}\vdash\,$
$\displaystyle\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
P\ (z\,\overline{{s_{1}}}\overline{{x_{2}}})$
$\displaystyle\triangleright\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
U^{\prime}[\overline{{s_{1}}}\overline{{x_{2}}}/\overline{{x}}]\land(\forall\overline{{x}}.\,U^{\prime}\Rightarrow
P\,(z\,\overline{{x}}))$
$\displaystyle\triangleright(\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
U^{\prime}[\overline{{s_{1}}}\overline{{x_{2}}}/\overline{{x}}])\land(\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow(\forall\overline{{x}}.\,U^{\prime}\Rightarrow
P\,(z\,\overline{{x}})))$

The right conjunct rewrites to
$\forall\overline{{x^{\prime}}}.\,U^{\prime}\Rightarrow
P\,(z\,\overline{{x^{\prime}}})$ by (Scope). Note
$U^{\prime}[\overline{{s_{1}}}\overline{{x_{2}}}/\overline{{x}}]$ is
$U^{\prime}_{|{\overline{{x_{1}}}}}[\overline{{s_{1}}}/\overline{{x_{1}}}]\land
U^{\prime}_{|{\overline{{x_{2}}}}}$, so the left conjunct rewrites with
(ImpAnd) and (Scope):

$\displaystyle V,\overline{{z}}\vdash\,$
$\displaystyle\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
U^{\prime}_{|{\overline{{x_{1}}}}}[\overline{{s_{1}}}/\overline{{x_{1}}}]\land
U^{\prime}_{|{\overline{{x_{2}}}}}$
$\displaystyle\triangleright(\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
U^{\prime}_{|{\overline{{x_{1}}}}}[\overline{{s_{1}}}/\overline{{x_{1}}}])\land(\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
U^{\prime}_{|{\overline{{x_{2}}}}})$ $\displaystyle\triangleright
U^{\prime}_{|{\overline{{x_{1}}}}}[\overline{{s_{1}}}/\overline{{x_{1}}}]\land(\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
U^{\prime}_{|{\overline{{x_{2}}}}})$

with the latter conjunct rewriting to $\mathsf{true}$ by the reflexivity of
implication. This gives us a rewrite of $U[\overline{{u}}/\overline{{y}}]$ to
$H_{1}$, proving (b):

$V,\overline{{z}}\vdash(\forall\overline{{x_{2}}}.\,U^{\prime}_{|{\overline{{x_{2}}}}}\Rightarrow
P\
(z\,\overline{{s_{1}}}\overline{{x_{2}}}))\triangleright^{*}U^{\prime}_{|{\overline{{x_{1}}}}}[\overline{{s_{1}}}/\overline{{x_{1}}}]\land(\forall\overline{{x}}.\,U^{\prime}\Rightarrow
P\,(z\,\overline{{x}}))$

  * •:

Otherwise, $s$ is of shape $z\ \overline{{w}}$ and
$\overline{{w}}[\overline{{u}}/\overline{{y}}]=\overline{{s}}$. Then take
$K:=U^{\prime}[\overline{{w}}/\overline{{x}}]$,
$H_{2}:=U^{\prime}[\overline{{s}}/\overline{{x}}]$, and
$U:=(\forall\overline{{x}}.\,U^{\prime}\Rightarrow P\,(z\,\overline{{x}}))$
and $H_{1}:=(\forall\overline{{x}}.\,U^{\prime}\Rightarrow
P\,(z\,\overline{{x}}))$. Now (a) follows by (Assm), (b) is trivial, and (c)
from
$K[\overline{{u}}/\overline{{y}}]=U^{\prime}[\overline{{w}}/\overline{{x}}][\overline{{u}}/\overline{{y}}]=H_{2}$.

(AndL), (AndR):

Since both are similar, we only show the former. In this case
$G[\overline{{u}}/\overline{{y}}]$ has shape
$G_{1}[\overline{{u}}/\overline{{y}}]\wedge
G_{2}[\overline{{u}}/\overline{{y}}]$, $H$ has shape $H_{1}\wedge
G_{2}[\overline{{u}}/\overline{{y}}]$ and we have that $V,\overline{{z}}\vdash
G_{1}[\overline{{u}}/\overline{{y}}]\triangleright H_{1}$. It follows from the
induction hypothesis that there are $K^{\prime}$, $U^{\prime}$ and we may
split $H_{1}$ as $H_{1}^{\prime}$ and $H_{2}^{\prime}$ such that the required
properties hold. Then take $U:=U^{\prime}$, $H_{1}:=H_{1}^{\prime}$,
$K:=K^{\prime}\wedge G_{2}$ and $H_{2}:=H_{2}^{\prime}\wedge
G_{2}[\overline{{u}}/\overline{{y}}]$. Then (a) holds because $G_{1}\wedge
G_{2}\triangleright^{*}U\wedge K^{\prime}\wedge G_{2}$ and both (b) and (c)
follow straightforwardly from the induction hypothesis.

(Imp):

In this case, $G[\overline{{u}}/\overline{{y}}]$ has shape
$\forall\overline{{x}}.\,W\Rightarrow
G^{\prime}[\overline{{u}}/\overline{{y}}]$ and $H$ has shape
$\forall\overline{{x}}.\,W\Rightarrow
H^{\prime}[\overline{{u}}/\overline{{y}}]$ and we have $V,\overline{{z}}\vdash
G^{\prime}[\overline{{u}}/\overline{{y}}]\triangleright H^{\prime}$. Note
that, as $W$ is an automaton body it only contain $\overline{{x}}$. It follows
from the induction hypothesis that there are $K^{\prime}$ and $U^{\prime}$ and
that we can split $H^{\prime}$ as $H_{1}^{\prime}\wedge H_{2}^{\prime}$, such
that the required properties hold. Then take $U:=U^{\prime}$,
$H_{1}:=H_{1}^{\prime}$, $K:=\forall\overline{{z}}.\,W\Rightarrow K^{\prime}$
and $H_{2}:=\forall\overline{{z}}.\,W\Rightarrow H_{2}^{\prime}$. Then (a)
follows because $U$ can only contain the $\overline{{y}}$ as free variables,
we can apply scoping to deduce:

$V,\overline{{y}}\overline{{z}}\vdash\forall\overline{{x}}.\,W\Rightarrow
G^{\prime}\triangleright\forall\overline{{x}}.\,W\Rightarrow K^{\prime}\wedge
U^{\prime}\triangleright(\forall\overline{{x}}.\,W\Rightarrow
K^{\prime})\wedge U^{\prime}$

and properties (b) and (c) follow from the induction hypothesis.

(ImpAnd):

In this case, $G[\overline{{u}}/\overline{{y}}]$ has shape
$\forall\overline{{x}}.\,U^{\prime}\Rightarrow
G_{2}[\overline{{u}}/\overline{{y}}]\wedge
G_{3}[\overline{{u}}/\overline{{y}}]$. Set $U:=\mathsf{true}$,
$H_{1}:=\mathsf{true}$, $K:=(\forall\overline{{x}}.\,U^{\prime}\Rightarrow
G_{2})\wedge(\forall\overline{{x}}.\,U^{\prime}\Rightarrow G_{3})$ and
$H_{2}:=H$. Then (a) follows by (ImpAnd), (b) and (c) are immediate.

(Scope):

In this case, $G[\overline{{u}}/\overline{{y}}]$ has shape
$\forall\overline{{x}}.\,U^{\prime}\Rightarrow
G[\overline{{u}}/\overline{{y}}]$ and $H$ has shape
$G[\overline{{u}}/\overline{{y}}]$. We assume
$G[\overline{{u}}/\overline{{y}}]$ does not contain any variable from
$\overline{{x}}$. Hence, neither does $G$ and so we can rewrite:

$V,\overline{{y}}\overline{{z}}\vdash\forall\overline{{x}}.\,U^{\prime}\Rightarrow
G\triangleright G$

Hence, the result follows by taking $U:=\mathsf{true}$,
$H_{1}:=\mathsf{true}$, $K:=G$ and $H_{2}:=G[\overline{{u}}/\overline{{y}}]$.

∎

###  C.1. Completeness

To show that $D\models G$ implies $\mathcal{V}(D)\models G$, we will argue
that one can use a proof of $D\vdash G$ as a guide to follow in order to
obtain exactly the automaton clauses $V\subseteq\mathcal{V}(D)$ needed to
replay the proof as $V\vdash G\triangleright\mathsf{true}$. Clearly, the main
aim of our argument will be to show that, wherever we made a resolution step
using a clause from $D$ in the proof of $D\vdash G$, we can find an automaton
clause in $\mathcal{V}(D)$ with which to simulate it when rewriting.

To see why, consider again the proof in Figure 4. We can observe that the
resolution steps at the leaves of the proof necessarily involve an automaton
clause as the side premise: it cannot be otherwise since a resolution step at
a leaf must be via a clause that has a vacuous body, such as
$\mathsf{true}\Rightarrow\mathsf{Closed}(\mathsf{c})$, and clauses of this
form are necessarily automaton.

Then, there may be many consecutive resolution steps leading up to this leaf
that all happen to involve clauses from $D$ that are automaton already. We
observe that such a situation gives rise to a maximal subproof, say of
$D\vdash H$ which can be viewed equivalently as a proof $\mathcal{V}(D)\vdash
H$, since it uses only clauses that are automaton (and hence in
$\mathcal{V}(D)$). In the case of Figure 4, the subproof rooted at
$\mathsf{V}(\mathsf{read}\ \mathsf{c}\ (\mathsf{putCont}\ \mathsf{id}))$ is of
this form, since (18) and (7) both happen to be automaton.

If the subproof $D\vdash H$ is the largest that contains only automaton
inferences, then continuing down the proof tree, the next resolution step
involves a clause from $D$ that is not itself automaton. Let us say that this
inference is of shape:

$\prftree[r,l]{(\forall\overline{{y}}.\ G^{\prime}\Rightarrow A)\in
D}{\textsf{\small{(Res)}}}{D\vdash
G^{\prime}[\overline{{s}}/\overline{{y}}]}{D\vdash
A[\overline{{s}}/\overline{{y}}]}$

and, for simplicity, that $H=G^{\prime}[\overline{{s}}/\overline{{y}}]$. The
fact that $\forall\overline{{y}}.\ G^{\prime}\Rightarrow A$ is not automaton
indicates that $G^{\prime}$ is not of the correct form. However, the subproof
$\mathcal{V}(D)\vdash H$ that sits on top of this inference shows us how to
prove $G^{\prime}[\overline{{s}}/\overline{{y}}]$ using only resolution with
automaton clauses. We can view this proof as a specification for rewriting
$G^{\prime}[\overline{{s}}/\overline{{y}}]$ to $\mathsf{true}$, we just need
to perform the same resolution steps in the same order. The following lemma
shows that performing the same rewriting sequence on the raw goal $G^{\prime}$
(which is the body that is preventing the (Res) inference from being
automaton) will give rise to an automaton formula.

###### Lemma C.3 (Decomposition).

If $V\vdash G[\overline{{u}}/\overline{{y}}]\triangleright^{*}\mathsf{true}$
then there is some $U$ such that:

  1. (a)

$V,\,\overline{{y}}\vdash G\triangleright^{*}U$

  2. (b)

and $V\vdash U[\overline{{u}}/\overline{{y}}]\triangleright^{*}\mathsf{true}$

###### Proof.

By induction on the length $n$ of the rewrite sequence $V\vdash
G[\overline{{u}}/\overline{{y}}]\triangleright^{n}\mathsf{true}$.

  * •

When $n=1$, $G=\mathsf{true}$ and so we can take $U:=\mathsf{true}$ too.

  * •

Otherwise, the sequence has shape $V\vdash
G[\overline{{u}}/\overline{{y}}]\triangleright
H\triangleright^{n-1}\mathsf{true}$ and we can invoke progress (Lemma C.2) to
obtain some $U^{\prime}$ and $K$ such that (a) $V\vdash
G\triangleright^{*}U^{\prime}\wedge K$ and we can split $H$ as $H_{1}\wedge
H_{2}$ with $V\vdash
U^{\prime}[\overline{{u}}/\overline{{y}}]\triangleright^{*}H_{1}$ and
$K[\overline{{u}}/\overline{{y}}]=H_{2}$. Since $V\vdash
H\triangleright^{n-1}\mathsf{true}$, there are sequences $V\vdash
H_{1}\triangleright^{*}\mathsf{true}$ and $V\vdash
H_{2}\triangleright^{*}\mathsf{true}$ of length at most $n-1$. So, by the
induction hypothesis, we obtain some $U^{\prime\prime}$ such that $V\vdash
K\triangleright^{*}U^{\prime\prime}$ and $V\vdash
U^{\prime\prime}[\overline{{u}}/\overline{{y}}]\triangleright^{*}\mathsf{true}$.
Hence, we choose $U:=U^{\prime}\wedge U^{\prime\prime}$.

∎

For example, in Figure 4, although the resolution step rooted at
$\mathsf{V}(\mathsf{putStrLn}\ \mathsf{read}\ \mathsf{c}\ \mathsf{id})$ uses
clause (10), namely $\forall x\,h\,k.\ \mathsf{V}(x\ h\ (\mathsf{putCont}\
k))\Rightarrow\mathsf{V}(\mathsf{putStrLn}\ x\ h\ k)$, the proof above this
point shows us that resolving with automaton clauses (7) and (18) allows for
rewriting $\mathsf{V}(\mathsf{read}\ \mathsf{c}\ (\mathsf{putCont}\
\mathsf{id}))$ to $\mathsf{true}$:

$\mathsf{V}(\mathsf{read}\ \mathsf{c}\ (\mathsf{putCont}\
\mathsf{id}))\triangleright\mathsf{Closed}(\mathsf{c})\triangleright\mathsf{true}$

Using (Assm), we can simulate these same resolution steps on the raw body of
clause (10) to obtain a new automaton formula:

$\mathsf{V}(x\ h\ (\mathsf{putCont}\
k))\triangleright\mathsf{Closed}(h)\wedge(\forall h^{\prime}\,k^{\prime}.\
\mathsf{Closed}(h^{\prime})\Rightarrow\mathsf{V}(x\ h^{\prime}\ k^{\prime}))$

Here, we are adding the assumption that $x$ behaves like $\mathsf{read}$ does,
according to clause (7). This then justifies adding a new automaton clause to
$\mathcal{V}(D)$ corresponding to (10):

$\forall x\,h\,k.\ \mathsf{Closed}(h)\wedge(\forall h^{\prime}\,k^{\prime}.\
\mathsf{Closed}(h^{\prime})\Rightarrow\mathsf{V}(x\ h^{\prime}\
k^{\prime}))\Rightarrow\mathsf{V}(\mathsf{putStrLn}\ x\ h\ k)$

This new clause allows us to extend our subproof now one further deduction,
to:

$D\vdash\mathsf{V}(\mathsf{putStrLn}\ \mathsf{read}\ \mathsf{c}\ \mathsf{id})$

This reflects that $\mathcal{V}(D)\vdash\mathsf{V}(\mathsf{putStrLn}\
\mathsf{read}\ \mathsf{c}\ \mathsf{id})\triangleright^{*}\mathsf{true}$. By
repeating this process we can replay the whole deduction using only automaton
clauses from $\mathcal{V}(D)$. Hence:

See 4.7

###### Proof.

We show $D\vdash G$ implies $\mathcal{V}(D)\vdash
G\triangleright^{*}\mathsf{true}$ by induction on the proof $D\vdash G$. The
result then follows from soundness (Theorem 4.5).

(True):

The result is immediate.

(Res):

In this case, $G$ is of shape $P\ s[\overline{{u}}/\overline{{y}}]$. The
premise is $D\vdash H[\overline{{u}}/\overline{{y}}]$ for some
$(\forall\overline{{y}}.\,H\Rightarrow P\ s)\in D$. It follows from the
induction hypothesis that $\mathcal{V}(D)\vdash
H[\overline{{u}}/\overline{{y}}]\triangleright^{*}\mathsf{true}$. Hence, by
decomposition, there is some $U$ such that
$\mathcal{V}(D),\,\overline{{y}}\vdash H\triangleright^{*}U$ and
$\mathcal{V}(D)\vdash
U[\overline{{u}}/\overline{{y}}]\triangleright^{*}\mathsf{true}$. Then, by
definition, $(\forall\overline{{y}}.\,U\Rightarrow P\ s)\in\mathcal{V}(D)$ and
so we can use (Step) to rewrite $\mathcal{V}(D)\vdash P\
s[\overline{{u}}/\overline{{y}}]\triangleright
U[\overline{{u}}/\overline{{y}}]\triangleright^{*}\mathsf{true}$, as required.

(And):

In this case, $G$ is of shape $H_{1}\wedge H_{2}$ and it follows from the
induction hypothesis that $\mathcal{V}(D)\vdash
H_{1}\triangleright^{*}\mathsf{true}$ and $\mathcal{V}(D)\vdash
H_{2}\triangleright^{*}\mathsf{true}$. Hence, the result follows
straightforwardly.

∎

###  C.2. Decidability

###### Theorem C.4 (Decidability).

Let $V$ be an automaton formula, $\overline{y}$ is a sequence of variables,
$G$ an arbitary goal formula and $U$ an automaton formula. Then
$V,\,\overline{y}\vdash G\triangleright^{*}U$ is decidable.

###### Proof.

###### Definition C.5.

The _weight_ of a clause is defined as follows:

$\displaystyle\mathsf{weight}(\textsf{true})$ $\displaystyle\coloneqq 0$
$\displaystyle\mathsf{weight}(P\ t)$ $\displaystyle\coloneqq 0pt{t}$
$\displaystyle\mathsf{weight}(G\wedge H)$
$\displaystyle\coloneqq\mathsf{weight}(G)+\mathsf{weight}(H)$
$\displaystyle\mathsf{weight}(\forall\overline{{x}}.\,U\Rightarrow\textsf{true})=1$
$\displaystyle\mathsf{weight}(\forall\overline{x}.\,U\Rightarrow P\ t)$
$\displaystyle\coloneqq\begin{cases}0pt{t}&\textrm{if}\
\mathsf{FV}(t)\cap\\{x\\}\neq\emptyset\\\
1+0pt{t}&\textrm{otherwise}\end{cases}$
$\displaystyle\mathsf{weight}(\forall\overline{x}.\,U\Rightarrow H_{1}\wedge
H_{2})$ $\displaystyle\coloneq
1+\mathsf{weight}(\forall\overline{{x}}.\,U\Rightarrow
H_{1})+\mathsf{weight}(\forall\overline{{x}}.\,U\Rightarrow H_{2})$
$\displaystyle\mathsf{weight}(\forall\overline{x}.\,U\Rightarrow(\forall\overline{y}.\,V\Rightarrow
G))$ $\displaystyle\coloneq
1+\mathsf{weight}(\forall\overline{y}.\,V\Rightarrow G)$

When multiple cases apply due to the quotient structure of conjunction, we
take the smallest weight.

###### Lemma C.6.

If $\mathsf{measure}(G)<\mathsf{measure}(G^{\prime})$, then
$\mathsf{measure}(\forall\overline{{x}}.U\Rightarrow
G)<\mathsf{measure}(\forall\overline{{x}}.U\Rightarrow G^{\prime})$.

###### Lemma C.7.

If $U$ is an automaton formula, then the weight of
$U[\overline{{s}}/\overline{{x}}]$ is at most $\max\\{0pt{s}\mid
s\in\overline{{s}}\\}$.

###### Proof.

In the case of $(P\ x)[\overline{{s}}/\overline{{x}}]$, we have that weight is
bounded by $\max\\{0pt{s}\mid s\in\overline{{s}}\\}$ as $x$ may be
instantiated with any $\overline{{s}}$. For
$(\forall\overline{{z}}.\,U\Rightarrow P\ (x\
\overline{{z}}))[\overline{{s}}/xx]$, we have weight
$0pt{s}\leq\max\\{0pts\mid\in\overline{{s}}\\}$ as $U$ only contains the
variables $\overline{{z}}$. Otherwise, $U$ is a conjunction of both cases and
we can proceed by structural induction. ∎

###### Lemma C.8.

Let $V$ be an automaton formula, $\overline{y}$ is a sequence of variables,
and $G$ and $H$ formulas such that $V,\,\overline{{y}}\vdash G\triangleright
H$. Then $\mathsf{weight}(H)<\mathsf{weight}(G)$.

###### Proof.

We proceed by induction on $V,\,\overline{{y}}\vdash G\triangleright H$:

(Refl):

Trivial.

(Step):

This case $G$ is the atom $P\ (f\ \overline{{s}})$ and has depth
$1+\max\\{0pts\mid s\in\overline{{s}}\\}$. By the previous lemma, the weight
of $U[\overline{{s}}/\overline{{x}}]$ is at most $\max\\{0pts\mid
s\in\overline{{s}}\\}$ as it is an automaton body. Therefore, we have a proper
decrease as required.

(Assm):

In this case, $G$ is the atom $P\ (x\ ss)$ which has depth $1+\max\\{0pts\mid
s\in\overline{{s}}\\}$ and the reduct is
$U[\overline{{s}}/\overline{{z}}]\wedge(\forall\overline{{z}}.\,U\Rightarrow
P\ (x\ \overline{{z}}))$ which has depth $\max\\{0pt{s}\mid
s\in\overline{{s}}\\}$, again by the previous lemma. Thus this case is also
satisfied.

(AndL), (AndR):

Trivial.

(Imp):

In this case, the goal is $\forall\overline{{x}}.\,U\Rightarrow G$ where $G$
is not of the form $P\ (y\ \overline{{x}})$. By induction on $V\wedge
U,\,\overline{{y}}\vdash G\triangleright G^{\prime}$, we have that
$\mathsf{weight}(G^{\prime})<\mathsf{weight}(G)$. Therefore,
$\textsf{measure}(\forall\overline{{x}}.\,U\Rightarrow
G)<\textsf{measure}(\forall\overline{{x}}.\,U\Rightarrow G^{\prime})$ as
required.

(ImpAnd):

Trivial.

(Scope):

In this case, the goal is $\forall\overline{{x}}.\,U\Rightarrow G$ where
$\mathsf{FV}{G}\cap\overline{{x}}=\emptyset$. Consider inductively the
possible shapes of $G$:

  * •:

$\mathsf{true}$ — the measure is $1$ and after rewritting is $0$.

  * •:

$P\ t$ — the measure is $1+0pt{t}$ and after rewriting is $1$.

  * •:

$G_{1}\wedge G_{2}$ — the measure is
$1+\textsf{measure}(\forall\overline{{x}}.\,U\Rightarrow
G_{1})+\textsf{measure}(\forall\overline{{x}}.\,U\Rightarrow
G_{2})>1+\textsf{measure}(G_{1})+\textsf{measure}(G_{2})$ and after rewritting
it is just $\textsf{measure}(G_{1})+\textsf{measure}(G_{2})$.

  * •:

Finally, for $\forall\overline{{y}}.\,U^{\prime}\Rightarrow G$, the measure is
$1+\textsf{measure}(\forall\overline{{y}}.\,U^{\prime}\Rightarrow G)$ and
after rewriting it is
$\textsf{measure}(\forall\overline{{y}}.\,U^{\prime}\Rightarrow G)$.

In each case, we have a strict decrease as required.

∎

###### Corollary C.9.

For any choice of $V$, $\overline{y}$ and $G$, there are finitely many reducts
$G^{\prime}$ such that $V,\,\overline{{y}}\vdash G\triangleright G^{\prime}$.

∎

##  Appendix D Supporting Material for Section 5

###  D.1. Types

##### Subtyping rules.

(Q-Bas):

if $(q_{1},q_{2})\in\Theta$, then $q_{1}\leq q_{2}$

(Q-Arr):

if ${\sigma_{\mathsf{t}}}_{2}\leq{\sigma_{\mathsf{t}}}_{1}$ and
$\tau_{1}\leq\tau_{2}$, then
${\sigma_{\mathsf{t}}}_{1}\to\tau_{1}\leq{\sigma_{\mathsf{t}}}_{2}\to\tau_{2}$

(Q-Fun):

if $\bigwedge_{i=1}^{n}\tau_{i}\leq\tau$, then
$\bigwedge_{i=1}^{n}({\sigma_{\mathsf{t}}}\to\tau_{i})\leq{\sigma_{\mathsf{t}}}\to\tau$

(Q-Prj):

for all $1\leq i\leq n$, $\bigwedge_{j=1}^{n}\tau_{j}\leq\tau_{i}$

(Q-Glb):

if, for all $1\leq i\leq n$, ${\sigma_{\mathsf{t}}}\leq\tau_{i}$, then
${\sigma_{\mathsf{t}}}\leq\bigwedge_{j=1}^{n}\tau_{j}$

(Q-Trs):

if $\theta_{1}\leq\theta_{2}$ and $\theta_{2}\leq\theta_{3}$, then
$\theta_{1}\leq\theta_{3}$

###### Lemma D.1.

$\textstyle\bigwedge_{i=1}^{n}\tau_{i}\leq\bigwedge_{j=1}^{m}\tau_{j}^{\prime}\quad\iff\quad\forall
j\in[1..m].\,\exists i_{j}\in[1..n].\,\tau_{i_{j}}\leq\tau_{j}^{\prime}$

###### Proof.

Direction $\Leftarrow$ follows from (Q-Glb) followed by (Q-Trs) and (Q-Prj).

For $\Rightarrow$, suppose
$\bigwedge_{i=1}^{n}\tau_{i}\leq\bigwedge_{j=1}^{m}\tau_{j}^{\prime}$. We use
induction on the subtyping rules, of which (Q-Bas), (Q-Prj), and (Q-Arr) are
immediate.

(Q-Fun):

Here, $j=1$ and the assumption is some
$\bigwedge_{i=1}^{n}({\sigma_{\mathsf{t}}}\to\tau_{i})\leq({\sigma_{\mathsf{t}}}\to\tau^{\prime})$.
The premise is $\bigwedge_{i=1}^{n}\tau_{i}\leq\tau^{\prime}$. By the IH,
there exists $i\in[1..n]$ such that $\tau_{i}\leq\tau^{\prime}$. It follows
from (Q-Arr) that
${\sigma_{\mathsf{t}}}\to\tau_{i}\leq{\sigma_{\mathsf{t}}}\to\tau^{\prime}$,
which proves the claim.

(Q-Glb):

The premises are $\bigwedge_{i=1}^{n}\tau_{i}\leq\tau_{j}^{\prime}$, for all
$j\in[1..m]$. By the IH, there exists $i_{j}\in[1..n]$ such that
$\tau_{i_{j}}\leq\tau_{j}^{\prime}$, for all $j\in[1..m]$, as required.

(Q-Trs):

The premises give us $\theta$ such that
$\bigwedge_{i=1}^{n}\tau_{i}\leq\theta$ and
$\theta\leq\bigwedge_{j=1}^{m}\tau_{j}^{\prime}$. Let $j\in[1..m]$. By the IH,
there exists $\tau^{\prime\prime}_{k}\in\theta$ such that
$\tau^{\prime\prime}_{k}\leq\tau^{\prime}_{j}$. Furthermore, there exists
$i_{k}\in[1..n]$ such that $\tau_{i_{k}}\leq\tau^{\prime\prime}_{k}$. By
transitivity, $\tau_{i_{k}}\leq\tau^{\prime}_{j}$, as required.

∎

###### Lemma D.2 (Weakening).

If $\Gamma\vdash{t}::{\tau}$ and $\overline{{z}}\cap\mathsf{FV}(t)=\emptyset$,
then
$\Gamma,{\overline{{z}}}::{\overline{{{\sigma_{\mathsf{t}}}}}}\vdash{t}::{\tau}$
for all $\overline{{{\sigma_{\mathsf{t}}}}}$ of the appropriate types. Idem
for ${G}::{\top_{o}}$.

###  D.2. Typing-rewriting correspondence

###### Lemma D.3.

If $V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow G_{1}\land
G_{2})\triangleright^{*}U^{\prime}$, then there exist
$U_{1}^{\prime},U_{2}^{\prime}$ such that
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
G_{1})\triangleright^{*}U_{1}^{\prime}$ and
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
G_{2})\triangleright^{*}U_{2}^{\prime}$ and $U^{\prime}=U_{1}^{\prime}\land
U_{2}^{\prime}$.

###### Lemma D.4.

For automaton formulas $U$ and $U^{\prime}$ over $\overline{{z}}$,
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
U^{\prime})\triangleright^{*}\mathsf{true}$ if and only if
$U\mathrel{\leq_{\mathsf{a}}}U^{\prime}$.

###### Proof.

We prove the claim by induction on automaton clause $U^{\prime}$: an outer
induction on the types of the variables in $U^{\prime}$ and an inner induction
on the number of conjuncts. First, note that both
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
U^{\prime})\triangleright^{*}\mathsf{true}$ and
$U\mathrel{\leq_{\mathsf{a}}}U^{\prime}$ hold for $U^{\prime}=\mathsf{true}$.

Proof of direction $\Rightarrow$:

  * •

Suppose $V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
P\,z_{i})\triangleright^{*}\mathsf{true}$. This rewrite must start with (Imp)
with (Refl), which has $P\,z_{i}\in U$ as side condition. It is immediate that
$\mathsf{fromCl}({U_{|{z_{i}}}})\leq\mathsf{fromCl}({{P\,z_{i}}_{|{z_{i}}}})$
and $U\mathrel{\leq_{\mathsf{a}}}P\,z_{i}$ follows.

  * •

Suppose $V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
U_{1}^{\prime}\land U_{2}^{\prime})\triangleright^{*}\mathsf{true}$ for
$U_{1}^{\prime},U_{2}^{\prime}$ containing only $z_{i}$ of type $\iota$ (and
at least one such $z_{i}$ each). By Lemma D.3, we may assume WLOG that this
rewrite starts with (ImpAnd), i.e.
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
U_{1}^{\prime}\land
U_{2}^{\prime})\triangleright(\forall\overline{{z}}.\,U\Rightarrow
U_{1}^{\prime})\land(\forall\overline{{z}}.\,U\Rightarrow
U_{2}^{\prime})\triangleright^{*}\mathsf{true}$. Thanks to (AndL) and (AndR),
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
U_{1}^{\prime})\triangleright^{*}\mathsf{true}$ and
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
U_{2}^{\prime})\triangleright^{*}\mathsf{true}$. We apply the IH for
$U\mathrel{\leq_{\mathsf{a}}}U_{1}^{\prime}$ and
$U\mathrel{\leq_{\mathsf{a}}}U_{2}^{\prime}$. Clearly, also
$U\mathrel{\leq_{\mathsf{a}}}U_{1}^{\prime}\land U_{2}^{\prime}$.

  * •

Suppose
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow(\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
P\,(z_{i}\,\overline{{x}})))\triangleright^{*}\mathsf{true}$ for some
$\overline{{x}}=x_{1}\dots x_{m}$.

    * –

Suppose this rewrite starts with (Imp). The only option for the premise is
another (Imp) with $V\land U\land U^{\prime\prime},\overline{{y}}\vdash
P\,(z_{i}\,\overline{{x}}))\triangleright U^{\prime\prime\prime}$ as premise.
We proceed as in the previous subcase.

  * •

Suppose $V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
U_{1}^{\prime}\land U_{2}^{\prime})\triangleright^{*}\mathsf{true}$. Again,
Lemma D.3 allows us to assume WLOG that this rewrite starts with (ImpAnd). We
proceed as in the first-order case.

Proof of direction $\Leftarrow$:

  * •

Suppose $U\mathrel{\leq_{\mathsf{a}}}P\,z_{i}$. This means that
$\mathsf{fromCl}({U_{|{z_{i}}}})\leq q_{P}$ and, thus,
$q_{P}\in\mathsf{fromCl}({U_{|{z_{i}}}})$ and $P\,z_{i}\in U$. We prove
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
P\,z_{i})\triangleright^{*}\mathsf{true}$ by (Imp) with (Refl), followed by
(Scope).

  * •

Suppose $U\mathrel{\leq_{\mathsf{a}}}U_{1}^{\prime}\land U_{2}^{\prime}$
containing only $z_{i}$ of type $\iota$ (and at least one such $z_{i}$ each).
This means that
$\mathsf{fromCl}({U_{|{z_{i}}}})\leq\mathsf{fromCl}({(U_{1}^{\prime}\land
U_{2}^{\prime})_{|{z_{i}}}})$, for all $i\in[1..n]$. Clearly, also
$\mathsf{fromCl}({U_{|{z_{i}}}})\leq\mathsf{fromCl}({{U_{1}}^{\prime}_{|{z_{i}}}})$
and
$\mathsf{fromCl}({U_{|{z_{i}}}})\leq\mathsf{fromCl}({{U_{2}}^{\prime}_{|{z_{i}}}})$,
for all $i\in[1..n]$. We now apply the IH to
$U\mathrel{\leq_{\mathsf{a}}}U_{1}^{\prime}$ and
$U\mathrel{\leq_{\mathsf{a}}}U_{2}^{\prime}$ for
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
U_{1}^{\prime})\triangleright^{*}\mathsf{true}$ and
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
U_{2}^{\prime})\triangleright^{*}\mathsf{true}$. This gives us a rewrite
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
U_{1}^{\prime})\land(\forall\overline{{z}}.\,U\Rightarrow
U_{2}^{\prime})\triangleright^{*}\mathsf{true}$ to which we prepend an
(ImpAnd)-step for $V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow
U_{1}^{\prime}\land U_{2}^{\prime})\triangleright^{*}\mathsf{true}$.

  * •

Suppose
$U\mathrel{\leq_{\mathsf{a}}}(\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
P\,(z_{i}\,\overline{{x}}))$ for some $\overline{{x}}=x_{1}\dots x_{m}$. This
means
$\mathsf{fromCl}({U_{|{z_{i}}}})\mathrel{\leq_{\mathsf{a}}}\mathsf{fromCl}({\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
P\,(z_{i}\,\overline{{x}})})$. By Lemma D.1, there exists
$(\forall\overline{{x}}.\,U^{\prime\prime\prime}\Rightarrow
P\,(z_{i}\,\overline{{x}}))\in U_{|{z_{i}}}$ such that
$\mathsf{fromCl}({\forall\overline{{x}}.\,U^{\prime\prime\prime}\Rightarrow
P\,(z_{i}\,\overline{{x}})})\mathrel{\leq_{\mathsf{a}}}\mathsf{fromCl}({\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
P\,(z_{i}\,\overline{{x}})})$.

This gives us
$\mathsf{fromCl}({U^{\prime\prime}_{|{x_{j}}}})\leq\mathsf{fromCl}({U^{\prime\prime\prime}_{|{x_{j}}}})$,
for all $j\in[1..m]$. This implies
$U^{\prime\prime}\mathrel{\leq_{\mathsf{a}}}U^{\prime\prime\prime}$, to which
we can apply the IH for
$V,\overline{{y}}\vdash(\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
U^{\prime\prime\prime})\triangleright^{*}\mathsf{true}$, because the types of
$\overline{{x}}$ are smaller than the type of $z_{i}$. Trivially, also $V\land
U,\overline{{y}}\vdash(\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
U^{\prime\prime\prime})\triangleright^{*}\mathsf{true}$.

We prepend (Step) with side condition
$(\forall\overline{{x}}.\,U^{\prime\prime\prime}\Rightarrow
P\,(z_{i}\,\overline{{x}}))\in U$ to this rewrite to obtain $V\land
U,\overline{{y}}\vdash(\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
P\,(z_{i}\,\overline{{x}}))\triangleright(\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
U^{\prime\prime\prime})\triangleright^{*}\mathsf{true}$. We replicate this
rewrite under an implication using (Imp) and conclude it with (Scope):

$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U\Rightarrow(\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
P\,(z_{i}\,\overline{{x}})))\triangleright^{*}(\forall\overline{{z}}.\,U\Rightarrow\mathsf{true})\triangleright\mathsf{true}$

This proves the case.

  * •

Suppose $U\mathrel{\leq_{\mathsf{a}}}U_{1}^{\prime}\land U_{2}^{\prime}$. As
the inductive first-order case.

∎

###### Lemma D.5 (Monotonicity of rewrite).

For all terms $t:\sigma_{1}\to\dots\to\sigma_{k}\to\iota$ over
$\overline{{y}}$, if ${\sigma_{\mathsf{t}}}\leq{\sigma_{\mathsf{t}}}^{\prime}$
and
$V,\overline{{y}}\vdash\mathsf{toCl}({{\sigma_{\mathsf{t}}}})({t})\triangleright^{*}U$,
then there exists $U^{\prime}$ such that
$V,\overline{{y}}\vdash\mathsf{toCl}({{\sigma_{\mathsf{t}}}^{\prime}})({t})\triangleright^{*}U^{\prime}$
and $U\mathrel{\leq_{\mathsf{a}}}U^{\prime}$.

###### Proof.

Let ${\sigma_{\mathsf{t}}}=\bigwedge_{i=1}^{n}\tau_{i}$ and
${\sigma_{\mathsf{t}}}^{\prime}=\bigwedge_{j=1}^{m}\tau_{j}^{\prime}$ such
that ${\sigma_{\mathsf{t}}}\leq{\sigma_{\mathsf{t}}}^{\prime}$ and
$V,\overline{{y}}\vdash\mathsf{toCl}({{\sigma_{\mathsf{t}}}})({t})\triangleright^{*}U$.
By Subtyping Lemma D.1, $\forall j\in[1..m].\,\exists
i_{j}\in[1..n].\,\tau_{i_{j}}\leq\tau_{j}^{\prime}$. Clearly,
${\sigma_{\mathsf{t}}}={\sigma_{\mathsf{t}}}^{\prime\prime}\land\bigwedge_{j=1}^{m}\tau_{i_{j}}$
for some ${\sigma_{\mathsf{t}}}^{\prime\prime}$ and, thus,
$\mathsf{toCl}({{\sigma_{\mathsf{t}}}})({t})=\mathsf{toCl}({{\sigma_{\mathsf{t}}}^{\prime\prime}})({t})\land\mathsf{toCl}({\bigwedge_{j=1}^{m}\tau_{i_{j}}})({t})$.

This allows us to derive separate rewrites
$V,\overline{{y}}\vdash\mathsf{toCl}({{\sigma_{\mathsf{t}}}^{\prime\prime}})({t})\triangleright^{*}U_{1}$
and
$V,\overline{{y}}\vdash\mathsf{toCl}({\bigwedge_{j=1}^{m}\tau_{i_{j}}})({t})\triangleright^{*}U_{2}$
such that $U=U_{1}\land U_{2}$ from assumption
$V,\overline{{y}}\vdash\mathsf{toCl}({{\sigma_{\mathsf{t}}}})({t})\triangleright^{*}U$.
Furthermore,
$\mathsf{toCl}({\bigwedge_{j=1}^{m}\tau_{i_{j}}})({t})=\mathsf{toCl}({\tau_{i_{1}}})({t})\land\dots\land\mathsf{toCl}({\tau_{i_{m}}})({t})$
allows us to separate the latter rewrite into
$V,\overline{{y}}\vdash\mathsf{toCl}({\tau_{i_{j}}})({t})\triangleright^{*}U_{2,j}$,
for all $j\in[1..m]$, such that $U_{2}=U_{2,1}\land\dots\land U_{2,m}$.

We aim to show that
$V,\overline{{y}}\vdash\mathsf{toCl}({\tau_{i_{j}}})({t})\triangleright^{*}U_{2,j}$
determines a
$V,\overline{{y}}\vdash\mathsf{toCl}({\tau_{j}^{\prime}})({t})\triangleright^{*}U_{2,j}^{\prime}$
with $U_{2,j}\mathrel{\leq_{\mathsf{a}}}U_{2,j}^{\prime}$, for all
$j\in[1..m]$. This suffices due to
$\mathsf{toCl}({{\sigma_{\mathsf{t}}}^{\prime}})({t})=\bigwedge_{j=1}^{m}\mathsf{toCl}({\tau_{j}^{\prime}})({t})$
and:

$U\mathrel{\leq_{\mathsf{a}}}U_{2}=\textstyle\bigwedge_{j=1}^{m}U_{2,j}\mathrel{\leq_{\mathsf{a}}}\bigwedge_{j=1}^{m}U_{2,j}^{\prime}$

We use case analysis on the type of $t$.

Suppose $t:\iota$. We only have trivial subtyping for type $\iota$, so
$\forall j\in[1..m].\,\exists
i_{j}\in[1..n].\,\tau_{i_{j}}=\tau_{j}^{\prime}$. The claim is immediate.

Suppose $t:\sigma_{1}\to\dots\to\sigma_{k}\to\iota$ for $k>0$. Fix a
$j\in[1..m]$ with a corresponding $i_{j}\in[1..n]$. Let
$\tau_{i_{j}}=\theta_{1}\to\dots\to\theta_{k}\to q_{P}$ and
$\tau_{j}^{\prime}=\theta_{1}^{\prime}\to\dots\to\theta_{k}^{\prime}\to
q_{P}$. We know from $\tau_{i_{j}}\leq\tau_{j}^{\prime}$ that
$\theta_{\ell}^{\prime}\leq\theta_{\ell}$, for all $\ell\in[1..k]$.

Consider the rewrite
$V,\overline{{y}}\vdash\mathsf{toCl}({\tau_{i_{j}}})({t})\triangleright^{*}U_{2,j}$
we obtained from assumption
$V,\overline{{y}}\vdash\mathsf{toCl}({{\sigma_{\mathsf{t}}}})({t})\triangleright^{*}U$;
since $\tau_{i_{j}}=\theta_{1}\to\dots\to\theta_{k}\to q_{P}$, it is equal to:

(†) $\displaystyle
V,\overline{{y}}\vdash(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta}}})({\overline{{z}}})\Rightarrow
P\,(t\,\overline{{z}}))\triangleright^{*}U_{2,j}$

We proceed by case analysis on the length of this rewrite † ‣ D.2.

  * •

Suppose rewrite † ‣ D.2 has length 0. Then,
$U_{2,j}=(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta}}})({\overline{{z}}})\Rightarrow
P\,(t\,\overline{{z}}))$ is automaton wrt $\overline{{y}}$. Clearly,
$(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta^{\prime}}}})({\overline{{z}}})\Rightarrow
P\,(t\,\overline{{z}}))$ is also automaton wrt $\overline{{y}}$, and
trivially:

$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta^{\prime}}}})({\overline{{z}}})\Rightarrow
P\,(t\,\overline{{z}}))\triangleright^{*}(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta^{\prime}}}})({\overline{{z}}})\Rightarrow
P\,(t\,\overline{{z}}))$

The inequality
$(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta}}})({\overline{{z}}})\Rightarrow
P\,(t\,\overline{{z}}))\mathrel{\leq_{\mathsf{a}}}(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta^{\prime}}}})({\overline{{z}}})\Rightarrow
P\,(t\,\overline{{z}}))$ concludes this subcase, which follows from
$\theta_{\ell}^{\prime}\leq\theta_{\ell}$, for all $\ell\in[1..k]$.

  * •

Suppose rewrite † ‣ D.2 has length greater than 0. The rewrite starts with
either (Step) or (Assm), depending on the top-level symbol in $t$. The case
for (Assm) is analogous to (Step); it merely introduces an extra conjunct that
is already automaton (in which case both the rewrite of
$\mathsf{toCl}({\tau_{i_{j}}})({t})$ and
$\mathsf{toCl}({\tau^{\prime}_{j}})({t})$ will introduce it; it must be a
conjunct in $U_{2,j}$ and $U_{2,j}^{\prime}$). Therefore, we assume
$t=f\,\overline{{t^{\prime}}}$ for some $f\in\Sigma$, so (Step) with some
$(\forall\overline{{x_{1}}}\,\overline{{x_{2}}}.\,U^{\prime\prime}\Rightarrow
P\,(f\,\overline{{x_{1}}}\,\overline{{x_{2}}}))\in V$ is the first rewrite
step in † ‣ D.2, resulting in:

$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta}}})({\overline{{z}}})\Rightarrow
P\,(t\,\overline{{z}}))\triangleright(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta}}})({\overline{{z}}})\Rightarrow
U^{\prime\prime}[\overline{{t^{\prime}}}/\overline{{x_{1}}},\overline{{z}}/\overline{{x_{2}}}])\triangleright^{*}U_{2,j}$

By Lemma D.3, $U_{2,j}=U_{2,j,1}\land U_{2,j,2}$ such that
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta}}})({\overline{{z}}})\Rightarrow
U^{\prime\prime}_{|{\overline{{x_{1}}}}}[\overline{{t^{\prime}}}/\overline{{x_{1}}}])\triangleright^{*}U_{2,j,1}$
and
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta}}})({\overline{{z}}})\Rightarrow
U^{\prime\prime}_{|{\overline{{x_{2}}}}}[\overline{{z}}/\overline{{x_{2}}}])\triangleright^{*}U_{2,j,2}$.
Let us consider both parts individually.

    * –

The goal formula
$U^{\prime\prime}_{|{\overline{{x_{1}}}}}[\overline{{t^{\prime}}}/\overline{{x_{1}}}]$
does not contain $\overline{{z}}$, so we obtain
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta^{\prime}}}})({\overline{{z}}})\Rightarrow
U^{\prime\prime}_{|{\overline{{x_{1}}}}}[\overline{{t^{\prime}}}/\overline{{x_{1}}}])\triangleright^{*}U_{2,j,1}$
immediately from the former rewrite.

    * –

The goal formula
$U^{\prime\prime}_{|{\overline{{x_{2}}}}}[\overline{{z}}/\overline{{x_{2}}}]$
does not contain $\overline{{y}}$, so $U_{2,j,2}=\mathsf{true}$.

Inequality $\overline{{\theta^{\prime}}}\leq\overline{{\theta}}$ gives us
$\mathsf{toCl}({\overline{{\theta^{\prime}}}})({\overline{{z}}})\mathrel{\leq_{\mathsf{a}}}\mathsf{toCl}({\overline{{\theta}}})({\overline{{z}}})$.
We use this in combination with Lemma D.4 to prove a sequence of implications:

$\displaystyle
V,\overline{{y}}\vdash(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta}}})({\overline{{z}}})\Rightarrow
U^{\prime\prime}_{|{\overline{{x_{2}}}}}[\overline{{z}}/\overline{{x_{2}}}])\triangleright^{*}\mathsf{true}$
$\displaystyle\quad\Rightarrow\mathsf{toCl}({\overline{{\theta}}})({\overline{{z}}})\mathrel{\leq_{\mathsf{a}}}U^{\prime\prime}_{|{\overline{{x_{2}}}}}[\overline{{z}}/\overline{{x_{2}}}]$
$\displaystyle\quad\Rightarrow\mathsf{toCl}({\overline{{\theta^{\prime}}}})({\overline{{z}}})\mathrel{\leq_{\mathsf{a}}}U^{\prime\prime}_{|{\overline{{x_{2}}}}}[\overline{{z}}/\overline{{x_{2}}}]$
$\displaystyle\quad\Rightarrow
V,\overline{{y}}\vdash(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta^{\prime}}}})({\overline{{z}}})\Rightarrow
U^{\prime\prime}_{|{\overline{{x_{2}}}}}[\overline{{z}}/\overline{{x_{2}}}])\triangleright^{*}\mathsf{true}$

We can put these two rewrites back together using (AndL) and (AndR):

$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta^{\prime}}}})({\overline{{z}}})\Rightarrow
U^{\prime\prime}_{|{\overline{{x_{1}}}}}[\overline{{t^{\prime}}}/\overline{{x_{1}}}])\land(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta^{\prime}}}})({\overline{{z}}})\Rightarrow
U^{\prime\prime}_{|{\overline{{x_{2}}}}}[\overline{{z}}/\overline{{x_{2}}}])\triangleright^{*}U_{2,j}$

All that remains is replicating the beginning of rewrite † ‣ D.2:

$\displaystyle
V,\overline{{y}}\vdash(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta^{\prime}}}})({\overline{{z}}})\Rightarrow
P\,(t\,\overline{{z}}))$
$\displaystyle\qquad\triangleright(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta^{\prime}}}})({\overline{{z}}})\Rightarrow
U^{\prime\prime}[\overline{{t^{\prime}}}/\overline{{x_{1}}},\overline{{z}}/\overline{{x_{2}}}])$
$\displaystyle\qquad\triangleright(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta^{\prime}}}})({\overline{{z}}})\Rightarrow
U^{\prime\prime}_{|{\overline{{x_{1}}}}}[\overline{{t^{\prime}}}/\overline{{x_{1}}}])\land(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{\theta^{\prime}}}})({\overline{{z}}})\Rightarrow
U^{\prime\prime}_{|{\overline{{x_{2}}}}}[\overline{{z}}/\overline{{x_{2}}}])$
$\displaystyle\qquad\triangleright^{*}U_{2,j}$

We have now proved that
$V,\overline{{y}}\vdash\mathsf{toCl}({\tau_{i_{j}}})({t})\triangleright^{*}U_{2,j}$
determines
$V,\overline{{y}}\vdash\mathsf{toCl}({\tau_{j}^{\prime}})({t})\triangleright^{*}U_{2,j}^{\prime}$
with $U_{2,j}\mathrel{\leq_{\mathsf{a}}}U_{2,j}^{\prime}$, for all
$j\in[1..m]$. Thus, for every conjunct in
$\mathsf{toCl}({{\sigma_{\mathsf{t}}}^{\prime}})({t})$, there exists a
conjunct in $\mathsf{toCl}({{\sigma_{\mathsf{t}}}})({t})$ that rewrites to
something smaller, which proves
$V,\overline{{y}}\vdash\mathsf{toCl}({{\sigma_{\mathsf{t}}}^{\prime}})({t})\triangleright^{*}U^{\prime}$
for a $U^{\prime}$ such that $U\mathrel{\leq_{\mathsf{a}}}U^{\prime}$. ∎

Given an isomorphic type environment and automaton formula as per Definition
5.4, we establish an equivalence between typing judgements and rewrites. To
bridge the gap, we define $\top_{o}$ as a type-equivalent of truth and type
goal formulas as in Figure 10. This typing system distills the term-typing
judgements that make a goal formula true.

$\begin{array}[]{cc}\prftree[l]{\textsf{\small{(GT-
Atom)}}}{\Gamma\vdash{t}::{q_{P}}}{\Gamma\vdash{P\,t}::{\top_{o}}}\par\hskip
20.0pt\par\prftree[l]{\textsf{\small{(GT-
Imp)}}}{\Gamma,{\overline{{z}}}::{\mathsf{fromCl}({U})}\vdash{G}::{\top_{o}}}{\Gamma\vdash{\forall\overline{{z}}.\,U\Rightarrow
G}::{\top_{o}\par}}\\\\[12.0pt] \prftree[l]{\textsf{\small{(GT-
And)}}}{\Gamma\vdash{G_{1}}::{\top_{o}}}{\dots}{\Gamma\vdash{G_{n}}::{\top_{o}}}{\Gamma\vdash{G_{1}\land\dots\land
G_{n}}::{\top_{o}\par}}\end{array}$ Figure 10. Typing rules for goal formulas

###### Lemma D.6.

For automaton formulas $U,U^{\prime}$ over $\overline{{y}}$,
$U\mathrel{\leq_{\mathsf{a}}}U^{\prime}$ implies
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{U^{\prime}}::{\top_{o}}$.

###### Proof.

We proceed by structural induction on $U^{\prime}$. Suppose
$U\mathrel{\leq_{\mathsf{a}}}U^{\prime}$.

  * •

Suppose $U^{\prime}=\mathsf{true}$. Both
$U\mathrel{\leq_{\mathsf{a}}}\mathsf{true}$ and
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{\mathsf{true}}::{\top_{o}}$
trivially hold.

  * •

Suppose $U^{\prime}=P\,y_{i}$. This means that
$\mathsf{fromCl}({U_{|{y_{i}}}})\leq q_{P}$ and, thus,
$q_{P}\in\mathsf{fromCl}({U_{|{y_{i}}}})$. We aim to show
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{P\,y_{i}}::{\top_{o}}$,
which holds just if
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{y_{i}}::{q_{P}}$.
We prove the latter with (T-Var), thanks to
$q_{P}\in\mathsf{fromCl}({U_{|{y_{i}}}})$.

  * •

Suppose $U^{\prime}=(\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
P\,(y_{i}\,\overline{{x}}))$ for some $\overline{{x}}=x_{1}\dots x_{m}$. This
means
$\mathsf{fromCl}({U_{|{y_{i}}}})\mathrel{\leq_{\mathsf{a}}}\mathsf{fromCl}({\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
P\,(y_{i}\,\overline{{x}})})$. By Lemma D.1, there exists $T\in U_{|{y_{i}}}$
such that
$\mathsf{fromCl}({T})\mathrel{\leq_{\mathsf{a}}}\mathsf{fromCl}({\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
P\,(y_{i}\,\overline{{x}})})$.

Let $T=(\forall\overline{{x}}.\,U^{\prime\prime\prime}\Rightarrow
P\,(y_{i}\,\overline{{x}}))$ be such a $T$. This gives us
$\mathsf{fromCl}({U^{\prime\prime}_{|{x_{j}}}})\leq\mathsf{fromCl}({U^{\prime\prime\prime}_{|{x_{j}}}})$
by subtyping rule (Q-Arr), for all $j\in[1..m]$, which implies
$U^{\prime\prime}\mathrel{\leq_{\mathsf{a}}}U^{\prime\prime\prime}$.

Finally, we apply (T-App) to:

    * –

$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{x}}}::{\mathsf{fromCl}({U^{\prime\prime}})}\vdash{y_{i}}::{\mathsf{fromCl}({\forall\overline{{x}}.\,U^{\prime\prime\prime}\Rightarrow
P\,(y_{i}\,\overline{{x}})})}$, by (T-Var)

    * –

for all $j\in[1..m]$:
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{x}}}::{\mathsf{fromCl}({U^{\prime\prime}})}\vdash{x_{j}}::{\mathsf{fromCl}({U^{\prime\prime}_{|{x_{j}}}})}$,
by (T-Var)

    * –

for all $j\in[1..m]$:
$\mathsf{fromCl}({U^{\prime\prime}_{|{x_{j}}}})\leq\mathsf{fromCl}({U^{\prime\prime\prime}_{|{x_{j}}}})$

This gives us
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{x}}}::{\mathsf{fromCl}({U^{\prime\prime}})}\vdash{y_{i}\,\overline{{x}}}::{q_{P}}$,
to which we apply (GT-Atom) and (GT-Imp) to prove the claim.

  * •

Suppose $U^{\prime}=U_{1}^{\prime}\land U_{2}^{\prime}$. This means that
$\mathsf{fromCl}({U_{|{y_{i}}}})\leq\mathsf{fromCl}({(U_{1}^{\prime}\land
U_{2}^{\prime})_{|{y_{i}}}})$, for all $i\in[1..n]$. Clearly, also
$\mathsf{fromCl}({U_{|{y_{i}}}})\leq\mathsf{fromCl}({{U_{1}}^{\prime}_{|{y_{i}}}})$
and
$\mathsf{fromCl}({U_{|{z_{i}}}})\leq\mathsf{fromCl}({{U_{2}}^{\prime}_{|{y_{i}}}})$,
for all $i\in[1..n]$. By the IH,
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{U_{1}^{\prime}}::{\top_{o}}$
and
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{U_{2}^{\prime}}::{\top_{o}}$.
Finally, (GT-And) gives us
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{U_{1}^{\prime}\land
U_{2}^{\prime}}::{\top_{o}}$.

∎

###### Lemma D.7 (Type-clause correspondence).

For all $U$, there exists $U^{\prime}$ such that
$U\mathrel{\leq_{\mathsf{a}}}U^{\prime}$ and $V,\overline{{y}}\vdash
G\triangleright^{*}U^{\prime}$ if, and only if
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{G}::{\top_{o}}$.

###### Proof.

Lemma D.6 proves
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{U^{\prime}}::{\top_{o}}$
from $U\mathrel{\leq_{\mathsf{a}}}U^{\prime}$, so it suffices to show the
following for direction $\Rightarrow$: if $V,\overline{{y}}\vdash
G_{1}\triangleright G_{2}$ and
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{G_{2}}::{\top_{o}}$,
then
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{G_{1}}::{\top_{o}}$.

We use case analysis on the rewrite rule used in $V,\overline{{y}}\vdash
G_{1}\triangleright G_{2}$.

(Refl):

Suppose $V,\overline{{y}}\vdash P\,x\triangleright\mathsf{true}$ and
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{\mathsf{true}}::{\top_{o}}$.
The side condition is $P\,x\in V$, which means
$q_{P}\in\mathsf{fromCl}({V_{|{x}}})$ and ${x}::{q_{P}}\in\Gamma_{V}$. Now,
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{P\,x}::{\top_{o}}$
can be proved using (GT-Atom) and (T-Var).

(Step):

Suppose $V,\overline{{y}}\vdash P\,(f\,\overline{{s}})\triangleright
U^{\prime}[\overline{{s}}/\overline{{x}}]$ and
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{U^{\prime}[\overline{{s}}/\overline{{x}}]}::{\top_{o}}$.
The side condition is $(\forall\overline{{x}}.\,U^{\prime}\Rightarrow
P\,(f\,\overline{{x}}))\in V$, which means
$\mathsf{fromCl}({\forall\overline{{x}}.\,U^{\prime}\Rightarrow
P\,(f\,\overline{{x}})})\in\mathsf{fromCl}({V_{|{f}}})$ and
${f}::{\mathsf{fromCl}({\forall\overline{{x}}.\,U^{\prime}\Rightarrow
P\,(f\,\overline{{x}})})}\in\Gamma_{V}$.

Let $U^{\prime}=T_{1}\land\dots\land T_{k}$. Clearly, there exists a proof
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{U^{\prime}[\overline{{s}}/\overline{{x}}]}::{\top_{o}}$
just if
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{T_{j}[\overline{{s}}/\overline{{x}}]}::{\top_{o}}$,
for all $j\in[1..k]$, using (GT-And). If $T_{j}$ contains a (single) variable
$x_{i}\in x_{1}\dots x_{n}$ of type $\iota$, then the proof
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{T_{j}[\overline{{s}}/\overline{{x}}]}::{\top_{o}}$
uses (GT-Atom) at the root. Otherwise, if the (single) variable $x_{i}\in
x_{1}\dots x_{n}$ in $T_{j}$ does not have type $\iota$, then the proof
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{T_{j}[\overline{{s}}/\overline{{x}}]}::{\top_{o}}$
uses (GT-Imp) at the root, followed by (GT-Atom); i.e. if
$T_{j}=(\forall\overline{{z}}.\,U^{\prime\prime}\Rightarrow
P^{\prime}\,(x_{i}\,\overline{{z}}))$, then we have
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{T_{j}[\overline{{s}}/\overline{{x}}]}::{\top_{o}}$
just if
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U^{\prime\prime}})}\vdash{P^{\prime}\,(s_{i}\,\overline{{z}})}::{\top_{o}}$.

We have now identified all $k$ nodes in
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{U^{\prime}[\overline{{s}}/\overline{{x}}]}::{\top_{o}}$
at which (GT-Atom) is used. Thanks to their premises,
$T_{j}=(\forall\overline{{z}}.\,U^{\prime\prime}\Rightarrow
P^{\prime}(x_{i}\,\overline{{z}}))$ implies
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U^{\prime\prime}})}\vdash{s_{i}\,\overline{{z}}}::{q_{P^{\prime}}}$.
Let $\overline{{z}}=z_{1}\dots z_{m}$. By (T-App), there exist
${\sigma_{\mathsf{t}}}_{\ell},{\sigma_{\mathsf{t}}}_{\ell}^{\prime}$, for all
$\ell\in[1..m]$, such that:

  * •:

$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U^{\prime\prime}})}\vdash{s_{i}}::{{\sigma_{\mathsf{t}}}_{1}\to\dots\to{\sigma_{\mathsf{t}}}_{m}\to
q_{P^{\prime}}}$

  * •:

for all $\ell\in[1..m]$:
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U^{\prime\prime}})}\vdash{z_{\ell}}::{{\sigma_{\mathsf{t}}}_{\ell}^{\prime}}$

  * •:

for all $\ell\in[1..m]$:
${\sigma_{\mathsf{t}}}_{\ell}^{\prime}\leq{\sigma_{\mathsf{t}}}_{\ell}$

Typing rule (T-Var) guarantees
${\sigma_{\mathsf{t}}}_{\ell}^{\prime}\subseteq\mathsf{fromCl}({U^{\prime\prime}_{|{z_{\ell}}}})$
and, thus,
$\mathsf{fromCl}({U^{\prime\prime}_{|{z_{\ell}}}})\leq{\sigma_{\mathsf{t}}}_{\ell}^{\prime}\leq{\sigma_{\mathsf{t}}}_{\ell}$.
It follows that
${\sigma_{\mathsf{t}}}_{1}\to\dots\to{\sigma_{\mathsf{t}}}_{m}\to
q_{P^{\prime}}\leq\mathsf{fromCl}({U^{\prime\prime}_{|{z_{1}}}})\to\dots\to\mathsf{fromCl}({U^{\prime\prime}_{|{z_{m}}}})\to
q_{P^{\prime}}=\mathsf{fromCl}({T_{j}})$.

Let us refer to
${\sigma_{\mathsf{t}}}_{1}\to\dots\to{\sigma_{\mathsf{t}}}_{m}\to
q_{P^{\prime}}$ as $\tau_{j}$, the type extracted from $T_{j}$ for (its only
variable) $x_{i}$. Recall $\tau_{j}\leq\mathsf{fromCl}({T_{j}})$. We define an
type $\theta_{i}$ for each $s_{i}$ such that
$\theta_{i}\leq\mathsf{fromCl}({U^{\prime}_{|{x_{i}}}})$:

$\displaystyle\theta_{i}$ $\displaystyle:=\\{\tau_{j}\mid T_{j}\in
U^{\prime}_{|{x_{i}}}\land j\in[1..k]\\}$

Finally, we have the following:

  * •:

$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{f}::{\mathsf{fromCl}({\forall\overline{{x}}.\,U^{\prime}\Rightarrow
P\,(f\,\overline{{x}})})}$, by (T-Con)

  * •:

for all $i\in[1..n]$:
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{s_{i}}::{\theta_{i}}$

  * •:

for all $i\in[1..n]$: $\theta_{i}\leq\mathsf{fromCl}({U^{\prime}_{|{x_{i}}}})$

We conclude the case with (T-App) with those premises, followed by (GT-Atom).

(Assm):

Let $\overline{{x}}=x_{1}\dots x_{n}$ and $\overline{{y}}=y_{1}\dots y_{m}$.
Suppose $V,\overline{{y}}\vdash P\,(y_{j}\,\overline{{s}})\triangleright
U^{\prime\prime}[\overline{{s}}/\overline{{x}}]\land(\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
P\,(y\,\overline{{x}}))$ and
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{U^{\prime\prime}[\overline{{s}}/\overline{{x}}]\land(\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
P\,(y_{j}\,\overline{{x}}))}::{\top_{o}}$, for some $j\in[1..m]$.

The typing proof uses (GT-And) at the root with
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{U^{\prime\prime}[\overline{{s}}/\overline{{x}}]}::{\top_{o}}$
on the LHS and on the RHS:

$\prftree[l]{\textsf{\small{(GT-Imp)}}}{\prftree[l]{\textsf{\small{(GT-
Atom)}}}{\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{x}}}::{\mathsf{fromCl}({U^{\prime\prime}})}\vdash{y_{j}\,\overline{{x}}}::{q_{P}}}{\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{x}}}::{\mathsf{fromCl}({U^{\prime\prime}})}\vdash{P\,(y_{j}\,\overline{{x}})}::{\top_{o}}}}{\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
P\,(y_{j}\,\overline{{x}})}::{\top_{o}}}$

Typing rule (T-App) now guarantees the existence of
${\sigma_{\mathsf{t}}}_{i},{\sigma_{\mathsf{t}}}_{i}^{\prime}$, for all
$i\in[1..n]$, such that:

  * •:

$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{x}}}::{\mathsf{fromCl}({U^{\prime\prime}})}\vdash{y_{j}}::{{\sigma_{\mathsf{t}}}_{1}\to\dots\to{\sigma_{\mathsf{t}}}_{m}\to
q_{P}}$

  * •:

for all $i\in[1..n]$:
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{x}}}::{\mathsf{fromCl}({U^{\prime\prime}})}\vdash{x_{i}}::{{\sigma_{\mathsf{t}}}^{\prime}_{i}}$

  * •:

for all $i\in[1..n]$:
${\sigma_{\mathsf{t}}}^{\prime}_{i}\leq{\sigma_{\mathsf{t}}}_{i}$

The first gives us
${\sigma_{\mathsf{t}}}_{1}\to\dots\to{\sigma_{\mathsf{t}}}_{m}\to
q_{P}\in\mathsf{fromCl}({U_{|{y_{j}}}})$ thanks to (T-Var), and the second
${\sigma_{\mathsf{t}}}_{i}^{\prime}\subseteq\mathsf{fromCl}({U^{\prime\prime}_{|{x_{i}}}})$.
This implies
$\mathsf{fromCl}({U^{\prime\prime}_{|{x_{i}}}})\leq{\sigma_{\mathsf{t}}}_{i}^{\prime}\leq{\sigma_{\mathsf{t}}}_{i}$.
The third bullet point now yields
${\sigma_{\mathsf{t}}}_{1}\to\dots\to{\sigma_{\mathsf{t}}}_{n}\to
q_{P}\leq\mathsf{fromCl}({U^{\prime\prime}_{|{x_{1}}}})\to\dots\to\mathsf{fromCl}({U^{\prime\prime}_{|{x_{n}}}})\to
q_{P}=\mathsf{fromCl}({\forall\overline{{x}}.\,U^{\prime\prime}\Rightarrow
P\,(y_{j}\,\overline{{x}})})$.

The left premise
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{U^{\prime\prime}[\overline{{s}}/\overline{{x}}]}::{\top_{o}}$
of the assumption allows us to prove the existence of $\theta_{i}$ such that
$\theta_{i}\leq\mathsf{fromCl}({U^{\prime\prime}_{|{x_{i}}}})$ and
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{s_{i}}::{\theta_{i}}$
for all $i\in[1..n]$, as we did in (Step). This means that
$\theta_{i}\leq\mathsf{fromCl}({U^{\prime\prime}_{|{x_{i}}}})\leq{\sigma_{\mathsf{t}}}_{i}^{\prime}\leq{\sigma_{\mathsf{t}}}_{i}$.

Finally, we prove
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{P\,(y_{j}\,\overline{{s}})}::{\top_{o}}$
with (T-App) and (GT-Atom) on:

  * •:

$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{y_{j}}::{{\sigma_{\mathsf{t}}}_{1}\to\dots\to{\sigma_{\mathsf{t}}}_{m}\to
q_{P}}$

  * •:

for all $i\in[1..n]$:
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{s_{i}}::{\theta_{i}}$

  * •:

for all $i\in[1..n]$: $\theta_{i}\leq{\sigma_{\mathsf{t}}}_{i}$

(ImpAnd):

Suppose
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U^{\prime\prime}\Rightarrow
G_{1}^{\prime}\land
G_{2}^{\prime})\triangleright(\forall\overline{{z}}.\,U^{\prime\prime}\Rightarrow
G_{1}^{\prime})\land(\forall\overline{{z}}.\,U^{\prime\prime}\Rightarrow
G_{2}^{\prime})$ and
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{(\forall\overline{{z}}.\,U^{\prime\prime}\Rightarrow
G_{1}^{\prime})\land(\forall\overline{{z}}.\,U^{\prime\prime}\Rightarrow
G_{2}^{\prime})}::{\top_{o}}$.

Our assumption
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{(\forall\overline{{z}}.\,U^{\prime\prime}\Rightarrow
G_{1}^{\prime})\land(\forall\overline{{z}}.\,U^{\prime\prime}\Rightarrow
G_{2}^{\prime})}::{\top_{o}}$ uses (GT-And) at the root with the subproofs
given by, for $i\in[1,2]$:

$\prftree[l]{\textsf{\small{(GT-
Imp)}}}{\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U^{\prime\prime}})}\vdash{G_{i}^{\prime}}::{\top_{o}}}{\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{\forall\overline{{z}}.\,U^{\prime\prime}\Rightarrow
G_{i}^{\prime}}::{\top_{o}}}$

Let us refer to premise
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U^{\prime\prime}})}\vdash{G_{i}^{\prime}}::{\top_{o}}$
as $\Delta_{i}$, for $i\in[1,2]$.

This allows us to construct:

$\prftree[l]{\textsf{\small{(GT-Imp)}}}{\prftree[l]{\textsf{\small{(GT-
And)}}}{\Delta_{1}\qquad\qquad\qquad\qquad}{\Delta_{2}}{\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U^{\prime\prime}})}\vdash{G_{1}^{\prime}\land
G_{2}^{\prime}}::{\top_{o}}}}{\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{\forall\overline{{z}}.\,U^{\prime\prime}\Rightarrow
G_{1}^{\prime}\land G_{2}^{\prime}}::{\top_{o}}}$

(Scope):

Suppose $V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U_{1}\Rightarrow
G_{2})\triangleright G_{2}$ and
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{G_{2}}::{\top_{o}}$
with $\overline{{z}}\cap\mathsf{FV}(G_{2})=\emptyset$. Thanks to Weakening
Lemma D.2,
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U_{1}})}\vdash{G_{2}}::{\top_{o}}$
also holds. Finally, (GT-Imp) proves this case.

(Imp):

This is the first inductive case. Suppose
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U_{1}\Rightarrow
G_{1}^{\prime})\triangleright(\forall\overline{{z}}.\,U_{1}\Rightarrow
G_{2}^{\prime})$ and
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{(\forall\overline{{z}}.\,U_{1}\Rightarrow
G_{2}^{\prime})}::{\top_{o}}$. The latter gives us
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U_{1}})}\vdash{G_{2}^{\prime}}::{\top_{o}}$
by (GT-Imp), which is equal to $\Gamma_{V\land
U_{1}},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{G_{2}^{\prime}}::{\top_{o}}$.

We use the IH on premise $V\land U_{1},\overline{{y}}\vdash
G_{1}^{\prime}\triangleright G_{2}^{\prime}$ of (Imp) for $\Gamma_{V\land
U_{1}},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{G_{1}^{\prime}}::{\top_{o}}$,
which is equal to
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U_{1}})}\vdash{G_{1}^{\prime}}::{\top_{o}}$.
Finally, (GT-Imp) gives us
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{(\forall\overline{{z}}.\,U_{1}\Rightarrow
G_{1}^{\prime})}::{\top_{o}}$, as required.

(AndL):

Suppose $V,\overline{{y}}\vdash G_{1}\land G_{2}\triangleright
G_{1}^{\prime}\land G_{2}$ and
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{G_{1}^{\prime}\land
G_{2}}::{\top_{o}}$. The proof is straightforward: use (backwards) (GT-And) on
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{G_{1}^{\prime}\land
G_{2}}::{\top_{o}}$, invoke the IH on the parts, and use (GT-And) for
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{G_{1}\land
G_{2}}::{\top_{o}}$.

For direction $\Leftarrow$, suppose
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{G}::{\top_{o}}$. We
use structural induction on $G$ to prove $V,\overline{{y}}\vdash
G\triangleright^{*}U_{0}$ for some $U_{0}$ such that
$U\mathrel{\leq_{\mathsf{a}}}U_{0}$.

(GT-Atom):

Suppose
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{P\,s}::{\top_{o}}$
with premise
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{s}::{q_{P}}$. We
use structural induction on term $s$.

(T-Con):

Suppose $s=f:\iota\in\Sigma$. By the premise,
$q_{P}\in\mathsf{fromCl}({V_{|{f}}})$ and, thus, $P\,f\in V_{|{f}}$. We use
(Refl) with this side condition for:

$V,\overline{{y}}\vdash P\,f\triangleright\mathsf{true}$

Since $U\leq\mathsf{true}$, this proves the case.

(T-Var):

If $s=z\not\in\overline{{y}}$, then we proceed as in the previous case, so
suppose $s=y_{j}\in\overline{{y}}$. Clearly, $P\,y_{j}$ is automaton wrt
$\overline{{y}}$. Thus, $V,\overline{{y}}\vdash
P\,y_{j}\triangleright^{*}P\,y_{j}$.

It remains to show $U\mathrel{\leq_{\mathsf{a}}}P\,y_{j}$. Premise
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{y_{j}}::{q_{P}}$
guarantees $q_{P}\in\mathsf{fromCl}({U_{|{y_{j}}}})$, by (T-Var), which
implies
$U\mathrel{\leq_{\mathsf{a}}}U_{|{y_{j}}}\mathrel{\leq_{\mathsf{a}}}P\,y_{j}$,
as required.

(T-App):

We must distinguish the case where $s=y_{j}\,\overline{{t}}$ with
$y_{j}\in\overline{{y}}$ from $s=f\,\overline{{t}}$ with $f\in\Sigma$, but
first assume $s=f\,t_{1}\dots t_{n}=f\,\overline{{t}}$ for some $f\in\Sigma$.

Premise
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{f\,\overline{{t}}}::{q_{P}}$
guarantees ${\sigma_{\mathsf{t}}}_{1}\to\dots\to{\sigma_{\mathsf{t}}}_{n}\to
q_{P}\in\mathsf{fromCl}({V_{|{f}}})$, by (T-App) and (T-Con), with
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{t_{i}}::{{\sigma_{\mathsf{t}}}_{i}^{\prime}}$
such that ${\sigma_{\mathsf{t}}}^{\prime}_{i}\leq{\sigma_{\mathsf{t}}}_{i}$,
for all $i\in[1..n]$. Thus, there exists an automaton clause
$(\forall\overline{{x}}.\,\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{1}})({x_{1}})\land\dots\land\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{n}})({x_{n}})\Rightarrow
P\,(f\,\overline{{x}}))\in V_{|{f}}$ we can use as a side condition for (Step)
in:

$V,\overline{{y}}\vdash
P\,(f\,\overline{{t}})\triangleright\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{1}})({t_{1}})\land\dots\land\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{n}})({t_{n}})$

We aim to show that each
$\mathsf{toCl}({\tau})({t_{i}})\in\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{i}})({t_{i}})$
rewrites to an automaton clause larger than $U$, for all $i\in[1..n]$. Let us
consider such a $\mathsf{toCl}({\tau})({t_{i}})$.

  * •:

Suppose $t_{i}:\iota$. Let $\tau=q_{P^{\prime}}$, so
$\mathsf{toCl}({\tau})({t_{i}})=P^{\prime}\,t_{i}$. Recall we have
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{t_{i}}::{{\sigma_{\mathsf{t}}}_{i}^{\prime}}$.
Since ${\sigma_{\mathsf{t}}}_{i}^{\prime}\leq{\sigma_{\mathsf{t}}}_{i}$
implies ${\sigma_{\mathsf{t}}}^{\prime}_{i}\supseteq{\sigma_{\mathsf{t}}}_{i}$
for type $\iota$, we also have
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{t_{i}}::{q_{P^{\prime}}}$.

Typing rule (GT-Atom) gives us
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{P^{\prime}\,t_{i}}::{\top_{o}}$,
to which we can apply the IH for $V,\overline{{y}}\vdash
P^{\prime}\,t_{i}\triangleright^{*}U_{\tau}$ such that
$U\mathrel{\leq_{\mathsf{a}}}U_{\tau}$.

  * •:

Suppose $t_{i}:\sigma_{1}\to\dots\to\sigma_{k}\to\iota$ for $k>0$. Thanks to
Lemma D.1, the inequality
${\sigma_{\mathsf{t}}}_{i}^{\prime}\leq{\sigma_{\mathsf{t}}}_{i}$ with
$\tau\in{\sigma_{\mathsf{t}}}_{i}$ guarantees the existence of
$\tau^{\prime}\in{\sigma_{\mathsf{t}}}^{\prime}$ such that
$\tau^{\prime}\leq\tau$.

Recall we have
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{t_{i}}::{{\sigma_{\mathsf{t}}}_{i}^{\prime}}$
and, thus,
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{t_{i}}::{\tau^{\prime}}$.
Let $\mathsf{toCl}({\tau})({t_{i}})=(\forall\overline{{z}}.\,U_{0}\Rightarrow
P^{\prime}\,(t_{i}\,\overline{{z}}))$ and
$\mathsf{toCl}({\tau^{\prime}})({t_{i}})=(\forall\overline{{z}}.\,U_{0}^{\prime}\Rightarrow
P^{\prime}\,(t_{i}\,\overline{{z}}))$. Since $\tau^{\prime}\leq\tau$, it holds
that $U_{0}\mathrel{\leq_{\mathsf{a}}}U_{0}^{\prime}$. This gives us the
following:

    * –:

$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U_{0}})}\vdash{t_{i}}::{\mathsf{fromCl}({\forall\overline{{z}}.\,U_{0}^{\prime}\Rightarrow
P^{\prime}\,(t_{i}\,\overline{{z}})})}$ by Weakening Lemma D.2

    * –:

for all $z_{\ell}\in\overline{{z}}$:
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U_{0}})}\vdash{z_{\ell}}::{\mathsf{fromCl}({{U_{0}}_{|{z_{\ell}}}})}$,
by (T-Var)

    * –:

for all $z_{\ell}\in\overline{{z}}$:
$\mathsf{fromCl}({{U_{0}}_{|{z_{\ell}}}})\leq\mathsf{fromCl}({{U_{0}^{\prime}}_{|{z_{\ell}}}})$

We apply (T-Var) to these premises for
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U_{0}})}\vdash{t_{i}\,\overline{{z}}}::{q_{P^{\prime}}}$.
By (GT-Atom),
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U_{0}})}\vdash{P^{\prime}\,(t_{i}\,\overline{{z}})}::{\top_{o}}$,
which is equal to $\Gamma_{V\land
U_{0}},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{P^{\prime}\,(t_{i}\,\overline{{z}})}::{\top_{o}}$.

Finally, by the IH, there exists $U_{\tau}$ such that $V\land
U_{0},\overline{{y}}\vdash
P^{\prime}\,(t_{i}\,\overline{{z}})\triangleright^{*}U_{\tau}$ and
$U\mathrel{\leq_{\mathsf{a}}}U_{\tau}$. Typing rule (GT-Imp) gives us
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U_{0}\Rightarrow
P^{\prime}\,(t_{i}\,\overline{{z}}))\triangleright^{*}(\forall\overline{{z}}.\,U_{0}\Rightarrow
U_{\tau})$. Observe that $U_{\tau}$ is automaton wrt $\overline{{y}}$.
Therefore, it does not contain $\overline{{z}}$, and we can apply (Scope) for:

$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U_{0}\Rightarrow
P^{\prime}\,(t_{i}\,\overline{{z}}))\triangleright^{*}(\forall\overline{{z}}.\,U_{0}\Rightarrow
U_{\tau})\triangleright U_{\tau}$

We have proved, for all $i\in[1..n]$, that every
$\mathsf{toCl}({\tau})({t_{i}})\in\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{i}})({t_{i}})$
rewrites to some automaton clause greater than $U$. Therefore, so does
$\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{i}})({t_{i}})$, and so does
$\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{1}})({t_{1}})\land\dots\land\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{n}})({t_{n}})$.
We conclude the case with:

$V,\overline{{y}}\vdash
P\,(f\,\overline{{t}})\triangleright\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{1}})({t_{1}})\land\dots\land\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{n}})({t_{n}})$

Now, suppose $s=y_{j}\,t_{1}\dots t_{n}$ with $y_{j}\in\overline{{y}}$
instead. Similar to before, premise
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{y_{j}\,\overline{{t}}}::{q_{P}}$
guarantees ${\sigma_{\mathsf{t}}}_{1}\to\dots\to{\sigma_{\mathsf{t}}}_{n}\to
q_{P}\in\mathsf{fromCl}({U_{|{y_{j}}}})$, by (T-App) and (T-Var), with
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{t_{i}}::{{\sigma_{\mathsf{t}}}_{i}^{\prime}}$
such that ${\sigma_{\mathsf{t}}}^{\prime}_{i}\leq{\sigma_{\mathsf{t}}}_{i}$,
for all $i\in[1..n]$. Thus, there exists an automaton clause
$T=(\forall\overline{{x}}.\,\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{1}})({x_{1}})\land\dots\land\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{n}})({x_{n}})\Rightarrow
P\,(y_{j}\,\overline{{x}}))\in U_{|{y_{j}}}$ we can use as assumption in
(Assm):

$V,\overline{{y}}\vdash
P\,(f\,\overline{{t}})\triangleright\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{1}})({t_{1}})\land\dots\land\mathsf{toCl}({{\sigma_{\mathsf{t}}}_{n}})({t_{n}})\land
T$

Conjunct $T$ is in $U$ by definition. For the other conjuncts, we proceed as
before.

(GT-And):

Suppose $\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{G_{1}\land
G_{2}}::{\top_{o}}$ with premises
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{G_{1}}::{\top_{o}}$
and
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{G_{2}}::{\top_{o}}$.
By the IH, there exist $U_{1},U_{2}$ such that $V,\overline{{y}}\vdash
G_{1}\triangleright^{*}U_{1}$ and $U\mathrel{\leq_{\mathsf{a}}}U_{1}$ and
$V,\overline{{y}}\vdash G_{2}\triangleright^{*}U_{2}$ and
$U\mathrel{\leq_{\mathsf{a}}}U_{2}$. Clearly,
$U\mathrel{\leq_{\mathsf{a}}}U_{1}\land U_{2}$, so the following rewrite
proves the case, using (AndL) and (AndR):

$V,\overline{{y}}\vdash G_{1}\land G_{2}\triangleright^{*}U_{1}\land
G_{2}\triangleright^{*}U_{1}\land U_{2}$

(GT-Imp):

Suppose
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{\forall\overline{{z}}.\,U^{\prime}\Rightarrow
G^{\prime\prime}}::{\top_{o}}$ with premise
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})},{\overline{{z}}}::{\mathsf{fromCl}({U^{\prime}})}\vdash{G^{\prime\prime}}::{\top_{o}}$,
which is equal to $\Gamma_{V\land
U^{\prime}},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{G^{\prime\prime}}::{\top_{o}}$.
By the IH, there exists $U^{\prime\prime}$ such that $V\land
U^{\prime},\overline{{y}}\vdash
G^{\prime\prime}\triangleright^{*}U^{\prime\prime}$ and
$U\mathrel{\leq_{\mathsf{a}}}U^{\prime\prime}$. Rewrite rule (Imp) gives us
$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U^{\prime}\Rightarrow
G^{\prime\prime})\triangleright^{*}(\forall\overline{{z}}.\,U^{\prime}\Rightarrow
U^{\prime\prime})$.

It remains to show this rewrites further to something larger than $U$. Observe
that $U^{\prime\prime}$ is automaton wrt $\overline{{y}}$. Therefore, it does
not contain $\overline{{z}}$, and we can apply (Scope) for:

$V,\overline{{y}}\vdash(\forall\overline{{z}}.\,U^{\prime}\Rightarrow
G^{\prime\prime})\triangleright^{*}(\forall\overline{{z}}.\,U^{\prime}\Rightarrow
U^{\prime\prime})\triangleright U^{\prime\prime}$

∎

See 5.6

###### Proof.

We aim to show $\Gamma\vdash{t}::{{\sigma_{\mathsf{t}}}}$ if, and only if,
$\Gamma\vdash{\mathsf{toCl}({{\sigma_{\mathsf{t}}}})({t})}::{\top_{o}}$; this
proves (i), since Lemma D.7 already gives us $\exists
U^{\prime}.\,U\mathrel{\leq_{\mathsf{a}}}U^{\prime}\land
V,\overline{{y}}\vdash\mathsf{toCl}({{\sigma_{\mathsf{t}}}})({t})\triangleright^{*}U^{\prime}$
if, and only if
$\Gamma_{V},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{\mathsf{toCl}({{\sigma_{\mathsf{t}}}})({t})}::{\top_{o}}$,
for all $U$. Furthermore, if $\lvert\overline{{y}}\rvert=0$, then
$U=\mathsf{true}$ and $U^{\prime}=\mathsf{true}$, so (ii) is an instance of
(i).

It remains to prove $\Gamma\vdash{t}::{{\sigma_{\mathsf{t}}}}$ if, and only
if, $\Gamma\vdash{\mathsf{toCl}({{\sigma_{\mathsf{t}}}})({t})}::{\top_{o}}$.

Suppose $t:\iota$. This yields the following sequence of equivalences:

$\displaystyle\Gamma\vdash{t}::{{\sigma_{\mathsf{t}}}}$
$\displaystyle\iff\forall
q_{P}\in{\sigma_{\mathsf{t}}}.\,\Gamma\vdash{t}::{q_{P}}$
$\displaystyle\iff\forall
q_{P}\in{\sigma_{\mathsf{t}}}.\,\Gamma\vdash{P\,t}::{\top_{o}}$
$\displaystyle\iff\forall
q_{P}\in{\sigma_{\mathsf{t}}}.\,\Gamma\vdash{\mathsf{toCl}({q_{P}})({t})}::{\top_{o}}$
$\displaystyle\iff\Gamma\vdash{\mathsf{toCl}({{\sigma_{\mathsf{t}}}})({t})}::{\top_{o}}$

where we rely on notation, (GT-Atom), $\mathsf{toCl}({q_{P}})({t})=P\,t$, and
(GT-And), resp.

Suppose $t:\sigma_{1}\to\dots\to\sigma_{m}\to\iota$ with $m>0$. It suffices to
prove the claim for a strict type $\tau$ of this type, thanks to (GT-And). Let
$\tau={\sigma_{\mathsf{t}}}_{1}\to\dots\to{\sigma_{\mathsf{t}}}_{m}\to q_{P}$.
We obtain the following equivalences:

$\displaystyle\Gamma\vdash{t}::{\tau}$
$\displaystyle\iff\Gamma,{\overline{{z}}}::{\overline{{{\sigma_{\mathsf{t}}}}}}\vdash{t}::{\tau}$
$\displaystyle\iff\Gamma,{\overline{{z}}}::{\overline{{{\sigma_{\mathsf{t}}}}}}\vdash{t\,\overline{{z}}}::{q_{P}}$
$\displaystyle\iff\Gamma,{\overline{{z}}}::{\overline{{{\sigma_{\mathsf{t}}}}}}\vdash{P\,(t\,\overline{{z}})}::{\top_{o}}$
$\displaystyle\iff\Gamma\vdash{\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{{\sigma_{\mathsf{t}}}}}})({\overline{{z}}})\Rightarrow
P\,(t\,\overline{{z}})}::{\top_{o}}$
$\displaystyle\iff\Gamma\vdash{\mathsf{toCl}({\tau})({t})}::{\top_{o}}$

where we respectively rely on Weakening Lemma D.2, (T-App), (GT-Atom), (GT-
Imp), and
$\mathsf{toCl}({\tau})({t})=(\forall\overline{{z}}.\,\mathsf{toCl}({\overline{{{\sigma_{\mathsf{t}}}}}})({\overline{{z}}})\Rightarrow
P\,(t\,\overline{{z}}))$.

∎

###  D.3. Reducing HORS intersection typing to MSL($\omega$)

###### Lemma D.8.

A non-empty $\Gamma$ is ${\mathcal{G}}$-coconsistent if, and only if, there
exist $(\forall\overline{{y}}.\,U\Rightarrow P\,(f\,\overline{{y}}))\in
V_{\Gamma}$ and $(\forall\overline{{y}}.\,P\,t\Rightarrow
P\,(f\,\overline{{y}}))\in D_{\mathcal{G}}$ such that:

$\Gamma\backslash\\{{f}::{\tau}\\}\text{ is }{\mathcal{G}}\text{-coconsistent
and }\exists
U^{\prime}.\,V_{\Gamma\backslash\\{{f}::{\tau}\\}},\overline{{y}}\vdash
P\,t\triangleright^{*}U^{\prime}\land U\mathrel{\leq_{\mathsf{a}}}U^{\prime}$

where $\tau=\mathsf{fromCl}({\forall\overline{{y}}.\,U\Rightarrow
P\,(f\,\overline{{y}})})$.

###### Proof.

Take the definition of ${\mathcal{G}}$-coconsistency for non-empty $\Gamma$,
and replace parts of the statement by equivalent ones, relying on the
isomorphism between types and clauses, the construction of $D_{\mathcal{G}}$,
and Proposition 5.6, resp.:

  * •

${f}::{\tau}\in\Gamma$ if, and only if, $(\forall\overline{{y}}.\,U\Rightarrow
P\,(f\,\overline{{y}}))\in V_{\Gamma}$

  * •

$\exists(f\,\overline{{y}}=t)\in{\mathcal{G}}$ if, and only if,
$\exists(\forall\overline{{y}}.\,P\,t\Rightarrow P\,(f\,\overline{{y}}))\in
D_{\mathcal{G}}$

  * •

$\Gamma\backslash\\{{f}::{\tau}\\},{\overline{{y}}}::{\mathsf{fromCl}({U})}\vdash{t}::{q_{P}}$
if, and only if, $\exists
U^{\prime}.\,V_{\Gamma\backslash\\{{f}::{\tau}\\}},\overline{{y}}\vdash
P\,t\triangleright^{*}U^{\prime}\land U\mathrel{\leq_{\mathsf{a}}}U^{\prime}$

∎

###### Lemma D.9.

  1. (1)

$\Gamma^{\infty}(D_{\mathcal{G}})=\Gamma_{\mathcal{V}(D_{\mathcal{G}})}$ is
${\mathcal{G}}$-coconsistent

  2. (2)

If ${\uparrow_{\mathsf{a}}}(V),\overline{{y}}\vdash G\triangleright^{*}U$,
then there exists $U^{\prime}$ such that $V,\overline{{y}}\vdash
G\triangleright^{*}U^{\prime}$ and $U\mathrel{\leq_{\mathsf{a}}}U^{\prime}$.

  3. (3)

If $V_{1}\mathrel{\leq_{\mathsf{a}}}V_{2}$, then
$V_{2}\subseteq{\uparrow_{\mathsf{a}}}(V_{1})$.

  4. (4)

If $\Gamma$ is ${\mathcal{G}}$-coconsistent, then
$\mathcal{V}(D_{\mathcal{G}})\mathrel{\leq_{\mathsf{a}}}V_{\Gamma}$.

  5. (5)

If $\Gamma\vdash{t}::{\tau}$ and $\Gamma$ is ${\mathcal{G}}$-coconsistent,
then there exists $\tau^{\prime}\leq\tau$ such that
$\Gamma_{\mathcal{V}(D_{\mathcal{G}})}\vdash{t}::{\tau^{\prime}}$.

###### Proof.