Lemma 3.25: substitution composition inclusion

Proved

MSKleene.subst_comp

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

formal-languagesmany-sorted-algebratree-automatauniversal-algebra

Substitution composition inclusion (Lemma 3.25).

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

Preamble

import Definitions.Def_MSKleene_Subst

Formal statement

namespace MSKleene

/-- **Substitution composition inclusion** (Lemma 3.25).

For `z ∈ X_u`, languages `L, L' ⊆ T_Σ(X)_u`, and `K ⊆ T_Σ(X)_s`,
`⟨z/⟨z/L⟩^♯ᵖ_u(L')⟩^♯ᵖ_s(K) ⊆ ⟨z/L⟩^♯ᵖ_s(⟨z/L'⟩^♯ᵖ_s(K))`. -/
theorem subst_comp {S : Type} (sig : Signature S) (X : SSet S) {u s : S}
    (z : X u) (L L' : Set (Term sig X u)) (K : Set (Term sig X s)) :
    substP z (substP z L u L') s K ⊆ substP z L s (substP z L' s K) := 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

\text{Fix a type } S \text{ of \textbf{sorts} in the lowest universe } (S : \mathrm{Type}_0).

The data of the statement are: a signature $\mathrm{sig} : \mathrm{List}\,S \to S \to \mathrm{Type}$ , assigning to every input word $w \in \mathrm{List}\,S$ and output sort $s$ a type $\mathrm{sig}(w,s)$ of operation symbols; an $S$ -indexed family of variable types $X : S \to \mathrm{Type}$ ; two implicit sorts $u, s \in S$ ; a single distinguished variable $z \in X_u$ of sort $u$ ; two sets $L, L' \subseteq \mathrm{Term}(\mathrm{sig}, X, u)$ of sort- $u$ terms; and a set $K \subseteq \mathrm{Term}(\mathrm{sig}, X, s)$ of sort- $s$ terms. Here $\mathrm{Term}(\mathrm{sig}, X, t)$ is the type of sort- $t$ terms, generated (mutually with sorted finite tuples of terms) by injecting a variable $x \in X_t$ as a term and by applying an operation symbol $\sigma \in \mathrm{sig}(w,t)$ to a length- $w$ vector of terms of the matching sorts. For the variable $z \in X_u$ and a set $L \subseteq \mathrm{Term}(\mathrm{sig},X,u)$ , define a nondeterministic substitution operator as follows: it is the (classically defined) algebra homomorphism from the term algebra into the power algebra of the term algebra — the algebra whose carrier at sort $t$ is $\mathrm{Set}\big(\mathrm{Term}(\mathrm{sig},X,t)\big)$ and whose operation $\sigma$ sends a tuple of sets to the set of all $\sigma$ -applications formed by choosing one representative from each argument set independently — determined by the assignment that sends the variable $z$ (of sort $u$ ) to the entire set $L$ and sends every other variable $y$ of any sort $t'$ (whether $t' \neq u$ , or $t' = u$ but $y \neq z$ , equality of variables being decided classically) to the singleton set $\{y\}$ ; writing $\mathrm{sub}_{z,L}(P) \subseteq \mathrm{Term}(\mathrm{sig},X,t)$ for the value of this homomorphism at a term $P \in \mathrm{Term}(\mathrm{sig},X,t)$ , it is concretely the set of all terms obtained from $P$ by replacing each leaf occurrence of $z$ independently by some element of $L$ while leaving all other variables fixed and without recursing into the substituted terms, so that $\mathrm{sub}_{z,L}(P) = \{P\}$ when $z$ does not occur in $P$ , and $\mathrm{sub}_{z,L}(P) = \varnothing$ when $z$ occurs in $P$ but $L = \varnothing$ . Then, for an explicitly given target sort $s$ and a set $K \subseteq \mathrm{Term}(\mathrm{sig},X,s)$ , set

\mathrm{subP}^{s}_{z,L}(K) \;=\; \bigcup_{P \in K} \mathrm{sub}_{z,L}(P) \;\subseteq\; \mathrm{Term}(\mathrm{sig},X,s),

which is $\varnothing$ when $K = \varnothing$ ; the sort $u$ of the substituted variable is an implicit argument recovered from $z$ , whereas the superscript sort is passed explicitly and pins down the common sort of the input set and of the result. The theorem asserts the single set inclusion

\mathrm{subP}^{s}_{\,z,\ \mathrm{subP}^{u}_{z,L}(L')}(K) \;\subseteq\; \mathrm{subP}^{s}_{z,L}\!\Big(\mathrm{subP}^{s}_{z,L'}(K)\Big),

where on the left one first forms $\mathrm{subP}^{u}_{z,L}(L') = \bigcup_{P \in L'} \mathrm{sub}_{z,L}(P) \subseteq \mathrm{Term}(\mathrm{sig},X,u)$ (substituting $z$ by elements of $L$ throughout the members of $L'$ , at target sort $u$ ) and then uses that set as the replacement set for a single substitution of $z$ into the members of $K$ ; and on the right one first substitutes $z$ by elements of $L'$ throughout the members of $K$ (at sort $s$ ) and then substitutes $z$ by elements of $L$ throughout the members of that intermediate result. In words: the set of terms produced by rewriting each occurrence of $z$ in some element of $K$ by a single element of the pre-composed set " $L'$ with $z$ replaced by $L$ " is contained in the set produced by two successive sweeps, first $z := L'$ over $K$ and then $z := L$ over the outcome. The quantified data $L$ , $L'$ , $K$ (together with the sorts $u, s$ , the variable $z$ , the signature $\mathrm{sig}$ , and the family $X$ ) are arbitrary, with no finiteness, nonemptiness, or occurrence hypotheses imposed; hence the degenerate cases $K = \varnothing$ (both sides equal $\varnothing$ ), $L' = \varnothing$ , and $L = \varnothing$ all fall under the claim, as does the case where members of $L$ or $L'$ themselves contain the variable $z$ (on the left such residual occurrences are left untouched by the outer single-pass substitution, whereas on the right they are exposed to the second substitution pass). The assertion is exactly this $\subseteq$ , not an equality and not the reverse inclusion.

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