2.1 Signatures, terms, and term algebras

A signature is a finite set F of function symbols that come with a nonnegative integer n, called arity, which is assigned to each member f of F. f is an n-ary function symbol. The subset of n-ary function symbols in F is denoted by $F_{n}$ . An algebra of type F is an ordered pair $\mathfrak{A}$ = $\langle A,F\rangle$ , where A is a nonempty set and F is a family of finitary operations on A indexed by the signature F such that corresponding to each n-ary function symbol f in $F_{n}$ there is an n-ary operation $f^{A}$ on A. The set A is called the carrier of the algebra.

Let X be a set of (distinct) variables. Let F be a signature. The set T(F,X) of (syntactic) terms of F over X is the smallest set

1. (i) comprising X and $F_{0}$ and

2. (ii) if $t_{1},\ldots,t_{n}$ in T(F,X) and f in $F_{n}$ , then $f(t_{1},\ldots,t_{n})$ in T(F,X)

The set of variable-free terms are called ground terms. The set of variables occurring in a term t is denoted by $\mathbf{Var}(t)$ . The set of subterms of a term $f(t_{1},\ldots,t_{n})$ contains the term itself and is closed recursively by containing $t_{1},\ldots,t_{n}$ . It is denoted by $\mathbf{Sub}(t)$ .

The set of terms can be given an algebraic structure called term algebra as usual.

2.2 Substitutions

A substitution is a (unique) homomorphism in the term algebra generated by a mapping $\sigma:X\longrightarrow T(F,X)$ from a finite set of variables to terms. Substitutions are generally denoted by small Greek letters $\alpha,\beta,\gamma,\sigma$ , etc. and they are represented explicitly as a function by a set of variable bindings $\sigma=\{x_{1}\mapsto s_{1},\ldots,x_{m}\mapsto s_{m}\}$ . $\mathcal{S}_{F,X}$ denotes the set of all substitutions. The application of the substitution $\sigma$ to a term t, denoted $t\sigma$ , is defined by induction on the structure of terms

The substitution $\varepsilon=\{\}$ with $t\varepsilon=t$ for all terms t in T(F,X) is called the identity. A substitution $\sigma=\{x_{1}\mapsto s_{1},\ldots,x_{m}\mapsto s_{m}\}$ has the finite domain:

The range of the substitution $\sigma$ is the set of terms

The set of variables occurring in the range is $\textbf{VRan}(\sigma)\;:=\;\textbf{Var}(\textbf{Ran}(\sigma))$ and $\textbf{Var}(\sigma)=\textbf{Dom}(\sigma)\cup\textbf{VRan}(\sigma)$ . The restriction of a substitution $\sigma$ to a set of variables $Y\subseteq X$ , denoted by $\sigma_{|Y}$ , is the substitution which is equal to the identity everywhere except over $Y\cap\textbf{Dom}(\sigma)$ , where it is equal to $\sigma$ . The composition of two substitutions $\sigma$ and $\theta$ is written $\sigma\circ\theta$ (to emphasize the composition) or just as $\sigma\theta$ . The application is defined by $t\sigma\theta=(t\sigma)\theta$ . This is fine if $\sigma\theta$ has no contradictory variable bindings, otherwise there are several solutions proposed in the literature which solve this problem and preserve functional composition, see, for example, Baader and Nipkow (1988) and Baader and Snyder (Reference Baader and Snyder2001).

Relations such as $=,\geq,\ldots$ between substitutions sometimes hold only if they are restricted to a certain set of variables V. A relation R which is restricted to V is denoted as $R^{V}$ , and defined as $\sigma R^{V}\tau\Longleftrightarrow x\sigma Rx\tau$ for all x in V. Two substitutions $\sigma$ and $\theta$ are equal, denoted $\sigma=\theta$ iff $x\sigma=x\theta$ for every variable x; they are equal restricted to V, x $\sigma$ $=^{V}\textit{x}\theta$ , iff $x\sigma=x\theta$ for all variables x in V.

2.3 Congruences and equations

An equivalence relation $\Theta$ on the underlying set (the carrier) of an algebra of type F is a congruence, if for each n-ary function symbol f in F and elements $a_{i},b_{i}$ of A, for all i in $1\leq i\leq n$ we have

The quotient algebra is the algebra whose carrier are the equivalence classes $A/\Theta$ and whose operations satisfy

We are interested in quotient algebras, where the congruence is defined by a set of equations E, which is denoted as $=_{E}$ . For a term t in T(F,X) and the congruence E the equivalence class of t is denoted as $[t]_{E}$ .

2.4 Ordering

Our main interest in this paper is to investigate if the set of most general, minimal, and complete unifiers $\varphi U\Sigma_{E}(\Gamma)$ exists under certain conditions and the main technique for showing this result is based on orderings, in particular on well-quasi-orderings.

A term t is (syntactically) an instance of a term s, if $s\sigma=t$ for some substitution $\sigma$ . We also say s subsumes t and this relation is a quasi-order. It is called the subsumption order on terms.

A term t (syntactically) encompasses a term s, if an instance of s is a subterm of t. Encompassment conveys the notion that s appears in t with some context “above” (in tree notation) and a substitution instance “below.” We say t encompasses s or s is encompassed by t. In particular, encompassment is called strict encompassment, if $s\sigma$ is a proper subterm of t.

A term s is homeomorphically embedded into t iff s can be obtained from t by erasing some “parts” in t. We usually abbreviate homeomorphical embedding just to embedding. Embedment conveys the notion that the structure of s and some corresponding symbols appear within t. A term s is instance-embedded into t, we also say it is $\lambda$ -embedded into t, iff an instance of s, that is $s\lambda$ , is embedded into t. This is the main notion of this paper, which we will generalize to embedment of substitutions later on.

More formally, we have the following orders on terms. Footnote ²

1. (1) A term s is a subterm of t if $s\in\textbf{Sub}(t)$ and we denote this by $s\preceq t$ . If s is a proper subterm of t, we write $s\prec t$ .

2. (2) A term s subsumes t, denoted $s\leq t$ , iff there exists a substitution $\sigma$ with $s\sigma=t$

3. (3) A term s is encompassed by t, denoted $s\sqsubseteq t$ , iff there exists a substitution $\sigma$ such that $s\sigma\in\textbf{Sub}(t)$ .

4. (4) A term s is embedded into a term t, denoted $s\trianglelefteq t$ , if $s=t$ or s is embedded into an argument of t or the argument terms of s and t embed, respectively:

   \[s\trianglelefteq t\,\iff\left\{ \begin{array}{ll}s=t,\:\textrm{or}\\t=f(t_{1},\ldots,t_{n})\;\textrm{and}\;\textrm{for}\;\textrm{some}\;i,\;1\leq i\leq n:\:s\trianglelefteq t_{i},\:\textrm{or}\\t=f(t_{1},\,.\,.\,.,t_{n}),\:s=f(s_{1},.\,.\,.,s_{n})\\\:\;\:\;\:\;\:\;\:\textrm{and}\:\;\forall i:\:s_{i}\trianglelefteq t_{i},\:1\leq i\leq n.\end{array}\right.\]
   We denote strictly embedding by $s\vartriangleleft t$ if s and t are not equal.

We also say that t embeds s, $t\trianglerighteq s$ , and use it either way depending on the context. Embedding is of practical interest, notably in term rewriting systems and logic programming languages, where it is used in termination proofs. Sometimes an equivalent definition is used in these fields based on a reduction system:

$\mathcal{R_{\textrm{F}}}\;:=\;\{f(x_{1},....x_{n})\longrightarrow x_{i}:\;n\geq1,\;f\in F_{n}\subseteq\Sigma,\;for\;i,\;1\leq i\leq n\}$ .

The following Proposition states a well-known fact, see, for example, Dershowitz and Jouannaud (Reference Dershowitz and Jouannaud1991) and Baader and Nipkow (1988).

The next definition for embedding involves instances of terms.

Some remarks: embedding implies $\lambda$ -embedding, but $\lambda$ -embedding does not necessarily imply embedding.

if $s\trianglelefteq t$ , then s is $\lambda$ -embedded into t, $s\varepsilon\trianglelefteq t$ , with the empty substitution $\varepsilon$ .

Otherwise:

does not imply $s\trianglelefteq t$ , for example, $s=f(a,x)$ and

$t=f(g(a,b),\,f(b,h(a)))$ and $\lambda=\{x\mapsto a\}$ . We have

,

because $s\lambda\trianglelefteq t$ ,

but $s\ntrianglelefteq t$ since $s=f(a,x)\ntrianglelefteq f(g(a,b),\,f(b,h(a)))=t$ .

These standard order relations are now extended to equality modulo E for the congruences induced by the equations in E.

1. (1) A term s is a subterm of t modulo E, denoted $s\preceq_{E}t$ , iff there exists an $s'=_{E}s$ and a term $t'=_{E}t$ such that $s'\preceq t'$ . We say s is an E-subterm of t.

2. (2) A term s subsumes t modulo E, $s\leqslant_{E}t$ , iff there exists a substitution $\sigma$ with $s\sigma=_{E}t$ . We say s E-subsumes t.

3. (3) A term s is encompassed by t modulo E, $s\sqsubseteq_{E}t$ iff there is a substitution $\sigma$ such that $s\sigma\preceq_{E}t$ . We say s is E-encompassed by t.

The subterm and the encompassment order are quasi-orders (reflexive and transitive). Fortunately, the extension to E-subterm and E-encompassment order preserves transitivity, so they are quasi-orders too:

Transitivity: for terms r,s,t if $r\preceq_{E}s,\:s\preceq_{E}t\Longrightarrow r\preceq_{E}t$ .

$r\preceq_{E}s\Longrightarrow\exists r'\in[r]_{E},s'\in[s]_{E}:r'\preceq s'$ and

$s\preceq_{E}t\Longrightarrow\exists s''\in[s]_{E},t''\in[t]_{E}:s''\preceq t''$ . Now because

$s''=_{E}s'$ we get a new term t’ from t” by replacing s” by s’.

And then we have $s'\preceq t'$ .

That is: $r'\preceq s'\preceq t'$ and transitivity of $\preceq$ yields $r'\preceq t'$ .

Hence, $r=_{E}r'\preceq t'=_{E}t\Longrightarrow r\preceq_{E}t$ .

The important observation for the following is that the term r’ in the above proof is not necessarily a subterm of t’. It is a subterm of t’ only when t” is transformed under $=_{E}$ into t’. This property is not valid for E-embedding and hence transitivity does not hold for this and other reasons. Thus, we cannot prove its quasi-order property. The reason is that if a term t embeds a term p, then there is not necessarily a $t'\in[t]_{E}$ , such that for a given E-variant of p, $p'\in[p]_{E}$ , t’ $\trianglerighteq_{E}$ p’. To see this and in order to motivate our Definition 10 below, consider the usual method to extend a quasi-order (relation) R to “R modulo E,” which is to take the transitive closure $=_{E}\circ R\circ=_{E}$ . Originally, we used this idea, where E-embedding is defined as: $t\trianglerighteq_{E}s$ iff $t=_{E}s,\:or\:\:\:\exists t'\in[t]_{E},s'\in[s]_{E}:\:t'\trianglerighteq s'$ . The problem is, however, that transitivity, namely: $t\trianglerighteq_{E}s\trianglerighteq_{E}r\Rightarrow t\trianglerighteq_{E}r$ does not hold in this case. Consider the following example:

Let $F=\{f,g,h,a,b,c\}$ be a signature and $E=\{f(b,b)=g(c,h(a))\}$

be an equational theory.

Now consider $t=f(g(b,a),f(b,a))$ and $s=f(b,b)$ and $r=h(a)$ , where

transitivity of $\trianglerighteq_{E}$ : $t\trianglerighteq_{E}s\trianglerighteq_{E}r\Rightarrow t\trianglerighteq_{E}r$ does not hold:

$t\trianglerighteq_{E}s$ because $t\trianglerighteq s$ and $s\trianglerighteq_{E}r$ because $s=_{E}s'=g(c,h(a))\trianglerighteq h(a)=r$ .

But there is no $t'\in[t]_{E}$ and no $r'\in[r]_{E}$ , such that $t'\trianglerighteq r'$ .

Therefore, we propose an enhanced definition for equational embedding by requiring that if an embedded term p of a term t E-embeds a term s, then t also E-embeds s. For our contribution, it is important that this E-embedding, respectively $\lambda_{E}-$ embedding, enhances the comparison of objects (i.e. unifying substitutions) and allows us to use the famous tree-embedding theorem Kruskal (Reference Kruskal1960). This theorem is valid for first-order terms and can be lifted to substitutions and we show later on that it holds for E-embeddings as well. E-embedment, respectively $\lambda_{E}-$ embedment, is then our fundamental tool in the rest of this paper. In the following definition and for the rest of this paper note: if two terms are equal under E, then they are embedment equivalent $\equiv_{E}$ too, because $s=_{E}t$ implies $\exists s'\in[s]_{E}$ and $\exists t'\in[t]$ with $s'=t'$ which implies $s'\trianglelefteq t'$ and $s'\trianglerighteq t'$ , hence $s\equiv_{E}t$ . So we just use $=_{E}$ in the following.

Let $\mathbf{Emb_{E}}$ (t) := $\left\{ p:\;p=_{E}p'\;and\;p'\trianglelefteq t\right\} $ be the set of the closure under E of all embedded terms in t.

The following is the crucial definition in this paper:

In order to show that $t\trianglerighteq_{E}s$ , we can use an E-embedding-chain of the following form:

$t=_{E}t'_{1}\vartriangleright t_{2}=_{E}t'_{2}\vartriangleright t_{3}=_{E}t'_{3}\vartriangleright.....\vartriangleright t_{n}=_{E}s$

where $\vartriangleright$ denotes strict embedding as in Definition 2. We abbreviate this chain as $t\blacktriangleright_{E}^{n}s$ , $n\geq1$ .

Note that this embedding chain has the typical regular structure where = $_{E}$ and $\vartriangleright$ alternate. The $t_{i}$ may be an embedded term as denoted by p in the second line of Definition 10.

$t=_{E}s$ , or there exists a strictly descending chain of the form:

$t=_{E}t_{1}'\vartriangleright t_{2}=_{E}t_{2}'\vartriangleright t_{3}=_{E}t_{3}'\vartriangleright.....\vartriangleright t'_{n}=_{E}s$ , abbreviated as $t\blacktriangleright_{E}^{n}s$ .

$t\blacktriangleright_{E}^{1}s:$ by Definition 10 $\exists t_{1}'\in[t]_{E},\exists s'\in[s]_{E}\;and\;\exists p\in\mathbf{Emb_{E}}(t'):p\vartriangleright s'$ .

Hence, $t=_{E}t_{1}'\vartriangleright s'=_{E}s$ .

$t\blacktriangleright_{E}^{n+1}s$ : that is $t\blacktriangleright_{E}^{n}t_{n}$ and $t_{n}\blacktriangleright_{E}^{1}s$ . By induction hypothesis, we have the chain

$t=_{E}t_{1}'\vartriangleright t_{2}=_{E}t_{2}'\vartriangleright......\vartriangleright t_{n}$ and $t_{n}\blacktriangleright_{E}^{1}s$ with $t_{n}=_{E}t_{n}'\vartriangleright t_{n+1}$ , where $t_{n+1}=s'$ .

So the whole E-embedding-chain is the following:

$t=_{E}t_{1}'\vartriangleright t_{2}=_{E}t_{2}'\vartriangleright t_{3}=_{E}........\vartriangleright t_{n}=_{E}t_{n}'\vartriangleright t_{n+1}=_{E}s$ .

The next definition extends instance-embedding to instance embedding modulo an equational theory E.

The relation E-embedding is recursively defined in Definition 10 and it can be computed using Proposition 4 as follows:

E-embedding Rewrite System, $\mathcal{E_{\textrm{F}}}$ , is defined as $\mathcal{E_{\textrm{F}}}$ := $(\stackrel{*}{\longrightarrow_{\mathcal{R_{\textrm{F}}}}}.\stackrel{*}{\longrightarrow}_{E})$ .

Then for terms s,t: $t\trianglerighteq_{E}s$ iff $\exists t'\in[t]_{E},\exists s'\in[s]_{E}:\:$ $t'\overset{*}{\longrightarrow_{\mathcal{E_{\textrm{F}}}}}s'$ .

That is: there is a finite chain of the form:

$\;\;\;\;+t\stackrel{*}{\longrightarrow_{E}}t'\stackrel{*}{\longrightarrow_{\mathcal{R_{\textrm{F}}}}}t_{1}\stackrel{*}{\longrightarrow_{E}}t'_{1}\stackrel{*}{\longrightarrow_{\mathcal{R_{\textrm{F}}}}}t_{2}....\stackrel{*}{\longrightarrow_{\mathcal{R_{\textrm{F}}}}}t_{n}\stackrel{*}{\longrightarrow_{E}}s$ .

With Definition 10 and Lemma 11, we obtain our first main result:

reflexivity: Because terms embed themselves.

transitivity: $t\trianglerighteq_{E}s\trianglerighteq_{E}r\Longrightarrow t\trianglerighteq_{E}r$ .

By Definition 10 and Lemma 11, we have $t\blacktriangleright_{E}^{m}s$ and $s\blacktriangleright_{E}^{n}r$

that is $t=_{E}t_{1}'\vartriangleright t_{2}=_{E}t_{2}'\vartriangleright t_{3}=_{E}t'_{3}........\vartriangleright t_{m}=_{E}s$ and

$s=_{E}s_{1}'\vartriangleright s_{2}=_{E}s_{2}'\vartriangleright s_{3}=_{E}s'_{3}........\vartriangleright s_{n}=_{E}r$ .

But since $t_{m}=_{E}s_{1}'$ we have the correct chain

$t=_{E}t_{1}'\vartriangleright t_{2}=_{E}t_{2}'\vartriangleright t_{3}=_{E}t_{3}........\vartriangleright t_{m}=_{E}s_{1}'\vartriangleright s_{2}=_{E}s_{2}'\vartriangleright s_{3}=_{E}s'_{3}........\vartriangleright s_{n}=_{E}r$

Hence, $t\blacktriangleright_{E}^{n+m}r$ , which means $t\trianglerighteq_{E}r$ .

The negation of E-subsumption and E-encompassment is obvious: $s\nleq_{E}t$ iff there exists no substitution $\sigma$ with $s\sigma=_{E}t$ and

iff there is no substitution $\sigma$ such that $s\sigma\preceq_{E}t$ . But the notions “not embedded” and “incomparable” with respect to $\trianglelefteq_{E}$ should be made more explicit.

1. (1) A term s is not embedded modulo E into a term t, $s\ntrianglelefteq_{E}t$ , iff for every element s’ of the class $[s]_{E}$ there exists no element t’ of the class $[t]_{E}$ such that $s'\trianglelefteq_{E}t'$ .

2. (2) Terms s and t are incomparable with respect to $\trianglelefteq_{E}$ iff $s\ntrianglelefteq_{E}t$ and $t\ntrianglelefteq_{E}s$ .

3. (3) Terms s and t are incomparable with respect to

   

   iff there exist no substitutions $\lambda_{1}$ and $\lambda_{2}$ with $s\lambda_{1}\trianglelefteq_{E}t$ and $t\lambda_{2}\trianglelefteq_{E}s$ .

We shall lift these orderings modulo E on terms now component-wise to orderings on substitutions in the sense that for all variables in the domain of the substitution we require that the corresponding images fulfill the order relation modulo E.

In the following, let $\sigma,\tau$ be substitutions with $\mathbf{Dom}(\sigma)=\mathbf{Dom}(\tau)\supseteq$ V, where V is some set of variables.

1. (1) A substitution $\sigma$ is a sub-substitution modulo E of $\tau$ restricted to V, denoted as $\sigma\preceq_{E}^{V}\tau$ , if for all x in V, $x\sigma$ is a subterm of $x\tau$ modulo E, that is $x\sigma\preceq_{E}x\tau$ .

2. (2) A substitution $\sigma$ E-subsumes a substitution $\tau$ restricted to V, denoted as $\sigma\leq_{E}^{V}\tau$ , if there exists a substitution $\lambda$ such that $\sigma\lambda=_{E}^{V}\tau$ . The relation $\leq_{E}^{V}$ is called the E-subsumption order for substitutions restricted to V.

We denote E-subsumption equivalence as $\sigma\thicksim_{E}^{V}\tau$ , if $\sigma\leq_{E}^{V}\tau\;and\;\tau\leq_{E}^{V}\sigma$ .

1. (3) A substitution $\sigma$ is E-encompassed by $\tau$ restricted to V, denoted $\sigma\sqsubseteq_{E}^{V}\tau$ , if there exists $\lambda$ , such that $(\sigma\lambda)$ restricted to V is a sub-substitution of $\tau$ modulo E, $\sigma\lambda\preceq_{E}^{V}\tau$ .

We denote E-encompassment equivalence as $\sigma\thickapprox_{E}^{V}\tau$ if $\sigma\sqsubseteq_{E}^{V}\tau\;and\;\tau\sqsubseteq_{E}^{V}\sigma$ .

1. (4) A substitution $\sigma$ is E-embedded into a substitution $\tau$ restricted to V, denoted as $\sigma\trianglelefteq_{E}^{V}\tau$ , iff for all x in V we have $x\sigma\trianglelefteq_{E}^{V}x\tau$ .

2. (5) A substitution $\sigma$ is $\lambda_{E}$ -embedded into a substitution $\tau$ restricted to V, denoted as

   ,

   iff there is a substitution $\lambda$ , such that $\forall x\in V:\:x(\sigma\lambda)$ is E-embedded into $x\tau$ .

The encompassment and embedment order on terms are well known as quasi-orderings, but the modulo E extension to substitutions requires verification.

reflexivity: $\sigma\sqsubseteq_{E}\sigma$ by Definition 16 .3 means $\sigma\lambda\preceq_{E}^{V}\sigma$ , setting $\lambda$ to the

substitution identity $\varepsilon$ we have $\sigma=_{E}\varepsilon\sigma=\sigma$ .

transitivity: $\sigma\sqsubseteq_{E}^{V}\tau$ and $\tau\sqsubseteq_{E}^{V}\psi$ implies $\sigma\sqsubseteq_{E}^{V}\psi$ , where by definition we have

$\mathbf{Dom}(\sigma)=\mathbf{Dom}(\tau)=\mathbf{Dom}(\psi)$ , so by Definition 16. 3.:

and by composition with $\lambda_{2}$ from the right

reflexivity: $\sigma\trianglelefteq_{E}^{V}\sigma$ since $x\sigma$ embeds itself for all x in V.

transitivity: we show: $\sigma\trianglelefteq_{E}^{V}\tau\trianglelefteq_{E}^{V}\psi$ implies $\sigma\trianglelefteq_{E}^{V}\psi$

By Definition 16.(4) : For $\sigma\trianglelefteq_{E}^{V}\tau$ we have $\forall x\in V:\:x\sigma\trianglelefteq_{E}x\tau$

and for $\tau\trianglelefteq_{E}^{V}\psi$ we have $\forall x\in V:\:x\tau\trianglelefteq_{E}x\psi$ .

Now $\forall x\in V:\:x\sigma\trianglelefteq_{E}x\tau\;and\;x\tau\trianglelefteq_{E}x\psi$ are assertions on terms,

so using Theorem 14 we have $\forall x\in V:\:x\sigma\trianglelefteq_{E}x\psi$

and then by Definition 16.(4) we have $\sigma\trianglelefteq_{E}^{V}\psi$ .

The following lemma asserts that if a term s (a substitution $\sigma$ ) is embedded into a term t (a substitution $\tau$ ) then their instances are embedded too, that is, the relation $\trianglelefteq$ is right composable with substitutions.

1. (1) For all $\lambda$ , if $s\trianglelefteq t$ , then $s\lambda\trianglelefteq t\lambda$

2. (2) For all $\lambda$ , if $s\trianglelefteq_{E}t$ , then $s\lambda\trianglelefteq_{E}t\lambda$

3. (3) For all $\lambda$ , if $\sigma\trianglelefteq_{E}\tau$ , then $\sigma\lambda\trianglelefteq_{E}\tau\lambda$

By Definition 2.(4), we have three cases:

1. (i) $s=t$ is trivial.

2. (ii) Let $t=f(t_{1},\ldots,t_{n})$ and $s\trianglelefteq t_{j}$ for some $j\leq n$ . Now $t\lambda=f(t_{1},\ldots,t_{n})\lambda=f(t_{1}\lambda,\ldots,\,t_{n}\lambda)$ . Since $t_{j}$ is smaller than t we obtain by an inductive argument that $s\lambda\trianglelefteq t_{j}\lambda$ . Hence, $s\lambda\trianglelefteq t\lambda$ .

3. (iii) Let $s=f(s_{1},\ldots,s_{n})$ and $t=f(t_{1},\ldots,t_{n})$ with $s_{1}\trianglelefteq t_{1},...,\,s_{n}\trianglelefteq t_{n}$ . We have $s\lambda=f(s_{1}\lambda,\ldots,\,s_{n}\lambda)$ and $f(t_{1}\lambda,\ldots t_{n}\lambda)=t\lambda$ and again by an inductive argument, we obtain $s_{i}\lambda\trianglelefteq t_{i}\lambda$ for $1\leq i\leq n$ . Hence, $s\lambda\trianglelefteq t\lambda$ .

4. (2) This is shown using the $\trianglerighteq_{E}$ -chain of Lemma 11 $t\overset{n}{\blacktriangleright_{E}}s$ , that is, there is a $\vartriangleright_{E}$ -chain $t=_{E}t_{1}\vartriangleright t'_{1}=_{E}t_{2}\vartriangleright........\vartriangleright t'_{n}=_{E}s$ . Applying assertion (1) of this lemma to every element of the chain yields: $t=_{E}t_{1}\Longrightarrow t\lambda=_{E}t_{1}\lambda$ , $t_{1}\vartriangleright t'_{1}\Longrightarrow t_{1}\lambda\vartriangleright t'_{1}\lambda$ , ……., $t'_{n}=_{E}s\Longrightarrow t'_{n}\lambda=_{E}s\lambda$ . Combining these into one chain yields: $t\lambda=_{E}t_{1}\lambda\vartriangleright{t_{1}}\lambda=_{E}t_{2}\lambda\vartriangleright......{t_{n}}\lambda=_{E}s\lambda$ . Hence, $t\lambda\trianglerighteq_{E}s\lambda$ , resp. $s\lambda\trianglelefteq_{E}t\lambda$ .

5. (3) By Definition 16.(4) $\sigma\trianglelefteq_{E}\tau$ : $\forall x\in\mathbf{Dom}(\sigma)=\mathbf{Dom}(\tau):x\sigma\trianglelefteq_{E}x\tau$ and since these are terms, we have with 19(2) that $\forall x\in\mathbf{Dom}(\sigma)=\mathbf{Dom}(\tau):x\sigma\lambda\trianglelefteq_{E}x\tau\lambda$ and thus $\sigma\lambda\trianglelefteq_{E}\tau\lambda$ .

The next theorem shows that instance E-embedding is also a quasi-order on first-order terms.

reflexivity: is obvious because every term $\lambda$ -embeds itself.

transitivity: we show

implies

.

By Definition 12, we have:

implies $\exists\sigma:s\trianglerighteq_{E}r\sigma$ and

implies $\exists\tau:t\trianglerighteq_{E}s\tau$ .

Furthermore with Lemma 20 and Theorem 14:

$s\trianglerighteq_{E}r\sigma\Longrightarrow$ $\exists m:s\overset{m}{\blacktriangleright_{E}}r\sigma$ and $t\trianglerighteq_{E}s\tau\Longrightarrow\exists n:t\overset{n}{\blacktriangleright_{E}}s\tau$ .

By Lemma 19 $\blacktriangleright$ is substitution-composable from the right, hence we have

$s\tau\overset{m}{\blacktriangleright_{E}}r\sigma\tau$ , which implies $t\overset{n}{\blacktriangleright_{E}}s\tau\overset{m}{\blacktriangleright_{E}}r\sigma\tau$ .

Using the transitivity of $\trianglerighteq_{E}$ we get: $t\overset{n+m}{\blacktriangleright_{E}}r\sigma\tau$ and hence $t\trianglerighteq_{E}r(\sigma\tau)$ ,

that is

.

Using Theorem 20, we can now show that instance E-embedding of terms lifted to substitutions is also a quasi-order:

transitivity:

implies

By Definition 16.(5), we have:

implies $\exists\lambda:\sigma\trianglerighteq_{E}\varrho\lambda$ and

implies

$\exists\delta:\tau\trianglelefteq_{E}\sigma\delta$ . Hence, by Lemma 19.(3) on the components of $\sigma$ and $\varrho$

we have $\sigma\delta\trianglerighteq_{E}\varrho(\lambda\delta)$ , which implies by definition

.

The following definition lists some well-known notions (see Kruskal (Reference Kruskal1960) and Nash-Williams (Reference Nash-Williams1963)) on quasi-orderings, which we shall use later on.

1. (1) An infinite sequence of elements of S, $a_{1},a_{2},a_{3},...$ is called a $\mathbf{\leq}-$ chain if $a_{i}\leq a_{i+1}$ for all $i\geq1$ . The sequence $a_{1},a_{2},a_{3},...$ is said to contain a chain if it has a subsequence that is a chain.

2. (2) The infinite sequence $a_{1},a_{2},a_{3},...$ is called an anti-chain if neither $a_{i}\leq a_{j}$ nor $a_{j}\leq a_{i}$ , for all $1\leq i<j$ .

3. (3) The quasi-ordering $\leq$ is well-founded (wfo) if it contains no infinite strictly descending $<$ -chain; that is, there is no infinite sequence $a_{1},a_{2},a_{3},...$ of elements of S such that $a_{i}>a_{i+1}$ for every $i\;in\;\mathbb{N}$ .

4. (4) A well-quasi-ordering on S (wqo), $\leq$ , is a quasi-ordering which is well-founded and it has no infinite anti-chains in S with respect to $\leq$ .

and

.

With Lemma 19.(2), we get $t_{2}\lambda_{2}\trianglerighteq_{E}t_{3}\lambda_{3}\lambda_{2}$ . Hence, $t_{1}\trianglerighteq_{E}t_{2}\lambda_{2}\trianglerighteq_{E}t_{3}\lambda_{3}\lambda_{2}$ .

Now we have the following induction hypotheses: with $\sigma_{2}\;:=\;\lambda_{2}$ and for $n>2$

$t_{1}\trianglerighteq_{E}t_{2}\lambda_{2}\trianglerighteq_{E}t_{3}\lambda_{3}\lambda_{2}\trianglerighteq_{E}....\trianglerighteq_{E}t_{n}\lambda_{n}\lambda_{n-1}\lambda_{n\text{-2}}...\lambda_{2}$

For more readability, let us use the following notation:

(*1) $\sigma_{1}\;:=\;\varepsilon,\sigma_{2}\;:=\;\lambda_{2},\sigma_{3}\;:=\;\lambda_{3}\lambda_{2}$ , that is: $\sigma_{i}\;:=\;\lambda_{i}\sigma_{i-1}$ , $i\geq2$ .

Now by induction.

$n=2:$

and using (*1) we have: $t_{1}\trianglerighteq_{E}t_{2}\sigma_{2}$

$n\rightarrow n+1:$ by induction hypotheses there exist substitutions $\lambda_{2},\lambda_{3},...,\lambda_{n}$

such that $t_{1}\trianglerighteq_{E}t_{2}\sigma_{2}\trianglerighteq_{E}t_{3}\sigma_{3}\trianglerighteq_{E}....\trianglerighteq_{E}t_{n}\sigma_{n}$ , where $\sigma_{i}\;:=\;\lambda_{i}\sigma_{i-1}$ , $i\geq2$ ,

as notated in (*1).

Now at the tail of the chain, we have

and by Definition 12 there is a

substitution $\lambda_{n+1}$ , such that $t_{n}\trianglerighteq_{E}t_{n+1}\lambda_{n+1}$ . Moreover with Lemma 19.(2) :

$t_{n}\sigma_{n}\trianglerighteq_{E}t_{n+1}\lambda_{n+1}\sigma_{n}$ , and using notation (*1): $t_{n}\sigma_{n}\trianglerighteq_{E}t_{n+1}\sigma_{n+1}$ .

Hence in the limit we obtain $t_{1}\trianglerighteq_{E}t_{2}\sigma_{2}\trianglerighteq_{E}t_{3}\sigma_{3}\trianglerighteq_{E}....$ .

The following Tree Theorem was first proposed as a hypothesis by A. Vonyi and proved by Kruskal (Reference Kruskal1960); Kruskal (Reference Kruskal1972), and later with a more elegant proof by Nash-Williams (Reference Nash-Williams1963). It states that the set of finite trees over a well-quasi-ordered set of labels is itself well-quasi-ordered under homeomorphic embedding. Kruskal uses a notation, where T(Y) denotes the collection of all (structured) trees over an alphabet Y.

The following theorem is a consequence of the tree theorem for the set of first-order terms T(F,X), built over a finite signature F and a finite set of variable symbols X. Hereby, we refer to the work of Gallier (Reference Gallier1991), whose terminology we like to use. He proves that “Given a finite alphabet $\Sigma$ = $F\cup X$ which is well quasi ordered then $\trianglerighteq$ is also a well quasi order on $T(F,\,X)$ ” and the next theorem is a generalization to “modulo E.” In the following, we assume that $\Sigma$ is well-quasi-ordered.

If not, then there exists an infinite strictly descending $\vartriangleright_{E}-$ chain over a finite alphabet: $t_{1}\vartriangleright_{E}t_{2}\vartriangleright_{E}t_{3}\vartriangleright_{E}...$ .

From this chain, we obtain the (sub-) sequence $s_{1},s{}_{2},s{}_{3},....$ where each $s_{i}$ corresponds to some $t_{j}$ with $s_{i}=_{E}t_{j}$ .

Then by the tree embedding theorem, there are indices $i<j$ such that $t_{i}\trianglelefteq t{}_{j}$ .

(see Gallier (Reference Gallier1991) for this formulation).

But $t_{i}\trianglelefteq t{}_{j}$ implies in particular $t_{i}\trianglelefteq_{E}t{}_{j}$ and hence contradicts that there is a

strictly descending $\vartriangleright_{E}-$ chain.

1. (ii) There are no infinite anti-chains with respect to $\trianglerighteq_{E}$ .

The argument is in the same spirit by contradiction, reducing $\trianglerighteq_{E}$ to $\trianglerighteq$ .

Proof. Similar to Theorem 25 Footnote ³ .

E-unification of first-order terms is based on an infinite set of variable symbols and it is well known that the embedding order of terms with an infinite set of variable symbols is not a well-quasi-order, since we have the anti-chain $x_{1},x_{2},x_{3},....$ . Of course the same is the case then for embedment modulo E.

But well foundedness of the syntactic embedding ordering is valid, since the number of symbols decreases in a strictly descending syntactic $\vartriangleright-$ chain. This well-known fact is stated in the next proposition.

Our interest in this paper is the extension to equational theories. But with an infinite set of variables Proposition 27 is not applicable, since in an infinite strictly decreasing $\trianglerighteq_{E}$ -chain the number of occurrences of symbols could increase. So one would conjecture that the E-embedding order is not a well-founded order (WFO). Unfortunately, we have yet no proof either way.

For an infinite set of variable symbols, we have to look for appropriate constraints on the equational theory E and a possible candidate is that for a term t the total number of variable symbols in $[t]_{E}$ is finite. This is achieved by requiring that every axiom $l=r$ in E has the property, that $\mathbf{Var}(l)=\mathbf{Var}(r)$ , a class of theories called regular theories.

Then for every rewrite step: $t_{i}\longrightarrow_{l_{i}\rightarrow r_{i}}t_{i+1}$ or $t_{i}\longrightarrow_{r_{i}\rightarrow l_{i}}t_{i+1}$

there is a substitution $\lambda_{i}$ such that $l_{i}\lambda_{i}$ (or $r_{i}\lambda_{i}$ ) is a subterm of $t_{i}$ ,

$l_{i}\lambda\preceq t$ (or $l_{i}\lambda\preceq t$ ) and $t_{i+1}$ is the result of replacing $l_{i}\lambda$ by $r_{i}\lambda$ (or $r_{i}\lambda$ by $l_{i}\lambda$ ).

But since $\mathbf{Var}(l_{i})=\mathbf{Var}(r_{i})$ this cannot introduce new variables in $t_{i+1}$ and

hence $\mathbf{Var}(t')\subseteq\mathbf{Var}(t)$ .

Well foundedness of E-embedding is now an easy consequence.

$t_{1}\vartriangleright_{E}t_{2}\vartriangleright_{E}t_{3}...\vartriangleright_{E}t_{i}\vartriangleright_{E}.....$

With Definition 10 and Lemma 11, this chain has the form:

$t_{1}=_{E}t_{1}'\overset{n_{1}}{\blacktriangleright_{E}}t{}_{2}=_{E}t_{2}'\overset{n_{2}}{\blacktriangleright_{E}}t{}_{3}=_{E}t_{3}'\overset{n_{3}}{\blacktriangleright_{E}}t{}_{4}.....$ which consists of E-variants of embedded

terms. Now with Lemma 28 and $W\;:=\;\mathbf{Var}(t_{1})\bigcup V_{E}$ we have,

that for all terms ˆ, which appear in the chain: Var(ˆ $)\subseteq W$ .

But then all elements of the chain and its E-equivalents are built over a finite

alphabet. Hence by Theorem 25, the $\trianglerighteq_{E}$ ordering is well founded.

The next theorem is similar and shows that $\lambda_{E}$ -embedding preserves well foundedness.

$t_{1}\gtrdot_{E}t_{2}\gtrdot_{E}t_{3}...\gtrdot_{E}t_{i}\gtrdot_{E}.....$

By Lemma 23, there exists a corresponding infinite strictly descending

$\vartriangleright_{E}$ -chain $t_{1}\vartriangleright_{E}t{}_{2}\sigma_{2}\vartriangleright_{E}t_{3}\sigma_{3}\vartriangleright_{E}t_{4}\sigma_{4}\vartriangleright_{E}....$ contradicting Theorem 29.

3.1 $\mathbf{E}$ -Unification

Let E be an equational theory and let F be the signature of the term algebra. An E-unification problem is a finite set of equations

Let V denote the set of variables in $\varGamma$ , $V=\mathbf{Var}(\varGamma)$ . An E-unifier for $\Gamma$ is a substitution $\sigma$ such that

The set of all E-unifiers of $\Gamma$ is denoted $\mathcal{U}\Sigma_{E}(\Gamma)$ . A complete set of E-unifiers $c\mathcal{U}\Sigma_{E}(\Gamma)$ for $\Gamma$ is a set of E-unifiers, such that for every E-unifier $\tau$ there exists $\sigma\in c\mathcal{U}\Sigma_{E}(\Gamma)$ with $\sigma\leq_{E}^{V}\tau$ . The set $\mu\mathcal{U}\Sigma_{E}(\Gamma)$ is called a minimal complete set of E-unifiers for $\Gamma$ , if it is complete and for all distinct elements $\sigma$ and $\sigma'$ in $\mu\mathcal{U}\Sigma_{E}(\Gamma)$ if $\sigma\leq_{E}^{V}\sigma'$ then $\sigma=_{E}^{V}\sigma'$ .

When a minimal complete set of E-unifiers of a unification problem $\Gamma$ exists, it is unique up to E-subsumption equivalence $\thicksim_{E}^{V}$ . Minimal complete sets of E-unifiers need not always exist, and if they do, they might be singular, finite, or infinite. Since minimal complete sets of E-unifiers are isomorphic whenever they exist, they can be used to classify theories with respect to their corresponding unification problem. This leads naturally to the concept of a unification hierarchy, see Siekmann (Reference Siekmann1989), Knight (Reference Knight1989), Gallier (Reference Gallier1991), Baader and Siekmann (Reference Baader and Siekmann1994), and Baader and Snyder (Reference Baader and Snyder2001) for the standard surveys on this aspect.

A unification problem $\Gamma$ is

• nullary, if $\Gamma$ is unifiable, but the minimal complete set of E-unifiers does not exist.

• unitary, if it is not nullary and the minimal complete set of E-unifiers for $\Gamma$ is of cardinality less than or equal to 1.

• finitary, if it is not nullary and the minimal complete set of E-unifiers is always finite.

• infinitary, if it is not nullary and the minimal complete set of E-unifiers is infinite.

An equational theory E is

• unitary, if all unification problems for E are unitary

• finitary, if all unification problems are finitary.

• infinitary, if there is at least one infinitary unification problem and all unification problems have minimal complete sets of E-unifiers.

• If there exists a solvable unification problem $\Gamma$ not having a minimal complete set of E-unifiers, then the equational theory E is nullary or of type zero.

3.2 E-Unifiers ordered by homeomorphic embedding

The essential problem in unification theory is to determine the relationship between the solutions of term equations. In other words: what is the structure of the solution space?

In the case of syntactic unification, the structural relationship between the unifiers is based on the fact that terms form a lattice under the subsumption order, that is, there is a least upper bound and a max lower bound. Hence, if a unification problem is solvable, then there is a single most general unifier. But for unification under an equational theory the answer is not as easy, because:

• the complete set of most general unifiers is mostly infinite

• the complete set of most general unifiers may not even exist for a solvable E-unification problem.

So the search for an order relation better than subsumption comes naturally. Our first idea was based on the observation that certain solutions contain the instances of other solutions as a sub-structure. We captured this idea technically with the encompassment order on terms and substitutions, which led to the notion of an E-essential unifier Footnote ⁴ . Sub-structure means, in this case, that a unifying substitution encompasses other unifiers and hence they need not necessarily be part of the new set that represents all solutions. Unfortunately, the encompassment order is not a wqo either and hence there are equational theories for which there are solvable E-unification problems, but the minimal and complete set of essential E-unifiers does not exist, so they are E-nullary w.r.t. encompassment (Baader, Reference Baader1988; Hoche, 2016; Szabo et al., Reference Szabo, Siekmann and Hoche2016).

This paper is based on the observation that certain solutions embed the instances of other solutions in the sense of the homeomorphic tree embedding theorem or Kruskal’s theorem. That is, the components of a unifying substitution embed the components of another unifying substitution. This then leads to the notion of free (instance embedment-) E-unifiers, free $\lambda_{E}$ -unifiers, where these free $\lambda_{E}$ -unifiers are the candidates of our new minimal and complete set of unifiers, which we name $\varphi U\varSigma_{E}(\varGamma)$ .

Since homeomorphic embedding is not a well-quasi-order on the set of terms with infinitely many variable symbols, we cannot use Theorem 25. But for all practical purposes it may be possible for an automated deduction system to set a limit to the number of new variables and the theorem may still be useful in that case.

Nevertheless, the infinite sequence of variables $x_{1},x_{2},x_{3},....$ is normally used as a case in point that we have an anti-chain and hence Kruskal’s theorem cannot be applied. But for the instance embedding order

this is not the case: For example, $x_{1}$ instance embeds $x_{2}$ with the instantiating substitution $\lambda=\{x_{2}\rightarrow x_{1}\}.$ So there is the open problem whether or not the $\lambda_{E}$ -embedding is a well-quasi-order. Unfortunately, currently we have neither a counter example nor a proof – so we state it here as an:

Open problem: Is the

-order a WQO even for an infinite number of variables?

For the rest of the paper, we shall also employ a standard technique used in the quest for termination proofs in logic programming Leuschel (Reference Leuschel1998); Leuschel (Reference Leuschel2002) as well as termination of term rewriting systems Dershowitz and Jouannaud (Reference Dershowitz and Jouannaud1990), namely to disregard the name of a variable and simply treat all variables as the same. In other words, the unification procedure processes them as if they were embedment equivalent. This observation leads to the notion of pure embedding, which we abbreviate to $\pi$ -embedding in the following and denote it as $t\trianglerighteq^{\pi}s$ . As before, we generalize embedding to pure instance embedding or $\lambda^{\pi}$ -embedding by saying a term s is $\lambda^{\pi}$ -embedded into a term t, if it is $\lambda$ -embedded and in addition all variables are embedding equivalent. It is defined (almost identical to Definition 2.(4), Definition 5 and 10) as follows:

1. (1) A term t $\pi$ -embeds a term s if:

   \begin{align*}t\trianglerighteq^{\pi}s\,\iff\left\{ \begin{array}{ll}s=t\;or\;s,t\in X\:or\\t=f(t_{1},\ldots,\:t_{n})\;and\:for\:some\;i,\:1\leq i\leq n,\:t_{i}\trianglerighteq^{\pi}s,or\\t=f(t_{1},\,.\,.\,.t_{n}),\:\;s=f(s_{1},.\,.\,.s_{n})\;and\:\;\forall i:\:t_{i}\trianglerighteq^{\pi}s_{i},\:1\leq i\leq n.\end{array}\right.\end{align*}

2. (2) A term s is instance $\pi$ -embedded ( $\lambda^{\pi}$ -embedded) into a term t, denoted

   ,

   if there is an instantiating substitution $\lambda$ such that $s\lambda$ is $\pi$ -embedded into t: $s\lambda\trianglelefteq^{\pi}t$ . We also say that s is $\lambda^{\pi}$ -embedded into t.

3. (3) A term t $\pi_{E}$ -embeds a term s modulo E, denoted $t\trianglerighteq_{E}^{\pi}s$ , if s and t are variables, or $s=_{E}t$ , or there is a term $s'=_{E}s$ and a term $t'=_{E}t$ and there is an embedded term p in $\mathbf{Emb_{E}}(t')$ such that $p\vartriangleright^{\pi}s'$ . More precisely:

   \[t\trianglerighteq_{E}^{\pi}s\,\iff\begin{cases}s=_{E}t,\:or\:s,t\in X\;or\\\exists t'\in[t]_{E},s'\in\left[s\right]_{E}\;and\:\:\exists p\in\mathbf{Emb_{E}}(t'):p\vartriangleright^{\pi}s'\end{cases}\]

4. (4) Similar to Definition 10 and Definition 12, we define that a term s is instance $\pi$ -embedded modulo E ( $\lambda_{E}^{\pi}$ -embedded) into a term t,

   .

5. (5) A substitution $\sigma$ is $\pi$ -embedded into a substitution $\tau$ for a set of variables V, denoted as

   ,

   iff V $\subseteq$ $\mathbf{Dom}(\sigma)$ and $\forall x\in V:x\sigma$ is $\pi-$ embedded into $x\tau$ .

6. (6) A substitution $\sigma$ is instance $\pi-$ embedded modulo E ( $\lambda_{E}^{\pi}$ -embedded) into a substitution $\tau$ for a set of variables V, denoted as

   ,

   iff V $\subseteq+\mathbf{Dom}(\sigma)$ and there is a substitution $\lambda$ , such that $\forall x\in V:x(\sigma\lambda)$ is $\pi$ -embedded into $x\tau$ .

$\pi_{E}$ -embedding and $\lambda_{E}^{\pi}$ -embedding are special cases of E-embedding and $\lambda_{E}$ -embedding, so we can use Theorem 25 using the fact that we now have only one variable (see also Leuschel (Reference Leuschel1998)):

In order to show the results below, we recall some well-known notions originally found in Higman (Reference Higman1952) and Nash-Williams (Reference Nash-Williams1963) and others, but now restricted to first-order terms (Gallier, Reference Gallier1991). Moreover, we define that a list of terms $l_{1}=(s_{1},s_{2},s_{3},...,s_{n})$ is $\lambda_{E}$ -embedded (is $\lambda_{E}^{\pi}$ -embedded) into a list of terms $l_{2}=(t_{1},t_{2},t_{3},...,t_{n})$ , $n\geq1$ , if there is an instantiating substitution $\sigma$ , such that $l_{1}\sigma$ is E-embedded into $l_{2}$ . That is every component $s_{i}\sigma$ of the list $l_{1}$ is E-embedded into the component $t_{i}$ of the list $l_{2}\;for\:1\leqslant i\leqslant n$ .

In the following proofs, we use two standard notions:

1. (1) A sequence of terms $t_{1},t_{2},t_{3},.....$ is called good , if there are indices i,j, and $i<j:t_{i}\trianglelefteq t_{j}$ otherwise it is called bad . A well-quasi-ordering (wqo) is a quasi-ordering over which every infinite sequence is good.

2. (2) Let $l_{1}\;:=\;(s_{1},s_{2},s_{3},....s_{n}),l_{2}\;:=\;(t_{1},t_{2},t_{3},....t_{n})$ be lists of terms (of equal length). Then $l_{1}$ is embedded into $l_{2}$ , $l_{1}\trianglelefteq l_{2}$ , iff $s_{i}\trianglelefteq t_{i},1\leqq i\leqq n$ .

Since a substitution is in fact a list of terms labeled with a variable, we have:

Proof. See the proof in, for example, Nash-Williams (Reference Nash-Williams1963) and Gallier (Reference Gallier1991)

This lemma can now be extended to equational embedding:

Proof. See Gallier (Reference Gallier1991) where this is proved in a more general setting.

Proof. See the proof in Nash-Williams (Reference Nash-Williams1963), Gallier (Reference Gallier1991), and Singh et al. (Reference Singh, Shuaibu and Ndayawo2013).

The following lemma lifts the previous results from terms to substitutions and note we have only a finite set of variables, since the terms are wqo:

Proof. A substitution can be seen as a list of terms, so by induction on the size of the associated lists.

$\mathbf{n=1}$ : If T(F,X) is wqo, then for every infinite sequence of substitutions

with a single component $\sigma_{1}=\{x\rightarrow s_{1}\},\sigma_{2}=\{x\rightarrow s_{2}\},\sigma_{3}=\{x\rightarrow s_{3}\},...$

the associated sequence of lists is $l_{1},l_{2},...,l_{i}$ ,… where $l_{i}=(s_{i})$ , $i\geq1$

and the corresponding infinite sequence is $s_{1},s_{2},s_{3},....$

Now because $s_{1},s_{2},s_{3},...$ is good, that is there exists an $i,\,j$ , $i<j$ : $s_{i}\trianglelefteq_{E}s_{j}$

the sequence $l_{1},l_{2},l_{3},...$ is also good. Consequently, $\sigma_{1},\sigma_{2},\sigma_{3},....$ is good.

$\mathbf{n\rightarrow n+1}:$ By induction hypothesis $\sigma_{1},\sigma_{2},\sigma_{3},....$

with $\sigma_{i}=\{x_{1}\rightarrow s_{i1},x_{2}\rightarrow s_{i2},...,x_{n}\rightarrow s_{in}\}$ has the associated sequences of lists

$l_{1},l_{2},...,l_{i}$ ,… with $l_{i}=(s_{i1},s_{i2},...,s_{in})$ which is good and therefore

$\sigma_{1},\sigma_{2},\sigma_{3},....$ is also good.

Now Lemma 35 can be used, which says that there exists an infinite ascending

E-embedding sub-chain $l'_{1}\trianglelefteq_{E}l'_{2}\trianglelefteq_{E}l'_{3}\trianglelefteq_{E}...+\trianglelefteq_{E}l'_{i}\trianglelefteq_{E}...$ where $l'_{i}=(s'_{i1},s'_{i2},...,s'_{in})$ .

Looking now for lists with size $n+1$ we have a similar list but with

$l'_{i}=(s'_{i1},s'_{i2},...,s'_{in},s'_{in+1})$ , $i\geq1$ and its ascending $\trianglelefteq_{E}$ -subchain

$l'_{1}\trianglelefteq_{E}l'_{2}\trianglelefteq_{E}l'_{3}\trianglelefteq_{E}...$ .

Now because T(F,X) is a wqo set w.r.t. E-embedding, the corresponding infinite sequence consisting of the $n+1$ ’th members, $s'_{1n+1,}s'_{2n+1},...,s'_{in+1},...$ must be good; therefore, there are indices i’,j’ such that $s'_{i'n+1}\leq s'_{j'n+1}$ which implies $l'_{i'}=(s'_{i'1},s'_{i'2},...,s'_{i'n+1})\trianglelefteq_{E}l'_{j'}=(s'_{j'1},s'_{j'2},...,s'_{j'n+1})$ , hence $l'_{1},l'_{2},l'_{3},...$ is good. So if we assume that l $_{1},l{}_{2},l{}_{3},...$ is bad then $\sigma_{1},\sigma_{2},\sigma_{3},....$ is also bad, but the infinite subsequence $l'_{1},l'{}_{2},l'{}_{3},...$ is good; therefore, l $_{1},l{}_{2},l{}_{3},...$ must also be good from which follows that $\sigma_{1},\sigma_{2},\sigma_{3},....$ . is also good. Hence, $\mathcal{S}_{F,X}$ is a well-quasi-ordered set.

The proofs for our various E-embeddings on substitutions are almost identical to those in Lemma 38; hence, we collect them in one lemma:

The results so far, namely the (homeomorphic) embedding of first-order terms and substitutions extended to various equational embeddings, namely E-embedding ( $\trianglelefteq_{E})$ , instance E-embedding (

), pure E-embedding ( $\trianglelefteq_{E}^{\pi}$ ), and pure instance E-embedding (

) can now be used to show the following properties for the set of E-unifiers, more importantly for the set of minimal E-unifiers, which is of course our main interest.

Proof. T(F,X) is a well-founded quasi-order with respect to instance E-embedding as a consequence of Theorem 30 and Lemma 37.

If the alphabet is finite and $\Gamma_{E}$ is bounded, we have the following stronger result :Footnote ⁵

For our final result, let us say a purified E-unification problem is a problem where we define all variables as embedment equivalent. Let $\varphi_{\pi}U\varSigma_{E}(\varGamma)$ be the corresponding complete set of pure and free $\lambda_{E}$ -unifiers, then: