The subterm order

Setup common to every declaration. A type $S$ is fixed (the sorts); its elements are drawn from universe $u$. A signature $sig$ over $S$ is a family that assigns to every pair $(w, s)$, where $w$ is a finite list of sorts and $s$ is a single sort, a type $sig\;w\;s$ whose elements are operation symbols of input profile $w$ and output sort $s$. An object $X$ of type $\mathrm{SSet}\,S$ is a family assigning to each sort $s$ a type $X_s$ of variables of sort $s$. The type family $\mathrm{Term}\,sig\,X : S \to \mathrm{Type}$ and the type family $\mathrm{TermVec}\,sig\,X : \mathrm{List}\,S \to \mathrm{Type}$ are defined by mutual induction: a term of sort $s$ is either $\mathrm{var}\,x$ for some variable $x : X_s$, or $\mathrm{app}\,\sigma\,ts$ where $\sigma : sig\;w\;s$ is an operation symbol and $ts$ is a term-vector over $w$; a term-vector over a list is either $\mathrm{nil}$ (over the empty list $[]$) or $\mathrm{cons}\,p\,ps$ (over $s :: w$), formed from a term $p$ of sort $s$ and a term-vector $ps$ over $w$. In the file, $sig$ and $X$ are implicit parameters of every declaration below (except where re-declared explicitly).

$\mathrm{STerm}$. Given an explicit signature $sig$ over $S$ and an explicit variable family $X : \mathrm{SSet}\,S$, the type $\mathrm{STerm}\,sig\,X$ is defined to be the dependent sum

$$\mathrm{STerm}\,sig\,X \;:=\; \sum_{s : S} \mathrm{Term}\,sig\,X\,s,$$

that is, the type of pairs $\langle s, t\rangle$ consisting of a sort $s : S$ together with a term $t$ of sort $s$ (over signature $sig$ with variables in $X$). It is placed in universe $u$. For an element $a : \mathrm{STerm}\,sig\,X$, its first component $a_1 : S$ is the sort and its second component $a_2 : \mathrm{Term}\,sig\,X\,a_1$ is the term.

$\mathrm{TermVec.Mem}$. This defines, for the fixed $S$, $sig$, $X$, an inductive proposition-valued relation. Its full argument list is: an implicit sort $t : S$, an implicit list of sorts $w : \mathrm{List}\,S$, an (explicit) term $p$ of sort $t$, and an (explicit) term-vector $ps$ over $w$; the statement $\mathrm{TermVec.Mem}\,p\,ps$ asserts that $p$ occurs as an entry of the term-vector $ps$. It is generated by exactly two constructors:

• head: for every sort $t$, every list $w$, every term $p$ of sort $t$, and every term-vector $ps$ over $w$, one has $\mathrm{TermVec.Mem}\,p\,(\mathrm{cons}\,p\,ps)$ — the vector obtained by prepending $p$ (the same term $p$, so this is the strict/heterogeneous equality forced by the constructor) to $ps$, which is a term-vector over $t :: w$.
• tail: for all sorts $t, s$, every list $w$, every term $p$ of sort $t$ (implicit), every term $q$ of sort $s$ (explicit), and every term-vector $ps$ over $w$ (implicit), if $\mathrm{TermVec.Mem}\,p\,ps$ holds then $\mathrm{TermVec.Mem}\,p\,(\mathrm{cons}\,q\,ps)$ holds, where $\mathrm{cons}\,q\,ps$ is a term-vector over $s :: w$.

In particular no term is a member of $\mathrm{nil}$, and membership of $p$ (of sort $t$) in a vector over $w$ is derivable only when $t$ actually occurs among the sorts listed in $w$ at a position holding a term equal to $p$.

$\mathrm{ImmSub}$. For two sorted terms $a, b : \mathrm{STerm}\,sig\,X$, the proposition $\mathrm{ImmSub}\,a\,b$ ("$a$ is an immediate subterm of $b$") is defined to hold iff there exist a list of sorts $w : \mathrm{List}\,S$, an operation symbol $\sigma : sig\;w\;b_1$ (input profile $w$, output sort equal to the sort $b_1$ of $b$), and a term-vector $ts$ over $w$, such that both:

$$b_2 = \mathrm{app}\,\sigma\,ts \qquad\text{and}\qquad \mathrm{TermVec.Mem}\,a_2\,ts.$$

The first conjunct is an equality of terms of sort $b_1$ stating that the term component of $b$ is literally the application of $\sigma$ to $ts$; the second conjunct states that the term component $a_2$ of $a$ (a term of sort $a_1$) occurs as an entry of the vector $ts$. Nothing constrains $a_1$ except through this membership. If $b_2$ is a variable, or an application whose argument vector is $\mathrm{nil}$, then no such $\sigma, ts$ with a member exist and $\mathrm{ImmSub}\,a\,b$ is false for every $a$.

$\mathrm{SubtermLT}$. For sorted terms $a, b : \mathrm{STerm}\,sig\,X$, the proposition $\mathrm{SubtermLT}\,a\,b$ is defined to be the transitive closure $\mathrm{TransGen}\,\mathrm{ImmSub}\,a\,b$ of the relation $\mathrm{ImmSub}$: there is a finite chain $a = c_0, c_1, \dots, c_n = b$ with $n \ge 1$ and $\mathrm{ImmSub}\,c_{i}\,c_{i+1}$ for each $0 \le i < n$. At least one $\mathrm{ImmSub}$ step is required; this relation is not reflexive.

$\mathrm{SubtermLE}$. For sorted terms $a, b : \mathrm{STerm}\,sig\,X$, the proposition $\mathrm{SubtermLE}\,a\,b$ is defined to be the reflexive–transitive closure $\mathrm{ReflTransGen}\,\mathrm{ImmSub}\,a\,b$ of the relation $\mathrm{ImmSub}$: either $a = b$, or there is a finite chain of one or more $\mathrm{ImmSub}$ steps from $a$ to $b$. Equivalently, a chain of zero or more $\mathrm{ImmSub}$ steps connects $a$ to $b$.

$\mathrm{Min}$. For a sorted term $b : \mathrm{STerm}\,sig\,X$, the proposition $\mathrm{Min}\,b$ is defined as

$$\forall\, a : \mathrm{STerm}\,sig\,X,\;\; \neg\,\mathrm{ImmSub}\,a\,b,$$

i.e. no sorted term $a$ is an immediate subterm of $b$. Given the definition of $\mathrm{ImmSub}$, this holds exactly when the term component $b_2$ of $b$ is a variable, or is an application $\mathrm{app}\,\sigma\,ts$ whose argument term-vector $ts$ has no entries (is $\mathrm{nil}$).

$\mathrm{Subt}$. Given an implicit sort $s : S$ and a term $P$ of sort $s$, the object $\mathrm{Subt}\,P$ has type $\mathrm{SSub}\,(\mathrm{Term}\,sig\,X)$, which unfolds to $(t : S) \to \mathrm{Set}\,(\mathrm{Term}\,sig\,X\,t)$: an $S$-indexed family of sets of terms. It is defined by

$$\mathrm{Subt}\,P \;:=\; \lambda t.\; \{\, Q : \mathrm{Term}\,sig\,X\,t \;\mid\; \mathrm{SubtermLE}\,\langle t, Q\rangle\,\langle s, P\rangle \,\},$$

that is, for each sort $t$, the set of all terms $Q$ of sort $t$ such that the sorted term $\langle t, Q\rangle$ stands in the relation $\mathrm{SubtermLE}$ to the sorted term $\langle s, P\rangle$ — i.e. $\langle t, Q\rangle$ is reachable from... reachable to $\langle s, P\rangle$ by zero or more $\mathrm{ImmSub}$ steps (a non-strict subterm of $P$, allowing $Q = P$ when $t = s$).