\publyear\papernumber

On Higher-Order Reachability Games vs May Reachability

Kazuyuki Asada
Tohoku University
Hiroyuki Kastura
The University of Tokyo
Naoki Kobayashi
The University of Tokyo

Abstract

We consider the reachability problem for higher-order functional programs and study the relationship between reachability games (i.e., the reachability problem for programs with angelic and demonic nondeterminism) and may-reachability (i.e., the reachability problem for programs with only angelic nondeterminism). We show that reachability games for order- $n$ programs can be reduced to may-reachability problems for order-( $n+1$ ) programs, and vice versa. We formalize the reductions by using higher-order fixpoint logic and prove their correctness. We also discuss applications of the reductions to higher-order program verification.

keywords:

Higher-order programs, reachability games, may-reachability

Higher-Order Reachability Games vs May Reachability

1 Introduction

This paper considers the reachability problem for simply-typed, call-by-name higher-order functional programs with integers, recursion, and two kinds of non-deterministic branches (angelic and demonic ones). The problem of solving reachability games (hereafter, simply called the reachability game problem) asks, given a higher-order functional program and a specific control point $\mathbf{succ}$ of the program, whether there exists a sequence of choices on angelic non-determinism that makes the program reach $\mathbf{succ}$ no matter what choices are made on demonic non-determinism. Thus, our reachability game problem is just a special case of the notion of two-player reachability games [1], where the game arena is specified as a higher-order functional program. (An important restriction compared to the general notion of reachability games is that each vertex may have only a finite number of outgoing edges, although there can be infinitely many vertices.)Various program verification problems can be reduced to the reachability game problem. For example, the termination problem, which asks whether a given program terminates for any sequence of non-deterministic choices, is a special case of the reachability game problem, where all the non-deterministic branches are demonic, and all the termination points are expressed by $\mathbf{succ}$ . The safety verification problem, which asks whether a given program may fall into an error state after some sequence of non-deterministic choices, is also a special case, where all the non-deterministic branches are angelic, and error states are expressed by $\mathbf{succ}$ .

We establish relations between the reachability game problem and the may-reachability problem, a special case of the reachability game problem where all the non-deterministic choices are angelic (hence, may-reachability is a one-player game). We show mutual translations between the reachability game problem for order- $n$ programs and the may-reachability problem for order-( $n+1$ ) programs. (Here, the order of a program is defined as the type-theoretic order; the order of a function that takes only integers is 0, and the order of a function that takes an order-0 function is 1, etc.) The translations are size-preserving in the sense that for any order- $n$ program $M$ , one can effectively construct an order-( $n+1$ ) program $M^{\prime}$ such that the answer to the reachability game problem for $M$ is the same as the answer to the may-reachability problem for $M^{\prime}$ , and the size of $M^{\prime}$ is polynomial in that of $M$ ; and vice versa.

The translation from reachability games to may-reachability allows us to use higher-order program verification tools specialized to may-reachability (or, unreachability to error states) such as MoCHi [2] and Liquid types [3] to check a wider class of properties represented as reachability games. Conversely, the translation from may-reachability to reachability games allows us, for example, to use verification tools that can solve reachability games for order-0 programs, such as CHC solvers [4, 5, 6] to check may-reachability of order-1 programs.

We formalize our translations for $\mu$ HFL(Z), which is a fragment HFL(Z) [7] without greatest fixpoint operators and modal operators, where HFL(Z) is an extension of Viswanathan and Viswanathan’s higher-order fixpoint logic [8] with integers. The use of higher-order fixpoint formulas rather than higher-order programs in the formalization of the translations is justified by the result of Kobayashi et al. [7, 9], that there is a direct correspondence between the reachability problem for higher-order programs and the validity problem for the corresponding higher-order fixpoint formulas, where angelic and demonic branches in programs correspond to disjunctions and conjunctions respectively.

The rest of this paper is structured as follows. Section 2 introduces $\mu$ HFL(Z), and clarifies the relationship between the validity checking problem for $\mu$ HFL(Z) and the reachability problem for higher-order programs. Section 3 formalizes a reduction from the order- $n$ reachability game problem to the order-( $n+1$ ) may-reachability problem (as a translation of $\mu$ HFL(Z) formulas), and proves its correctness. Section 4 formalizes a reduction in the opposite direction, from the order-( $n+1$ ) may-reachability problem to the order- $n$ reachability game problem, and proves its correctness. Section 5 discusses applications of the reductions and reports some experimental results. Section 6 discusses related work and Section 7 concludes the paper. This is an extended and revised version of the paper that appeared in Proceedings of RP 2022 [10]. We have added definitions, examples and full proofs.

2 $\mu$ HFL(Z) and Reachability Problems

In this section, we first introduce $\mu$ HFL(Z), a fragment of higher-order fixpoint logic HFL(Z) [7] (which is in turn an extension of Viswanathan and Viswanathan’s higher-order fixpoint logic [8] with integers) without greatest fixpoint operators. We then review the relationship between $\mu$ HFL(Z) and reachability problems, and state the main theorem of this paper.

2.1 Syntax

The set of (simple) types, ranged over by $\kappa$ , is given by:

\begin{array}[]{l}\kappa\mbox{ (types)}::=\mathtt{Int}\mid\tau\\ \tau\mbox{ (predicate types)}::=\star\mid\kappa\to\tau.\end{array}

For a type $\kappa$ , the order and arity of $\kappa$ , written $\mathtt{ord}(\kappa)$ and $\mathtt{ar}(\kappa)$ respectively, are defined by:

\begin{array}[]{l}\mathtt{ord}(\mathtt{Int})=-1\qquad\mathtt{ord}(\star)=0\\ \mathtt{ord}(\kappa\to\tau)=\max(\mathtt{ord}(\tau),\mathtt{ord}(\kappa)+1)\\ \mathtt{ar}(\mathtt{Int})=\mathtt{ar}(\star)=0\qquad\mathtt{ar}(\kappa\to\tau)=\mathtt{ar}(\tau)+1.\end{array}

For example, $\mathtt{ord}(\mathtt{Int}\to\mathtt{Int}\to\star)=0$ and $\mathtt{ord}((\mathtt{Int}\to\star)\to\star)=1$ .¹¹1Defining the order of $\mathtt{Int}$ as $-1$ is a bit unusual, but convenient for stating our technical result.

The set of $\mu$ HFL(Z) formulas, ranged over by $\varphi$ , is given by:

	$\displaystyle\varphi\mbox{ (formulas) }::=x\mid\varphi_{1}\lor\varphi_{2}\mid\varphi_{1}\land\varphi_{2}\mid\mu x^{\tau}.\varphi\mid\varphi_{1}\varphi_{2}\mid\lambda x^{\kappa}.\varphi\ \mid\varphi\,e\mid e_{1}\leq e_{2}$
	$\displaystyle e\mbox{ (integer expressions) }::=n\mid x\mid e_{1}+e_{2}\mid e_{1}\times e_{2}.$

Intuitively, $\mu x^{\tau}.\varphi$ denotes the least predicate $x$ of type $\tau$ such that $x=\varphi$ . We write $\mathtt{true}$ and $\mathtt{false}$ for $0\leq 0$ and $1\leq 0$ respectively. For a formula $\varphi$ , the order of $\varphi$ is defined as: $\max(\{0\}\cup\{\mathtt{ord}(\tau)\mid\mu x^{\tau}.\varphi^{\prime}\mbox{ occurs in }\varphi\})$ . We call a $\mu$ HFL(Z) formula $\varphi$ disjunctive if the conjunction $\land$ occurs in $\varphi$ only in the form of $e_{1}\leq e_{2}\land\varphi_{1}$ (i.e., the left-hand side of $\varphi$ is a primitive constraint on integers).

We write $\widetilde{\varphi}_{j,\ldots,k}$ for a sequence of formulas $\varphi_{j},\ldots,\varphi_{k}$ ; it denotes an empty sequence if $k<j$ . We often omit the subscript and just write $\widetilde{\varphi}$ for $\widetilde{\varphi}_{j,\ldots,k}$ when the subscript is not important. Similarly, we also write $\widetilde{e}$ and $\widetilde{\kappa}$ for sequences of expressions and types respectively. We use the metavariables $\alpha$ , $\beta$ , and $\gamma$ to denote either a formula or an integer expression.

The simple type system for $\mu$ HFL(Z) formulas is defined in Figure 1. Henceforth, we consider only well-typed formulas (i.e., formulas $\varphi$ such that $\mathcal{K}\vdash_{\mathtt{ST}}\varphi:\kappa$ for some $\mathcal{K}$ and $\kappa$ ). A formula $\varphi$ is called a closed formula of type $\kappa$ if $\emptyset\vdash_{\mathtt{ST}}\varphi:\kappa$ .

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K},x\mathbin{:}\kappa\vdash_{\mathtt{ST}}x:\kappa\end{array}}$ (T-Var)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{1}:\star\quad\quad\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{2}:\star\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{1}\lor\varphi_{2}:\star\end{array}}$ (T-Or)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K},x\mathbin{:}\tau\vdash_{\mathtt{ST}}\varphi:\tau\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash_{\mathtt{ST}}\mu x^{\tau}.\varphi:\tau\end{array}}$ (T-Mu)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{1}:\tau_{2}\to\tau\quad\quad\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{2}:\tau_{2}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{1}\varphi_{2}:\tau\end{array}}$ (T-App)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K},x\mathbin{:}\kappa\vdash_{\mathtt{ST}}\varphi:\tau\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash_{\mathtt{ST}}\lambda x^{\kappa}.\varphi:\kappa\to\tau\end{array}}$ (T-Abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash_{\mathtt{ST}}\varphi:\mathtt{Int}\to\tau\quad\quad\mathcal{K}\vdash_{\mathtt{ST}}e:\mathtt{Int}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash_{\mathtt{ST}}\varphi\,e:\tau\end{array}}$ (T-AppInt)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash_{\mathtt{ST}}e_{1}:\mathtt{Int}\quad\quad\mathcal{K}\vdash_{\mathtt{ST}}e_{2}:\mathtt{Int}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash_{\mathtt{ST}}e_{1}\leq e_{2}:\star\end{array}}$ (T-Le)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash_{\mathtt{ST}}n:\mathtt{Int}\end{array}}$ (T-Int)

Figure 1: Simple Type System for

\mu

HFL(Z)

2.2 Semantics of $\mu$ HFL(Z) Formulas

For each simple type $\kappa$ , we define the partially ordered set $\mathop{[\![}\kappa\mathop{]\!]}=(\mathop{(\!|}\kappa\mathop{|\!)},\sqsubseteq_{\kappa})$ where $\sqsubseteq_{\kappa}\subseteq\mathop{(\!|}\kappa\mathop{|\!)}\times\mathop{(\!|}\kappa\mathop{|\!)}$ by:

\begin{array}[]{l}\mathop{(\!|}\mathtt{Int}\mathop{|\!)}=\mathbf{Z}\quad m\sqsubseteq_{\mathtt{Int}}n\Leftrightarrow m=n\quad\mathop{(\!|}\star\mathop{|\!)}=\{\bot,\top\}\quad x\sqsubseteq_{\star}y\Leftrightarrow x=\bot\lor y=\top\\ \mathop{(\!|}\kappa\to\tau\mathop{|\!)}=\{f\in\mathop{(\!|}\kappa\mathop{|\!)}\to\mathop{(\!|}\tau\mathop{|\!)}\mid\forall x,y\in\mathop{(\!|}\kappa\mathop{|\!)}.x\sqsubseteq_{\kappa}y\Rightarrow f(x)\sqsubseteq_{\tau}f(y)\}\\ f\sqsubseteq_{\kappa\to\tau}g\Leftrightarrow\forall x\in\mathop{(\!|}\kappa\mathop{|\!)}.f(x)\sqsubseteq_{\tau}g(y).\\ \end{array}

Here, $\mathbf{Z}$ denotes the set of integers. For each $\tau$ , $\mathop{[\![}\tau\mathop{]\!]}$ (but not $\mathop{[\![}\mathtt{Int}\mathop{]\!]}$ ) forms a complete lattice. We write $\bot_{\tau}$ ( $\top_{\tau}$ ) for the least (greatest, resp.) element of $\mathop{[\![}\tau\mathop{]\!]}$ , and $\sqcap_{\tau}$ ( $\sqcup_{\tau}$ , resp.) for the greatest lower bound (least upper bound, resp.) operation with respect to $\sqsubseteq_{\tau}$ . We also define the least fixpoint operator $\mathbf{LFP}_{\tau}\in\mathop{(\!|}(\tau\to\tau)\to\tau\mathop{|\!)}$ by:

\begin{array}[]{l}\mathbf{LFP}_{\tau}(f)=\sqcap_{\tau}\{g\in\mathop{(\!|}\tau\mathop{|\!)}\mid f(g)\sqsubseteq_{\tau}g\}\\ \end{array}

For a simple type environment $\mathcal{K}$ , we write $\mathop{(\!|}\mathcal{K}\mathop{|\!)}$ for the set of maps $\rho$ such that $\mathit{dom}(\rho)=\mathit{dom}(\mathcal{K})$ and $\rho(x)\in\mathop{(\!|}\mathcal{K}(x)\mathop{|\!)}$ for each $x\in\mathit{dom}(\rho)$ .

For each valid type judgment $\mathcal{K}\vdash_{\mathtt{ST}}\varphi:\kappa$ , its semantics $\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi:\kappa\mathop{]\!]}\in\mathop{(\!|}\mathcal{K}\mathop{|\!)}\to\mathop{(\!|}\kappa\mathop{|\!)}$ is defined by:

	$\displaystyle\mathop{[\![}\mathcal{K},x\mathbin{:}\kappa\vdash_{\mathtt{ST}}x\mathbin{:}\kappa\mathop{]\!]}(\rho)=\rho(x)$
	$\displaystyle\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{1}\lor\varphi_{2}:\star\mathop{]\!]}{\rho}=\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{1}:\star\mathop{]\!]}{\rho}\sqcup_{\star}\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{2}:\star\mathop{]\!]}{\rho}$
	$\displaystyle\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{1}\land\varphi_{2}:\star\mathop{]\!]}{\rho}=\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{1}:\star\mathop{]\!]}{\rho}\sqcap_{\star}\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{2}:\star\mathop{]\!]}{\rho}$
	$\displaystyle\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\mu x^{\tau}.\varphi:\tau\mathop{]\!]}{\rho}=\mathbf{LFP}_{\tau}(\lambda v\in\mathop{(\!\|}\tau\mathop{\|\!)}.\mathop{[\![}\mathcal{K},x\mathbin{:}\tau\vdash_{\mathtt{ST}}\varphi:\tau\mathop{]\!]}(\rho\{x\mapsto v\}))$
	$\displaystyle\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\lambda x^{\kappa}.\varphi:\tau\mathop{]\!]}{\rho}=\lambda w\in\mathop{(\!\|}\kappa\mathop{\|\!)}.\mathop{[\![}\mathcal{K},x\mathbin{:}\kappa\vdash_{\mathtt{ST}}\varphi:\tau\mathop{]\!]}(\rho\{x\mapsto w\})$
	$\displaystyle\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{1}\varphi_{2}:\tau\mathop{]\!]}{\rho}=\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{1}:\tau_{2}\to\tau\mathop{]\!]}{\rho}\,(\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{2}:\tau_{2}\mathop{]\!]}{\rho})$
	$\displaystyle\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi\,e:\tau\mathop{]\!]}{\rho}=\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi:\mathtt{Int}\to\tau\mathop{]\!]}{\rho}\,(\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}e:\mathtt{Int}\mathop{]\!]}{\rho})$
	$\displaystyle\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}e_{1}\leq e_{2}:\star\mathop{]\!]}{\rho}=\left\{\begin{array}[]{ll}\top&\mbox{if $\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}e_{1}:\mathtt{Int}\mathop{]\!]}{\rho}\leq\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}e_{2}:\mathtt{Int}\mathop{]\!]}{\rho}$}\\ \bot&\mbox{otherwise}\end{array}\right.$
	$\displaystyle\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}n:\mathtt{Int}\mathop{]\!]}{\rho}=n$
	$\displaystyle\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}e_{1}+e_{2}:\mathtt{Int}\mathop{]\!]}{\rho}=\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}e_{1}:\mathtt{Int}\mathop{]\!]}{\rho}+\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}e_{2}:\mathtt{Int}\mathop{]\!]}{\rho}$
	$\displaystyle\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}e_{1}\times e_{2}:\mathtt{Int}\mathop{]\!]}{\rho}=\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}e_{1}:\mathtt{Int}\mathop{]\!]}{\rho}\times\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}e_{2}:\mathtt{Int}\mathop{]\!]}{\rho}$

For a closed formula $\varphi$ of type $\star$ , we just write $\mathop{[\![}\varphi\mathop{]\!]}$ for $\mathop{[\![}\emptyset\vdash_{\mathtt{ST}}\varphi:\star\mathop{]\!]}$ . The validity checking problem for $\mu$ HFL(Z) is the problem of deciding whether $\mathop{[\![}\varphi\mathop{]\!]}=\top$ , given a closed $\mu$ HFL(Z) formula $\varphi$ of type $\star$ . Note that the validity checking problem is undecidable.

For closed formulas, the following alternative semantics is sometimes convenient. Let us define the reduction relation $\varphi\longrightarrow\varphi^{\prime}$ by the following rules.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}i\in\{1,2\}\end{array}}{\begin{array}[]{@{}c@{}}E[\varphi_{1}\lor\varphi_{2}]\longrightarrow E[\varphi_{i}]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}E[\mathtt{true}\land\varphi]\longrightarrow E[\varphi]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}E[\mathtt{false}\land\varphi]\longrightarrow E[\mathtt{false}]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}E[\mu x.\varphi]\longrightarrow E[[\mu x.\varphi/x]\varphi]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}E[(\lambda x.\varphi)e]\longrightarrow E[[e/x]\varphi]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}E[(\lambda x.\varphi)\psi]\longrightarrow E[[\psi/x]\varphi]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}b=\left\{\begin{array}[]{ll}\mathtt{true}&\mbox{if $\mathop{[\![}\vdash_{\mathtt{ST}}e_{1}:\mathtt{Int}\mathop{]\!]}\leq\mathop{[\![}\vdash_{\mathtt{ST}}e_{2}:\mathtt{Int}\mathop{]\!]}$}\\ \mathtt{false}&\mbox{otherwise}\end{array}\right.\end{array}}{\begin{array}[]{@{}c@{}}E[e_{1}\leq e_{2}]\longrightarrow E[b]\end{array}}$

Here, $E$ denotes an evaluation context, defined by:

E::=[\,]\mid E\land\varphi\mid E\,\varphi.

We write $\longrightarrow^{*}$ for the reflexive and transitive closure of $\longrightarrow$ . We have the following fact (see, e.g., [11]).

Fact 1

Suppose $\vdash_{\mathtt{ST}}\varphi:\star$ . Then, $\mathop{[\![}\varphi\mathop{]\!]}=\top$ if and only if $\varphi\longrightarrow^{*}\mathtt{true}$ .

Due to the fact above, the validity checking problem is equivalent to the problem of deciding whether $\varphi\longrightarrow^{*}\mathtt{true}$ , given a closed $\mu$ HFL(Z) formula $\varphi$ of type $\star$ .

Example 2.1

Suppose $\vdash_{\mathtt{ST}}\varphi:\mathtt{Int}\to\star$ . Then,

\psi\mathbin{:=}(\mu x^{\mathtt{Int}\to\star}.\lambda y.\varphi\,y\lor\varphi(-y)\lor x(y+1))0\longrightarrow^{*}\mathtt{true}

just if $\varphi\,n\longrightarrow^{*}\mathtt{true}$ for some $n$ . Thus, the formula $\psi$ represents $\exists z.\varphi\,z$ .

The example above indicates that existential quantifiers on integers are expressible in $\mu$ HFL(Z). Below, we treat existential quantifiers as if they were primitives.

2.3 Relationship with Reachability Problems

We consider reachability problems for a call-by-name, simply-typed $\lambda$ -calculus extended with two kinds of non-determinism ( $\blacksquare$ and $\square$ ) and a special term $\mathbf{succ}$ , which represents that the designated target has been reached.²²2In the context of program verification, we are often interested in (un)reachability to bad states. Thus, in that context, $\mathbf{succ}$ in this section is actually interpreted as an error state, and the terms “angelic” and “demonic” below are swapped. The sets of types and terms, ranged over by $\sigma$ and $M$ respectively, are defined by:

	$\displaystyle\sigma$	$\displaystyle::=\mathtt{Int}\mid\eta\qquad\eta::=\mathtt{unit}\mid\sigma\to\eta$
	$\displaystyle M$	$\displaystyle::=(\,)\mid\mathbf{succ}\mid x\mid\lambda x.M\mid M_{1}\,M_{2}\mid M\,e$
		$\displaystyle\mid\mathbf{fix}^{\eta}(x,M)\mid M_{1}\blacksquare M_{2}\mid M_{1}\square M_{2}\mid\mathbf{assume}(e_{1}\leq e_{2});M.$

Here, the meta-variable $e$ ranges over the set of integer expressions as defined in Section 2.1. The term $\mathbf{fix}^{\eta}(x,M)$ denotes a recursive function $x$ of type $\eta$ such that $x=M$ . The term $M_{1}\blacksquare M_{2}$ denotes a demonic choice between $M_{1}$ and $M_{2}$ , where the choice is up to the environment (or, the opponent $\mathtt{O}$ of the reachability game), and $M_{1}\square M_{2}$ denotes an angelic choice between $M_{1}$ and $M_{2}$ , where the choice is up to the term (or, the player $\mathtt{P}$ of the reachability game). The term $\mathbf{assume}(e_{1}\leq e_{2});M$ first checks whether $e_{1}\leq e_{2}$ holds and if so, proceeds to evaluate $M$ ; otherwise aborts the evaluation of the whole term. Using $\mathbf{assume}$ , we can express a conditional expression $\mathbf{if}\ e_{1}\leq e_{2}\ \mathbf{then}\ M_{1}\ \mathbf{else}\ M_{2}$ as $(\mathbf{assume}(e_{1}\leq e_{2});M_{1})\square(\mathbf{assume}(e_{2}+1\leq e_{1});M_{2})$ .

A simple type system for the language is given in Figure 2. In the figure, ${{\Sigma}}\downarrow_{\mathtt{Int}}$ denotes the type environment obtained by restricting ${\Sigma}$ to bindings on $\mathtt{Int}$ , i.e., ${{\Sigma}}\downarrow_{\mathtt{Int}}=\{x\mathbin{:}\sigma\in{\Sigma}\mid\sigma=\mathtt{Int}\}$ . Henceforth, we consider only well-typed terms.

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}{\Sigma}\vdash_{\mathtt{LST}}(\,):\mathtt{unit}\end{array}}$ (LT-Unit)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}{\Sigma}\vdash_{\mathtt{LST}}\mathbf{succ}:\mathtt{unit}\end{array}}$ (LT-Succ)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}{\Sigma},x\mathbin{:}\sigma\vdash_{\mathtt{LST}}x:\sigma\end{array}}$ (LT-Var)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}{\Sigma},x\mathbin{:}\sigma\vdash_{\mathtt{LST}}M:\eta\end{array}}{\begin{array}[]{@{}c@{}}{\Sigma}\vdash_{\mathtt{LST}}\lambda x.M:\sigma\to\eta\end{array}}$ (T-Abs)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}{\Sigma}\vdash_{\mathtt{LST}}M_{1}:\eta_{2}\to\eta\quad\quad{\Sigma}\vdash_{\mathtt{LST}}M_{2}:\eta_{2}\end{array}}{\begin{array}[]{@{}c@{}}{\Sigma}\vdash_{\mathtt{LST}}M_{1}M_{2}:\eta\end{array}}$ (LT-App)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}{\Sigma}\vdash_{\mathtt{LST}}\varphi:\mathtt{Int}\to\tau\quad\quad{{\Sigma}}\downarrow_{\mathtt{Int}}\vdash_{\mathtt{ST}}e:\mathtt{Int}\end{array}}{\begin{array}[]{@{}c@{}}{\Sigma}\vdash_{\mathtt{LST}}\varphi\,e:\tau\end{array}}$ (LT-AppInt)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}{\Sigma},x\mathbin{:}\eta\vdash_{\mathtt{LST}}M:\eta\end{array}}{\begin{array}[]{@{}c@{}}{\Sigma}\vdash_{\mathtt{LST}}\mathbf{fix}^{\eta}(x,M):\eta\end{array}}$ (LT-Fix)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}{\Sigma}\vdash_{\mathtt{LST}}M_{1}:\mathtt{unit}\quad\quad{\Sigma}\vdash_{\mathtt{LST}}M_{2}:\mathtt{unit}\end{array}}{\begin{array}[]{@{}c@{}}{\Sigma}\vdash_{\mathtt{LST}}M_{1}\blacksquare M_{2}:\mathtt{unit}\end{array}}$ (LT-DChoice)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}{\Sigma}\vdash_{\mathtt{LST}}M_{1}:\mathtt{unit}\quad\quad{\Sigma}\vdash_{\mathtt{LST}}M_{2}:\mathtt{unit}\end{array}}{\begin{array}[]{@{}c@{}}{\Sigma}\vdash_{\mathtt{LST}}M_{1}\square M_{2}:\mathtt{unit}\end{array}}$ (LT-AChoice)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}{{\Sigma}}\downarrow_{\mathtt{Int}}\vdash_{\mathtt{ST}}e_{1}:\mathtt{Int}\quad\quad{{\Sigma}}\downarrow_{\mathtt{Int}}\vdash_{\mathtt{ST}}e_{2}:\mathtt{Int}\\ {\Sigma}\vdash_{\mathtt{LST}}M:\mathtt{unit}\end{array}}{\begin{array}[]{@{}c@{}}{\Sigma}\vdash_{\mathtt{LST}}\mathbf{assume}(e_{1}\leq e_{2});M:\mathtt{unit}\end{array}}$ (LT-Assume)

Figure 2: Simple Type System for the Language.

The order of a type $\sigma$ is defined by:

\begin{array}[]{l}\mathtt{ord}(\mathtt{Int})=-1\qquad\mathtt{ord}(\mathtt{unit})=0\qquad\mathtt{ord}(\sigma\to\eta)=\max(\mathtt{ord}(\eta),\mathtt{ord}(\sigma)+1).\end{array}

The order of a term $M$ is defined as the largest order of type $\eta$ such that $M$ has a subterm of the form $\mathbf{fix}^{\eta}(x,M^{\prime})$ . We write $\mathtt{Int}^{n}\to\star$ for $\underbrace{\mathtt{Int}\to\cdots\mathtt{Int}}_{n}\to\star$ .

For a closed simply-typed term $M$ of type $\mathtt{unit}$ , a play is a (possibly infinite) sequence of reductions of $M$ . The play is won by the player $\mathtt{P}$ if it ends with $\mathbf{succ}$ ; otherwise the play is won by the opponent $\mathtt{O}$ . The reachability game for $M$ is the problem of deciding which player ( $\mathtt{P}$ or $\mathtt{O}$ ) has a winning strategy. For the general notion of reachability games and strategies, we refer the reader to [1]. As a special case of the translation of Watanabe et al. [9] from temporal properties of programs to HFL(Z) formulas, we obtain the following translation $(\cdot)^{\dagger}$ from reachability games to $\mu$ HFL(Z) formulas.

	$\displaystyle(\,)^{\dagger}=\mathtt{false}\quad\mathbf{succ}^{\dagger}=\mathtt{true}\quad x^{\dagger}=x\quad(\lambda x.M)^{\dagger}=\lambda x.M^{\dagger}\quad(M_{1}M_{2})^{\dagger}=M_{1}^{\dagger}M_{2}^{\dagger}$
	$\displaystyle(M\,e)^{\dagger}=M^{\dagger}\,e\quad(\mathbf{fix}(x,M))^{\dagger}=\mu x.M^{\dagger}\quad(M_{1}\blacksquare M_{2})^{\dagger}=M_{1}^{\dagger}\land M_{2}^{\dagger}$
	$\displaystyle(M_{1}\square M_{2})^{\dagger}=M_{1}^{\dagger}\lor M_{2}^{\dagger}\quad(\mathbf{assume}(e_{1}\leq e_{2});M)^{\dagger}=e_{1}\leq e_{2}\land M^{\dagger}.$

The following is a special case of the result of Watanabe et al. [9].

Theorem 2.2 ([9])

For any closed simply-typed term $M$ of type $\mathtt{unit}$ and order $k$ , $M^{\dagger}$ is a closed $\mu$ HFL(Z) formula of type $\star$ and order $k$ . The player $\mathtt{P}$ wins the reachability game for $M$ , if and only if, $\mathop{[\![}M^{\dagger}\mathop{]\!]}=\top$ .

Based on the result above, we focus on the validity checking problem for $\mu$ HFL(Z) formulas, instead of directly discussing the reachability problem. Note that the may-reachability problem (of asking whether, given a closed term $M$ of which all the branches are angelic, there exists a reduction sequence from $M$ to $\mathbf{succ}$ ) corresponds to the validity checking problem for disjunctive $\mu$ HFL(Z) formulas.

Example 2.3

Let us consider the following OCaml program.

  let rec sum x k =
    assert(x>=0); if x=0 then k 0 else sum(x-1)(fun y-> k(x+y))
  in sum n (fun r -> assert(r>=n))

Suppose we are interested in checking whether the program suffers from an assertion failure. It is modeled as the reachability problem for the term $M_{\textit{sum}}\,n\,(\lambda r.\mathbf{assume}(r<n);\mathbf{succ})$ , where $M_{\textit{sum}}$ is:

	$\displaystyle\mathbf{fix}(\textit{sum},\lambda x.\lambda k.(\mathbf{assume}(x<0);\mathbf{succ})$
	$\displaystyle\qquad\qquad\square(\mathbf{assume}(x=0);k\,0)\square(\mathbf{assume}(x>0);\textit{sum}\,(x-1)\,(\lambda y.k(x+y)))).$

Here, note that an assertion failure is modeled as $\mathbf{succ}$ in our language. By Theorem 2.2, the above term is reachable to $\mathbf{succ}$ just if the (disjunctive) $\mu$ HFL(Z) formula $\varphi_{\textit{ex1}}:=\varphi_{\textit{sum}}\,n\,(\lambda r.r<n)$ is valid, where $\varphi_{\textit{sum}}$ is:

\displaystyle\mu\mathit{sum}.\lambda x.\lambda k.x<0\lor(x=0\land k\,0)\lor(x>0\land\mathit{sum}\,(x-1)\,(\lambda y.k(x+y))).

The formula $\varphi_{\textit{ex1}}$ is valid only if $n<0$ , which implies that the OCaml program suffers from an assertion failure just if $\texttt{n}<0$ . ∎

2.4 Main Theorem

The main theorem of this paper is stated as follows.

Theorem 2.4

There exist polynomial-time translations $(\cdot)^{\#}$ and $(\cdot)^{\flat}$ between order- $n$ $\mu$ HFL(Z) formulas and order- $(n+1)$ disjunctive $\mu$ HFL(Z) formulas that satisfy the following properties.

(i)

For any order- $n$ closed $\mu$ HFL(Z) formula $\varphi$ , $\varphi^{\#}$ is an order-( $n+1$ ) closed disjunctive $\mu$ HFL(Z) formula such that $\mathop{[\![}\varphi\mathop{]\!]}=\mathop{[\![}\varphi^{\#}\mathop{]\!]}$ .
(ii)

For any order-( $n+1$ ) closed disjunctive $\mu$ HFL(Z) formula $\varphi$ , $\varphi^{\flat}$ is an order- $n$ closed $\mu$ HFL(Z) formula such that $\mathop{[\![}\varphi\mathop{]\!]}=\mathop{[\![}\varphi^{\flat}\mathop{]\!]}$ .

Due to the connection between reachability problems and $\mu$ HFL(Z) validity checking problems discussed in Section 2.3, the theorem above implies that any order- $n$ reachability game can be converted in polynomial time to order-( $n+1$ ) may-reachability problem, and vice versa. The result allows us to use a tool for checking the may-reachability of higher-order programs (such as MoCHi [2]) to solve the reachability game, and conversely, to use a tool for solving the order- $n$ reachability game (such as $\nu$ HFL(Z) validity checkers [12, 13] and a HoCHC solver [14]) to check the may-reachability of order-( $n+1$ ) programs; see Section 5 for more discussion on the applications.

3 From Order- $n$ Reachability Games to Order-( $n+1$ ) May-Reachability

In this section, we show the translation $(\cdot)^{\#}$ from order- $n$ $\mu$ HFL(Z) formulas to order-( $n+1$ ) disjunctive $\mu$ HFL(Z) formulas. The idea is to transform each proposition $\varphi$ (i.e. a formula of type $\star$ ) to a predicate $\varphi^{\#^{\prime}}$ of type $\star\to\star$ , so that $\mathtt{true}$ and $\mathtt{false}$ are respectively converted to the identity function $\lambda x.x$ and the constant function $\lambda x.\mathtt{false}$ . We can then encode the conjunction $\varphi_{1}\land\varphi_{2}$ as $\lambda x^{\star}.\varphi_{1}^{\#^{\prime}}(\varphi_{2}^{\#^{\prime}}x)$ , which is equivalent to the identity function if both $\varphi_{1}^{\#^{\prime}}$ and $\varphi_{2}^{\#^{\prime}}$ are so, and is equivalent to $\lambda x.\mathtt{false}$ if one of $\varphi_{1}^{\#^{\prime}}$ and $\varphi_{2}^{\#^{\prime}}$ is so.

The translation $(\cdot)^{\#}$ for formulas and types is defined as follows.

	$\displaystyle\varphi^{\#}=\varphi^{\#^{\prime}}\,\mathtt{true}\qquad(e_{1}\leq e_{2})^{\#^{\prime}}=\lambda x^{\star}.(e_{1}\leq e_{2}\land x)\quad(\lambda x^{\kappa}.M)^{\#^{\prime}}=\lambda x^{\kappa^{\#}}.M^{\#^{\prime}}$
	$\displaystyle(\varphi_{1}\varphi_{2})^{\#^{\prime}}=\varphi_{1}^{\#^{\prime}}\varphi_{2}^{\#^{\prime}}\quad(\varphi\,e)^{\#^{\prime}}=\varphi^{\#^{\prime}}\,e\quad(\mu x^{\tau}.\varphi)^{\#^{\prime}}=\mu x^{\tau^{\#}}.\varphi^{\#^{\prime}}$
	$\displaystyle(\varphi_{1}\lor\varphi_{2})^{\#^{\prime}}=\lambda x^{\star}.\varphi_{1}^{\#^{\prime}}x\lor\varphi_{2}^{\#^{\prime}}x\quad(\varphi_{1}\land\varphi_{2})^{\#^{\prime}}=\lambda x^{\star}.\varphi_{1}^{\#^{\prime}}(\varphi_{2}^{\#^{\prime}}x)$
	$\displaystyle\mathtt{Int}^{\#}=\mathtt{Int}\qquad\star^{\#}=\star\to\star\qquad(\kappa\to\tau)^{\#}=\kappa^{\#}\to\tau^{\#}.$

Example 3.1

Consider the formula $\varphi:=(\mu p^{\mathtt{Int}\to\star}.\lambda y.y=0\lor(p\,(y-1)\land p\,(y+1)))\,n$ (where $n$ is an integer constant). We obtain the following formula as $\varphi^{\#}$ :

	$\displaystyle(\mu p^{\mathtt{Int}\to\star\to\star}.\lambda y.\lambda x^{\star}.(\lambda x^{\star}.y=0\land x)x$
	$\displaystyle\qquad\qquad\qquad\lor(\lambda x^{\star}.p\,(y-1)\,(p\,(y+1)\,x))\,x)\,n\,\mathtt{true}.$

By simplifying the formula with $\beta$ -reductions, we obtain:

	$\displaystyle(\mu p^{\mathtt{Int}\to\star\to\star}.\lambda y.\lambda x^{\star}.$
	$\displaystyle\qquad(y=0\land x)\lor p\,(y-1)\,(p\,(y+1)\,x))\,n\,\mathtt{true}.$

The following theorem states the correctness of the translation.

Theorem 3.2

If $\varphi$ is an order- $n$ closed $\mu$ HFL(Z) formula, then $\varphi^{\#}$ is an order-( $n+1$ ) closed disjunctive $\mu$ HFL(Z) formula, and $\mathop{[\![}\varphi\mathop{]\!]}=\mathop{[\![}\varphi^{\#}\mathop{]\!]}$ .

To show the theorem above, we first extend the translation of types to that of type environments by: $(x_{1}\mathbin{:}\kappa_{1},\ldots,x_{k}\mathbin{:}\kappa_{k})^{\#}=x_{1}\mathbin{:}\kappa_{1}^{\#},\ldots,x_{k}\mathbin{:}\kappa_{k}^{\#}$ .

The following lemma guarantees that the translation preserves typing.

Lemma 3.3

If $\mathcal{K}\vdash_{\mathtt{ST}}\varphi:\kappa$ , then $\mathcal{K}^{\#}\vdash_{\mathtt{ST}}\varphi^{\#^{\prime}}:\kappa^{\#}$ .

Proof 3.4

Straightforward induction on the derivation of $\mathcal{K}\vdash_{\mathtt{ST}}\varphi:\kappa$ .

Corollary 3.5

If $\varphi$ is an order- $n$ closed $\mu$ HFL(Z) formula of type $\star$ , then $\varphi^{\#}$ is an order-( $n+1$ ) closed disjunctive $\mu$ HFL(Z) formula of type $\star$ .

Proof 3.6

Suppose $\varphi$ is an order- $n$ closed $\mu$ HFL(Z) formula. By Lemma 3.3, we have $\emptyset\vdash_{\mathtt{ST}}\varphi^{\#^{\prime}}:\star\to\star$ , which implies $\emptyset\vdash_{\mathtt{ST}}\varphi^{\#}:\star$ . Since each $\mu$ -formula $\mu x^{\tau}.\varphi^{\prime}$ in $\varphi$ is translated to $\mu x^{\tau^{\#}}.\varphi^{\prime}$ and $\mathtt{ord}(\tau^{\#})=\mathtt{ord}(\tau)+1$ , $\varphi^{\#}$ is an order-( $n+1$ ) formula. Furthermore, all the conjunctions in $\varphi^{\#}$ are of the form $e_{1}\leq e_{2}\land\psi$ ; hence it is disjunctive.

To prove the latter part of the theorem (i.e., $\mathop{[\![}\varphi\mathop{]\!]}=\mathop{[\![}\varphi^{\#}\mathop{]\!]}$ ), we define the relation $\sim_{\kappa}\subseteq\mathop{[\![}\kappa\mathop{]\!]}\times\mathop{[\![}\kappa^{\#}\mathop{]\!]}$ between the values of the source and the target of the translation, by induction on $\kappa$ .

	$\displaystyle\sim_{\mathtt{Int}}=\{(n,n)\mid n\in\mathop{[\![}\mathbf{Z}\mathop{]\!]}\}$
	$\displaystyle\sim_{\star}=\{(\bot,\lambda x\in\mathop{[\![}\star\mathop{]\!]}.\bot)\}\cup\{(\top,\lambda x\in\mathop{[\![}\star\mathop{]\!]}.x)\}$
	$\displaystyle\sim_{\kappa\to\tau}=$
	$\displaystyle\quad\{(f,g)\mid\forall(v,w)\in\mathop{[\![}\kappa\mathop{]\!]}\times\mathop{[\![}\kappa^{\#}\mathop{]\!]}.v\sim_{\kappa}w\Rightarrow f\,v\sim_{\tau}g\,w\}.$

We extend $\sim_{\kappa}$ pointwise to the relation $\sim_{\mathcal{K}}\subseteq\mathop{[\![}\mathcal{K}\mathop{]\!]}\times\mathop{[\![}\mathcal{K}^{\#}\mathop{]\!]}$ on environments by:

\rho\sim_{\mathcal{K}}\rho^{\prime}\Leftrightarrow\rho(x)\sim_{\mathcal{K}(x)}\rho^{\prime}(x)\mbox{ for every $x\in\mathit{dom}(\rho)$}.

We first prepare the following lemma.

Lemma 3.7

If $f\sim_{\tau\to\tau}g$ , then $\mathbf{LFP}_{\tau}(f)\sim_{\tau}\mathbf{LFP}_{\tau^{\#}}(g)$ .

Proof 3.8

By Cousot and Cousot’s fixpoint theorem [15], there exists an ordinal $\gamma$ such that $\mathbf{LFP}(f)=f^{\gamma}(\bot_{\tau})$ and $\mathbf{LFP}(g)=g^{\gamma}(\bot_{\tau^{\#}})$ . Here, $f^{\gamma}(x)$ is defined by:

f(x)=\left\{\begin{array}[]{ll}x&\mbox{if $\gamma=0$}\\ f(f^{\gamma^{\prime}}(x))&\mbox{if $\gamma=\gamma^{\prime}+1$}\\ \sqcup_{\gamma^{\prime}<\gamma}f^{\gamma^{\prime}}(x)&\mbox{if $\gamma$ is a limit ordinal.}\\ \end{array}\right.

Thus, it suffices to show $f^{\gamma}(\bot_{\tau})\sim_{\tau}g^{\gamma}(\bot_{\tau^{\#}})$ by induction on $\gamma$ . The case where $\gamma=0$ or $\gamma=\gamma^{\prime}+1$ is trivial. Suppose $\gamma$ is a limit ordinal. Suppose $\tau=\kappa_{1}\to\cdots\to\kappa_{k}\to\star$ , and $v_{i}\sim_{\kappa_{i}}w_{i}$ for $i\in\{1,\ldots,k\}$ . It suffices to show

f^{\gamma}(\bot_{\tau})v_{1}\,\cdots\,v_{k}\sim_{\star}g^{\gamma}(\bot_{\tau^{\#}})w_{1}\,\cdots\,w_{k}.

By the induction hypothesis, we have $f^{\gamma^{\prime}}(\bot_{\tau})\sim_{\tau}g^{\gamma^{\prime}}(\bot_{\tau^{\#}})$ for any $\gamma^{\prime}<\gamma$ . Thus, we have:

	$\displaystyle f^{\gamma}(\bot_{\tau})v_{1}\,\cdots\,v_{k}$
	$\displaystyle=(\sqcup_{\gamma^{\prime}<\gamma}f^{\gamma^{\prime}}(\bot_{\tau}))v_{1}\,\cdots\,v_{k}$
	$\displaystyle=\sqcup_{\gamma^{\prime}<\gamma}(f^{\gamma^{\prime}}(\bot_{\tau})v_{1}\,\cdots\,v_{k})$
	$\displaystyle\sim_{\star}\sqcup_{\gamma^{\prime}<\gamma}(g^{\gamma^{\prime}}(\bot_{\tau})w_{1}\,\cdots\,w_{k})$
	$\displaystyle=(\sqcup_{\gamma^{\prime}<\gamma}g^{\gamma^{\prime}}(\bot_{\tau}))w_{1}\,\cdots\,w_{k}$
	$\displaystyle=g^{\gamma}(\bot_{\tau})w_{1}\,\cdots\,w_{k}$

Theorem 3.2 is an immediate corollary of the following lemma.

Lemma 3.9

Suppose $\mathcal{K}\vdash_{\mathtt{ST}}\varphi:\kappa$ . Then $\rho\sim_{\mathcal{K}}\rho^{\prime}$ implies $\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi:\kappa\mathop{]\!]}\rho\sim_{\kappa}\mathop{[\![}\mathcal{K}^{\#}\vdash_{\mathtt{ST}}\varphi^{\#^{\prime}}:\kappa^{\#}\mathop{]\!]}\rho^{\prime}$ .

Proof 3.10

The proof proceeds by induction on the derivation of $\mathcal{K}\vdash_{\mathtt{ST}}\varphi:\kappa$ . Since the other cases are similar or trivial, we show only the main cases.

•

Case T-And: In this case, $\varphi=\varphi_{1}\land\varphi_{2}$ and $\varphi^{\#^{\prime}}=\lambda x.\varphi_{1}^{\#^{\prime}}(\varphi_{2}^{\#^{\prime}}\,x)$ , with $\kappa=\star$ and $\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{i}:\star$ . By the induction hypothesis, we have $\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{i}:\star\mathop{]\!]}\rho\sim_{\star}\mathop{[\![}\mathcal{K}^{\#}\vdash_{\mathtt{ST}}\varphi_{i}^{\#^{\prime}}:\star^{\#}\mathop{]\!]}\rho^{\prime}$ for $i\in\{1,2\}$ . If $\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi:\star\mathop{]\!]}\rho=\top$ , then $\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{i}:\star\mathop{]\!]}\rho=\top$ for both $i=1$ and $2$ . Thus, $\mathop{[\![}\mathcal{K}^{\#}\vdash_{\mathtt{ST}}\varphi_{i}^{\#^{\prime}}:\star^{\#}\mathop{]\!]}\rho^{\prime}=\lambda x.x$ for both $i=1$ and $2$ . Therefore, we have $\mathop{[\![}\mathcal{K}^{\#}\vdash_{\mathtt{ST}}\varphi^{\#^{\prime}}:\star^{\#}\mathop{]\!]}\rho^{\prime}=\lambda x.x$ as required. Otherwise, i.e., if $\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi:\star\mathop{]\!]}\rho=\bot$ , then $\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{i}:\star\mathop{]\!]}\rho=\bot$ for $i=1$ or $2$ . Thus, $\mathop{[\![}\mathcal{K}^{\#}\vdash_{\mathtt{ST}}\varphi_{i}^{\#^{\prime}}:\star^{\#}\mathop{]\!]}\rho^{\prime}=\lambda x.\bot$ for such $i$ . Therefore, we have $\mathop{[\![}\mathcal{K}^{\#}\vdash_{\mathtt{ST}}\varphi^{\#^{\prime}}:\star^{\#}\mathop{]\!]}\rho^{\prime}=\lambda x.\bot$ as required.
•

Case T-Mu: In this case, $\varphi=\mu x^{\tau}.\varphi^{\prime}$ and $\varphi^{\#^{\prime}}=\mu x^{\tau^{\#}}.\varphi^{\prime\#^{\prime}}$ with $\kappa=\tau$ and $\mathcal{K},x\mathbin{:}\tau\vdash_{\mathtt{ST}}\varphi^{\prime}:\tau$ . By the induction hypothesis, we have $\mathop{[\![}\mathcal{K},x\mathbin{:}\tau\vdash_{\mathtt{ST}}\varphi^{\prime}:\tau\mathop{]\!]}(\rho\{x\mapsto v\})\sim_{\tau}\mathop{[\![}\mathcal{K},x\mathbin{:}\tau^{\#}\vdash_{\mathtt{ST}}\varphi^{\prime\#^{\prime}}:\tau^{\#}\mathop{]\!]}(\rho^{\prime}\{x\mapsto w\})$ for any $v\sim_{\tau}w$ , which implies $\mathop{[\![}\mathcal{K}\vdash_{\mathtt{ST}}\lambda x.\varphi^{\prime}:\tau\to\tau\mathop{]\!]}\rho\sim_{\tau}\mathop{[\![}\mathcal{K}^{\#}\vdash_{\mathtt{ST}}\lambda x.\varphi^{\prime\#^{\prime}}:(\tau\to\tau)^{\#}\mathop{]\!]}\rho^{\prime}$ . Thus, the required result follows by Lemma 3.7.

We are now ready to prove Theorem 3.2.

\PRstyle
Proof of Theorem 3.2:
Suppose $\emptyset\vdash_{\mathtt{ST}}\varphi:\star$ . By Corollary 3.5, $\varphi^{\#^{\prime}}$ is an order- $(n+1)$ closed disjunctive $\mu$ HFL(Z) formula. By Lemma 3.9, we have $\mathop{[\![}\varphi\mathop{]\!]}=\mathop{[\![}\emptyset\vdash_{\mathtt{ST}}\varphi:\star\mathop{]\!]}\emptyset\sim_{\star}\mathop{[\![}\emptyset\vdash_{\mathtt{ST}}\varphi^{\#^{\prime}}:\star\mathop{]\!]}\emptyset$ . Thus, if $\mathop{[\![}\varphi\mathop{]\!]}=\top$ , then $\mathop{[\![}\varphi^{\#}\mathop{]\!]}=\mathop{[\![}\varphi^{\#^{\prime}}\mathop{]\!]}\top=(\lambda x.x)\top=\top$ . If $\mathop{[\![}\varphi\mathop{]\!]}=\bot$ , then $\mathop{[\![}\varphi^{\#}\mathop{]\!]}=\mathop{[\![}\varphi^{\#^{\prime}}\mathop{]\!]}\top=(\lambda x.\bot)\top=\bot$ , as required. \QED

4 From Order-( $n+1$ ) May-Reachability to Order- $n$ Reachability Games

In this section, we show the translation $(\cdot)^{\flat}$ from order-( $n+1$ ) disjunctive $\mu$ HFL(Z) formulas to order- $n$ $\mu$ HFL(Z) formulas. The translation $(\cdot)^{\flat}$ is much more involved than the translation $(\cdot)^{\#}$ . We first give some intuitions on the first-order case in Section 4.1. We then give the translation for the general case in Section 4.2, and prove the correctness in Section 4.3.

4.1 Intuitions for the Order-1 Case

Let us recall the formula $\varphi_{\textit{ex1}}:=\varphi_{\textit{sum}}\,n\,(\lambda r.r<n)$ in Example 2.3, where $\varphi_{\mathit{sum}}\mathbin{:}\mathtt{Int}\to(\mathtt{Int}\to\star)\to\star$ is:

\displaystyle\mu\mathit{sum}.\lambda x.\lambda k.x<0\lor(x=0\land k\,0)\lor(x>0\land\mathit{sum}\,(x-1)\,(\lambda y.k(x+y))).

Note that the order of the formula above is $1$ . We wish to construct a formula $\psi$ of order $0$ , such that $\mathop{[\![}\varphi_{\mathit{ex1}}\mathop{]\!]}=\mathop{[\![}\psi\mathop{]\!]}$ . Recall that, by Fact 1, $\mathop{[\![}\varphi_{\mathit{ex1}}\mathop{]\!]}=\top$ just if $\varphi_{\mathit{ex1}}\longrightarrow^{*}\mathtt{true}$ . There are two cases where the formula $\varphi_{\mathit{ex1}}$ may be reduced to $\mathtt{true}$ : (i) $\varphi_{\mathit{ex1}}$ is reduced to $\mathtt{true}$ without the order-0 argument $\lambda r.r<n$ being called; and (ii) $\varphi_{\mathit{ex1}}$ is reduced to $(\lambda r.r<n)m$ for some $m$ , and then $(\lambda r.r<n)m$ is reduced to $\mathtt{true}$ . Let $\varphi_{\mathit{sum}_{0}}\,n$ be the condition for the first case to occur, and let $\varphi_{\mathit{sum}_{1}}\,n\,m$ be the condition that $\varphi_{\mathit{ex1}}$ is reduced to $(\lambda r.r<n)m$ . Then, $\varphi_{\mathit{sum}_{0}}$ and $\varphi_{\mathit{sum}_{1}}$ can be expressed as follows.

	$\displaystyle\varphi_{\mathit{sum}_{0}}\mathbin{:=}$	$\displaystyle\mu\mathit{sum}_{0}.\lambda x.x<0\lor(x>0\land\mathit{sum}_{0}\,(x-1)).$
	$\displaystyle\varphi_{\mathit{sum}_{1}}\mathbin{:=}$	$\displaystyle\mu\mathit{sum}_{1}.\lambda x.\lambda z.(x=0\land z=0)\lor(x>0\land\exists y.\mathit{sum}_{1}\,(x-1)\,y\land z=x+y).$

To understand the formula $\varphi_{\mathit{sum}_{1}}$ , notice that $\varphi_{\mathit{sum}}\,(x-1)\,(\lambda y.k(x+y))$ is reduced to $k\,z$ just if $\mathit{sum}\,(x-1)\,(\lambda y.k(x+y))$ is first reduced to $(\lambda y.k(x+y))y$ for some $y$ (the condition for which is expressed by ${\mathit{sum}_{1}}\,(x-1)\,y$ ), and $z=x+y$ holds.

Using $\varphi_{\mathit{sum}_{0}}$ and $\varphi_{\mathit{sum}_{1}}$ above, the formula $\varphi_{\textit{ex1}}$ can be translated to:

\psi\mathbin{:=}\varphi_{\mathit{sum}_{0}}\,n\lor\exists r.\varphi_{\mathit{sum}_{1}}\,n\,r\land r<n.

Note that the order of $\psi$ is $0$ . In general, if $\varphi$ is an order-1 (disjunctive) formula of type

\mathtt{Int}^{k}\to(\mathtt{Int}^{\ell_{1}}\to\star)\to\cdots\to(\mathtt{Int}^{\ell_{m}}\to\star)\to\star

and $\psi_{i}$ ( $i\in\{1,\ldots,m\}$ ) is a formula of type $\mathtt{Int}^{\ell_{i}}\to\star$ , then $\varphi\,\widetilde{e}_{1,\ldots,k}\,\psi_{1}\,\cdots\,\psi_{m}$ can be translated to an order-0 formula of the form:

\varphi_{0}\,\widetilde{e}_{1,\ldots,k}\lor\bigvee_{i\in\{1,\ldots,m\}}\exists\widetilde{y}_{1,\ldots,\ell_{i}}.(\varphi_{i}\,\widetilde{e}_{1,\ldots,k}\,\widetilde{y}_{1,\ldots,\ell_{i}}\land\psi_{i}\,\widetilde{y}_{1,\ldots,\ell_{i}}),

where the part $\varphi_{0}\,\widetilde{e}_{1,\ldots,k}$ expresses the condition for $\varphi\,\widetilde{e}_{1,\ldots,k}\,\psi_{1}\,\cdots\,\psi_{m}$ to be reduced to $\mathtt{true}$ without $\psi_{i}$ being called, and the part $\varphi_{i}\,\widetilde{e}_{1,\ldots,k}\,\widetilde{y}_{1,\ldots,\ell_{i}}$ expresses the condition for $\varphi\,\widetilde{e}_{1,\ldots,k}\,\psi_{1}\,\cdots\,\psi_{m}$ to be reduced to $\psi_{i}\,\widetilde{y}_{1,\ldots,\ell_{i}}$ .

4.2 Translation for the General Case

For higher-order formulas, the translation is more involved. To simplify the formalization, we assume that a formula as an input or output of our translation is given in the form $(\Theta,D,\varphi_{0})$ , called an equation system; here $D$ is a set of mutually recursive fixpoint equations of the form $\{F_{1}\,\widetilde{x}_{1}=_{\mu}\varphi_{1},\ldots,F_{n}\,\widetilde{x}_{n}=_{\mu}\varphi_{n}\}$ and $\Theta$ is the type environment for $F_{1},\ldots,F_{n}$ . We sometimes omit $\Theta$ and just write $(D,\varphi_{0})$ . Here, each $\varphi_{i}$ ( $i\in\{0,\ldots,n\}$ ) should be fixpoint-free, $\varphi_{0}$ is well-typed under $\Theta$ , and $\varphi_{i}$ ( $i\in\{1,\ldots,n\}$ ) should have some type $\tau_{i}$ under the type environment $\Theta,x_{i,1}\mathbin{:}\kappa_{i,1},\ldots,x_{i,m_{i}}\mathbin{:}\kappa_{i,m_{i}}$ , where $\Theta(F_{i})=\kappa_{i,1}\to\cdots\to\kappa_{i,m_{i}}\to\tau_{i}$ and $\widetilde{x}_{i}=x_{i,1}\cdots x_{i,m_{i}}$ . The $\mu$ HFL(Z) formula $(D,\varphi_{0})^{\mu}$ represented by $(\Theta,D,\varphi_{0})$ is defined by:

\displaystyle(\emptyset,\varphi)^{\mu}=\varphi\quad(D\cup\{F\,\widetilde{x}=_{\mu}\psi\},\varphi)^{\mu}=([\mu F.\lambda\widetilde{x}.\psi/F]D,[\mu F.\lambda\widetilde{x}.\psi/F]\varphi)^{\mu}.

We write $\mathop{[\![}(D,\varphi)\mathop{]\!]}$ for $\mathop{[\![}(D,\varphi)^{\mu}\mathop{]\!]}$ .

For an equation system as an input of our translation, we further assume, without loss of generality, the following conditions.

(I)

Each $\varphi_{i}$ ( $i\in\{1,\ldots,n\}$ ) on the right-hand side of a definition in $D$ has type $\star$ and is generated by the following grammar (where the metavariable $x$ may be a fixpoint variable $F_{j}$ or its parameters):

\begin{array}[]{l}\varphi::=x\mid\varphi_{1}\lor\varphi_{2}\mid e_{1}\leq e_{2}\land\varphi\mid\varphi_{1}\varphi_{2}\mid\varphi\,e.\end{array}

(1)

In particular, (i) $\varphi_{i}$ is a disjunctive $\mu$ HFL(Z) formula, (ii) $\varphi_{i}$ contains neither $\lambda$ -abstractions nor fixpoint operators, and (iii) a formula of the form $e_{1}\leq e_{2}$ may occur only in the form $e_{1}\leq e_{2}\land\varphi$ .

(II)

Every integer predicate (i.e., a formula of type of the form $\mathtt{Int}^{\ell}\to\star$ with $\ell\geq 0$ ) that occurs in an argument position has the same arity $M$ . In other words, in any function type $\kappa\to\tau$ , either $\kappa=\mathtt{Int}^{M}\to\star$ , or $\mathtt{ord}(\kappa)\neq 0$ .
(III)

The “main formula” $\varphi_{0}$ is a formula of the form $F\,\lambda\widetilde{x}_{1,\ldots,M}.\mathtt{true}$ .

Note that the assumption above does not lose generality. Given an order- $(n+1)$ disjunctive $\mu$ HFL(Z) formula $\varphi$ , it can be first transformed to a formula of the form $\varphi^{\prime}\,\mathtt{true}$ , where $\mathtt{true}$ does not occur on the right-hand side of any conjunction in $\varphi^{\prime}$ . We then set $M$ to the largest arity of integer predicates that occur in argument positions in $\varphi^{\prime}\,\mathtt{true}$ , and raise the arity of every integer predicate argument to $M$ by adding dummy arguments. For example, given

(\lambda f^{\mathtt{Int}\to\star}.f\,1)((\lambda g^{\mathtt{Int}\to\mathtt{Int}\to\star}.g\,1)(\lambda x^{\mathtt{Int}}.\lambda y^{\mathtt{Int}}.x\leq y)),

we can set $M$ to $2$ , and replace the formula with:

\displaystyle(\lambda f^{\prime\mathtt{Int}\to\mathtt{Int}\to\star}.f^{\prime}\,1\,0)\lambda z_{1}.\lambda z_{2}.((\lambda g^{\mathtt{Int}\to\mathtt{Int}\to\star}.g\,1)(\lambda x^{\mathtt{Int}}.\lambda y^{\mathtt{Int}}.x\leq y))\,z_{1}.

Here, we have inserted dummy (actual and formal) parameters $0$ and $z_{2}$ to increase the arities of $f$ and the argument of $\lambda f^{\mathtt{Int}\to\star}.f\,1$ . We can then apply $\lambda$ -lifting to remove $\lambda$ -abstractions and generate a set of top-level definitions $D$ .

The formula $\varphi_{\mathit{ex1}}$ given earlier in this section is represented as: $(\Theta_{\mathit{sum}},D_{\mathit{sum}},S\,\lambda z.\mathtt{true})$ , where $D_{\mathit{sum}}$ consists of the following equations. Here, $M$ is set to $1$ .

	$\displaystyle S\;t=_{\mu}\mathit{sum}\,t\,n\,(C\,t)$
	$\displaystyle C\;t\;r=_{\mu}r<n\land t\,0$
	$\displaystyle\mathit{sum}\;t\;x\;k=_{\mu}(x<0\land t\,0)\lor(x=0\land k\,0)\lor(x>0\land\mathit{sum}\,t\,(x-1)\,(K\,k\,x))$
	$\displaystyle K\;k\;x\;y=_{\mu}k(x+y),$

and $\Theta_{\mathit{sum}}$ is:

	$\displaystyle S\mathbin{:}(\mathtt{Int}\to\star)\to\star,C\mathbin{:}(\mathtt{Int}\to\star)\to\mathtt{Int}\to\star,$
	$\displaystyle\mathit{sum}\mathbin{:}(\mathtt{Int}\to\star)\to\mathtt{Int}\to(\mathtt{Int}\to\star)\to\star,$
	$\displaystyle K\mathbin{:}(\mathtt{Int}\to\star)\to\mathtt{Int}\to\mathtt{Int}\to\star.$

We translate each equation $F\,y_{1}\,\cdots\,y_{m}=_{\mu}\varphi$ in $D$ as follows. We first decompose the formal parameters $y_{1},\ldots,y_{m}$ to two parts: $y_{1},\ldots,y_{j}$ and $y_{j+1},\ldots,y_{m}$ , where the orders of (the types of) $y_{j+1},\ldots,y_{m}$ are at most $0$ , and the order of $y_{j}$ is at least $1$ ; note that the sequences $y_{1},\ldots,y_{j}$ and $y_{j+1},\ldots,y_{m}$ are possibly empty. We further decompose $y_{j+1},\ldots,y_{m}$ into order-0 variables $x_{1},\ldots,x_{k}$ and integer variables $z_{1},\ldots,z_{p}$ (thus, $j+k+p=m$ ). Formally, the decomposition of formal parameters is defined by:

	$\displaystyle\mathtt{decomparg}(\epsilon,\star)=(\epsilon,\epsilon,\epsilon)$
	$\displaystyle\mathtt{decomparg}(u\cdot\widetilde{y},\kappa\to\tau)=$
	$\displaystyle\left\{\begin{array}[]{ll}((u\mathbin{:}\kappa)\cdot\mathcal{K},\widetilde{x},\widetilde{z})&\mbox{if $\mathtt{decomparg}(\widetilde{y},\tau)=(\mathcal{K},\widetilde{x},\widetilde{z}),\mathcal{K}\neq\epsilon$}\\ (u\mathbin{:}\kappa,\widetilde{x},\widetilde{z})&\mbox{if $\mathtt{ord}(\kappa)>0$},\mbox{$\mathtt{decomparg}(\widetilde{y},\tau)=(\epsilon,\widetilde{x},\widetilde{z})$}\\ (\epsilon,u\cdot\widetilde{x},\widetilde{z})&\mbox{if $\kappa=\mathtt{Int}^{M}\to\star$, }\mbox{$\mathtt{decomparg}(\widetilde{y},\tau)=(\epsilon,\widetilde{x},\widetilde{z})$}\\ (\epsilon,\widetilde{x},u\cdot\widetilde{z})&\mbox{if $\kappa=\mathtt{Int},\mathtt{decomparg}(\widetilde{y},\tau)=(\epsilon,\widetilde{x},\widetilde{z})$}\end{array}\right.$

Here, $\mathtt{decomparg}(\widetilde{y}_{1,\ldots,m},\Theta(F))$ decomposes the sequence of variables $\widetilde{y}_{1,\ldots,m}$ and returns a triple $(\mathcal{K},\widetilde{x},\widetilde{z})$ , where $\mathcal{K}$ is the type environment for $y_{1},\ldots,y_{j}$ , $\widetilde{x}$ is the sequence of integer predicate variables, and $\widetilde{z}$ is the sequence of integer variables.

For example, given an equation $F\,u_{1}\,u_{2}\,u_{3}\,u_{4}\,u_{5}=_{\mu}\varphi$ , where $\Theta(F)=\mathtt{Int}\to((\mathtt{Int}\to\star)\to\star)\to\mathtt{Int}\to(\mathtt{Int}\to\star)\to\mathtt{Int}\to\star$ , the formal parameters $u_{1}\,\cdots\,u_{5}$ are decomposed as follows.

\displaystyle\mathtt{decomparg}(u_{1}\,\cdots\,u_{5},\Theta(F))=(\{u_{1}\mathbin{:}\mathtt{Int},u_{2}\mathbin{:}(\mathtt{Int}\to\star)\to\star\},u_{4},u_{3}u_{5}).

Given an equation $F\,\widetilde{y}=_{\mu}\varphi$ where $\mathtt{decomparg}(\widetilde{y},\Theta(F))=(\mathcal{K},\widetilde{x}_{1,\ldots,k},\widetilde{z})$ with $\mathcal{K}=y_{1}\mathbin{:}\kappa_{1},\ldots,y_{j}\mathbin{:}\kappa_{j}$ , we generate equations for new fixpoint variables $F_{0},\ldots,F_{k}$ . As in the order-1 case, for $i\in\{1,\ldots,k\}$ , $F_{i}\,\widetilde{\varphi}^{\prime}_{1,\ldots,j}\,\widetilde{z}\,\widetilde{u}_{1,\ldots,M}$ represents the condition for $F\,\widetilde{\varphi}_{1,\ldots,j}\,\widetilde{w}$ to be reduced to $x_{i}\,\widetilde{u}_{1,\ldots,M}$ (where $\widetilde{\varphi}^{\prime}_{1,\ldots,j}$ is the sequence of formulas obtained by translating $\widetilde{\varphi}_{1,\ldots,j}$ in a recursive manner, and $\widetilde{w}$ is a sequence obtained by shuffling $\widetilde{x}_{1,\ldots,k}$ and $\widetilde{z}$ ). $F_{0}$ is a new component required to deal with higher-order formulas; it is used to compute the condition for $F\,\widetilde{y}$ to be reduced to $x\,\widetilde{u}_{1,\ldots,\ell_{i}}$ for some order-0 predicate $x$ , which has been passed through higher-order parameters $\widetilde{y}_{1,\ldots,j}$ . For example, consider a formula $F\,(G\,x)\,y$ where $F\mathbin{:}((\mathtt{Int}\to\star)\to\star)\to(\mathtt{Int}\to\star)\to\star,G\mathbin{:}(\mathtt{Int}\to\star)\to(\mathtt{Int}\to\star)\to\star$ . Then, the condition for $F\,(G\,x)\,y$ to be reduced to $y\,n$ is computed by using $F_{1}$ , while the condition for $F\,(G\,x)\,y$ to be reduced to $x\,n$ is computed by using $F_{0}$ ; see Example 4.1 for a concrete version of this example.

To compute $F_{0},\ldots,F_{k}$ , we translate each subformula $\varphi$ of the body of $F$ to:

(\varphi_{*},\varphi_{0},\varphi_{1},\ldots,\varphi_{k},\varphi_{k+1},\ldots,\varphi_{k+\mathtt{gar}(\tau)}),

where $\tau$ is the type of $\varphi$ , and $\mathtt{gar}(\tau)$ denotes the number of order-0 arguments passed after the last argument of order greater than $0$ . More precisely, we define the decomposition of types as follows.

	$\displaystyle\mathtt{decomp}(\star)=(\epsilon,\epsilon,0)$
	$\displaystyle\mathtt{decomp}(\kappa\to\tau)=\left\{\begin{array}[]{ll}(\kappa\cdot\widetilde{\kappa},m,n)&\mbox{if $\mathtt{decomp}(\tau)=(\widetilde{\kappa},m,n),\widetilde{\kappa}\neq\epsilon$}\\ (\kappa,m,n)&\mbox{if $\mathtt{ord}(\kappa)>0,\mathtt{decomp}(\tau)=(\epsilon,m,n)$}\\ (\epsilon,m+1,n)&\mbox{if $\kappa=\mathtt{Int}^{M}\to\star,\mathtt{decomp}(\tau)=(\epsilon,m,n)$}\\ (\epsilon,m,n+1)&\mbox{if $\kappa=\mathtt{Int},\mathtt{decomp}(\tau)=(\epsilon,m,n)$}\end{array}\right.$

Then, $\mathtt{gar}(\tau)$ denotes $m$ when $\mathtt{decomp}(\tau)=(\widetilde{\kappa},m,n)$ . For example, for $\tau=(\mathtt{Int}\to\star)\to((\mathtt{Int}\to\star)\to\star)\to(\mathtt{Int}\to\star)\to\mathtt{Int}\to(\mathtt{Int}\to\star)\to\star$ , $\mathtt{decomp}(\tau)=((\mathtt{Int}\to\star)\cdot((\mathtt{Int}\to\star)\to\star),2,1)$ ; hence $\mathtt{gar}(\tau)=2$ . Here, $\varphi_{1},\ldots,\varphi_{k}$ are analogous to $F_{1},\ldots,F_{k}$ : they are used for computing the condition for $\varphi\,\widetilde{\psi}$ to be reduced to $x_{i}\,\widetilde{n}$ . Similarly, $\varphi_{k+i}$ (where $i\in\{1,\ldots,\mathtt{gar}(\tau)\}$ ) is used for computing the condition for $\varphi\,\widetilde{\psi}$ to be reduced to $\psi_{i}\,\widetilde{n}$ , where $\psi_{i}$ is the $i$ -th order-0 argument of $\varphi$ . The component $\varphi_{0}$ is analogous to $F_{0}$ , and used to compute the condition for $\varphi\,\widetilde{\psi}$ to be reduced to $x\,\widetilde{n}$ , where $x$ is an order-0 predicate passed through higher-order arguments of $\varphi$ . The other component $\varphi_{*}$ is similar to $\varphi_{0}$ , but the target order-0 predicate $x$ may have already been set inside $\varphi_{*}$ .

Based on the intuition above, we formalize the translation of a formula as the relation:

\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi:\tau\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{k+\mathtt{gar}(\tau)}).

Here, $\Theta$ denotes the type environment for fixpoint variables defined by $D$ . If $\varphi$ is a subformula of the body of $F$ , and $F$ is defined by $F\,\widetilde{y}=_{\mu}\varphi_{F}$ , then $\mathcal{K}$ and $\widetilde{x}_{1,\ldots,k}$ are set to $\mathcal{K}_{F},\widetilde{z}\mathbin{:}\widetilde{\mathtt{Int}}$ and $\widetilde{x}_{F}$ respectively, where $\mathtt{decomparg}(\widetilde{y},\Theta(F))=(\mathcal{K}_{F},\widetilde{x}_{F},\widetilde{z})$ .

The output $(\varphi_{*},\varphi_{0},\ldots,\varphi_{k+\mathtt{gar}(\tau)})$ of the translation has type $\tau^{\flat,k+2}$ under the type environment $\Theta^{\flat^{\prime}},\mathcal{K}^{\flat}$ , where the translations of types and type environments are defined by:

	$\displaystyle\mathtt{Int}^{\flat,k}=\mathtt{Int}$
	$\displaystyle\tau^{\flat,k}=(\Pi_{i=1,\ldots,k}(\widetilde{\kappa}^{\flat,2}\to\mathtt{Int}^{n+M}\to\star))\times(\Pi_{i=1,\ldots,m}(\widetilde{\kappa}^{\flat,1}\to\mathtt{Int}^{n+M}\to\star))$
	(if $\mathtt{decomp}(\tau)=(\widetilde{\kappa},m,n)$ )
	$\displaystyle\emptyset^{\flat}=\emptyset$
	$\displaystyle(\mathcal{K},y\mathbin{:}\mathtt{Int})^{\flat}=\mathcal{K}^{\flat},y\mathbin{:}\mathtt{Int}$
	$\displaystyle(\mathcal{K},y\mathbin{:}\tau)^{\flat}=\mathcal{K}^{\flat},y_{}\mathbin{:}\tau_{},y_{0}\mathbin{:}\tau_{0},\ldots,y_{k}\mathbin{:}\tau_{k}\mbox{where $\tau^{\flat,2}=\tau_{*}\times\tau_{0}\times\cdots\times\tau_{k}$}$
	$\displaystyle\emptyset^{\flat^{\prime}}=\emptyset$
	$\displaystyle(\Theta,F\mathbin{:}\tau)^{\flat^{\prime}}=\Theta^{\flat^{\prime}},F_{0}\mathbin{:}\tau_{0},\ldots,F_{k}\mathbin{:}\tau_{k}\mbox{where $\tau^{\flat,1}=\tau_{0}\times\cdots\times\tau_{k}$}.$

Here, we have extended simple types with product types; we extend the definition of the order of a type by: $\mathtt{ord}(\tau_{1}\times\cdots\times\tau_{n})=\max(\mathtt{ord}(\tau_{1}),\ldots,\mathtt{ord}(\tau_{n}))$ . Note that the translation of a type decreases the order of the type by one, i.e., $\mathtt{ord}(\tau^{\flat,k})=\max(0,\mathtt{ord}(\tau)-1)$ .

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\varphi_{j}=\left\{\begin{array}[]{ll}\lambda\widetilde{z}_{1,\ldots,M}.\lambda\widetilde{w}_{1,\ldots,M}.\wedge_{p=1,\ldots,M}(z_{p}=w_{p}),&\mbox{if $j=i$}\\ \lambda\widetilde{z}_{1,\ldots,M}.\lambda\widetilde{w}_{1,\ldots,M}.\mathtt{false}&\mbox{otherwise}\end{array}\right.\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}x_{i}:\mathtt{Int}^{M}\to\star\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{k})\end{array}}$ (Tr-VarG)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathtt{decomp}(\mathcal{K}(y))=(\widetilde{\kappa},m,p)\\ \end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}y:\mathcal{K}(y)\leadsto(y_{*},\underbrace{y_{0},\ldots,y_{0}}_{k+1},y_{1},\ldots,y_{m})\end{array}}$ (Tr-Var)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathtt{decomp}(\Theta(F))=(\widetilde{\kappa},m,p)\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}F:\Theta(F)\leadsto(F_{0},\underbrace{F_{0},\ldots,F_{0}}_{k+1},F_{1},\ldots,F_{m})\end{array}}$ (Tr-VarF)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi:\star\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{k})\quad\quad\psi_{j}=\lambda\widetilde{z}_{1,\ldots,M}.e_{1}\leq e_{2}\land\varphi_{j}\,\widetilde{z}_{1,\ldots,M}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}e_{1}\leq e_{2}\land\varphi:\star\leadsto(\psi_{*},\psi_{0},\ldots,\psi_{k})\end{array}}$ (Tr-Le)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathtt{ord}(\kappa_{0}\to\tau)>1\quad\quad\mathtt{gar}(\kappa_{0}\to\tau)=m\quad\quad\mathtt{gar}(\kappa_{0})=m^{\prime}\\ \mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi:\kappa_{0}\to\tau\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{k+m})\quad\quad\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\psi:\kappa_{0}\leadsto(\psi_{*},\psi_{0},\ldots,\psi_{k+m^{\prime}})\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi\,\psi:\tau\leadsto(\varphi_{*}(\psi_{*},\psi_{0},\psi_{k+1},\ldots,\psi_{k+m^{\prime}}),\varphi_{0}(\psi_{0},\psi_{0},\psi_{k+1},\ldots,\psi_{k+m^{\prime}}),\\ \qquad\qquad\qquad\varphi_{1}(\psi_{1},\psi_{0},\psi_{k+1},\ldots,\psi_{k+m^{\prime}}),\ldots,\varphi_{k}(\psi_{k},\psi_{0},\psi_{k+1},\ldots,\psi_{k+m^{\prime}}),\\ \qquad\qquad\qquad\varphi_{k+1}(\psi_{0},\psi_{k+1},\ldots,\psi_{k+m^{\prime}}),\ldots,\varphi_{k+m}(\psi_{0},\psi_{k+1},\ldots,\psi_{k+m^{\prime}}))\end{array}}$ (Tr-App)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathtt{decomp}(\tau)=(\epsilon,m-1,p)\quad\quad\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi:(\mathtt{Int}^{M}\to\star)\to\tau\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{k+m})\\ \mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\psi:{\mathtt{Int}}^{M}\to\star\leadsto(\psi_{*},\psi_{0},\ldots,\psi_{k})\\ \xi_{j}=\lambda\widetilde{z}_{1,\ldots,p}.\lambda\widetilde{w}_{1,\ldots,M}.\varphi_{j}\,\widetilde{z}\,\widetilde{w}\lor\exists\widetilde{u}_{1,\ldots,M}.(\varphi_{k+1}\,\widetilde{z}\,\widetilde{u}_{1,\ldots,M}\land\psi_{j}\,\widetilde{u}_{1,\ldots,M}\,\widetilde{w}_{1,\ldots,M})\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi\,\psi:\tau\leadsto(\xi_{*},\xi_{0},\ldots,\xi_{k},\varphi_{k+2},\ldots,\varphi_{k+m})\end{array}}$ (Tr-AppG)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi:\mathtt{Int}\to\tau\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{\ell+k})\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi\,e:\tau\leadsto(\varphi_{*}\,e,\varphi_{0}\,e,\ldots,\varphi_{\ell+k}\,e)\end{array}}$ (Tr-AppI)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi:\star\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{k})\quad\quad\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\psi:\star\leadsto(\psi_{*},\psi_{0},\ldots,\psi_{k})\\ \xi_{j}=\lambda\widetilde{z}_{1,\ldots,M}.{\varphi_{j}\,\widetilde{z}_{1,\ldots,M}}\lor{\psi_{j}\,\widetilde{z}_{1,\ldots,M}}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi\lor\psi:\star\leadsto(\xi_{*},\xi_{0},\ldots,\xi_{k})\end{array}}$ (Tr-Disj)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathtt{decomparg}(\widetilde{w},\Theta(F))=(\widetilde{y}\mathbin{:}\widetilde{\kappa},\widetilde{x}_{1,\ldots,k},\widetilde{z})\\ y_{1}\mathbin{:}\kappa_{1},\ldots,y_{m}\mathbin{:}\kappa_{m},\widetilde{z}\mathbin{:}\widetilde{\mathtt{Int}};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi:\star\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{k})\\ \Bigg{\{}\begin{aligned} \ &\widetilde{y}_{i}=(y_{i,*},y_{i,0},\ldots,y_{i,\mathtt{gar}(\kappa_{i})})&&\widetilde{y}^{\prime}_{i}=(y_{i,0},\ldots,y_{i,\mathtt{gar}(\kappa_{i})})&&\text{if }i\in\{1,\dots,m\},\ \kappa_{i}\neq\mathtt{Int}\\ &\widetilde{y}_{i}=y_{i}&&\widetilde{y}^{\prime}_{i}=y_{i}&&\text{if }i\in\{1,\dots,m\},\ \kappa_{i}=\mathtt{Int}\end{aligned}\end{array}}{\begin{array}[]{@{}c@{}}\vdash_{\Theta}(F\,\widetilde{w}=_{\mu}\varphi)\leadsto\{F_{0}\,\widetilde{y}_{1}\,\cdots\,\widetilde{y}_{m}\,\widetilde{z}=_{\mu}\varphi_{*}\}\cup\{F_{i}\,\widetilde{y}^{\prime}_{1}\,\cdots\,\widetilde{y}^{\prime}_{m}\,\widetilde{z}=_{\mu}\varphi_{i}\mid i\in\{1,\ldots,k\}\}\end{array}}$ (Tr-Def)

$\displaystyle\frac{\begin{array}[]{@{}c@{}}D^{\prime}=\bigcup\{D^{\prime\prime}\mid\vdash_{\Theta}(F\,\widetilde{y}=_{\mu}\varphi)\leadsto D^{\prime\prime}\mid F\,\widetilde{y}=_{\mu}\varphi\in D\}\end{array}}{\begin{array}[]{@{}c@{}}(D,S\,\lambda\widetilde{z}.\mathtt{true})\leadsto(D^{\prime},\exists\widetilde{z}.S_{1}\,\widetilde{z})\end{array}}$ (Tr-Main)

Figure 3: Translation from order-(

n+1

) disjunctive

\mu

HFL(Z) to order-

n

\mu

HFL(Z).

The translation rules are given in Figure 3. We explain the main rules below. In the rule Tr-VarG for an order-0 variable $x_{i}$ (which should disappear after the translation), $\varphi_{j}\;\widetilde{z}_{1,\ldots,M}\;\widetilde{w}_{1,\ldots,M}$ should represent the condition for $x_{i}\;\widetilde{z}_{1,\ldots,M}\longrightarrow^{*}x_{j}\;\widetilde{w}_{1,\ldots,M}$ ; thus $\varphi_{j}$ is defined so that $\widetilde{z}_{1,\ldots,M}\;\widetilde{w}_{1,\ldots,M}$ is equivalent to $\mathtt{true}$ just if $i=j$ and $\widetilde{z}_{1,\ldots,M}=\widetilde{w}_{1,\ldots,M}$ . In the rule Tr-Var for a variable $y$ in $\mathcal{K}$ , the output of the translation is constructed from $(y_{*},y_{0},y_{1},\ldots,y_{m})$ , whose values will be provided by the environment. Because the environment does not know order-0 variables $x_{1},\ldots,x_{k}$ , we use $y_{0}$ to compute the condition for $y\,\widetilde{\psi}$ to be reduced to $x_{i}\,\widetilde{m}$ . The rule Tr-VarF for fixpoint variables is almost the same as Tr-Var, except that the component $F_{0}$ is reused for $F_{*}$ . The rationale for this is as follows: both $\varphi_{*}$ and $\varphi_{0}$ are used for computing the condition for a target order-0 predicate variable (which is set by the environment) to be reached, and the only difference between them is that the target predicate may have already been set in $\varphi_{*}$ , but since $F$ is a closed formula, such distinction does not make any difference; hence $F_{0}$ and $F_{*}$ need not be distinguished from each other.

In the rule Tr-App, the first two components ( $\varphi_{*}(\psi_{*},\ldots)$ and $\varphi_{0}(\psi_{0},\ldots)$ ) are used for computing the condition for some target predicates (set by the environment) to be reached, and the next $k$ components ( $\varphi_{1}(\psi_{1},\ldots),\ldots,\varphi_{k}(\psi_{k},\ldots)$ ) are used for computing the condition for predicate $x_{1},\ldots,x_{k}$ to be reached. The rule Tr-AppG is another rule for applications, where the argument $\psi$ is an order-0 predicate. The component $\xi_{j}$ of the output is used for computing the condition for the predicate $x_{i}$ to be reached (i.e., the condition for a formula of the form $\varphi\,\psi\,\widetilde{\psi^{\prime}}$ to be reduced to $x_{i}\,\widetilde{w}_{1,\ldots,\ell_{j}}$ , where $\widetilde{\psi^{\prime}}$ consists of order-0 predicates and integer arguments $\widetilde{z}_{1,\ldots,p}$ ). The formula $\varphi\,\psi\,\widetilde{\psi^{\prime}}$ may be reduced to $x_{i}\,\widetilde{w}_{1,\ldots,\ell_{j}}$ if either (i) $\varphi\,\psi\,\widetilde{\psi^{\prime}}\longrightarrow^{*}x_{i}\,\widetilde{w}_{1,\ldots,\ell_{j}}$ without $\psi$ being called, or (ii) $\varphi\,\psi\,\widetilde{\psi^{\prime}}$ is reduced to $\psi\,\widetilde{z}\,\widetilde{u}$ for some $\widetilde{u}$ , and then $\psi\,\widetilde{z}\,\widetilde{u}$ is reduced to $x_{i}\,\widetilde{w}_{1,\ldots,\ell_{j}}$ . The part $\varphi_{j}\,\widetilde{z}\,\widetilde{w}$ represents the former condition, and the part $\exists\widetilde{u}.\cdots$ represents the latter condition. In the rule Tr-Def for definitions, the bodies of the definitions for $F_{0},\ldots,F_{k}$ are set to the corresponding components of the translation of the body of $F$ .

Example 4.1

Consider $S\,(\lambda x.\mathtt{true})$ , where $S$ is defined by:

	$\displaystyle S\,t=_{\mu}F\,(G\,t)\,t$
	$\displaystyle F\,v\,w=_{\mu}v\,H\lor w\,2$
	$\displaystyle G\,p\,q=_{\mu}p\,1$
	$\displaystyle H\,x=_{\mu}H\,x$

There are the following two ways for $S\,t$ to be reduced to $t\,n$ for some $n$ :

	$\displaystyle S\,t\longrightarrow F\,(G\,t)\,t\longrightarrow G\,t\,H\lor t\,2\longrightarrow G\,t\,H\longrightarrow t\,1$
	$\displaystyle S\,t\longrightarrow F\,(G\,t)\,t\longrightarrow G\,t\,H\lor t\,2\longrightarrow t\,2.$

The output of our transformations (with some simplification) is $\exists z.S_{1}\,z$ where:

	$\displaystyle S_{1}=_{\mu}\lambda w_{1}.F_{0}\,(\lambda w_{1}.G_{0}\,w_{1}\lor G_{1}\,w_{1},G_{0},G_{2})\,w_{1}\lor F_{1}\,(G_{0},G_{2})\,w_{1}$
	$\displaystyle F_{0}\,(v_{},v_{0},v_{1})=_{\mu}\lambda z_{1}.v_{}\,z_{1}\lor\exists u_{1}.v_{1}\,u_{1}\land H_{0}\,u_{1}\,z_{1}$
	$\displaystyle F_{1}\,(v_{0},v_{1})=_{\mu}\lambda z_{1}.v_{0}\,z_{1}\lor(\exists u_{1}.v_{1}\,u_{1}\land H_{0}\,u_{1}\,z_{1})\lor 2=z_{1}$
	$\displaystyle G_{0}=_{\mu}\lambda w_{1}.\mathtt{false}\quad G_{1}=_{\mu}\lambda w_{1}.1=w_{1}\quad G_{2}=_{\mu}\lambda w_{1}.\mathtt{false}\quad H_{0}\,x=_{\mu}H_{0}\,x.$

Notice that the formula $S_{1}\,z$ has the following two reduction sequences that lead to the conditions of the form $z=n$ for some $n$ .

	$\displaystyle S_{1}\,z\longrightarrow^{}F_{0}\,(\lambda w_{1}.G_{0}\,w_{1}\lor G_{1}\,w_{1},G_{0},G_{2})\,z\longrightarrow^{}(\lambda w_{1}.G_{0}\,w_{1}\lor G_{1}\,w_{1})z\longrightarrow^{*}1=z$
	$\displaystyle S_{1}\,z\longrightarrow^{}F_{1}\,(G_{0},G_{2})\,z\longrightarrow^{}G_{0}\,z\lor(\exists u_{1}.G_{2}\,u_{1}\land H_{0}\,u_{1}\,z)\lor 2=z\longrightarrow^{*}2=z.$

The former reduction sequence corresponds to the reduction sequence of the original formula $S\,t\longrightarrow^{*}t\,1$ where $t$ embedded in the first argument of $F$ (in $F\,(G\,t)\,t$ ) is called, and the latter reduction sequence corresponds to the reduction sequence $S\,t\longrightarrow^{*}t\,2$ where the second argument $t$ of $F$ (in $F\,(G\,t)\,t$ ) is called. Note that the first condition $1=z$ has been computed by using $F_{0}$ , and the second condition $2=z$ has been computed by using $F_{1}$ . ∎

Example 4.2

Recall the example of $D_{\mathit{sum}}$ given earlier in this section. The following is the output of the translation (with some simplification by $\beta$ -reductions and simple quantifier eliminations).

	$\displaystyle S_{0}=_{\mu}\lambda w_{1}.\mathit{sum}_{0}\,n\,w_{1}\lor\exists u_{1}.\mathit{sum}_{2}\,n\,u_{1}\land C_{0}\,u_{1}\,w_{1}$
	$\displaystyle S_{1}=_{\mu}\lambda w_{1}.\mathit{sum}_{0}\,n\,w_{1}\lor\mathit{sum}_{1}\,n\,w_{1}\lor\exists u_{1}.\mathit{sum}_{2}\,n\,u_{1}\land(C_{0}\,u_{1}\,0\lor c_{1}\,u_{1}\,w_{1})$
	$\displaystyle C_{0}\,x=_{\mu}\lambda z_{1}.\mathtt{false}$
	$\displaystyle C_{1}\,x=_{\mu}\lambda z_{1}.x<n\land 0=z_{1}$
	$\displaystyle\mathit{sum}_{0}\,x=_{\mu}\lambda z_{1}.(x>0\land(\mathit{sum}_{0}\,(x-1)\,z_{1}\lor\exists u_{1}.\mathit{sum}_{2}\,(x-1)\,u_{1}\land K_{0}\,x\,u_{1}\,z_{1}))$
	$\displaystyle\mathit{sum}_{1}\,x=_{\mu}x<0\lor(x>0\land(\mathit{sum}_{0}\,(x-1)\,0\lor\mathit{sum}_{1}(x-1)\lor\exists u_{1}.\mathit{sum}_{2}\,(x-1)\,u_{1}\land K_{0}\,x\,u_{1}\,0))$
	$\displaystyle\mathit{sum}_{2}\,x=_{\mu}\lambda z_{1}.x=0\land 0=z_{1}$
	$\displaystyle\qquad\qquad\qquad\lor(x>0\land(\mathit{sum}_{0}\,(x-1)\,z_{1}$
	$\displaystyle\qquad\qquad\qquad\qquad\lor\exists u_{1}.\mathit{sum}_{2}\,(x-1)\,u_{1}\land(K_{0}\,x\,u_{1}\,z_{1}\lor\exists u_{2}.(K_{1}\,x\,u_{1}\,u_{2}\land u_{2}=z_{1}))))$
	$\displaystyle K_{0}\,x\,y=_{\mu}\lambda w_{1}.\mathtt{false}$
	$\displaystyle K_{1}\,x\,y=_{\mu}\lambda w_{1}.x+y=w_{1}.$

Although the output may look complicated, since the order of the resulting formula is $0$ , we can directly translate its validity checking problem to a CHC solving problem using the method of [16], for which various automated solvers are available [4, 5, 6]. ∎

Example 4.3

Let us consider the formula $S\,\lambda z.\mathtt{true}$ ³³3Taken from [12]., where:

	$\displaystyle S\,t=_{\mu}\mathit{sum}\,\mathit{plus}\,n\,(C\,t)$
	$\displaystyle C\,t\,x=_{\mu}x<n\land t\,0$
	$\displaystyle\mathit{sum}\,f\,x\,k=_{\mu}x\leq 0\land k\,0\lor x>0\land f\,x\,(D\,f\,x\,k)$
	$\displaystyle\mathit{plus}\,x\,k=_{\mu}k(x+x)$
	$\displaystyle D\,f\,x\,k\,y=_{\mu}\mathit{sum}\,f\,(x-1)\,(E\,y\,k)$
	$\displaystyle E\,y\,k\,z=_{\mu}k(y+z).$

It is translated to $\exists z.S_{1}\,z$ , where:⁴⁴4This is a mechanically generated output based on the transformation rules, followed by slight manual simplification.

	$\displaystyle S_{1}=_{\mu}\lambda w_{1}.\mathit{sum}_{0}\,(\mathit{plus}_{0},\mathit{plus}_{0},\mathit{plus}_{1})\,n\,w_{1}$
	$\displaystyle\quad\lor\exists u_{1}.\mathit{sum}_{1}(\mathit{plus}_{0},\mathit{plus}_{1})\,n\,u_{1}\land(C_{0}\,u_{1}\,w_{1}\lor C_{1}\,u_{1}\,w_{1})$
	$\displaystyle C_{0}\,x=_{\mu}\lambda z_{1}.\mathtt{false}$
	$\displaystyle C_{1}\,x=_{\mu}\lambda w_{1}.x<n\land 0=z_{1}$
	$\displaystyle\mathit{sum}_{0}\,(f_{},f_{0},f_{1})\,x=_{\mu}\lambda z_{1}.x>0\land(f_{}\,x\,z_{1}$
	$\displaystyle\qquad\qquad\lor\exists u_{1}.f_{1}\,x\,u_{1}\land D_{0}(f_{*},f_{0},f_{1})\,x\,u_{1}\,z_{1})$
	$\displaystyle\mathit{sum}_{1}\,(f_{0},f_{1})\,x=_{\mu}\lambda z_{1}.x\leq 0\land 0=z_{1}\lor x>0\land(f_{0}\,x\,z_{1}\lor$
	$\displaystyle\qquad\exists u_{1}.f_{1}\,x\,u_{1}\land(D_{0}(f_{0},f_{0},f_{1})\,x\,u_{1}\,z_{1}\lor D_{1}(f_{0},f_{1})\,x\,u_{1}\,z_{1}))$
	$\displaystyle\mathit{plus}_{0}\,x=_{\mu}\lambda w_{1}.\mathtt{false}$
	$\displaystyle\mathit{plus}_{1}\,x=_{\mu}\lambda w_{1}.x+x=w_{1}$
	$\displaystyle D_{0}\,(f_{},f_{0},f_{1})\,x\,y=_{\mu}\lambda w_{1}.\mathit{sum}_{0}\,(f_{},f_{0},f_{1})\,(x-1)\,w_{1}$
	$\displaystyle\qquad\lor\exists u_{1}.\mathit{sum}_{1}\,(f_{0},f_{1})\,(x-1)\,u_{1}\land E_{0}\,y\,u_{1}\,w_{1}$
	$\displaystyle D_{1}\,(f_{0},f_{1})\,x\,y=_{\mu}\lambda w_{1}.\mathit{sum}_{0}\,(f_{0},f_{0},f_{1})\,(x-1)\,w_{1}$
	$\displaystyle\qquad\lor\exists u_{1}.\mathit{sum}_{1}(f_{0},f_{1})\,u_{1}$
	$\displaystyle\qquad\qquad\land(E_{0}\,y\,u_{1}\,w_{1}\lor\exists u_{2}.E_{1}\,y\,u_{1}\,u_{2}\land u_{2}=w_{1})$
	$\displaystyle E_{0}\,y\,z=_{\mu}\lambda w_{1}.\mathtt{false}$
	$\displaystyle E_{1}\,y\,z=_{\mu}\lambda w_{1}.y+z=w_{1}.$

The order of the original formula is $2$ (since $\mathit{sum}:(\mathtt{Int}\to(\mathtt{Int}\to\star)\to\star)\to\mathtt{Int}\to(\mathtt{Int}\to\star)\to\star$ ), while the order of the formula obtained by the translation is $1$ ; note that $\mathit{sum}_{0}:(\mathtt{Int}^{2}\to\star)\times(\mathtt{Int}^{2}\to\star)\times(\mathtt{Int}^{2}\to\star)\to\mathtt{Int}^{2}\to\star$ . By further simplifications (note that the $0$ -components $\mathit{sum}_{0},C_{0},D_{0},\ldots$ actually return $\mathtt{false}$ ), we obtain:

	$\displaystyle S_{1}=_{\mu}\lambda w_{1}.\exists u_{1}.\mathit{sum}_{1}(\mathit{plus}_{0},\mathit{plus}_{1})\,n\,u_{1}\land C_{1}\,u_{1}\,w_{1}$
	$\displaystyle C_{1}\,x=_{\mu}\lambda w_{1}.x<n\land 0=z_{1}$
	$\displaystyle\mathit{sum}_{1}\,(f_{0},f_{1})\,x=_{\mu}\lambda z_{1}.x\leq 0\land 0=z_{1}$
	$\displaystyle\qquad\lor x>0\land(f_{0}\,x\,z_{1}\lor\exists u_{1}.f_{1}\,x\,u_{1}\land D_{1}(f_{0},f_{1})\,x\,u_{1}\,z_{1})$
	$\displaystyle\mathit{plus}_{0}\,x=_{\mu}\lambda w_{1}.\mathtt{false}$
	$\displaystyle\mathit{plus}_{1}\,x=_{\mu}\lambda w_{1}.x+x=w_{1}$
	$\displaystyle D_{1}\,(f_{0},f_{1})\,x\,y=_{\mu}\lambda w_{1}.\exists u_{1}.\mathit{sum}_{1}(f_{0},f_{1})\,u_{1}\land E_{1}\,y\,u_{1}\,w_{1}$
	$\displaystyle E_{1}\,y\,z=_{\mu}\lambda w_{1}.y+z=w_{1}.$

∎

4.3 Correctness

We show the correctness of the translation.

The following lemma states that the output of the translation is well-typed.

Lemma 4.4

If $\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi:\tau\leadsto(\varphi_{*},\widetilde{\varphi}_{0,\dots,k+\mathtt{gar}(\tau)})$ , then $\Theta^{\flat^{\prime}},\mathcal{K}^{\flat}\vdash_{\mathtt{ST}}(\varphi_{*},\widetilde{\varphi}_{0,\dots,k+\mathtt{gar}(\tau)}):\tau^{\flat,k+2}$ . Also, for $(y\mathbin{:}\tau)\in\mathcal{K}$ , $y_{*}$ does not occur free in $\widetilde{\varphi}_{0,\dots,k+\mathtt{gar}(\tau)}$ .

Proof 4.5

Straightforward induction on the derivation of $\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi:\tau\leadsto(\varphi_{*},\widetilde{\varphi}_{0,\dots,k+\mathtt{gar}(\tau)})$ .

The following theorem states the correctness of the translation.

Theorem 4.6

If $(D,S\,\lambda\widetilde{z}_{1,\ldots,M}.\mathtt{true})\leadsto(D^{\prime},\psi)$ , then $\mathop{[\![}(D,S\,\lambda\widetilde{z}_{1,\ldots,M}.\mathtt{true})\mathop{]\!]}=\mathop{[\![}(D^{\prime},\psi)\mathop{]\!]}$ .

The rest of this section is devoted to the proof of Theorem 4.6. The proof consists of the following two steps: (i) we first reduce the proof of Theorem 4.6 to the case where a given equation system is recursion-free (in Section 4.3.1), by using a standard technique of finite approximation, and then (ii) we show the recursion-free case (in Section 4.3.3, with some preparation in Section 4.3.2).

For an equation system $(\Theta,D,S\,\mathtt{true})$ , we define $=_{D}$ as follows: $\varphi=_{D}\psi$ if $\mathop{[\![}(D,\varphi)\mathop{]\!]}=\mathop{[\![}(D,\psi)\mathop{]\!]}$ . For $(F\,\widetilde{x}=_{\mu}\varphi)\in D$ , we may drop the subscript $\mu$ and write $F\,\widetilde{x}=\varphi$ if there is no confusion. We write $[\psi_{i}/x_{i}]_{i=1}^{m}\varphi$ for the substitution $[\psi_{1}/x_{1},\dots,\psi_{m}/x_{m}]\varphi$ .

4.3.1 Reduction to the Recursion-free Case

Here we briefly explain how we can reduce Theorem 4.6 to the recursion-free case.

For an equation system $(\Theta,D,\varphi_{0})$ and $m\in\mathbb{N}$ , the $m$ -th approximation $(\Theta^{(m)},D^{(m)},\varphi_{0}^{(m)})$ is defined as follows:

	$\displaystyle\Theta^{(m)}:=$	$\displaystyle\ \{F^{(i)}\mapsto\Theta(F)\mid F\in\mathit{dom}(\Theta),0\leq i\leq m\}$
	$\displaystyle\varphi^{(i)}:=$	$\displaystyle\ [F^{(i)}/F]_{F\in\mathit{dom}(\Theta)}\varphi\quad(\text{for any $\varphi$ and $i\in\{0,\dots,m\}$})$
	$\displaystyle D^{(m)}:=$	$\displaystyle\ \{F^{(i)}\,\widetilde{x}=\varphi^{(i-1)}\mid(F\,\widetilde{x}=\varphi)\in D,1\leq i\leq m\}$
	$\displaystyle\cup$	$\displaystyle\ \{F^{(0)}\,\widetilde{x}=\mathtt{false}\land\varphi^{(0)}\mid(F\,\widetilde{x}=\varphi)\in D\}.$

For $F^{(0)}$ above, we use $\mathtt{false}\land\varphi^{(0)}$ rather than $\mathtt{false}$ , in order to keep the form of Equation 1. By the technique in [17, Appendix B.1], we can show that

\mathop{[\![}(D,\varphi_{0})\mathop{]\!]}=\sqcup_{\tau}\{\mathop{[\![}(D^{(m)},\varphi_{0}^{(m)})\mathop{]\!]}\mid m\in\mathbb{N}\}.

An equation system $(\Theta,D,\varphi_{0})$ is called recursion free if there is no cyclic dependency on $D$ . More precisely, we define a binary relation $\succ$ on $\mathit{dom}(\Theta)$ as follows: $F\succ F^{\prime}$ iff $F^{\prime}\in\mathrm{FV}^{\prime}(\varphi)$ where $(F\widetilde{x}=\varphi)\in D$ and $\mathrm{FV}^{\prime}(\varphi)$ is defined by the following:

	$\displaystyle\mathrm{FV}^{\prime}(x)$	$\displaystyle=\{x\},$
	$\displaystyle\mathrm{FV}^{\prime}(\varphi_{1}\lor\varphi_{2})$	$\displaystyle=\mathrm{FV}^{\prime}(\varphi_{1})\cup\mathrm{FV}^{\prime}(\varphi_{2}),$
	$\displaystyle\mathrm{FV}^{\prime}(e_{1}\leq e_{2}\land\varphi)$	$\displaystyle=\begin{cases}\emptyset&(e_{1}\leq e_{2}=\mathtt{false})\\ \mathrm{FV}^{\prime}(\varphi)&(e_{1}\leq e_{2}\neq\mathtt{false})\end{cases},$
	$\displaystyle\mathrm{FV}^{\prime}(\varphi_{1}\,\varphi_{2})$	$\displaystyle=\mathrm{FV}^{\prime}(\varphi_{1})\cup\mathrm{FV}^{\prime}(\varphi_{2}),$
	$\displaystyle\mathrm{FV}^{\prime}(\varphi\,e)$	$\displaystyle=\mathrm{FV}^{\prime}(\varphi).$

Then $D$ is recursion free if the transitive closure $\succ^{*}$ of $\succ$ is irreflexive (i.e., $F\succ^{*}F$ for no $F\in\mathit{dom}(\Theta)$ ). Clearly $(D^{(m)},\varphi_{0}^{(m)})$ is recursion-free.

Now, since our translation is compositional, we can easily show the following:

Lemma 4.7

If $(D^{(m)},(S\,\lambda\widetilde{z}.\mathtt{true})^{(m)})\leadsto(D_{m},\varphi_{m})$ , then $\mathop{[\![}(D_{m},\varphi_{m})\mathop{]\!]}=\mathop{[\![}(D^{\prime(m)},(\exists\widetilde{z}.S_{1}\,\widetilde{z})^{(m)})\mathop{]\!]}$ .

Then we can reduce the proof of Theorem 4.6 to the recursion-free case as follows. Let $(D,S\,\lambda\widetilde{z}.\mathtt{true})\leadsto(D^{\prime},\exists\widetilde{z}.S_{1}\,\widetilde{z})$ and $(D^{(m)},(S\,\lambda\widetilde{z}.\mathtt{true})^{(m)})\leadsto(D_{m},\varphi_{m})$ ; then

	$\displaystyle\mathop{[\![}(D,S\,\lambda\widetilde{z}.\mathtt{true})\mathop{]\!]}$	$\displaystyle=\sqcup_{\star}\{\mathop{[\![}(D^{(m)},(S\,\lambda\widetilde{z}.\mathtt{true})^{(m)})\mathop{]\!]}\mid m\in\mathbb{N}\}$
		$\displaystyle=\sqcup_{\star}\{\mathop{[\![}(D_{m},\varphi_{m})\mathop{]\!]}\mid m\in\mathbb{N}\}$
		$\displaystyle=\sqcup_{\star}\{\mathop{[\![}(D^{\prime(m)},(\exists\widetilde{z}.S_{1}\,\widetilde{z})^{(m)})\mathop{]\!]}\mid m\in\mathbb{N}\}$
		$\displaystyle=\mathop{[\![}(D^{\prime},\exists\widetilde{z}.S_{1}\,\widetilde{z})\mathop{]\!]}$

where for the second equation we assume the recursion-free case.

4.3.2 Reduction Relation with Explicit Substitution

In our proof of the recursion-free case, we show a subject reduction property. To this end, we modify the reduction strategy by using explicit substitution, keeping the adequacy for the semantics. For this modification, we first extend the syntax of formulas as follows:

	$\displaystyle\varphi::=$	$\displaystyle x\mid\varphi_{1}\lor\varphi_{2}\mid e_{1}\leq e_{2}\land\varphi\mid\varphi_{1}\varphi_{2}\mid\varphi\,e$		(2)
	$\displaystyle\mid$	$\displaystyle\{\varphi_{1}/x_{1},\dots,\varphi_{m}/x_{m}\}\varphi$		(2)

Here $\{\varphi_{1}/x_{1},\dots,\varphi_{m}/x_{m}\}\varphi$ is called an explicit substitution, and limited to ground types as follows:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash_{\mathtt{ST}}\varphi_{i}:\mathtt{Int}^{M}\to\star\quad(i=1,\dots,m)\\ \mathcal{K},x_{1}\mathbin{:}\mathtt{Int}^{M}\to\star,\dots,x_{m}\mathbin{:}\mathtt{Int}^{M}\to\star\vdash_{\mathtt{ST}}\varphi:\star\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K}\vdash_{\mathtt{ST}}\{\varphi_{1}/x_{1},\dots,\varphi_{m}/x_{m}\}\varphi:\star\end{array}}$ (T-ESub)

Its meaning is given through

(D,\{\varphi_{1}/x_{1},\dots,\varphi_{m}/x_{m}\}\varphi)^{\mu}:=(D,[\varphi_{1}/x_{1},\dots,\varphi_{m}/x_{m}]\varphi)^{\mu}.

Thus explicit substitution has the same meaning as ordinary substitution, but delays substitution until we need $\varphi_{i}$ for further reduction. As in the definition of $\longrightarrow_{D}$ below, while we use ordinary substitutions for $\beta$ -redex to which we can apply Tr-App and Tr-AppI, we use explicit substitution for those corresponding to Tr-AppG because, the argument after the translation by Tr-AppG is never substituted.

We extend the translation by adding the following rule for explicit substitutions:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mspace{10.0mu}\begin{aligned} &\mathcal{K};\,\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\xi_{i}:{\mathtt{Int}}^{M}{\to}\star\leadsto(\xi_{i,*},\xi_{i,0},\ldots,\xi_{i,k})\mspace{-100.0mu}\\ &&(i=1,\dots,m)&\\ &\mathcal{K};\,\widetilde{x}_{1,\ldots,k},\,\widetilde{x^{\prime}}_{1,\dots,m}\vdash_{\Theta}\varphi:\star\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{k+m})\mspace{-100.0mu}\\ &\psi_{j}=\lambda\widetilde{w}_{1,\ldots,M}.\,\varphi_{j}\,\widetilde{w}\lor\textstyle\bigvee_{i=1}^{m}\exists\widetilde{u}_{1,\ldots,M}.\big{(}\varphi_{k+i}\,\widetilde{u}\land\xi_{i,j}\,\widetilde{u}\,\widetilde{w}\big{)}\mspace{-100.0mu}\\ &&(j=*,0,\dots,k)&\end{aligned}\mspace{-10.0mu}\end{array}}{\begin{array}[]{@{}c@{}}\mathcal{K};\,\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\{\xi_{1}/x^{\prime}_{1},\dots,\xi_{m}/x^{\prime}_{m}\}\varphi:\star\leadsto(\psi_{*},\psi_{0},\ldots,\psi_{k})\end{array}}$ (Tr-ESub)

In the rest of this section, by a formula we mean a formula that may contain extended substitutions, except for formulas in an equation system and except for the case where we explain explicitly. Note that output formulas of the extended translation never contain explicit substitutions.

Let $(\Theta,D,S\,\lambda\widetilde{z}.\mathtt{true})$ be an equation system. For decomposing actual arguments $\alpha_{1},\dots,\alpha_{m}$ of a function $F\in\mathit{dom}(\Theta)$ —recall that $\alpha_{i}$ ranges over formulas and integer expressions—we define $\mathtt{decompArg}(\alpha_{1},\dots,\alpha_{m^{\prime}},\Theta(F))$ in the same way as $\mathtt{decomparg}$ as follows:

	$\displaystyle\mathtt{decompArg}(\epsilon,\star)=(\epsilon,\epsilon,\epsilon)$
	$\displaystyle\mathtt{decompArg}(\alpha\cdot\widetilde{\beta},\kappa\to\tau)=$
	$\displaystyle\left\{\begin{array}[]{ll}(\alpha\cdot\widetilde{\varphi},\widetilde{\psi},\widetilde{e})&\mbox{if $\mathtt{decompArg}(\widetilde{\beta},\tau)=(\widetilde{\varphi},\widetilde{\psi},\widetilde{e}),\widetilde{\varphi}\neq\epsilon$}\\ (\alpha,\widetilde{\psi},\widetilde{e})&\mbox{if $\mathtt{ord}(\kappa)>0,\mathtt{decompArg}(\widetilde{\beta},\tau)=(\epsilon,\widetilde{\psi},\widetilde{e})$}\\ (\epsilon,\alpha\cdot\widetilde{\psi},\widetilde{e})&\mbox{if $\kappa=\mathtt{Int}^{M}\to\star$,}\\ &\ \mbox{$\mathtt{decompArg}(\widetilde{\beta},\tau)=(\epsilon,\widetilde{\psi},\widetilde{e})$}\\ (\epsilon,\widetilde{\psi},\alpha\cdot\widetilde{e})&\mbox{if $\kappa=\mathtt{Int},\mathtt{decompArg}(\widetilde{\beta},\tau)=(\epsilon,\widetilde{\psi},\widetilde{e})$}\end{array}\right.$

Now we define the modified reduction relation $\longrightarrow_{D}$ for a formula $\varphi$ such that $\Theta,x_{1}\mathbin{:}\mathtt{Int}^{M}{\to}\star,\ldots,x_{k}\mathbin{:}\mathtt{Int}^{M}{\to}\star\vdash_{\mathtt{ST}}\varphi:\star$ holds for some $x_{1},\ldots,x_{k}$ . We define the set of evaluation contexts by:

E::=[\,]\mid E\lor\varphi\mid\varphi\lor E\mid\{\varphi_{1}/x_{1},\dots,\varphi_{m}/x_{m}\}E.

Then $\longrightarrow_{D}$ is defined by the following rules:

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathop{[\![}\vdash_{\mathtt{ST}}e_{1}:\mathtt{Int}\mathop{]\!]}>\mathop{[\![}\vdash_{\mathtt{ST}}e_{2}:\mathtt{Int}\mathop{]\!]}\quad\quad(e_{1}\leq e_{2})\neq\mathtt{false}\end{array}}{\begin{array}[]{@{}c@{}}E[e_{1}\leq e_{2}\land\varphi]\longrightarrow_{D}E[\mathtt{false}\land\varphi]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\mathop{[\![}\vdash_{\mathtt{ST}}e_{1}:\mathtt{Int}\mathop{]\!]}\leq\mathop{[\![}\vdash_{\mathtt{ST}}e_{2}:\mathtt{Int}\mathop{]\!]}\end{array}}{\begin{array}[]{@{}c@{}}E[e_{1}\leq e_{2}\land\varphi]\longrightarrow_{D}E[\varphi]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}(F\,w_{1}\,\cdots\,w_{m}=\varphi)\in D\\ \mathtt{decompArg}(\alpha_{1},\cdots,\alpha_{m},\Theta(F))=(\widetilde{\varphi},\widetilde{\psi},\widetilde{e})\\ \mathtt{decomparg}(w_{1},\cdots,w_{m},\Theta(F))=(\widetilde{y}\mathbin{:}\widetilde{\kappa},\widetilde{x},\widetilde{z})\\ \widetilde{x}\text{ do not occur in }E[F\,\alpha_{1}\,\cdots\,\alpha_{m}]\end{array}}{\begin{array}[]{@{}c@{}}E[F\,\alpha_{1}\,\cdots\,\alpha_{m}]\longrightarrow_{D}E[\{\widetilde{\psi}/\widetilde{x}\}[\widetilde{e}/\widetilde{z}][\widetilde{\varphi}/\widetilde{y}]\varphi]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}E[\{\widetilde{\varphi}/\widetilde{x}\}(x_{i}\,\widetilde{e})]\longrightarrow_{D}E[\varphi_{i}\,\widetilde{e}]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}x\notin\{x_{1},\dots,x_{|\widetilde{x}|}\}\cup\mathit{dom}(\Theta)\end{array}}{\begin{array}[]{@{}c@{}}E[\{\widetilde{\varphi}/\widetilde{x}\}(x\,\widetilde{e})]\longrightarrow_{D}E[x\,\widetilde{e}]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}E[\{\widetilde{\varphi}/\widetilde{x}\}(\psi_{1}\lor\psi_{2})]\longrightarrow_{D}E[(\{\widetilde{\varphi}/\widetilde{x}\}\psi_{1})\lor(\{\widetilde{\varphi}/\widetilde{x}\}\psi_{2})]\end{array}}$

$\displaystyle\frac{\begin{array}[]{@{}c@{}}\end{array}}{\begin{array}[]{@{}c@{}}E[\{\widetilde{\varphi}/\widetilde{x}\}(\mathtt{false}\land\varphi)]\longrightarrow_{D}E[\mathtt{false}\land(\{\widetilde{\varphi}/\widetilde{x}\}\varphi)]\end{array}}$

Note that the above reduction preserves the form of (2) and hence the applicability of the translation $\leadsto$ . For any $\varphi$ , $\varphi$ is a normal form with respect to $\longrightarrow_{D}$ iff $\varphi$ is generated by:

\zeta::=x\,\widetilde{e}\ (x\notin\mathit{dom}(\Theta))\mid\mathtt{false}\land\varphi\mid\zeta\lor\zeta.

(3)

Clearly we have:

Lemma 4.8

If $\varphi\longrightarrow_{D}\psi$ , then $\mathop{[\![}(D,\varphi)\mathop{]\!]}=\mathop{[\![}(D,\psi)\mathop{]\!]}$ .

4.3.3 Correctness in the Recursion-free Case

It remains to show the correctness in the recursion-free case, which follows from the subject reduction property below. For a type $\tau=\kappa_{1}\to\cdots\to\kappa_{n}\to\tau^{\prime}$ , we write ${\tau}^{@n}$ for $\tau^{\prime}$ .

Lemma 4.9 (subject reduction)

Suppose that we have $(D,S\,\lambda\widetilde{z}.\mathtt{true})\leadsto(D^{\prime},\exists\widetilde{z}.S_{1}\,\widetilde{z})$ . If $\varphi\longrightarrow_{D}\psi$ and

\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi:\star\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{k}),

then there exist $\psi_{0},\ldots,\psi_{k+1}$ such that

\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\psi:\star\leadsto(\psi_{*},\psi_{0},\ldots,\psi_{k})

and $\varphi_{i}=_{D^{\prime}}\psi_{i}$ for each $i\in\{*,0,\ldots,k\}$ .

As the proof of the above lemma is quite technical and long, we defer it to Appendix A.

The following lemma states the correctness in the recursion-free case, from which Theorem 4.6 follows.

Lemma 4.10

Suppose that $(D,S\,\lambda\widetilde{z}_{1,\ldots,M}.\mathtt{true})$ is a recursion-free equation system. If $(D,S\,\lambda\widetilde{z}_{1,\ldots,M}.\mathtt{true})\leadsto(D^{\prime},\exists\widetilde{z}.\,S_{1}\,\widetilde{z})$ , then $\mathop{[\![}(D,S\,\lambda\widetilde{z}_{1,\ldots,M}.\mathtt{true})\mathop{]\!]}=\mathop{[\![}(D^{\prime},\exists\widetilde{z}.\,S_{1}\,\widetilde{z})\mathop{]\!]}$ .

Proof 4.11

Let the rule of $S$ be $S\,x=\varphi$ ; then $D^{\prime}$ has the rule $S_{1}=\varphi_{1}$ where $S_{1}$ and $\varphi_{1}$ has type $\mathtt{Int}^{M}\to\star$ . Since $\mathop{[\![}(D,S\,\lambda\widetilde{z}_{1,\ldots,M}.\mathtt{true})\mathop{]\!]}=\mathop{[\![}(D,[\lambda\widetilde{z}_{1,\ldots,M}.\mathtt{true}/x]\varphi)\mathop{]\!]}$ , it suffices to show

\mathop{[\![}(D,[\lambda\widetilde{z}_{1,\ldots,M}.\mathtt{true}/x]\varphi)\mathop{]\!]}=\mathop{[\![}(D^{\prime},\exists\widetilde{z}.\,\varphi_{1}\,\widetilde{z})\mathop{]\!]}.

Since $(D,S\,\lambda\widetilde{z}_{1,\ldots,M}.\mathtt{true})$ is recursion-free, $\varphi$ has a normal form $\zeta$ with respect to $\longrightarrow_{D}$ . We have $\varphi\longrightarrow_{D}^{*}\zeta$ and let $x\vdash_{\Theta}\varphi:\star\leadsto(\varphi_{*},\varphi_{0},\varphi_{1})$ ; then by subject reduction (Lemma 4.9), we have $x\vdash_{\Theta}\zeta:\star\allowbreak\leadsto(\zeta_{*},\zeta_{0},\zeta_{1})$ and $\mathop{[\![}(D^{\prime},\varphi_{i})\mathop{]\!]}=\mathop{[\![}(D^{\prime},\zeta_{i})\mathop{]\!]}$ $(i=*,0,1)$ . Also, we have $\mathop{[\![}(D,\varphi)\mathop{]\!]}=\mathop{[\![}(D,\zeta)\mathop{]\!]}$ by Lemma 4.8, and hence $\mathop{[\![}(D,[\lambda\widetilde{z}_{1,\ldots,M}.\mathtt{true}/x]\varphi)\mathop{]\!]}=\mathop{[\![}(D,[\lambda\widetilde{z}_{1,\ldots,M}.\mathtt{true}/x]\zeta)\mathop{]\!]}$ . Therefore we can assume that $\varphi$ is a normal form without loss of generality.

Then we can directly check $\mathop{[\![}(D,[\lambda\widetilde{z}_{1,\ldots,M}.\mathtt{true}/x]\zeta)\mathop{]\!]}=\mathop{[\![}(D^{\prime},\exists\widetilde{z}.\,\zeta_{1}\,\widetilde{z})\mathop{]\!]}$ by induction on the structure of normal forms (3) in Section 4.3.2.

5 Applications

As mentioned already, the translation from order- $n$ reachability games to order-( $n+1$ ) may-reachability enables us to use automated (un)reachability checkers for solving the reachability game problem, and the translation in the other direction enables us to use, for example, reachability game solvers for non-higher-order programs as a may-reachability checker for order-1 programs.

As a direct application of the former translation, we have applied it to the $\nu$ HFL(Z) solver ReTHFL [13], which is a refinement-type-based validity checker for formulas of $\nu$ HFL(Z), the fragment of HFL(Z) without least fixpoint operators (but with greatest fixpoint operators). The fragment $\nu$ HFL(Z) is dual to $\mu$ HFL(Z), in the sense that, for every closed formula $\varphi$ of type $\star$ of $\mu$ HFL(Z), there exists a $\nu$ HFL(Z) formula $\overline{\varphi}$ such that $\varphi$ is valid if and only if $\overline{\varphi}$ is invalid, and vice versa; $\overline{\varphi}$ is obtained from $\varphi$ by just replacing each logical operator (including fixpoint operators) with its de Morgan dual, and $e_{1}\leq e_{2}$ with $e_{1}>e_{2}$ . Using a refinement type system, ReTHFL reduces the validity of a given $\nu$ HFL(Z) formula in a sound (but incomplete) manner to an extended CHC (constraint Horn clauses) problem, where disjunction is allowed in the head of each clause, and passes the problem to an extended CHC solver called PCSat [18]. For a fragment of $\nu$ HFL(Z) corresponding to disjunctive $\mu$ HFL(Z), however, the reduced problem is actually an ordinary CHC problem, for which more efficient tools [4, 5, 6] can be invoked. Thus, we can use the translation in Section 3 to improve the efficiency of ReTHFL.

From the benchmark suite of ReTHFL [13] (which originates from [12], https://github.com/Hogeyama/hfl-benchmark/tree/master/inputs/hfl/HO-nontermination), we picked the “non-termination” benchmark set, which consists of formulas obtained from non-termination verification of higher-order programs. All the formulas in that benchmark set do not belong to (the dual of) disjunctive $\mu$ HFL(Z) (in contrast, the problems in the other benchmark sets belong to disjunctive $\mu$ HFL(Z), hence our translation is not required). We have implemented the translation in Section 3, applied it to the problems in the “non-termination” benchmark set, and then ran ReTHFL with a CHC solver HoIce [6, 19] as the back-end solver. We have compared the result with plain ReTHFL (without the transformation), which uses the extended CHC solver PCSat.

Table 1: Experimental results. Times are in seconds, with the timeout of 180 seconds.

input	ReTHFL	ReTHFL+i.s.	ReTHFL+ tr.
fixpoint_nonterm	11.579	0.054	0.102
unfoldr_nonterm	timeout	unknown	4.22
indirect_e	16.832	0.035	0.066
alternate	unknown	unknown	unknown
fib_CPS_nonterm	timeout	0.047	0.075
foldr_nonterm	8.447	unknown	0.122
passing_cond	116.423	unknown	0.444
indirectHO_e	11.582	0.044	0.073
inf_closure	timeout	20.171	9.080
loopHO	timeout	0.026	0.121

The results are summarized in Table 1. The column ’ReTHFL’ shows the result of plain ReTHFL with PCSat as the back-end extended CHC solver (since ordinary CHC solvers are inapplicable to this benchmark set, as explained above). The column ’ReTHFL+i.s.’ show the result of ReTHFL where the subtyping relation has been replaced by the imprecise one (equivalent to that of Horus [14], a HoCHC solver that can also be viewed as a $\nu$ HFL(Z) solver) so that the type checking problem is reduced to ordinary CHC solving. The column ’ReTHFL+tr.’ shows the result of ReTHFL with our translation. In both ’ReTHFL+i.s.’ and ’ReTHFL+tr.’, HoIce was used as the back-end CHC solver. The entry “unknown” indicates that the solver terminated with the answer “ill-typed”, in which case, we do not know whether the formula is valid or invalid, due to the incompleteness of the underlying refinement type system.⁵⁵5Although the understanding of the refinement type systems ReTHFL is not required below, interested readers may wish to consult [13]. The refinement type system used in ’ReTHFL+i.s.’ is less precise than the one used in ReTHFL; hence, it returns more unknowns. As clear from the table, our translation significantly improved the efficiency of ReTHFL.

The translation in the other direction given in Section 4 also helps ReTHFL, especially for relaxing the limitation caused by the incompleteness of the underlying refinement type system. For example, consider the formula $S\,\mathtt{true}$ , where:

\displaystyle S\,t

\displaystyle=_{\mu}\mathit{App}\,(\lambda x.x\neq 0\land t)\,0\qquad\mathit{App}\,p\,y=_{\mu}p\,y\lor\mathit{App}\,(\lambda z.p(z-1))\,(y+1).

The formula is invalid, but ReTHFL (nor Horus [14], a higher-order CHC solver based on a refinement type system) cannot prove the validity of the dual formula, due to the incompleteness of the refinement type system (which is related to the incompleteness of a refinement type system addressed by [20] by inserting extra arguments). The translation in Section 4 yields the following order-0 formula:⁶⁶6We have implemented a prototype translator, but have not yet integrated it into ReTHFL. For readability, here we show the formula obtained by some manual simplification of the automatically generated formula.

	$\displaystyle S_{1}=_{\mu}\exists x.\mathit{App}_{1}\,0\,x\land x\neq 0$
	$\displaystyle\mathit{App}_{1}\,y\,z=_{\mu}y=z\lor\exists w.\mathit{App}_{1}\,(y+1)\,w\land w-1=z.$

Here, $\mathit{App}_{1}\,y\,z$ intuitively means that $\mathit{App}\,p\,y$ can be reduced to $p\,z$ . The underlying type system of ReTHFL is complete for order-0 formulas, and indeed, the order-0 formula above can automatically be proved invalid by ReTHFL.

6 Related Work

The relationship between order- $n$ reachability games and order-( $n+1$ ) may-reachability has some deep connection to the relationship between order- $n$ tree languages and order-( $n+1)$ word languages [21, 22, 23], intuitively because the may-reachability problem is concerned about the set of “paths” of the execution tree of a given program, whereas the reachability game problem is also concerned about the branching structures of the execution tree. Indeed, our translations (especially, the use of $\varphi_{*}$ and $\varphi_{0}$ components in the translation in Section 4) have been inspired by Asada and Kobayashi’s translations between tree and word languages [23]. Kobayashi et al. [24] have also used a similar idea for a characterization of termination probabilities of higher-order probabilistic programs.

For finite-data programs (programs in Section 2.3 without integers), according to the complexity results on HORS model checking [25, 26], both the order- $n$ reachability game problem and the order-( $n+1$ ) may-reachability game problem are $n$ -EXPTIME complete, which imply that there are mutual translations between them. Concrete translations have, however, not been given (except unnatural translations through Turing machines). Also, the complexity-theoretic argument for the existence of translations does not apply in the presence of integers.

For HORS model checking, Parys [27] developed an order-decreasing transformation for higher-order grammars, which shares some ideas with our translation in Section 4. The details of the translations are however quite different. His translation makes use of finiteness in a crucial manner, and is not applicable in the presence of integers. Also, his translation is not size-preserving.

For order-1 programs, Kobayashi et al. [16] have shown that linear-time omega regular properties can be translated to order-0 HFL(Z) formulas. Our translation in Section 4 may be viewed as a higher-order extension of their translation, while the properties are restricted to may-reachability.

The fragment $\mu$ HFL(Z) (or its dual fragment $\nu$ HFL(Z)) is essentially (modulo the restriction of data domains to integers) equivalent to HoCHC [14], a higher-order extension of CHC. Therefore, the result of this paper should be useful also for improving HoCHC solvers.

7 Conclusion

We have shown translations between order- $n$ reachability games and order-( $n+1$ ) may-reachability, and proved their correctness. We have applied the translations to higher-order program verification, and obtained promising results in preliminary experiments. As mentioned in Section 6, our results are closely related to the correspondence between higher-order word and tree languages [23]. A deeper investigation of the relationship and generalization of the translations that subsume the related translations [23, 24] are left for future work.

Acknowledgments

We would like to thank anonymous referees for useful comments. This work was supported by JSPS KAKENHI Grant Number JP20H05703, JP24K14814 and JST SPRING Grant Number JPMJSP2108.

References

[1] Grädel E, Thomas W, Wilke T (eds.). Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002.
[2] Kobayashi N, Sato R, Unno H. Predicate Abstraction and CEGAR for Higher-Order Model Checking. In: PLDI 2011. ACM Press, 2011 pp. 222–233.
[3] Rondon PM, Kawaguchi M, Jhala R. Liquid types. In: PLDI 2008. 2008 pp. 159–169.
[4] Komuravelli A, Gurfinkel A, Chaki S. SMT-based model checking for recursive programs. Formal Methods Syst. Des., 2016. 48(3):175–205. URL https://doi.org/10.1007/s10703-016-0249-4.
[5] Hojjat H, Rümmer P. The ELDARICA Horn Solver. In: 2018 Formal Methods in Computer Aided Design (FMCAD). 2018 pp. 1–7.
[6] Champion A, Chiba T, Kobayashi N, Sato R. ICE-Based Refinement Type Discovery for Higher-Order Functional Programs. J. Autom. Reason., 2020. 64(7):1393–1418. URL https://doi.org/10.1007/s10817-020-09571-y.
[7] Kobayashi N, Tsukada T, Watanabe K. Higher-Order Program Verification via HFL Model Checking. In: Ahmed A (ed.), Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, volume 10801 of Lecture Notes in Computer Science. Springer, 2018 pp. 711–738. 10.1007/978-3-319-89884-1_25.
[8] Viswanathan M, Viswanathan R. A Higher Order Modal Fixed Point Logic. In: CONCUR, volume 3170 of LNCS. Springer, 2004 pp. 512–528.
[9] Watanabe K, Tsukada T, Oshikawa H, Kobayashi N. Reduction from branching-time property verification of higher-order programs to HFL validity checking. In: Hermenegildo MV, Igarashi A (eds.), Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM@POPL 2019, Cascais, Portugal, January 14-15, 2019. ACM, 2019 pp. 22–34. 10.1145/3294032.3294077.
[10] Asada K, Katsura H, Kobayashi N. On Higher-Order Reachability Games Vs May Reachability. In: Lin AW, Zetzsche G, Potapov I (eds.), Reachability Problems - 16th International Conference, RP 2022, Kaiserslautern, Germany, October 17-21, 2022, Proceedings, volume 13608 of Lecture Notes in Computer Science. Springer, 2022 pp. 108–124. 10.1007/978-3-031-19135-0_8. URL https://doi.org/10.1007/978-3-031-19135-0_8.
[11] Tsukada T. On Computability of Logical Approaches to Branching-Time Property Verification of Programs. In: Hermanns H, Zhang L, Kobayashi N, Miller D (eds.), LICS ’20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020. ACM, 2020 pp. 886–899. 10.1145/3373718.3394766.
[12] Iwayama N, Kobayashi N, Suzuki R, Tsukada T. Predicate Abstraction and CEGAR for $\nu$ HFL_Z Validity Checking. In: Pichardie D, Sighireanu M (eds.), Static Analysis - 27th International Symposium, SAS 2020, Virtual Event, November 18-20, 2020, Proceedings, volume 12389 of Lecture Notes in Computer Science. Springer, 2020 pp. 134–155. 10.1007/978-3-030-65474-0_7.
[13] Katsura H, Iwayama N, Kobayashi N, Tsukada T. A New Refinement Type System for Automated $\nu$ HFL_Z Validity Checking. In: d S Oliveira BC (ed.), Programming Languages and Systems - 18th Asian Symposium, APLAS 2020, Fukuoka, Japan, November 30 - December 2, 2020, Proceedings, volume 12470 of Lecture Notes in Computer Science. Springer, 2020 pp. 86–104. 10.1007/978-3-030-64437-6_5.
[14] Burn TC, Ong CL, Ramsay SJ. Higher-order constrained Horn clauses for verification. Proc. ACM Program. Lang., 2018. 2(POPL):11:1–11:28. 10.1145/3158099.
[15] Cousot P, Cousot R. Constructive Versions of Tarski’s Fixed Point Theorems. Pacific Journal of Mathematics, 1979. 81(1):43–57.
[16] Kobayashi N, Nishikawa T, Igarashi A, Unno H. Temporal Verification of Programs via First-Order Fixpoint Logic. In: Chang BE (ed.), Static Analysis - 26th International Symposium, SAS 2019, Porto, Portugal, October 8-11, 2019, Proceedings, volume 11822 of Lecture Notes in Computer Science. Springer, 2019 pp. 413–436. 10.1007/978-3-030-32304-2_20.
[17] Kobayashi N, Tsukada T, Watanabe K. Higher-Order Program Verification via HFL Model Checking. CoRR, 2017. abs/1710.08614. A short version appeared in Proceedings of ESOP 2018.
[18] Satake Y, Unno H, Yanagi H. Probabilistic Inference for Predicate Constraint Satisfaction. In: The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020. AAAI Press, 2020 pp. 1644–1651.
[19] Champion A, Kobayashi N, Sato R. HoIce: An ICE-Based Non-linear Horn Clause Solver. In: Ryu S (ed.), Programming Languages and Systems - 16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2-6, 2018, Proceedings, volume 11275 of Lecture Notes in Computer Science. Springer, 2018 pp. 146–156. 10.1007/978-3-030-02768-1_8.
[20] Unno H, Satake Y, Terauchi T. Relatively complete refinement type system for verification of higher-order non-deterministic programs. Proc. ACM Program. Lang., 2018. 2(POPL):12:1–12:29. 10.1145/3158100.
[21] Damm W. The IO- and OI-Hierarchies. Theor. Comput. Sci., 1982. 20:95–207.
[22] Asada K, Kobayashi N. On Word and Frontier Languages of Unsafe Higher-Order Grammars. In: Chatzigiannakis I, Mitzenmacher M, Rabani Y, Sangiorgi D (eds.), 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy, volume 55 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. ISBN 978-3-95977-013-2, 2016 pp. 111:1–111:13. 10.4230/LIPIcs.ICALP.2016.111.
[23] Asada K, Kobayashi N. Size-Preserving Translations from Order-(n+1) Word Grammars to Order-n Tree Grammars. In: Ariola ZM (ed.), 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29-July 6, 2020, Paris, France (Virtual Conference), volume 167 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020 pp. 22:1–22:22. 10.4230/LIPIcs.FSCD.2020.22.
[24] Kobayashi N, Dal Lago U, Grellois C. On the Termination Problem for Probabilistic Higher-Order Recursive Programs. In: Proceedings of LICS 2019. IEEE, 2019 .
[25] Ong CHL. On Model-Checking Trees Generated by Higher-Order Recursion Schemes. In: LICS 2006. IEEE Computer Society Press, 2006 pp. 81–90.
[26] Kobayashi N, Ong CHL. Complexity of Model Checking Recursion Schemes for Fragments of the Modal Mu-Calculus. LMCS, 2011. 7(4).
[27] Parys P. Higher-Order Model Checking Step by Step. In: Bansal N, Merelli E, Worrell J (eds.), 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, July 12-16, 2021, Glasgow, Scotland (Virtual Conference), volume 198 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021 pp. 140:1–140:16. 10.4230/LIPIcs.ICALP.2021.140.

Appendix

Appendix A Proof of Lemma 4.9

We first prepare two substitution lemmas that correspond to the application rules Tr-App and Tr-AppI.

The following is the substitution lemma corresponding to Tr-AppI:

Lemma A.1 (Substitution lemma (integer))

Let $\varphi$ be a formula that does not contain an explicit substitution, $e$ be a closed integer expression, and

\mathcal{K},\,z\mathbin{:}\mathtt{Int};\,\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi:\tau\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{k+m}).

where $m=\mathtt{gar}(\tau)$ . Then we have

\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}[e/z]\varphi:\tau\leadsto([e/z]\varphi_{*},[e/z]\varphi_{0},\ldots,[e/z]\varphi_{k+m}).

Proof A.2

By straightforward induction on $\varphi$ .

Next we show the substitution lemma corresponding to Tr-App. First we prepare some definitions and a lemma.

For a formula $\varphi$ , we write ${\rm ChineseAstron.Astrophys.}{\varphi}{k}{m}$ for $(\varphi_{0},\varphi_{k+1},\dots,\varphi_{k+m})$ . Note that the translation result of $\varphi\,\psi$ in Tr-App in Figure 3 can be written as the following:

	$\displaystyle\big{(}\varphi_{}(\psi_{},{\rm ChineseAstron.Astrophys.}{\psi}{k}{m^{\prime}}),\,\varphi_{0}(\psi_{0},{\rm ChineseAstron.Astrophys.}{\psi}{k}{m^{\prime}}),\,$	$\displaystyle\varphi_{1}(\psi_{1},{\rm ChineseAstron.Astrophys.}{\psi}{k}{m^{\prime}}),$	$\displaystyle\ldots,\,$	$\displaystyle\varphi_{k}(\psi_{k},{\rm ChineseAstron.Astrophys.}{\psi}{k}{m^{\prime}})$	,
		$\displaystyle\varphi_{k+1}({\rm ChineseAstron.Astrophys.}{\psi}{k}{m^{\prime}}),$	$\displaystyle\ldots,\,$	$\displaystyle\varphi_{k+m}({\rm ChineseAstron.Astrophys.}{\psi}{k}{m^{\prime}})$	$\displaystyle\big{)}$

The following can be shown easily by induction on $\varphi$ .

Lemma A.3 (weakening)

\displaystyle\mathcal{K};\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi:\tau\leadsto(\varphi_{*},\varphi_{0},\varphi_{1},\ldots,\varphi_{k},\varphi_{k+1},\ldots,\varphi_{k+m})

then

\displaystyle\mathcal{K};\widetilde{x}_{1,\ldots,k},x\vdash_{\Theta}\varphi:\tau\leadsto(\varphi_{*},\varphi_{0},\varphi_{1},\ldots,\varphi_{k},\varphi_{0},\varphi_{k+1},\ldots,\varphi_{k+m}).

Now we show the substitution lemma. Here we consider simultaneous substitution, because we cannot apply this lemma repeatedly since $[\widetilde{\psi}/\widetilde{y}]\varphi$ below may contain an explicit substitution.

Lemma A.4 (Substitution lemma (higher-order))

Let $\varphi$ be a formula that does not contain an explicit substitution, and

	$\displaystyle\widetilde{y}_{1,\dots,q}\mathbin{:}\widetilde{\kappa};\ \widetilde{x^{\prime}}_{1,\dots,m}\vdash_{\Theta}\varphi:\tau\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{m+\mathtt{gar}(\tau)})$
	$\displaystyle m^{\prime}_{i}=\mathtt{gar}(\kappa_{i})\quad\mathtt{decomp}(\kappa_{i})=(\widetilde{\kappa_{i}},m^{\prime}_{i},p_{i})\quad(i=1,\dots,q)$
	$\displaystyle\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\psi_{i}:\kappa_{i}\leadsto(\psi_{i,*},\psi_{i,0},\dots,\psi_{i,k+m^{\prime}_{i}})\quad(i=1,\dots,q)$
	$\displaystyle\widetilde{y}_{i}=(y_{i,*},y_{i,0},\dots,y_{i,\mathtt{gar}(\kappa_{i})})\qquad\widetilde{y}^{\circ}_{i}=(y_{i,0},\dots,y_{i,\mathtt{gar}(\kappa_{i})})$
	$\displaystyle\begin{aligned} \theta^{j}&=\big{[}&(\psi_{i,j},{\rm ChineseAstron.Astrophys.}{\psi_{i}}{k}{m^{\prime}_{i}})/\widetilde{y}_{i}&\big{]}_{i=1}^{q}\qquad&&(j=*,0,\dots,k)\\ \theta^{\circ}&=\big{[}&{\rm ChineseAstron.Astrophys.}{\psi_{i}}{k}{m^{\prime}_{i}}/\widetilde{y}^{\circ}_{i}&\big{]}_{i=1}^{q}\end{aligned}$
	$\displaystyle\widetilde{x}_{1,\ldots,k},\widetilde{x^{\prime}}_{1,\dots,m}\vdash_{\Theta}[\widetilde{\psi}/\widetilde{y}]\varphi:\tau\leadsto(\varphi^{\circ}_{*},\varphi^{\circ}_{0},\dots,\varphi^{\circ}_{k+m+\mathtt{gar}(\tau)}).$

Then we have:

1.

$\theta^{0}\varphi_{*}=\theta^{0}\varphi_{0}$ .
2.

$\mspace{-20.0mu}\begin{aligned} t]{20}(&\varphi^{\circ}_{*}&&,\varphi^{\circ}_{0}&&,\varphi^{\circ}_{1}&&,\dots&&,\varphi^{\circ}_{k}&&,\varphi^{\circ}_{k+1}&&,\dots&&,\varphi^{\circ}_{k+m+\mathtt{gar}(\tau)}&&)\\ =_{D^{\prime}}(&\theta^{*}\varphi_{*}&&,\theta^{0}\varphi_{*}&&,\theta^{1}\varphi_{*}&&,\ldots&&,\theta^{k}\varphi_{*}&&,\theta^{\circ}\varphi_{1}&&,\ldots&&,\theta^{\circ}\varphi_{m+\mathtt{gar}(\tau)}&&).\end{aligned}$

Proof A.5

We can show Item 1 easily by induction on $\varphi$ and case analysis on the last rule used for the derivation $\widetilde{y}_{1,\dots,q}\mathbin{:}\widetilde{\kappa};\ \widetilde{x^{\prime}}_{1,\dots,m}\vdash_{\Theta}\varphi:\tau\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{m+\mathtt{gar}(\tau)})$ . We show Item 2 by the same induction and case analysis. Basically the proof is straightforward, where we use the latter part of Lemma 4.4. Here we show only the cases of Tr-Var and Tr-App; in the latter case, we use Item 1.

$\bullet$ Case of Tr-Var: Let the last rule be the following, where $i\in\{1,\dots,q\}$ :

\begin{aligned} &\widetilde{y}\mathbin{:}\widetilde{\kappa};\widetilde{x^{\prime}}_{1,\dots,m}\vdash_{\Theta}(\varphi=)\ y_{i}:\kappa_{i}\\ &\quad\leadsto\big{(}\begin{aligned} t]{10}&(\varphi_{*}&&,\varphi_{0}&&,\varphi_{1}&&,\ldots&&,\varphi_{m}&&,\varphi_{m+1}&&,\ldots&&,\varphi_{m+\mathtt{gar}(\tau)}&&)=\big{)}\\ &(y_{i,*}&&,y_{i,0}&&,y_{i,0}&&,\ldots&&,y_{i,0}&&,y_{i,1}&&,\ldots&&,y_{i,m^{\prime}_{i}}&&)\end{aligned}\end{aligned}\lx@proof@logical@and\begin{aligned} \end{aligned}\mathtt{decomp}(\kappa_{i})=(\widetilde{\kappa_{i}},m^{\prime}_{i},p_{i}){}$$\par Bytheweakeninglemma(Lemma~{}\ref{lem:weakening}),wehave\begin{aligned} &\widetilde{x}_{1,\ldots,k},\widetilde{x^{\prime}}_{1,\dots,m}\vdash_{\Theta}([\widetilde{\psi}/\widetilde{y}]\varphi=)\ \psi_{i}:\kappa_{i}\leadsto\\ &\begin{aligned} \big{(}&(\varphi^{\circ}_{*}&&,\varphi^{\circ}_{0}&&,\varphi^{\circ}_{1}&&,\dots&&,\varphi^{\circ}_{k}&&,\varphi^{\circ}_{k+1}&&,\dots&&,\varphi^{\circ}_{k+m}&&,\varphi^{\circ}_{k+m+1}&&,\dots&&,\varphi^{\circ}_{k+m+m^{\prime}_{i}}&&)=\big{)}\\ &(\psi_{i,*}&&,\psi_{i,0}&&,\psi_{i,1}&&,\dots&&,\psi_{i,k}&&,\psi_{i,0}&&,\dots&&,\psi_{i,0}&&,\psi_{i,k+1}&&,\dots&&,\psi_{i,k+m^{\prime}_{i}}&&)\end{aligned}\end{aligned}Thenwecanchecktherequiredequationcomponent-wise.\par$\bullet$\ Caseof\mathrm{\mathchoice{\mbox{\sc Tr-App}}{\mbox{\sc Tr-App}}{\mbox{\small\sc Tr-App}}{\mbox{\tiny TR-APP}}}:Letthelastrulebethefollowing:$$\begin{aligned} &\widetilde{y}\mathbin{:}\widetilde{\kappa};\widetilde{x^{\prime}}_{1,\dots,m}\vdash_{\Theta}(\varphi=)\ \varphi^{\prime}\,\psi^{\prime}:\tau\leadsto\\ &\quad\big{(}(\varphi_{*},\varphi_{0},\varphi_{1}\ldots,\varphi_{m},\varphi_{m+1}\ldots,\varphi_{m+\mathtt{gar}(\tau)})=\big{)}\\ &\quad\phantom{\big{(}}\big{(}\varphi^{\prime}_{*}(\psi^{\prime}_{*},{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}}),\,\varphi^{\prime}_{0}(\psi^{\prime}_{0},{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}}),\,\\ &\quad\begin{aligned} \phantom{\big{(}\big{(}}&\varphi^{\prime}_{1}(\psi^{\prime}_{1},{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}}),&&\ldots,\,&&\varphi^{\prime}_{m}(\psi^{\prime}_{m},{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})&&,\\ \phantom{\big{(}\big{(}}&\varphi^{\prime}_{m+1}({\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}}),&&\ldots,\,&&\varphi^{\prime}_{m+m^{\prime}}({\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})&&\big{)}\end{aligned}\end{aligned}\lx@proof@logical@and\begin{aligned} \end{aligned}\mathtt{ord}(\kappa^{\prime}\to\tau)>1\quad\quad\mathtt{gar}(\kappa^{\prime}\to\tau)=m^{\prime}\quad\quad\mathtt{gar}(\kappa^{\prime})=m^{\prime\prime}{\\ }\widetilde{y}\mathbin{:}\widetilde{\kappa};\widetilde{x^{\prime}}_{1,\dots,m}\vdash_{\Theta}\varphi^{\prime}:\kappa^{\prime}\to\tau\leadsto(\varphi^{\prime}_{*},\varphi^{\prime}_{0},\ldots,\varphi^{\prime}_{m+m^{\prime}}){\\ }\widetilde{y}\mathbin{:}\widetilde{\kappa};\widetilde{x^{\prime}}_{1,\dots,m}\vdash_{\Theta}\psi^{\prime}:\kappa^{\prime}\leadsto(\psi^{\prime}_{*},\psi^{\prime}_{0},\ldots,\psi^{\prime}_{m+m^{\prime\prime}}){}$$Herenotethatwehave$\mathtt{gar}(\tau)=\mathtt{gar}(\kappa^{\prime}\to\tau)=m^{\prime}$since$\mathtt{ord}(\kappa^{\prime}\to\tau)>1$.\par Byinductionhypothesis,thereexist$\varphi^{\prime\circ}_{*},\varphi^{\prime\circ}_{0},\dots,\varphi^{\prime\circ}_{k+m+m^{\prime}}$suchthat\begin{aligned} &\widetilde{x}_{1,\ldots,k},\widetilde{x^{\prime}}_{1,\dots,m}\vdash_{\Theta}[\widetilde{\psi}/\widetilde{y}]\varphi^{\prime}:\kappa^{\prime}\to\tau\leadsto\\ &\begin{aligned} (&\varphi^{\prime\circ}_{*}&&,\varphi^{\prime\circ}_{0}&&,\varphi^{\prime\circ}_{1}&&,\dots&&,\varphi^{\prime\circ}_{k}&&,\varphi^{\prime\circ}_{k+1}&&,\dots&&,\varphi^{\prime\circ}_{k+m+m^{\prime}}&&)\\ =_{D^{\prime}}(&\theta^{*}\varphi^{\prime}_{*}&&,\theta^{0}\varphi^{\prime}_{*}&&,\theta^{1}\varphi^{\prime}_{*}&&,\ldots&&,\theta^{k}\varphi^{\prime}_{*}&&,\theta^{\circ}\varphi^{\prime}_{1}&&,\ldots&&,\theta^{\circ}\varphi^{\prime}_{m+m^{\prime}}&&),\end{aligned}\end{aligned}andthereexist$\psi^{\prime\circ}_{*},\psi^{\prime\circ}_{0},\dots,\psi^{\prime\circ}_{k+m+m^{\prime\prime}}$suchthat\begin{aligned} &\widetilde{x}_{1,\ldots,k},\widetilde{x^{\prime}}_{1,\dots,m}\vdash_{\Theta}[\widetilde{\psi}/\widetilde{y}]\psi^{\prime}:\kappa^{\prime}\leadsto\\ &\begin{aligned} (&\psi^{\prime\circ}_{*}&&,\psi^{\prime\circ}_{0}&&,\psi^{\prime\circ}_{1}&&,\dots&&,\psi^{\prime\circ}_{k}&&,\psi^{\prime\circ}_{k+1}&&,\dots&&,\psi^{\prime\circ}_{k+m+m^{\prime\prime}}&&)\\ =_{D^{\prime}}(&\theta^{*}\psi^{\prime}_{*}&&,\theta^{0}\psi^{\prime}_{*}&&,\theta^{1}\psi^{\prime}_{*}&&,\ldots&&,\theta^{k}\psi^{\prime}_{*}&&,\theta^{\circ}\psi^{\prime}_{1}&&,\ldots&&,\theta^{\circ}\psi^{\prime}_{m+m^{\prime\prime}}&&).\end{aligned}\end{aligned}\par Forany$j$and$j^{\prime}\in\{*,0,1,\dots,k,\circ\}$,bythelatterpartofLemma~{}\ref{lem:well-typedAndOccurrence},$\theta^{j}\xi=\theta^{j^{\prime}}\xi$foranyformula$\xi$thatoccursin\begin{aligned} \big{(}\varphi^{\prime}_{0}(\psi^{\prime}_{0},{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}}),\,&\varphi^{\prime}_{1}(\psi^{\prime}_{1},{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})&&,\ldots&&,\,\varphi^{\prime}_{m}(\psi^{\prime}_{m},{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})&&,\\ &\varphi^{\prime}_{m+1}({\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})&&,\ldots&&,\,\varphi^{\prime}_{m+m^{\prime}}({\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})&&\big{)}.\end{aligned}Especially,forany$j\in\{*,0,1,\dots,k,\circ\}$,wehave\begin{aligned} {\rm ChineseAstron.Astrophys.}{\psi^{\prime\circ}}{k+m}{m^{\prime\prime}}=\ &(\psi^{\prime\circ}_{0},\psi^{\prime\circ}_{k+m+1},\dots,\psi^{\prime\circ}_{k+m+m^{\prime\prime}},)\\ =_{D^{\prime}}\ &(\theta^{0}\psi^{\prime}_{*},\theta^{\circ}\psi^{\prime}_{m+1},\ldots,\theta^{\circ}\psi^{\prime}_{m+m^{\prime\prime}})\\ =\ &(\theta^{0}\psi^{\prime}_{0},\theta^{\circ}\psi^{\prime}_{m+1},\ldots,\theta^{\circ}\psi^{\prime}_{m+m^{\prime\prime}})\\ =\ &(\theta^{j}\psi^{\prime}_{0},\theta^{j}\psi^{\prime}_{m+1},\ldots,\theta^{j}\psi^{\prime}_{m+m^{\prime\prime}})=\theta^{j}{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}}.\end{aligned}\par Now,with\mathrm{\mathchoice{\mbox{\sc Tr-App}}{\mbox{\sc Tr-App}}{\mbox{\small\sc Tr-App}}{\mbox{\tiny TR-APP}}},wehave\begin{aligned} &(\varphi^{\circ}_{*},\varphi^{\circ}_{0},\varphi^{\circ}_{1},\dots,\varphi^{\circ}_{k},\varphi^{\circ}_{k+1},\dots,\varphi^{\circ}_{k+m},\varphi^{\circ}_{k+m+1},\dots,\varphi^{\circ}_{k+m+m^{\prime}})\\ =\ &\begin{aligned} \big{(}&\varphi^{\prime\circ}_{*}(\psi^{\prime\circ}_{*},{\rm ChineseAstron.Astrophys.}{\psi^{\prime\circ}}{k+m}{m^{\prime\prime}}),\,\varphi^{\prime\circ}_{0}(\psi^{\prime\circ}_{0},{\rm ChineseAstron.Astrophys.}{\psi^{\prime\circ}}{k+m}{m^{\prime\prime}}),\,\\ &\begin{aligned} t]{10}&\varphi^{\prime\circ}_{1}(\psi^{\prime\circ}_{1},{\rm ChineseAstron.Astrophys.}{\psi^{\prime\circ}}{k+m}{m^{\prime\prime}})&&,\ldots,\,&&\varphi^{\prime\circ}_{k}(\psi^{\prime\circ}_{k},{\rm ChineseAstron.Astrophys.}{\psi^{\prime\circ}}{k+m}{m^{\prime\prime}})&&,\\ &\varphi^{\prime\circ}_{k+1}(\psi^{\prime\circ}_{k+1},{\rm ChineseAstron.Astrophys.}{\psi^{\prime\circ}}{k+m}{m^{\prime\prime}})&&,\ldots,\,&&\varphi^{\prime\circ}_{k+m}(\psi^{\prime\circ}_{k+m},{\rm ChineseAstron.Astrophys.}{\psi^{\prime\circ}}{k+m}{m^{\prime\prime}})&&,\\ &\varphi^{\prime\circ}_{k+m+1}({\rm ChineseAstron.Astrophys.}{\psi^{\prime\circ}}{k+m}{m^{\prime\prime}})&&,\ldots,\,&&\varphi^{\prime\circ}_{k+m+m^{\prime}}({\rm ChineseAstron.Astrophys.}{\psi^{\prime\circ}}{k+m}{m^{\prime\prime}})&&\big{)}\end{aligned}\end{aligned}\\ =_{D^{\prime}}\ &\begin{aligned} \big{(}&\theta^{*}\varphi^{\prime}_{*}(\theta^{*}\psi^{\prime}_{*},\theta^{*}{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}}),\,\theta^{0}\varphi^{\prime}_{*}(\theta^{0}\psi^{\prime}_{*},\theta^{0}{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}}),\,\\ &\begin{aligned} t]{10}&\theta^{1}\varphi^{\prime}_{*}(\theta^{1}\psi^{\prime}_{*},\theta^{1}{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})&&,\ldots,\,&&\theta^{k}\varphi^{\prime}_{*}(\theta^{k}\psi^{\prime}_{*},\theta^{k}{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})&&,\\ &\theta^{\circ}\varphi^{\prime}_{1}(\theta^{\circ}\psi^{\prime}_{1},\theta^{\circ}{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})&&,\ldots,\,&&\theta^{\circ}\varphi^{\prime}_{m}(\theta^{\circ}\psi^{\prime}_{m},\theta^{\circ}{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})&&,\\ &\theta^{\circ}\varphi^{\prime}_{m+1}(\theta^{\circ}{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})&&,\ldots,\,&&\theta^{\circ}\varphi^{\prime}_{m+m^{\prime}}(\theta^{\circ}{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})&&\big{)}\end{aligned}\end{aligned}\\ =\ &\begin{aligned} \big{(}&\theta^{*}\big{(}\varphi^{\prime}_{*}(\psi^{\prime}_{*},{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})\big{)},\,\theta^{0}\big{(}\varphi^{\prime}_{*}(\psi^{\prime}_{*},{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})\big{)},\,\\ &\begin{aligned} t]{10}&\theta^{1}\big{(}\varphi^{\prime}_{*}(\psi^{\prime}_{*},{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})\big{)}&&,\ldots,\,&&\theta^{k}\big{(}\varphi^{\prime}_{*}(\psi^{\prime}_{*},{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})\big{)}&&,\\ &\theta^{\circ}\big{(}\varphi^{\prime}_{1}(\psi^{\prime}_{1},{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})\big{)}&&,\ldots,\,&&\theta^{\circ}\big{(}\varphi^{\prime}_{m}(\psi^{\prime}_{m},{\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})\big{)}&&,\\ &\theta^{\circ}\big{(}\varphi^{\prime}_{m+1}({\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})\big{)}&&,\ldots,\,&&\theta^{\circ}\big{(}\varphi^{\prime}_{m+m^{\prime}}({\rm ChineseAstron.Astrophys.}{\psi^{\prime}}{m}{m^{\prime\prime}})\big{)}&&\big{)}\end{aligned}\end{aligned}\\ =\ &(\theta^{*}\varphi_{*},\theta^{0}\varphi_{*},\theta^{1}\varphi_{*},\ldots,\theta^{k}\varphi_{*},\theta^{\circ}\varphi_{1},\ldots,\theta^{\circ}\varphi_{m+m^{\prime}}),\end{aligned}asrequired.\par\par\par\par\par\end{proof}\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par\par NowwearereadytoproveLemma~{}\ref{lem:subjectReduction}.\trivlist\PRstyle\par\trivlist@item@[]{ProofofLemma~{}\ref{lem:subjectReduction}:}\newline Fortheconvenienceoftheproof,werenamethemetavariables$\varphi,\psi,\varphi_{i},\psi_{i}$with$\varphi^{\prime},\psi^{\prime},\varphi^{\prime}_{i},\psi^{\prime}_{i}$:sowesuppose$\varphi^{\prime}\longrightarrow_{D}\psi^{\prime}$and$\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi^{\prime}:\star\leadsto(\varphi^{\prime}_{*},\varphi^{\prime}_{0},\ldots,\varphi^{\prime}_{k})$,andprovethatwehave$\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\psi^{\prime}:\star\leadsto(\psi^{\prime}_{*},\psi^{\prime}_{0},\ldots,\psi^{\prime}_{k})$and$\varphi^{\prime}_{i}=_{D^{\prime}}\psi^{\prime}_{i}$.Theproofproceedsbyinductionon$\varphi^{\prime}$.\par Let$\varphi^{\prime}$beoftheform$E[\varphi^{\prime\prime}]$where$\varphi^{\prime\prime}$isaredexof$\longrightarrow_{D}$.Thecasewhere$E\neq[\,]$canbeeasilyprovedbyusinginductionhypothesis.Soweconsideronlythecasewhere$E=[\,]$.Thenweperformcaseanalysison$\varphi^{\prime}\longrightarrow_{D}\psi^{\prime}$,butwefocusonlyonthenon-trivialcasewhereweusethesubstitutionlemmas.\par$\bullet$\ Casewhere$\varphi^{\prime}\longrightarrow_{D}\psi^{\prime}$isoftheform$$F\,\alpha_{1}\,\cdots\,\alpha_{h^{\prime}}\longrightarrow_{D}\{\widetilde{\xi}/\widetilde{x^{\prime\prime}}\}[\widetilde{e^{\prime\prime}}/\widetilde{z^{\prime\prime}}][\widetilde{\varphi^{\prime\prime}}/\widetilde{y^{\prime\prime}}]\varphi$$withthefollowingconditions:\begin{aligned} &(F\,\widetilde{w^{\prime}}=\varphi)\in D\\ &\mathtt{decomp}(\Theta(F))=(\widetilde{\kappa^{\prime\prime}}_{1,\dots,h^{\prime\prime}},m,p)\\ &\mathtt{decompArg}(\widetilde{\alpha},\Theta(F))=(\widetilde{\varphi^{\prime\prime}},\widetilde{\xi},\widetilde{e^{\prime\prime}})\\ &\mathtt{decomparg}(\widetilde{w^{\prime}},\Theta(F))=(\widetilde{y^{\prime\prime}}\mathbin{:}\widetilde{\kappa^{\prime\prime}},\widetilde{x^{\prime\prime}},\widetilde{z^{\prime\prime}})\\ &\text{$\widetilde{x^{\prime\prime}}$ do not occur in $F\,\alpha_{1}\,\cdots\,\alpha_{m}$.}\end{aligned}Bythelastconditionabove,wecanassume$\{x_{i}\}_{i}\cap\{x^{\prime\prime}_{i}\}_{i}=\emptyset$.\par Nowthereexist$q$,$r_{1},\dots,r_{q+m+1}$,$\widetilde{\psi}_{1,\dots,q}$,$\widetilde{e}_{1,\dots,r_{q+m+1}}$thatsatisfythefollowingconditions,wherewewrite$\widetilde{e}_{(i)}$(orsimply$\widetilde{e}$if$i$isclear)for$\widetilde{e}_{r_{i-1}+1,\dots,r_{i}}$($i=1,\dots,q+m+1$)and$r_{0}:=0$:\begin{aligned} &r_{1}\leq\dots\leq r_{q+m+1}\\ &(\alpha_{1},\dots,\alpha_{h^{\prime\prime}})=(\widetilde{e}_{(1)},\psi_{1},\dots,\widetilde{e}_{(q)},\psi_{q})\\ &(\alpha_{h^{\prime\prime}+1},\dots,\alpha_{h^{\prime}})=(\widetilde{e}_{(q+1)},\xi_{1},\dots,\widetilde{e}_{(q+m)},\xi_{m},\widetilde{e}_{(q+m+1)})\\ &p=r_{q+m+1}-r_{q}.\end{aligned}Let$\kappa_{i}$bethetypeof$\psi_{i}$(i.e.,$\kappa_{i}:=\kappa^{\prime\prime}_{r_{i}+i}$).Thenwealsohave\begin{aligned} \Theta(F)=\ &\mathtt{Int}^{r_{1}}\to\kappa_{1}\to\cdots\mathtt{Int}^{r_{q}-r_{q-1}}\to\kappa_{q}\to\\ &\mathtt{Int}^{r_{q+1}-r_{q}}\to(\mathtt{Int}^{M}\to\star)\to\\ &\cdots\mathtt{Int}^{r_{q+m}-r_{q+m-1}}\to(\mathtt{Int}^{M}\to\star)\to\\ &\mathtt{Int}^{r_{q+m+1}-r_{q+m}}\to\star.\end{aligned}\par Inthederivationtreeof$$\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}(\varphi^{\prime}=)\ F\,\alpha_{1}\,\cdots\,\alpha_{h^{\prime}}:\star\leadsto(\varphi^{\prime}_{*},\varphi^{\prime}_{0},\ldots,\varphi^{\prime}_{k}),$$theleftmostpathfromtheheadposition$F$consistsof:(i)\mathrm{\mathchoice{\mbox{\sc Tr-VarF}}{\mbox{\sc Tr-VarF}}{\mbox{\small\sc Tr-VarF}}{\mbox{\tiny TR-VARF}}}attheleaf,then(ii)repeatedapplicationsofeither\mathrm{\mathchoice{\mbox{\sc Tr-App}}{\mbox{\sc Tr-App}}{\mbox{\small\sc Tr-App}}{\mbox{\tiny TR-APP}}}or\mathrm{\mathchoice{\mbox{\sc Tr-AppI}}{\mbox{\sc Tr-AppI}}{\mbox{\small\sc Tr-AppI}}{\mbox{\tiny TR-APPI}}},andthen(iii)repeatedapplicationsofeither\mathrm{\mathchoice{\mbox{\sc Tr-AppG}}{\mbox{\sc Tr-AppG}}{\mbox{\small\sc Tr-AppG}}{\mbox{\tiny TR-APPG}}}or\mathrm{\mathchoice{\mbox{\sc Tr-AppI}}{\mbox{\sc Tr-AppI}}{\mbox{\small\sc Tr-AppI}}{\mbox{\tiny TR-APPI}}}.Morespecifically,attheleafof\mathrm{\mathchoice{\mbox{\sc Tr-VarF}}{\mbox{\sc Tr-VarF}}{\mbox{\small\sc Tr-VarF}}{\mbox{\tiny TR-VARF}}}wehave$$\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}F:\Theta(F)\leadsto(F_{0},F_{0},(F_{0})^{k},F_{1},\ldots,F_{m})$$where$(F_{0})^{k}$denotesthesequenceoflength$k$whoseallcomponentsare$F_{0}$.Thenby\mathrm{\mathchoice{\mbox{\sc Tr-AppI}}{\mbox{\sc Tr-AppI}}{\mbox{\small\sc Tr-AppI}}{\mbox{\tiny TR-APPI}}}wehave\begin{aligned} &\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}F\,\widetilde{e}_{(1)}:{\Theta(F)}^{@r_{0}}\leadsto\\ &\quad(F_{0}\,\widetilde{e}_{(1)},F_{0}\,\widetilde{e}_{(1)},(F_{0}\,\widetilde{e}_{(1)})^{k},F_{1}\,\widetilde{e}_{(1)},\ldots,F_{m}\,\widetilde{e}_{(1)}).\end{aligned}Thenby\mathrm{\mathchoice{\mbox{\sc Tr-App}}{\mbox{\sc Tr-App}}{\mbox{\small\sc Tr-App}}{\mbox{\tiny TR-APP}}}(and\mathrm{\mathchoice{\mbox{\sc Tr-AppI}}{\mbox{\sc Tr-AppI}}{\mbox{\small\sc Tr-AppI}}{\mbox{\tiny TR-APPI}}})wehave\begin{aligned} &\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\psi_{i}:\kappa_{i}\leadsto(\psi_{i,*},\psi_{i,0},\dots,\psi_{i,k+m^{\prime}_{i}})\quad(i=1,\dots,q)\\ &\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}F\,\widetilde{e}_{(1)}\,\psi_{1}\cdots\widetilde{e}_{(q)}\,\psi_{q}:{\Theta(F)}^{@r_{q-1}+q}\leadsto\\ &\quad\big{(}F_{0}\,\widetilde{e}_{(1)}\,(\psi_{1,*},{\rm ChineseAstron.Astrophys.}{\psi_{1}}{k}{m^{\prime}_{1}})\cdots\widetilde{e}_{(q)}\,(\psi_{q,*},{\rm ChineseAstron.Astrophys.}{\psi_{q}}{k}{m^{\prime}_{q}}),\\ &\quad\phantom{\big{(}}F_{0}\,\widetilde{e}_{(1)}\,(\psi_{1,0},{\rm ChineseAstron.Astrophys.}{\psi_{1}}{k}{m^{\prime}_{1}})\cdots\widetilde{e}_{(q)}\,(\psi_{q,0},{\rm ChineseAstron.Astrophys.}{\psi_{q}}{k}{m^{\prime}_{q}}),\\ &\quad\phantom{\big{(}}F_{0}\,\widetilde{e}_{(1)}\,(\psi_{1,1},{\rm ChineseAstron.Astrophys.}{\psi_{1}}{k}{m^{\prime}_{1}})\cdots\widetilde{e}_{(q)}\,(\psi_{q,1},{\rm ChineseAstron.Astrophys.}{\psi_{q}}{k}{m^{\prime}_{q}}),\\ &\quad\phantom{\big{(}}\ldots,F_{0}\,\widetilde{e}_{(1)}\,(\psi_{1,k},{\rm ChineseAstron.Astrophys.}{\psi_{1}}{k}{m^{\prime}_{1}})\cdots\widetilde{e}_{(q)}\,(\psi_{q,k},{\rm ChineseAstron.Astrophys.}{\psi_{q}}{k}{m^{\prime}_{q}}),\\ &\quad\phantom{\big{(}}F_{1}\,\widetilde{e}_{(1)}\,({\rm ChineseAstron.Astrophys.}{\psi_{1}}{k}{m^{\prime}_{1}})\cdots\widetilde{e}_{(q)}\,({\rm ChineseAstron.Astrophys.}{\psi_{q}}{k}{m^{\prime}_{q}}),\\ &\quad\phantom{\big{(}}\ldots,F_{m}\,\widetilde{e}_{(1)}\,({\rm ChineseAstron.Astrophys.}{\psi_{1}}{k}{m^{\prime}_{1}})\cdots\widetilde{e}_{(q)}\,({\rm ChineseAstron.Astrophys.}{\psi_{q}}{k}{m^{\prime}_{q}})\big{)}\\ &m^{\prime}_{i}:=\mathtt{gar}(\kappa_{i})\quad(i=1,\dots,q)\\ &\mathtt{decomp}(\kappa_{i})=(\widetilde{\kappa_{i}},m^{\prime}_{i},p_{i})\quad(i=1,\dots,q).\end{aligned}Andthenby\mathrm{\mathchoice{\mbox{\sc Tr-AppG}}{\mbox{\sc Tr-AppG}}{\mbox{\small\sc Tr-AppG}}{\mbox{\tiny TR-APPG}}}(and\mathrm{\mathchoice{\mbox{\sc Tr-AppI}}{\mbox{\sc Tr-AppI}}{\mbox{\small\sc Tr-AppI}}{\mbox{\tiny TR-APPI}}})wehave\begin{aligned} &p^{\circ}_{i}:=r_{q+m}-r_{q-1+i}\quad(i=1,\dots,m)\\ &\varphi^{\circ}_{1}:=F\,\widetilde{e}_{(1)}\,\psi_{1}\cdots\widetilde{e}_{(q)}\,\psi_{q}\widetilde{e}_{(q+1)}\\ &\varphi^{\circ}_{i+1}:=\varphi^{\circ}_{i}\,\xi_{i}\,\widetilde{e}_{(q+i+1)}\quad(i=1,\dots,m)\\ &\tau_{i}:={\Theta(F)}^{@r_{q+i}+q+i}\quad(i=1,\dots,m)\\ &\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi^{\circ}_{i}:(\mathtt{Int}^{M}{\to}\star)\,{\to}\,\tau_{i}\leadsto(\varphi^{\circ}_{i,*},\varphi^{\circ}_{i,0},\ldots,\varphi^{\circ}_{i,k+m+1-i})\\ &\\ &\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\xi_{i}:{\mathtt{Int}}^{M}{\to}\star\leadsto(\xi_{i,*},\xi_{i,0},\ldots,\xi_{i,k})\\ &\begin{aligned} \overline{\xi_{i,j}}:=\ &\lambda\widetilde{z}_{1,\ldots,p^{\circ}_{i}}.\lambda\widetilde{w}_{1,\ldots,M}.\\ &\varphi^{\circ}_{i,j}\,\widetilde{z}\,\widetilde{w}\,\lor\exists\widetilde{u}_{1,\ldots,M}.(\varphi^{\circ}_{i,k+1}\,\widetilde{z}\,\widetilde{u}\land\xi_{i,j}\,\widetilde{u}\,\widetilde{w})\end{aligned}\\ &\\ &\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}\varphi^{\circ}_{i+1}(=\varphi^{\circ}_{i}\,\xi_{i}\,\widetilde{e}_{(q+i+1)}):(\mathtt{Int}^{M}{\to}\star)\,{\to}\,\tau_{i+1}\leadsto\\ &\quad(\overline{\xi_{i,*}}\,\widetilde{e},\overline{\xi_{i,0}}\,\widetilde{e},\dots,\overline{\xi_{i,k}}\,\widetilde{e},\varphi^{\circ}_{i,k+2}\,\widetilde{e},\dots,\varphi^{\circ}_{i,k+m+1-i}\,\widetilde{e})\\ &\mspace{320.0mu}(i=1,\dots,m).\end{aligned}Then,foreach$i=2,\dots,m+1$,wehave\begin{aligned} &(\varphi^{\circ}_{i,*}&&\,,\ &&\varphi^{\circ}_{i,0}&&\,,\ &&\ldots,\varphi^{\circ}_{i,k}&&\,,\ &&\varphi^{\circ}_{i,k+1}&&\,,\ &&\ldots,\varphi^{\circ}_{i,k+m+1-i}&&\,)\\ =\ &(\overline{\xi_{i-1,*}}\,\widetilde{e}&&\,,\ &&\overline{\xi_{i-1,0}}\,\widetilde{e}&&\,,\ &&\dots,\overline{\xi_{i-1,k}}\,\widetilde{e}&&\,,\ &&\varphi^{\circ}_{i-1,k+2}\,\widetilde{e}&&\,,\ &&\dots,\varphi^{\circ}_{i-1,k+m+2-i}\,\widetilde{e}&&\,)\end{aligned}where$\widetilde{e}=\widetilde{e}_{(q+i)}$.Hence,foreach$i=1,\dots,m$,\begin{aligned} \varphi^{\circ}_{i,k+1}&=\varphi^{\circ}_{i-1,k+2}\,\widetilde{e}_{(q+i)}=\varphi^{\circ}_{i-2,k+3}\,\widetilde{e}_{(q+i-1)}\,\widetilde{e}_{(q+i)}=\dots\\ &=\varphi^{\circ}_{1,k+i}\,\widetilde{e}_{(q+2)}\cdots\widetilde{e}_{(q+i)}\\ &=F_{i}\,\widetilde{e}_{(1)}\,({\rm ChineseAstron.Astrophys.}{\psi_{1}}{k}{m^{\prime}_{1}})\cdots\widetilde{e}_{(q)}\,({\rm ChineseAstron.Astrophys.}{\psi_{q}}{k}{m^{\prime}_{q}})\,\widetilde{e}_{(q+1)}\cdots\widetilde{e}_{(q+i)}\end{aligned}wherethelastequalityfollowsfromthecalculationresultof\mathrm{\mathchoice{\mbox{\sc Tr-App}}{\mbox{\sc Tr-App}}{\mbox{\small\sc Tr-App}}{\mbox{\tiny TR-APP}}}above.Also,foreach$i=2,\dots,m$and$j=*,0,\dots,k$,wehave\begin{aligned} &\overline{\xi_{i,j}}\,\widetilde{z}_{1,\ldots,p^{\circ}_{i}}\,\widetilde{w}_{1,\ldots,M}\\ =_{D^{\prime}}\ &\overline{\xi_{i-1,j}}\,\widetilde{e}_{(q+i)}\,\widetilde{z}\,\widetilde{w}\,\lor\exists\widetilde{u}_{1,\ldots,M}.(\varphi^{\circ}_{i,k+1}\,\widetilde{z}\,\widetilde{u}\land\xi_{i,j}\,\widetilde{u}\,\widetilde{w})\end{aligned}\par Now,since$\varphi^{\prime}=\varphi^{\circ}_{m+1}$,foreach$j=*,0,\dots,k$,wehave\begin{aligned} &\varphi^{\prime}_{j}\,\widetilde{w}_{1,\ldots,M}=\varphi^{\circ}_{m+1,j}\,\widetilde{w}=\overline{\xi_{m,j}}\,\widetilde{e}_{(q+m+1)}\,\widetilde{w}\\ =_{D^{\prime}}\ &\overline{\xi_{m-1,j}}\,\widetilde{e}_{(q+m)}\,\widetilde{e}_{(q+m+1)}\,\widetilde{w}\\ &\lor\exists\widetilde{u}_{1,\ldots,M}.(\varphi^{\circ}_{m,k+1}\,\widetilde{e}_{(q+m+1)}\,\widetilde{u}\land\xi_{m,j}\,\widetilde{u}\,\widetilde{w})\\ =_{D^{\prime}}\ &\overline{\xi_{m-2,j}}\,\widetilde{e}_{(q+m-1)}\,\widetilde{e}_{(q+m)}\,\widetilde{e}_{(q+m+1)}\,\widetilde{w}\\ &\lor\exists\widetilde{u}_{1,\ldots,M}.(\varphi^{\circ}_{m-1,k+1}\,\widetilde{e}_{(q+m)}\,\widetilde{e}_{(q+m+1)}\,\widetilde{u}\land\xi_{m-1,j}\,\widetilde{u}\,\widetilde{w})\\ &\lor\exists\widetilde{u}_{1,\ldots,M}.(\varphi^{\circ}_{m,k+1}\,\widetilde{e}_{(q+m+1)}\,\widetilde{u}\land\xi_{m,j}\,\widetilde{u}\,\widetilde{w})\\ =_{D^{\prime}}\ &\cdots\\ =_{D^{\prime}}\ &\overline{\xi_{1,j}}\,\widetilde{e}_{(q+2)}\cdots\widetilde{e}_{(q+m+1)}\,\widetilde{w}\\ &\lor\exists\widetilde{u}_{1,\ldots,M}.(\varphi^{\circ}_{2,k+1}\,\widetilde{e}_{(q+3)}\cdots\widetilde{e}_{(q+m+1)}\,\widetilde{u}\land\xi_{2,j}\,\widetilde{u}\,\widetilde{w})\\ &\lor\cdots\\ &\lor\exists\widetilde{u}_{1,\ldots,M}.(\varphi^{\circ}_{m,k+1}\,\widetilde{e}_{(q+m+1)}\,\widetilde{u}\land\xi_{m,j}\,\widetilde{u}\,\widetilde{w})\\ =_{D^{\prime}}\ &\varphi^{\circ}_{1,j}\,\widetilde{e}_{(q+2)}\cdots\widetilde{e}_{(q+m+1)}\,\widetilde{w}\\ &\lor\exists\widetilde{u}_{1,\ldots,M}.(\varphi^{\circ}_{1,k+1}\,\widetilde{e}_{(q+2)}\cdots\widetilde{e}_{(q+m+1)}\,\widetilde{u}\land\xi_{1,j}\,\widetilde{u}\,\widetilde{w})\\ &\lor\exists\widetilde{u}_{1,\ldots,M}.(\varphi^{\circ}_{2,k+1}\,\widetilde{e}_{(q+3)}\cdots\widetilde{e}_{(q+m+1)}\,\widetilde{u}\land\xi_{2,j}\,\widetilde{u}\,\widetilde{w})\\ &\lor\cdots\\ &\lor\exists\widetilde{u}_{1,\ldots,M}.(\varphi^{\circ}_{m,k+1}\,\widetilde{e}_{(q+m+1)}\,\widetilde{u}\land\xi_{m,j}\,\widetilde{u}\,\widetilde{w})\\ =_{D^{\prime}}\ &\varphi^{\circ}_{1,j}\,\widetilde{e}_{(q+2)}\cdots\widetilde{e}_{(q+m+1)}\,\widetilde{w}\\ &\lor\textstyle\bigvee_{i=1}^{m}\exists\widetilde{u}_{1,\ldots,M}.(\varphi^{\circ}_{i,k+1}\widetilde{e}_{(q+i+1)}\cdots\widetilde{e}_{(q+m+1)}\,\widetilde{u}\land\xi_{i,j}\,\widetilde{u}\,\widetilde{w})\\ =_{D^{\prime}}\ &\varphi^{\circ}_{1,j}\,\widetilde{e}_{(q+2)}\cdots\widetilde{e}_{(q+m+1)}\,\widetilde{w}\\ &\lor\textstyle\bigvee_{i=1}^{m}\exists\widetilde{u}_{1,\ldots,M}.(\begin{aligned} &\begin{aligned} F_{i}\,&\widetilde{e}_{(1)}\,({\rm ChineseAstron.Astrophys.}{\psi_{1}}{k}{m^{\prime}_{1}})\cdots\widetilde{e}_{(q)}\,({\rm ChineseAstron.Astrophys.}{\psi_{q}}{k}{m^{\prime}_{q}})\\ &\widetilde{e}_{(q+1)}\cdots\widetilde{e}_{(q+m+1)}\,\widetilde{u}\end{aligned}\\ &\land\xi_{i,j}\,\widetilde{u}\,\widetilde{w}).\end{aligned}\end{aligned}\par Tocalculate$\varphi^{\circ}_{1,j}$and$F_{i}$above,letusconsidertherulesof$F_{0},\dots,F_{m}$,whicharegivenby\mathrm{\mathchoice{\mbox{\sc Tr-Def}}{\mbox{\sc Tr-Def}}{\mbox{\small\sc Tr-Def}}{\mbox{\tiny TR-DEF}}}asfollows.Recall$$\mathtt{decomparg}(\widetilde{w^{\prime}},\Theta(F))=(\widetilde{y^{\prime\prime}}\mathbin{:}\widetilde{\kappa^{\prime\prime}},\widetilde{x^{\prime\prime}},\widetilde{z^{\prime\prime}})$$andlet\begin{aligned} &\widetilde{y^{\prime\prime}}\mathbin{:}\widetilde{\kappa^{\prime\prime}},\widetilde{z^{\prime\prime}}\mathbin{:}\widetilde{\mathtt{Int}};\,\widetilde{x^{\prime\prime}}_{1,\dots,m}\vdash_{\Theta}\varphi:\star\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{m})\\ &\widetilde{y^{\prime\prime}}_{i}:=(y^{\prime\prime}_{i,*},y^{\prime\prime}_{i,0},\ldots,y^{\prime\prime}_{i,\mathtt{gar}(\kappa^{\prime\prime}_{i})})\quad\widetilde{y^{\prime\prime}}^{\circ}_{i}:=(y^{\prime\prime}_{i,0},\ldots,y^{\prime\prime}_{i,\mathtt{gar}(\kappa^{\prime\prime}_{i})})\\ \\ &\widetilde{y^{\prime\prime}}_{i}:=y^{\prime\prime}_{i}\quad\widetilde{y^{\prime\prime}}^{\circ}_{i}:=y^{\prime\prime}_{i}\mspace{47.0mu}(i\in\{1,\dots,h^{\prime\prime}\}\text{ and }\kappa^{\prime\prime}_{i}=\mathtt{Int}).\end{aligned}Thenweobtain\begin{aligned} \vdash_{\Theta}(F\,\widetilde{w^{\prime}}=\varphi)\leadsto\,&\{F_{0}\,\widetilde{y^{\prime\prime}}_{1}\,\cdots\,\widetilde{y^{\prime\prime}}_{h^{\prime\prime}}\,\widetilde{z^{\prime\prime}}=\varphi_{*}\}\\ \cup&\{F_{i}\,\widetilde{y^{\prime\prime}}^{\circ}_{1}\,\cdots\,\widetilde{y^{\prime\prime}}^{\circ}_{h^{\prime\prime}}\,\widetilde{z^{\prime\prime}}=\varphi_{i}\mid i\in\{1,\ldots,m\}\}.\end{aligned}Recallthat$\kappa_{i}:=\kappa^{\prime\prime}_{r_{i}+i}$($i=1,\dots,q$),andlet\begin{aligned} &y_{i}:=y^{\prime\prime}_{r_{i}+i}\quad(i=1,\dots,q)\\ &y_{i,j}:=y^{\prime\prime}_{r_{i}+i,j}\quad(i=1,\dots,q,\ j=*,0,\dots,\mathtt{gar}(\kappa_{i}))\\ &\widetilde{y}_{i}:=\widetilde{y^{\prime\prime}}_{r_{i}+i}=(y_{i,*},y_{i,0},\dots,y_{i,\mathtt{gar}(\kappa_{i})})\\ &\widetilde{y}^{\circ}_{i}:=\widetilde{y^{\prime\prime}}^{\circ}_{r_{i}+i}=(y_{i,0},\dots,y_{i,\mathtt{gar}(\kappa_{i})}).\end{aligned}Thenlet$\widetilde{z}_{1,\dots,r_{q+m+1}}$beasequenceofvariablesoftype$\mathtt{Int}$thatsatisfiesthefollowingequations,wherewewrite$\widetilde{z}_{(i)}$(orsimply$\widetilde{z}$if$i$isclear)for$\widetilde{z}_{r_{i-1}+1,\dots,r_{i}}$($i=1,\dots,q+m+1$):\begin{aligned} &(w^{\prime}_{1},\dots,w^{\prime}_{h^{\prime\prime}})=(y^{\prime\prime}_{1},\dots,y^{\prime\prime}_{h^{\prime\prime}})=(\widetilde{z}_{(1)},y_{1},\dots,\widetilde{z}_{(q)},y_{q})\\ &(w^{\prime}_{h^{\prime\prime}+1},\dots,w^{\prime}_{h^{\prime}})=(\widetilde{z}_{(q+1)},x^{\prime\prime}_{1},\dots,\widetilde{z}_{(q+m)},x^{\prime\prime}_{m},\widetilde{z}_{(q+m+1)})\\ &(\widetilde{y^{\prime\prime}}_{1},\dots,\widetilde{y^{\prime\prime}}_{h^{\prime\prime}},\widetilde{z^{\prime\prime}})=(\widetilde{z}_{(1)},\widetilde{y}_{1},\dots,\widetilde{z}_{(q)},\widetilde{y}_{q},\widetilde{z}_{r_{q}+1,\dots,r_{q+m+1}})\\ &(\widetilde{y^{\prime\prime}}^{\circ}_{1},\dots,\widetilde{y^{\prime\prime}}^{\circ}_{h^{\prime\prime}},\widetilde{z^{\prime\prime}})=(\widetilde{z}_{(1)},\widetilde{y}^{\circ}_{1},\dots,\widetilde{z}_{(q)},\widetilde{y}^{\circ}_{q},\widetilde{z}_{r_{q}+1,\dots,r_{q+m+1}}).\end{aligned}\par Now,for$j=*,0,\dots,k$,wehave\begin{aligned} &\varphi^{\circ}_{1,j}\,\widetilde{e}_{(q+2)}\cdots\widetilde{e}_{(q+m+1)}\,\widetilde{w}_{1,\ldots,M}\\ =_{D^{\prime}}\ &F_{0}\,\widetilde{e}_{(1)}(\psi_{1,j},{\rm ChineseAstron.Astrophys.}{\psi_{1}}{k}{m^{\prime}_{1}})\cdots\widetilde{e}_{(q)}(\psi_{q,j},{\rm ChineseAstron.Astrophys.}{\psi_{q}}{k}{m^{\prime}_{q}})\widetilde{e}_{(q+1)}\cdots\widetilde{e}_{(q+m+1)}\widetilde{w}\\ =_{D^{\prime}}\ &\big{(}\big{[}(\psi_{i^{\prime},j},{\rm ChineseAstron.Astrophys.}{\psi_{i^{\prime}}}{k}{m^{\prime}_{i^{\prime}}})/\widetilde{y}_{i^{\prime}}\big{]}_{i^{\prime}=1}^{q}\big{[}e_{j^{\prime}}/z_{j^{\prime}}\big{]}_{j^{\prime}=1}^{r_{q+m+1}}\varphi_{*}\big{)}\,\widetilde{w}.\end{aligned}Alsoforeach$i=1,\dots,m$,wehave\begin{aligned} &F_{i}\,\widetilde{e}_{(1)}\,({\rm ChineseAstron.Astrophys.}{\psi_{1}}{k}{m^{\prime}_{1}})\cdots\widetilde{e}_{(q)}\,({\rm ChineseAstron.Astrophys.}{\psi_{q}}{k}{m^{\prime}_{q}})\,\widetilde{e}_{(q+1)}\cdots\widetilde{e}_{(q+m+1)}\,\widetilde{u}\\ =_{D^{\prime}}\ &\big{(}\big{[}{\rm ChineseAstron.Astrophys.}{\psi_{i^{\prime}}}{k}{m^{\prime}_{i^{\prime}}}/\widetilde{y}^{\circ}_{i^{\prime}}\big{]}_{i^{\prime}=1}^{q}\big{[}e_{j^{\prime}}/z_{j^{\prime}}\big{]}_{j^{\prime}=1}^{r_{q+m+1}}\varphi_{i}\big{)}\,\widetilde{u}.\end{aligned}\par Next,letusconsider$\psi^{\prime}$.Nowwehave\begin{aligned} \psi^{\prime}&=\{\widetilde{\xi}/\widetilde{x^{\prime\prime}}\}[\widetilde{e^{\prime\prime}}/\widetilde{z^{\prime\prime}}][\widetilde{\varphi^{\prime\prime}}/\widetilde{y^{\prime\prime}}]\varphi\\ &=\{\widetilde{\xi}/\widetilde{x^{\prime\prime}}\}[\psi_{i^{\prime}}/y_{i^{\prime}}]_{i^{\prime}=1}^{q}[e_{j^{\prime}}/z_{j^{\prime}}]_{j^{\prime}=1}^{r_{q+m+1}}\varphi.\end{aligned}Recall\begin{aligned} &\widetilde{y^{\prime\prime}}\mathbin{:}\widetilde{\kappa^{\prime\prime}},\ \widetilde{z^{\prime\prime}}\mathbin{:}\widetilde{\mathtt{Int}};\ \widetilde{x^{\prime\prime}}_{1,\dots,m}\vdash_{\Theta}\varphi:\star\leadsto(\varphi_{*},\varphi_{0},\ldots,\varphi_{m}),\\ &(\widetilde{y^{\prime\prime}},\widetilde{z^{\prime\prime}})=(\widetilde{z}_{(1)},y_{1},\dots,\widetilde{z}_{(q)},y_{q},\widetilde{z}_{(q+1)},\dots,\widetilde{z}_{(q+m+1)}),\end{aligned}andlet\begin{aligned} &\widetilde{y}:\widetilde{\kappa};\ \widetilde{x^{\prime\prime}}_{1,\dots,m}\vdash_{\Theta}[e_{j^{\prime}}/z_{j^{\prime}}]_{j^{\prime}=1}^{r_{q+m+1}}\varphi:\star\leadsto\\ &\quad(\psi^{\prime\prime\prime}_{*},\psi^{\prime\prime\prime}_{0},\ldots,\psi^{\prime\prime\prime}_{m}),\\ &\widetilde{x}_{1,\ldots,k},\ \widetilde{x^{\prime\prime}}_{1,\dots,m}\vdash_{\Theta}[\psi_{i^{\prime}}/y_{i^{\prime}}]_{i^{\prime}=1}^{q}[e_{j^{\prime}}/z_{j^{\prime}}]_{j^{\prime}=1}^{r_{q+m+1}}\varphi:\star\leadsto\\ &\quad(\psi^{\prime\prime}_{*},\psi^{\prime\prime}_{0},\ldots,\psi^{\prime\prime}_{k+m}).\end{aligned}Then,byapplyingLemma~{}\ref{lem:substitutionHigher}\lx@cref{creftypecap~refnum}{item:mainOfSubstLemma},andthenbyapplyingLemma~{}\ref{lem:substitutionInt},weobtain:\begin{aligned} \psi^{\prime\prime}_{j}&=_{D^{\prime}}\big{[}(\psi_{i^{\prime},j},{\rm ChineseAstron.Astrophys.}{\psi_{i^{\prime}}}{k}{m^{\prime}_{i^{\prime}}})/\widetilde{y}_{i^{\prime}}\big{]}_{i^{\prime}=1}^{q}\psi^{\prime\prime\prime}_{*}\\ &=\big{[}(\psi_{i^{\prime},j},{\rm ChineseAstron.Astrophys.}{\psi_{i^{\prime}}}{k}{m^{\prime}_{i^{\prime}}})/\widetilde{y}_{i^{\prime}}\big{]}_{i^{\prime}=1}^{q}\big{[}e_{j^{\prime}}/z_{j^{\prime}}\big{]}_{j^{\prime}=1}^{r_{q+m+1}}\varphi_{*}\\ \psi^{\prime\prime}_{k+i}&=_{D^{\prime}}\big{[}{\rm ChineseAstron.Astrophys.}{\psi_{i^{\prime}}}{k}{m^{\prime}_{i^{\prime}}}/\widetilde{y}^{\circ}_{i^{\prime}}\big{]}_{i^{\prime}=1}^{q}\psi^{\prime\prime\prime}_{i}\\ &=\big{[}{\rm ChineseAstron.Astrophys.}{\psi_{i^{\prime}}}{k}{m^{\prime}_{i^{\prime}}}/\widetilde{y}^{\circ}_{i^{\prime}}\big{]}_{i^{\prime}=1}^{q}\big{[}e_{j^{\prime}}/z_{j^{\prime}}\big{]}_{j^{\prime}=1}^{r_{q+m+1}}\varphi_{i}\\ \end{aligned}\par Now,for$j=*,0,\dots,k$,let\begin{aligned} \psi^{\prime}_{j}=\lambda\widetilde{w}_{1,\ldots,M}.\psi^{\prime\prime}_{j}\,\widetilde{w}\lor\textstyle\bigvee_{i=1}^{m}\exists\widetilde{u}_{1,\ldots,M}.\Big{(}\psi^{\prime\prime}_{k+i}\,\widetilde{u}\land\xi_{i,j}\,\widetilde{u}\,\widetilde{w}\Big{)}.\\ \end{aligned}Thenby\mathrm{\mathchoice{\mbox{\sc Tr-ESub}}{\mbox{\sc Tr-ESub}}{\mbox{\small\sc Tr-ESub}}{\mbox{\tiny TR-ESUB}}},wehave\begin{aligned} &\widetilde{x}_{1,\ldots,k}\vdash_{\Theta}(\psi^{\prime}=)\{\widetilde{\xi}/\widetilde{x^{\prime\prime}}\}[\psi_{i^{\prime}}/y_{i^{\prime}}]_{i^{\prime}=1}^{q}[e_{j^{\prime}}/z_{j^{\prime}}]_{j^{\prime}=1}^{r_{q+m+1}}\varphi:\star\leadsto\\ &\quad(\psi^{\prime}_{*},\psi^{\prime}_{0},\ldots,\psi^{\prime}_{k}).\end{aligned}Also,by\lx@cref{creftypepluralcap~refnum}{eq:subRedMain1},\lx@cref{refnum}{eq:subRedMain2-1},\lx@cref{refnum}{eq:subRedMain2-3},\lx@cref{refnum}{eq:subRedMain3}and~\lx@cref{refnum}{eq:subRedMain5},wehave$\varphi^{\prime}_{j}=_{D^{\prime}}\psi^{\prime}_{j}$for$j=*,0,\dots,k$,asrequired.\QED\par\endtrivlist\@add@PDF@RDFa@triples\par\end{document}