Lemma 3.28: iteration absorption

Proved

MSKleene.iter_absorb

by Cosme · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

formal-languagesmany-sorted-algebratree-automatauniversal-algebra

Iteration absorption (Lemma 3.28).

Let $s\in S$ , $z\in X_{s}$ , $L\subseteq\mathrm{T}_{\Sigma}(X)_{s}$ . Then $\left(\!\begin{smallmatrix}z\\L^{\star z}\end{smallmatrix}\!\right)^{\sharp\mathsf{p}}_{s}(L)\subseteq L^{\star z}$ .

Preamble

import Definitions.Def_MSKleene_Iteration

Formal statement

namespace MSKleene

/-- **Iteration absorption** (Lemma 3.28).

For `z ∈ X_s` and a language `L ⊆ T_Σ(X)_s`,
`⟨z/L^{⋆z}⟩^♯ᵖ_s(L) ⊆ L^{⋆z}`. -/
theorem iter_absorb {S : Type} (sig : Signature S) (X : SSet S) {s : S}
    (z : X s) (L : Set (Term sig X s)) :
    substP z (iterate z L) s L ⊆ iterate z L := by
  sorry

end MSKleene

Source

Gong, Ruiz Mora, Sanmartín Vich, Cosme Llópez, "A Kleene theorem for free many-sorted algebras", 2026

Read-back

What the Lean code literally says, in plain math · claude-sonnet-5

Read-back of `MSKleene.iter_absorb`

Fix a type $S$ (a set of sorts), an $S$ -sorted signature $\mathrm{sig}$ — a family assigning to each finite word $w\in\mathrm{List}(S)$ and each sort $s\in S$ a type $\mathrm{sig}(w,s)$ of operation symbols of arity $w$ and result sort $s$ — and an $S$ -indexed family of variable types $X=(X_s)_{s\in S}$ . Let $\mathrm{Term}_{\mathrm{sig},X}(r)$ denote the terms of sort $r$ built from these variables and symbols: each $x\in X_r$ yields a term $\mathrm{var}(x)$ , and each $\sigma\in\mathrm{sig}(w,r)$ applied to a length-matching tuple of subterms yields a term $\sigma(t_1,\dots,t_n)$ . The theorem further fixes a sort $s\in S$ , a distinguished variable $z\in X_s$ , and an arbitrary set $L\subseteq\mathrm{Term}_{\mathrm{sig},X}(s)$ of terms of sort $s$ . Here $\mathrm{sig}$ and $X$ are explicit parameters, $s$ is implicit, and $z,L$ are explicit; there are no typeclass assumptions or other hypotheses.

For any set $M\subseteq\mathrm{Term}_{\mathrm{sig},X}(s)$ , define a set-valued substitution operator $\theta_{z,M}$ , acting on a term $P$ of sort $r$ and returning a subset $\theta_{z,M}(P)\subseteq\mathrm{Term}_{\mathrm{sig},X}(r)$ , as the structural (homomorphic) extension of the variable assignment " $z\mapsto M$ , and every other variable $y$ of any sort $\mapsto\{\mathrm{var}(y)\}$ ", i.e. recursively

\theta_{z,M}(\mathrm{var}(y))= \begin{cases} M & \text{if } r=s \text{ and } y=z,\\[2pt] \{\mathrm{var}(y)\} & \text{otherwise,} \end{cases} \qquad \theta_{z,M}\big(\sigma(t_1,\dots,t_n)\big)=\big\{\,\sigma(u_1,\dots,u_n)\ \big|\ u_j\in\theta_{z,M}(t_j)\ \text{for each } j\,\big\}.

Thus $\theta_{z,M}(P)$ is the set of all terms obtained from $P$ by replacing every occurrence of the variable $z$ — independently at each occurrence — by some element of $M$ , leaving all other variables untouched. For a set $K\subseteq\mathrm{Term}_{\mathrm{sig},X}(s)$ put

\mathrm{substP}(z,M,K)\ =\ \bigcup_{P\in K}\theta_{z,M}(P)\ \subseteq\ \mathrm{Term}_{\mathrm{sig},X}(s).

Define sets $I_i\subseteq\mathrm{Term}_{\mathrm{sig},X}(s)$ for $i\in\mathbb{N}$ by

I_0=\{\mathrm{var}(z)\},\qquad I_{i+1}=I_i\ \cup\ \mathrm{substP}(z,\ I_i,\ L),

so that $I_{i+1}$ adjoins to $I_i$ every term obtained from a term of $L$ by replacing each occurrence of $z$ by some element of $I_i$ ; and set

\mathrm{iterate}(z,L)\ =\ \bigcup_{i\in\mathbb{N}} I_i .

The theorem asserts exactly the one set inclusion

\mathrm{substP}\big(z,\ \mathrm{iterate}(z,L),\ L\big)\ \subseteq\ \mathrm{iterate}(z,L),

equivalently: for every term $P\in L$ and every term $u\in\theta_{z,\,\mathrm{iterate}(z,L)}(P)$ — i.e. every $u$ gotten from $P$ by substituting, independently at each occurrence of $z$ , some element of $\mathrm{iterate}(z,L)$ — one has $u\in I_i$ for some $i\in\mathbb{N}$ .

Edge cases folded into the quantifiers: if $L=\varnothing$ the left-hand side is the empty union $\varnothing$ and the inclusion holds vacuously (and then $\mathrm{iterate}(z,L)=\{\mathrm{var}(z)\}$ ); the union defining $\mathrm{iterate}$ includes the index $i=0$ , so $\mathrm{var}(z)\in\mathrm{iterate}(z,L)$ always; a term $P\in L$ in which $z$ does not occur satisfies $\theta_{z,M}(P)=\{P\}$ and hence contributes $P$ itself to the left-hand side; and $S$ is necessarily inhabited because $s\in S$ is supplied.

Human review

Endorsed by Shuze Chen · Sep 9, 2026
Endorsed by Cosme · Sep 9, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Lemma 3.28: iteration absorption

Read-back of MSKleene.iter_absorb

Read-back of `MSKleene.iter_absorb`