Claim 4.13 (Main Claim): the auxiliary languages are regular

Read-back of MSKleene.main_claim

Fix a type $S$ of sorts that is finite ($[\text{Finite }S]$; note that some sort $u\in S$ is provided, so $S$ is inhabited in any instance). A signature $\Sigma$ assigns to every arity word $w\in S^{*}$ (a finite list of sorts) and every result sort $s\in S$ a type $\Sigma_{w,s}$ of operation symbols; a sorted variable family $X$ assigns to every sort $s$ a type $X_s$. The hypotheses $\mathrm{hsig}$ and $\mathrm{hX}$ assert respectively that the total collection $\sum_{w,s}\Sigma_{w,s}$ of all operation symbols is finite and that the total collection $\sum_{s}X_s$ of all variables is finite. A Kleene context $\mathrm{ctx}$ over $(\Sigma,X)$ consists of three pieces of data: a function $n\colon S\to\mathbb{N}$; for every symbol $\sigma\in\Sigma_{w,s}$ an interpreting map $\mathrm{Nop}_\sigma\colon \prod_{i}\mathrm{Fin}(n_{w_i})\to \mathrm{Fin}(n_s)$ (so the tuple of finite sets $\big(\mathrm{Fin}(n_s)\big)_{s\in S}$, with these operations, forms a $\Sigma$-algebra $\mathcal N$); and a variable assignment $\mathrm{fgen}$ sending each $x\in X_s$ to an element $\mathrm{fgen}_s(x)\in\mathrm{Fin}(n_s)$. Write $Z_s := X_s \oplus \mathrm{Fin}(n_s)$ for the disjoint union (this is ctx.Z), with left injection $\iota_1\colon X_s\hookrightarrow Z_s$ and right injection $\iota_2\colon \mathrm{Fin}(n_s)\hookrightarrow Z_s$. Let $\mathcal T_s$ denote the set of $\Sigma$-terms of sort $s$ with variables drawn from $Z$: each such term is either $\mathrm{var}(z)$ for some $z\in Z_s$, or $\sigma(t_1,\dots,t_k)$ for a symbol $\sigma\in\Sigma_{w,s}$ and terms $t_i\in\mathcal T_{w_i}$. There is a canonical evaluation homomorphism $h\colon \mathcal T_s\to \mathrm{Fin}(n_s)$ determined by

and for a sort‑tagged term $Q=(s,q)$ we write $\mathrm{hVal}(Q) := h(q)\in\mathbb{N}$ (the underlying natural number of the element of $\mathrm{Fin}(n_s)$).

The theorem's remaining inputs are: a distinguished sort $u\in S$; a family $C$ assigning to every sort $s$ a subset $C_s\subseteq \mathrm{Fin}(n_s)$; a function $K\colon S\to\mathbb{N}$; a hypothesis $\mathrm{hK}$ stating $K_s\le n_s$ for every sort $s$ (this is satisfiable, e.g. by $K\equiv 0$, and $K$ enters the conclusion only through $\mathrm{auxLang}$ below); and a distinguished element $l\in \mathrm{Fin}(n_u)$ (whose existence forces $n_u\ge 1$; for any sort $t$ with $n_t=0$ one necessarily has $C_t=\varnothing$ and $K_t=0$). Call a variable-occurrence condition $C$-admissible for a term: every variable appearing at a leaf that has the form $\iota_2(m)$ at sort $t$ satisfies $m\in C_t$, while leaves of the form $\iota_1(x)$ are unconstrained (formally Term.varsIn (ctx.inXC C), using $\mathrm{Sum.elim}$ to send $\iota_1$‑variables to $\mathrm{True}$ and $\iota_2(m)$ at sort $t$ to $m\in C_t$). Let $\mathrm{proper\ subterm}$ mean the strict, transitive closure of the immediate‑subterm relation, where $Q$ is an immediate subterm of $R$ iff $R$'s term is an application $\sigma(t_1,\dots,t_k)$ (over the plain signature $\Sigma$) and $Q$'s term is one of the $t_i$ (at the corresponding sort); and call a sort‑tagged term minimal if it has no immediate subterm at all — i.e. it is either a variable or an application of a symbol to the empty argument list. Then $\mathrm{auxLang}_u(C,K,l)$ is the subset of $\mathcal T_u$ consisting of exactly those terms $P$ such that:

1. $P$ is $C$-admissible (every $\iota_2(m)$-variable occurring anywhere in $P$, at whatever sort $t$, has $m\in C_t$);
2. for every sort‑tagged term $Q=(s_Q,q)$ that is a proper subterm of $(u,P)$, that is not minimal (so $q$ is an application with at least one argument), and that is itself $C$-admissible, one has

(if $P$ is a variable or a nullary application this condition is vacuous); 3. $h(P) = l$ in $\mathrm{Fin}(n_u)$.

Next, the regular signature $\widehat\Sigma$ over $Z$ has, at arity $(w,s)$, the following operation symbols: $\mathrm{base}(\sigma)$ for each $\sigma\in\Sigma_{w,s}$; a symbol $\mathbf 0_s$ of arity $([\,],s)$; a symbol $\mathrm{iter}_s(z)$ of arity $([s],s)$ for each $z\in Z_s$; a symbol $\mathrm{plus}_s$ of arity $([s,s],s)$; and a symbol $\mathrm{subst}_{t,s}(z)$ of arity $([t,s],s)$ for each $z\in Z_t$. A regular expression of sort $u$, RegExpr sig ctx.Z u, is a term of sort $u$ over $\widehat\Sigma$ whose variables are drawn from $Z$. Its interpretation $\llbracket R\rrbracket \subseteq \mathcal T_s$ (this is interpExpr sig ctx.Z s, the unique homomorphic extension into the powerset $\Sigma$-algebra whose carrier at sort $s$ is $\mathcal P(\mathcal T_s)$, sending each generator $\mathrm{var}(z)$ to the singleton $\{\mathrm{var}(z)\}$) is defined recursively by:

Here $P[z:=M]$ denotes the set of all terms obtained from $P$ by replacing each occurrence of the specific variable $z$ (matched by both its sort and its identity in $Z_t$) independently by an arbitrary term of $M$, leaving every other variable and every operation symbol unchanged (the nondeterministic substitution homomorphism substHom). The claim of the theorem is that, under all the hypotheses above, there exists a regular expression $R\in\texttt{RegExpr}\ \Sigma\ Z\ u$ such that

as subsets of $\mathcal T_u$ — i.e. the language $\mathrm{auxLang}_u(C,K,l)$ is exactly the interpretation of some regular expression over $\widehat\Sigma$ with variables in $Z$. The existential is plain ($\exists$, not $\exists!$): no uniqueness of $R$ is asserted, and the finiteness hypotheses $[\text{Finite }S]$, $\mathrm{hsig}$, $\mathrm{hX}$, together with $\mathrm{hK}$, are assumed but do not otherwise appear in the concluding equation.