The $z$-iteration $L^{\star z}$

iterStage (noncomputable definition)

Fix a universe $u$, a type $S$ of sorts, an implicit signature $\Sigma$ over $S$ (which assigns to each finite list of sorts $w$ and each sort $s$ a type $\Sigma_{w,s}$ of operation symbols), and an implicit $S$-indexed family of variable sets $X$, with $X_s$ the variables of sort $s$. Let $T_s$ denote the type of $\Sigma$-terms of sort $s$ over $X$: each $x \in X_s$ gives a term $\mathrm{var}(x) \in T_s$, and each operation symbol $\sigma \in \Sigma_{w,s}$ applied to a matching tuple of subterms gives a term $\mathrm{app}(\sigma,\dots) \in T_s$.

For a sort $s$, a variable $z \in X_s$, and a set $L \subseteq T_s$ of terms of sort $s$, iterStage defines a function $\mathrm{iterStage}(z,L,-) : \mathbb{N} \to \mathcal{P}(T_s)$ by recursion on the natural-number argument:

• $\mathrm{iterStage}(z,L,0) = \{\mathrm{var}(z)\}$, the singleton set whose only element is the term consisting of the bare variable $z$;
• $\mathrm{iterStage}(z,L,i+1) = \mathrm{iterStage}(z,L,i)\ \cup\ \mathrm{substP}\big(z,\ \mathrm{iterStage}(z,L,i),\ s,\ L\big)$.

Here $\mathrm{substP}(z,M,s,K)$, for $M \subseteq T_s$ and $K \subseteq T_s$, is

$$\mathrm{substP}(z,M,s,K) \;=\; \bigcup_{P \in K} \Phi_{z,M}(P),$$

where $\Phi_{z,M}$ is the "replace occurrences of $z$ by members of $M$" operator: it is the homomorphic extension to terms of the assignment sending the variable $z$ (of sort $s$) to the set $M$ and every other variable $y \in X_t$ to the singleton $\{\mathrm{var}(y)\}$, evaluated in the power algebra of the term algebra. Concretely: $\Phi_{z,M}(\mathrm{var}(z)) = M$; $\Phi_{z,M}(\mathrm{var}(y)) = \{\mathrm{var}(y)\}$ whenever $y$ is a different variable from $z$ (or of a different sort); and

$$\Phi_{z,M}\big(\mathrm{app}(\sigma,(t_1,\dots,t_n))\big) = \big\{\, \mathrm{app}(\sigma,(u_1,\dots,u_n)) \;\big|\; u_k \in \Phi_{z,M}(t_k)\ \text{for each } k \,\big\},$$

each argument position choosing its replacement independently.

Thus in the successor clause the set iterated over is $L$ itself (the role of $K$), while the set spliced in for occurrences of $z$ is the previously built stage $\mathrm{iterStage}(z,L,i)$ (the role of $M$): stage $i+1$ is stage $i$ together with every term obtainable from some $P \in L$ by replacing each occurrence of $z$ in $P$ with an independently chosen element of stage $i$, all other variables left fixed. By construction each stage contains the previous one (the left summand of the union). Edge cases: if $L = \emptyset$ then the second summand is empty for every $i$, so every stage equals $\{\mathrm{var}(z)\}$; if $P \in L$ contains no occurrence of $z$, then $\Phi_{z,M}(P) = \{P\}$ for every $M$; if $P$ contains at least one occurrence of $z$ and $M = \emptyset$, then $\Phi_{z,M}(P) = \emptyset$. The result set always consists of terms of the same sort $s$ as $z$. The definition is marked noncomputable, and the underlying substitution assignment is built with classical logic for the sort- and variable-equality tests.

iterate (noncomputable definition)

With the same ambient data ($S$, $\Sigma$, $X$, term types $T_s$) as above, for a sort $s$, a variable $z \in X_s$, and a set $L \subseteq T_s$, iterate is defined as the countable union of all iteration stages:

$$\mathrm{iterate}(z,L) \;=\; \bigcup_{i \in \mathbb{N}} \mathrm{iterStage}(z,L,i) \;\subseteq\; T_s,$$

where $\mathrm{iterStage}(z,L,i)$ is the family from iterStage: $\mathrm{iterStage}(z,L,0) = \{\mathrm{var}(z)\}$ and $\mathrm{iterStage}(z,L,i+1) = \mathrm{iterStage}(z,L,i) \cup \bigcup_{P \in L} \Phi_{z,\ \mathrm{iterStage}(z,L,i)}(P)$, with $\Phi_{z,M}(P)$ the set of all terms obtained from $P$ by replacing every occurrence of the variable $z$ with independently chosen elements of $M$ and leaving all other variables unchanged. Since $i$ ranges over all of $\mathbb{N}$, including $0$, the term $\mathrm{var}(z)$ always belongs to $\mathrm{iterate}(z,L)$; in particular if $L = \emptyset$ then $\mathrm{iterate}(z,L) = \{\mathrm{var}(z)\}$. The definition is marked noncomputable.

iterStage_zero (theorem, @[simp])

For every sort $s$, every variable $z \in X_s$, and every set $L \subseteq T_s$ of terms of sort $s$ (with $S$, $\Sigma$, $X$ the ambient implicit data), the zeroth iteration stage equals the singleton containing the bare variable term:

$$\mathrm{iterStage}(z,L,0) \;=\; \{\mathrm{var}(z)\}.$$

The equality is asserted to hold by definitional unfolding (its proof is rfl) and is registered as a simp lemma. The set $L$ is universally quantified but does not occur on the right-hand side.

iterStage_succ (theorem)

For every sort $s$, every variable $z \in X_s$, every set $L \subseteq T_s$, and every natural number $i$, the $(i+1)$-st iteration stage satisfies

$$\mathrm{iterStage}(z,L,i+1) \;=\; \mathrm{iterStage}(z,L,i)\ \cup\ \mathrm{substP}\big(z,\ \mathrm{iterStage}(z,L,i),\ s,\ L\big),$$

where $\mathrm{substP}(z,M,s,L) = \bigcup_{P \in L} \Phi_{z,M}(P)$, $\Phi_{z,M}(P)$ is the set of all terms produced from $P$ by replacing each occurrence of the variable $z$ with an independently chosen element of $M$ (all other variables untouched), and here $M = \mathrm{iterStage}(z,L,i)$. Equivalently: stage $i+1$ is stage $i$ together with every result of substituting elements of stage $i$ for the occurrences of $z$ in the terms of $L$. The equality is asserted to hold by definitional unfolding (proof rfl). It is quantified over all $i \in \mathbb{N}$, including $i = 0$, in which case it reads $\mathrm{iterStage}(z,L,1) = \{\mathrm{var}(z)\} \cup \bigcup_{P \in L} \Phi_{z,\{\mathrm{var}(z)\}}(P)$.