Proposition 3.4: unique readability of terms

Proved

MSKleene.term_char

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

formal-languagesmany-sorted-algebratree-automatauniversal-algebra

Unique readability of terms (Proposition 3.4).

For every sort $s\in S$ and every $P\in\mathrm{T}_{\Sigma}(X)_{s}$ , exactly one of the following holds, and the data is unique in each case: (1) $P=x$ for a unique variable $x\in X_{s}$ ; (2) $P=\sigma^{\mathbf{T}_{\Sigma}(X)}$ for a unique constant symbol $\sigma\in\Sigma_{\lambda,s}$ ; (3) $P=\sigma^{\mathbf{T}_{\Sigma}(X)}((P_{j})_{j})$ for a unique non-empty arity $\mathbf{s}$ , a unique $\sigma\in\Sigma_{\mathbf{s},s}$ , and a unique family $(P_{j})_{j}$ .

Preamble

import Definitions.Def_MSKleene_Term

Formal statement

namespace MSKleene

/-- **Unique readability of terms** (Proposition 3.4).

For every sort `s` and every term `P ∈ T_Σ(X)_s`, there is a unique
decomposition belonging to exactly one of the following cases:
1. `P = var x` for a unique variable `x ∈ X_s`;
2. `P = app σ .nil` for a unique constant symbol `σ ∈ Σ_{[],s}`;
3. `P = app σ ts` for a unique non-empty arity `w`, a unique `σ ∈ Σ_{w,s}`, and
   a unique argument vector `ts`. -/
theorem term_char {S : Type} (sig : Signature S) (X : SSet S) {s : S}
    (P : Term sig X s) :
    ∃! c : X s ⊕ (sig [] s ⊕ ((w : List S) × sig w s × TermVec sig X w)),
      match c with
      | .inl x => P = Term.var x
      | .inr (.inl σ) => P = Term.app σ TermVec.nil
      | .inr (.inr p) => p.1 ≠ [] ∧ P = Term.app p.2.1 p.2.2 := 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 · gpt-5

For every type $S$ of sorts, every $S$ -sorted signature $\Sigma$ assigning a type $\Sigma_{w,s}$ of operation symbols to each finite list $w$ of input sorts and output sort $s$ , every $S$ -indexed family $X=(X_s)_{s\in S}$ , every sort $s\in S$ , and every term $P$ of sort $s$ , there exists exactly one tagged datum

c\in X_s\;\sqcup\!\left(\Sigma_{[],s}\;\sqcup\!\coprod_{w:\operatorname{List}(S)} \bigl(\Sigma_{w,s}\times \operatorname{TermVec}_{\Sigma,X}(w)\bigr)\right)

satisfying its corresponding condition: if $c$ is tagged as a variable $x\in X_s$ , then $P=\operatorname{var}(x)$ ; if $c$ is tagged as a nullary symbol $\sigma\in\Sigma_{[],s}$ , then $P=\operatorname{app}(\sigma,\operatorname{nil})$ ; and if $c$ is tagged as $(w,\sigma,\vec t)$ , where $\sigma\in\Sigma_{w,s}$ and $\vec t$ is a heterogeneous vector containing one term of each successive sort in $w$ , then $w\ne[]$ and $P=\operatorname{app}(\sigma,\vec t)$ . Here terms are generated inductively from variables and applications, and term vectors are generated from the empty vector and by prepending a term of the required sort. No finiteness, nonemptiness, or decidable-equality assumption is imposed on $S$ , $\Sigma$ , or $X$ ; empty components and empty collections of symbols are therefore included wherever the supplied term $P$ permits them.

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