Read-back: MSKleene.subterm_wf

Fix an arbitrary type $S$ (its inhabitants are called sorts), an arbitrary family $\Sigma$ assigning to every pair consisting of a finite list $w$ of sorts and a single sort $s$ a type $\Sigma(w,s)$ (the operation symbols of argument profile $w$ and result sort $s$; formally $\mathrm{sig} : \mathrm{List}\,S \to S \to \mathrm{Type}$), and an arbitrary family $X$ assigning to every sort $s$ a type $X_s$ (the variables of sort $s$; formally $X : S \to \mathrm{Type}$). Here $S$ is an implicit parameter while $\Sigma$ and $X$ are explicit; the theorem asserts the statement below for every such $S$, $\Sigma$, $X$. Over this data one has the mutually inductively defined families $\mathrm{Term}(s)$ (terms of sort $s$) and $\mathrm{TermVec}(w)$ (term-vectors of profile $w$), whose constructors are: $\mathrm{var}(x) \in \mathrm{Term}(s)$ for each $x \in X_s$; $\mathrm{app}(\sigma,\vec t\,) \in \mathrm{Term}(s)$ for each list $w$, each $\sigma \in \Sigma(w,s)$ and each $\vec t \in \mathrm{TermVec}(w)$; $\mathrm{nil} \in \mathrm{TermVec}([\,])$; and $\mathrm{cons}(t,\vec r\,) \in \mathrm{TermVec}(s :: w)$ for each $t \in \mathrm{Term}(s)$ and $\vec r \in \mathrm{TermVec}(w)$. Let

be the type of dependent pairs $b = (b_1, b_2)$ with $b_1 \in S$ a sort and $b_2 \in \mathrm{Term}(b_1)$ a term of that sort (a sorted term). Write $p \in \vec{ts}$ for the inductively defined membership predicate on term-vectors: $p \in \mathrm{cons}(p,\vec{ps})$ always holds (this base case requires $p$ to be literally the head entry and of the same sort as the head), and $p \in \mathrm{cons}(q,\vec{ps})$ holds whenever $p \in \vec{ps}$ (regardless of the head $q$). Define the immediate-subterm relation $\mathrm{ImmSub}(a,b)$ on $\mathrm{STerm}$ to hold iff

the first equation being an equation in the (dependent) type $\mathrm{Term}(b_1)$; note the sort $a_1$ of $a$ is not constrained beyond being whatever sort makes $a_2$ occur in $\vec{ts}$. Define $\mathrm{SubtermLT}(a,b)$ to be the transitive closure of $\mathrm{ImmSub}$, i.e. there is a finite chain $a = c_0,\, c_1,\, \dots,\, c_n = b$ with $n \ge 1$ and $\mathrm{ImmSub}(c_{i-1}, c_i)$ for every $i \in \{1,\dots,n\}$ (at least one step; reflexivity is not included). Define $\mathrm{Min}(b)$ to hold iff $\ \forall\, a \in \mathrm{STerm},\ \neg\, \mathrm{ImmSub}(a,b)$, i.e. no sorted term is an immediate subterm of $b$.

The theorem asserts the conjunction of the following two statements.

(1) The relation $\mathrm{SubtermLT}$ on $\mathrm{STerm}$ is well-founded: every element of $\mathrm{STerm}$ is accessible for $\mathrm{SubtermLT}$; equivalently, there is no infinite sequence $(a_k)_{k \in \mathbb{N}}$ of sorted terms with $\mathrm{SubtermLT}(a_{k+1}, a_k)$ for all $k$ (no infinitely descending chain of proper subterms), and equivalently every non-empty predicate on $\mathrm{STerm}$ has a $\mathrm{SubtermLT}$-minimal element.

(2) For every sorted term $b \in \mathrm{STerm}$,

both equalities being equalities in $\mathrm{Term}(b_1)$; that is, $b$ has no immediate subterm exactly when its term component is either a variable of sort $b_1$, or an operation symbol whose argument profile is the empty list and whose result sort is $b_1$, applied to the empty term-vector (a nullary/constant application). This is a genuine biconditional in both directions.

Degenerate cases the quantifiers silently include: if $S$ is empty then $\mathrm{STerm}$ is empty, so $\mathrm{SubtermLT}$ is well-founded vacuously and the universally quantified biconditional in (2) holds vacuously; more generally, for any $b$ for which neither disjunct on the right of (2) is satisfiable (for instance when $X_{b_1}$ and $\Sigma([\,],b_1)$ are both empty, or when $b_2$ has the form $\mathrm{app}(\sigma,\vec{ts})$ that matches neither shape), statement (2) forces $\neg\,\mathrm{Min}(b)$. The types $X_s$ and $\Sigma(w,s)$ are permitted to be empty or infinite; no finiteness, decidability, or non-emptiness hypotheses are imposed on $S$, $\Sigma$, or $X$.