Lemma 3.18: the collapse lemma

Let $S$ be a type of sorts and $sig$ an $S$-sorted signature (for each arity $w \in \mathrm{List}\,S$ and result sort $s$, a type $sig\,w\,s$ of operation symbols). Let $X$ be an $S$-sorted family of variable types (a type $X_t$ for each sort $t$). Let $A$ be a $sig$-algebra (a carrier family $A_t$ together with an interpretation of every operation symbol on argument tuples), and let $g$ be a homomorphism from the free/term algebra $\mathrm{Free}(sig,X)$ — whose sort-$t$ carrier is the inductive type $\mathrm{Term}_{sig,X}(t)$ of terms of sort $t$ over $X$ (a term is either a variable $\mathsf{var}(x)$ with $x \in X_t$, or an application $\sigma(t_1,\dots,t_k)$ of a symbol $\sigma \in sig\,w\,t$ to a length-matched vector of argument terms) — into $A$. Write $g_t : \mathrm{Term}_{sig,X}(t) \to A_t$ for the sort-$t$ component of $g$. The statement also fixes an implicit sort $u$, a variable $z \in X_u$, an implicit sort $s$, and a term $R \in \mathrm{Term}_{sig,X}(s)$.

An $S$-term $\langle t, T\rangle$ is a dependent pair of a sort $t$ and a term $T \in \mathrm{Term}_{sig,X}(t)$; write $\pi_1,\pi_2$ for its two components. Call $\langle t, T\rangle$ an immediate subterm of $\langle t', T'\rangle$ when $T'$ is an application $\sigma(\dots)$ of some symbol to an argument vector one of whose entries is exactly $T$ (at the matching sort $t$). Write $a \prec b$ for the transitive closure of "immediate subterm" (one or more such steps; strictly proper — reflexivity is not included). Call $b$ minimal, $\mathrm{Min}(b)$, if it has no immediate subterm, i.e. its term component is a variable or a symbol applied to the empty argument vector (a constant). The hypothesis $hR$ is $\neg\,\mathrm{Min}(\langle s, R\rangle)$: $R$ is an application of an operation symbol to a nonempty argument vector (it has at least one immediate subterm).

For $P \in \mathrm{Term}_{sig,X}(s)$, let $\mathrm{occ}_z(P) \in \mathbb{N}$ be the number of leaf positions of $P$ that are exactly the variable $z$ (a leaf $\mathsf{var}(x)$ of sort $t$ counts iff $t = u$ and $x = z$). Given a family $q : \mathrm{Fin}(\mathrm{occ}_z(P)) \to \mathrm{Term}_{sig,X}(u)$ indexed by those occurrences, let $\mathrm{substFam}(z,P,q) \in \mathrm{Term}_{sig,X}(s)$ be the term obtained from $P$ by replacing, in left-to-right depth-first traversal order, the $k$-th occurrence of the variable $z$ by $q(k)$ for $k = 0,\dots,\mathrm{occ}_z(P)-1$, and leaving every other leaf of $P$ unchanged. Throughout, an expression written $h \triangleright T$ denotes $T$ transported along a proof $h$ of an equality of sorts, so that it can be read at the target sort.

Claim. There exist a term $P \in \mathrm{Term}_{sig,X}(s)$ and a family $q : \mathrm{Fin}(\mathrm{occ}_z(P)) \to \mathrm{Term}_{sig,X}(u)$ such that all of the following hold:

1. $R = \mathrm{substFam}(z, P, q)$: the given term $R$ is exactly $P$ with each of its $\mathrm{occ}_z(P)$ occurrences of the variable $z$ replaced, in traversal order, by the corresponding $q(k)$, all other leaves of $P$ preserved. (If $\mathrm{occ}_z(P) = 0$, then $q$ is the empty family and this clause reads $R = P$.)

2. $g_s(P) = g_s(R)$: $P$ and $R$ have the same image under $g$ at sort $s$.

3. For every index $\alpha \in \mathrm{Fin}(\mathrm{occ}_z(P))$, both:

   • $\langle u, q(\alpha)\rangle \prec \langle s, R\rangle$ — the inserted term $q(\alpha)$ is a strictly proper subterm of $R$; and
   • $g_u(q(\alpha)) = g_u(\mathsf{var}(z))$ — $q(\alpha)$ has the same $g$-image at sort $u$ as the one-variable term $z$.

   (This clause is vacuous when $\mathrm{occ}_z(P) = 0$.)

4. For every $S$-term $M = \langle \pi_1 M, \pi_2 M\rangle$ such that $M \prec \langle s, P\rangle$ (a strictly proper subterm of $P$) and $\neg\,\mathrm{Min}(M)$ ($\pi_2 M$ is an operation symbol applied to a nonempty argument vector), both:

   • (a) There is no proof $h$ of $\pi_1 M = u$ for which $g_u(h \triangleright \pi_2 M) = g_u(\mathsf{var}(z))$. Equivalently: it is not the case that $M$'s sort is $u$ and $\pi_2 M$, read at sort $u$, has the same $g$-image at sort $u$ as the variable term $z$.
   • (b) There exists an $S$-term $N = \langle \pi_1 N, \pi_2 N\rangle$ with $N \prec \langle s, R\rangle$ (a strictly proper subterm of $R$), $\neg\,\mathrm{Min}(N)$ ($\pi_2 N$ is an operation symbol applied to a nonempty argument vector), and a proof $h$ of $\pi_1 N = \pi_1 M$ (so $N$ and $M$ have the same sort) such that $g_{\pi_1 M}(h \triangleright \pi_2 N) = g_{\pi_1 M}(\pi_2 M)$ — i.e. $\pi_2 N$, read at $M$'s sort, has the same $g$-image at that sort as $\pi_2 M$.

The four clauses are conjoined under the single existential over $(P, q)$. Degenerate readings the quantifiers admit: $\mathrm{occ}_z(P) = 0$ is allowed, forcing $R = P$ in clause 1 and emptying clause 3; the universally quantified $M$ in clause 4 ranges only over strictly-proper non-minimal subterms of $P$, so if $P$ has no such subterm (e.g. $P$ is a variable, a constant, or an application all of whose arguments are variables/constants) clause 4 is vacuously satisfied.