Corollary 3.17: homomorphism invariance under state-preserving substitution

The theorem, stated in a namespace MSKleene, concerns many-sorted universal algebra. Fix a type $S$ of sorts (here $S : \mathrm{Type}$, i.e. in the lowest universe). A signature $\mathrm{sig}$ over $S$ assigns to each list of argument sorts $w$ and each result sort $s$ a type $\mathrm{sig}\,w\,s$ of operation symbols. An $S$-sorted set $X$ is a family of types $X_s$ indexed by $s\in S$; think of $X_s$ as the variables of sort $s$. A $\mathrm{sig}$-algebra $A$ consists of a carrier family $A_s$ ($s\in S$) together with, for every symbol $\sigma\in\mathrm{sig}\,w\,s$, an operation sending a tuple of arguments of sorts $w$ to an element of $A_s$. The terms $\mathrm{Term}\,\mathrm{sig}\,X\,s$ of sort $s$ are built inductively: either $\mathrm{var}(x)$ for some $x\in X_s$, or $\sigma(\vec t\,)$ where $\sigma\in\mathrm{sig}\,w\,s$ and $\vec t$ is a tuple of terms whose sorts are exactly the entries of $w$. These terms form the carrier of the free algebra on $X$, whose operations are just term formation.

The statement fixes:

• a signature $\mathrm{sig}$ over $S$, an $S$-sorted set $X$, and a $\mathrm{sig}$-algebra $A$;
• a homomorphism $g$ from the free algebra on $X$ to $A$; concretely $g$ supplies maps $g_s:\mathrm{Term}\,\mathrm{sig}\,X\,s\to A_s$ for all $s$, and these commute with every operation symbol (applying $g$ to $\sigma(\vec t\,)$ equals applying $A$'s $\sigma$-operation to the componentwise $g$-images of $\vec t$);
• implicit sorts $u,s\in S$;
• a variable $z\in X_u$ of sort $u$;
• a term $P\in\mathrm{Term}\,\mathrm{sig}\,X\,s$ of sort $s$.

Let $N:=\mathrm{occ}(z,P)\in\mathbb N$ be the occurrence count of $z$ in $P$: traversing $P$, it counts each leaf $\mathrm{var}(x)$ whose sort equals $u$ and for which (after the identification of sorts) $x=z$; leaves that are a different variable, or a variable of a sort other than $u$, contribute $0$, and the count is additive over the argument tuples of every $\sigma$-node.

The statement further fixes a family

of $N$ replacement terms, all of sort $u$ (indexed by $\mathrm{Fin}\,N$), and assumes the hypothesis

i.e. $g$ sends every replacement term $q_\alpha$ to the very same element of $A_u$ that it assigns to the one‑variable term $\mathrm{var}(z)$.

Write $\mathrm{substFam}(z,P,q)\in\mathrm{Term}\,\mathrm{sig}\,X\,s$ for the family substitution: form the list $[q_0,q_1,\dots,q_{N-1}]$, then traverse $P$ from left to right (each $\sigma$-node's arguments processed in order, recursively), and at the $k$-th encountered occurrence of $z$ (for $k=0,1,\dots$) replace that leaf $\mathrm{var}(z)$ by the current head $q_k$ of the list, passing the remaining tail forward; non-matching leaves and all operation nodes are left in place. Because the list has exactly $N$ entries and there are exactly $N$ matching occurrences, every replacement term is used once and in occurrence order, and the leftover list is empty; the result term is returned (the unused tail is discarded). In the internal definition, if the list were ever exhausted at a matching occurrence that leaf would be kept unchanged, but that branch does not arise here since the lengths coincide.

The conclusion asserted (its proof is omitted) is the equality in $A_s$

applying the homomorphism $g$ to the term obtained from $P$ by replacing its occurrences of $z$ with the terms $q_0,\dots,q_{N-1}$ yields the same element of $A_s$ as applying $g$ to $P$ itself.

Edge cases folded into the quantifiers: $g$ is an arbitrary homomorphism, not necessarily the canonical evaluation map; no finiteness or decidability hypotheses are imposed on $S$, $\mathrm{sig}$, or $X$. If $N=\mathrm{occ}(z,P)=0$ (in particular if $z$ does not occur in $P$, or occurs only at sorts $\neq u$), then the index type $\mathrm{Fin}\,N$ is empty, $q$ is the empty family, the hypothesis $hq$ holds vacuously, $\mathrm{substFam}(z,P,q)$ returns $P$ unchanged, and the conclusion is the trivial identity $g_s(P)=g_s(P)$. If $P=\mathrm{var}(z)$ with $s=u$, then $N=1$ and the conclusion is exactly the instance $g_u(q_0)=g_u(\mathrm{var}(z))$ of $hq$.