Lemma 4.9: every singleton of a term is regular

For every type of sorts $S$ equipped with the assumption that $S$ is finite; every many-sorted signature $\mathit{sig}$, meaning a family of types $\mathit{sig}(w,s)$ of operation symbols indexed by a finite list $w$ of input sorts and an output sort $s$; every sorted family of variable types $X=(X_t)_{t\in S}$; assumptions that the dependent sum of all operation-symbol types $\sum_{w:\operatorname{List}(S)}\sum_{t:S}\mathit{sig}(w,t)$ is finite and that the dependent sum $\sum_{t:S}X_t$ is finite; every sort $s\in S$; and every finite $\mathit{sig}$-term $P$ of sort $s$ built recursively either from a variable in $X$ of the appropriate sort or by applying an operation symbol to a matching tuple of subterms, the following conjunction holds. First, if $P$ is converted to a regular expression by leaving every variable node unchanged and replacing every original operation-symbol node by the corresponding base-symbol node, then interpreting that expression as a language of $\mathit{sig}$-terms—variables denote their singleton variable terms and a base operation applied to languages denotes all operation applications obtained by choosing one argument term from each component language—gives exactly the singleton language $\{P\}$. Second, $\{P\}$ is regular in the following literal sense: there exist a sorted family of auxiliary variable types $E=(E_t)_{t\in S}$ for which $\sum_{t:S}(X_t\mathbin{\sqcup}E_t)$ is finite, and a regular expression $R$ of sort $s$ over the enlarged variables $X_t\mathbin{\sqcup}E_t$, such that the language denoted by $R$ is exactly the image of $\{P\}$ under recursive relabelling along the injections $X_t\hookrightarrow X_t\mathbin{\sqcup}E_t$. Here such a regular expression is a term whose operation symbols are either base symbols from $\mathit{sig}$ or the added empty-language, binary-union, variable-indexed iteration, and variable-indexed substitution symbols, interpreted respectively as the empty set, union, finite-stage iteration, and completely additive term substitution. The existentially asserted $E$ and $R$ in the second conjunct are not stated to be any particular choices, and in particular the statement does not identify $R$ with the converted expression from the first conjunct. No nonemptiness assumption is imposed on $S$, $X$, or the signature; when there is no possible choice of the explicitly quantified $s$ and $P$, the corresponding universal assertion has no instances.