\section{Tools for constructing algebras}

We will use a somewhat involved construction, and will
require some preliminary definitions.  Recall that the 
{\em path} of a subterm was defined in the previous section.

To help visualize terms, we can represent them as
rooted trees where interior nodes are labeled with operations and
leaves are labeled with variables or constants. For example, suppose
$f$ is a ternary operation, $g$ is binary, $c$ is a constant, and
$u$, $v$, $w$, $x$, $y$ and $z$ are variables. We let $s=f(g(u,v),f(w,x,f(u,v,w)),c)$
and let $t=f(g(v,v),f(w,w,g(y,z)),c)$ . Then the subterm of $s$
with path $f_{1}g_{1}$is $u$, and the subterm of $t$ with path
$f_{1}g_{1}$is $v$.


\begin{figure}
\includegraphics[scale=0.85]{TwoTrees.pdf}\caption{Trees for two terms}

\end{figure}


Note that the subterms of $s$ and $t$ with path $f_{2}f_{3}$ are
$f(u,v,w)$ and $g(y,z)$ respectively. Since these subterms have
different principal operation symbols, the terms $s$ and $t$ can
not be unified. Applying {\em Decompose}
to $s=t$ with path $f_2f_3$ gives $f(u,v,w) \equiv g(y,z)$, after 
which {\em Conflict} gives $\mathbf{False}$.

Our long-term goal is to form an algebra that
separates any two non-unifiable terms $s$ and $t$, such as those
in our example. We will need some preliminary ideas in order to do
this. Our algebras will have elements which are vectors 
over the $2$-element field $Z_{2}$. We take the index set
of the components of these vectors to be the set of natural numbers
$\mathbf{N}=\{0,1,2,\dots\}$. All of our vectors will be  
zero in all but finitely many components.
Given any finite set of such vectors, we let $M$ be the set of all
indices where any of the vectors is
nonzero. Then all these vectors lie
in the finite subspace consisting of vectors with all their components
outside of $M$ equal to $0$. We will usually leave this final reduction
to a finite algebra to the reader. 

We will actually be only using
the additive structure of the field $\mathbf{Z}_{2}$ , and viewing
it as an abelian group. The operations of our algebras will be sums
of linear transformations of the input vectors, sometimes with constant
elements added. Since we are working over $\mathbf{Z}_{2}$, all additions
of values will be done modulo $2$. We will periodically note this
fact, but not always. We will simply write $x_{i}$ for a vector
variable instead of $\vec{x_{i}}$, and write $x_{i}[a]$ for the
$a$-th component of the vector $x_{i}$. We will define operations
by their actions on components, and
can treat any term $t$ as a vector which denotes the value of
$t(x_1,x_2,\dots,x_n)$.  To specify the operation $f(x_{1,}x_{2},\dots x_{n})$,
it then suffices to say what $f[i]$ is for all $i$. We will do this
by giving a sequence of equations for the $f[i]$. To emphasize that
values are being assigned to the components $f[i]$, we will use $:=$
instead of the normal equality symbol. One further convention is that
each $f[i]$ will be zero, unless it is explicitly assigned a value.
With this convention, each equation corresponds to a linear transformation
from the direct product of the input vector spaces to the output vector
space, where $f[i]:=x_{j}[k]$ corresponds to the transformation that
takes the $n$-tuple of vectors
$\langle x_{1},x_{2},\dots x_{n}\rangle$ to the vector with
all components $0$ except that the $i$-th component is equal to
the $k$-th component of the vector $x_{j}$.

As an example, we will now construct an algebra
that separates our terms 
$s=f(g(u,v),f(w,x,f(u,v,w)),c)$ and $t=f(g(v,v),f(w,w,g(y,z)),c)$.
The separation will be assured because the output vectors $s$ and
$t$ will always differ on their $0$-th component, which we will arrange
as follows. The crucial difference between $s$ and $t$ is that their
subterms with path $f_{2}f_{3}$ have principal operations $f$ and
$g$, respectively. So we start our definition of $f$ by putting
the vector $\langle 0,0,0,0,\dots\rangle$ into the sum that defines
it, while putting $\langle 0,0,1,0,\dots\rangle$ into the sum that
defines $g$. So far, this makes the subterms $f(u,v,w)$ and $g(y,z)$
differ on their $2$nd component. Now we have to transfer this distinction
to the $0$-th components of $s$ and $t$, along the path $f_{2}f_{3}$.
This first application of $f$ comes via the $3$rd input, so we need
to have $f$ transfer the value in the $2$nd component to an unused
component, say the $1$st. This gives us the linear transformation
with equation $f[1]:=x_{3}[2]$. Since this transfers the value in
the $2$nd component to the $1$st component along the path $f_{3}$,
our notation for this linear transformation will be $\|2,f_{3},1\|$.
The next application of $f$ is to the $2$nd input, where we want
to take the value in the $1$st component and send it to the $0$-th
component. The equation for this is $f[0] := x_{2}[1]$, and our notation
for this linear transformation is $\| 1,f_{2},0 \|$. Adding together
the pieces we have produced, we have that 
$f=\langle 0,0,0,\dots \rangle + \|2,f_{3},1\| + \|1,f_{2},0\|$,
while $g$ is just $\langle 1,0,0,0,\dots\rangle$. 

To produce a finite
algebra that separates $s$ and $t$ , we note that only components
$0$, $1$ and $2$ are used, so the universe of our algebra can be
$\mathbf{Z}_{2}^{3}$. We define $g$ by $g(x,y) = \langle 1,0,0\rangle$,
and $f$ by 
$f(x,y,z) = \langle 0,0,0\rangle + \langle 0,0,z(0)\rangle + 
\langle 0,y(2),0 \rangle = \langle 0,y(2),z(0)\rangle$.
The constant $c$ was not used, so we can assign an arbitrary value
to it, and choose $c = \langle 0,0,0 \rangle$. To confirm that this works,
we compute $s[0]$ and $t[0]$. We have $s=f(g(u,v),f(w,x,f(u,v,w)),c)$,
so $s[0]$ gets its value from $f$, actually from $\| 1,f_{2},0 \|$,
which is the only piece of $f$ that assigns a value to the $0$-th
component. Thus $s[0]$ is $f(w,x,f(u,v,w))[1]$. To find the value
of this, we use that the only piece of $f$ assigning a value to the
$1$st component is $\| 2,f_{3},1 \|$, and get 
$f(w,x,f(u,v,w))[1] = f(u,v,w)[2]$.
No piece of $f$ assigns a value to the $2$nd component, so $f(u,v,w)[2] = 0$,
the default value. Thus $s[0] = f(w,x,f(u,v,w))[1] = f(u,v,w)[2] = 0$.
Similarly, $t=f(g(v,v),f(w,w,g(y,z)),c)$ gives us 
$t[0] = f(w,w,g(y,z))[1] = g(y,z)[2] = 1$.

Note that we can treat the sum $\| 2,f_{3},1 \| + \| 1,f_{2},0 \|$ in $f$
as a single transformation, that takes the $2$nd component of the
subterm with path $f_{2}f_{3}$ to the $0$-th component of the main
term. We write this as $\| 2,f_{2}f_{3},0 \|$, which does not mention
the use of the $1$st component in an intermediate step. Since all
we needed was that the component not be used elsewhere, this is reasonable.
So we will assume that indices such as $a$, $b$
and so on are always chosen to minimize {\em collisions}. This
means that no indices will be equal unless they are explicitly represented
with equivalent expressions. This can be easily achieved by appropriate
choices of values for the indices, and will not jeopardize the finiteness
of any algebras we produce. As long as there are no collisions, algebras
obtained for different values of $a$ will be isomorphic. Accordingly,
we will speak of {\em the} algebra operation $\|2,f_{2}f_{3},0\|$,
 etc.

Extending this idea, we can define the transformation $\| j,\rho, k\|$
that takes the $j$-th component to the $k$-th component along path
$\rho$, where $\rho$ is any non-empty string.

\begin{definition}\label{basic operation def}
If $\rho$ is
$f_{i}$ for some operation symbol $f = f(x_{1},\dots,x_{i},\dots,x_{n})$,
we define $\| j,f_{i},k \|$ by the equation 
$f[k] := x_{i}[j]$.
If $\rho$ is $f_{i}\sigma$ where $\sigma\neq\Lambda$, we define
$\| j,\rho,k \|$ to be $\| j,\sigma,m \| + \| m,f_{i},k \|$, where $m$
is understood to be an index not used elsewhere.
\end{definition}

This definition produces a sum of transformations for possibly many
different operations, which is not a problem. To recover the actual
operations from a sum of transformations, $\Sigma$,
we merely let each operation
be the sum of the transformations and constant vectors that reference
that operation, where operations that are not referenced have constant
value $\langle0,0,0,\dots\rangle$.
We denote the algebra with operations defined this way by 
$\mathop{\rm Alg}(\Sigma)$.  Our understanding is that only indices with non-zero
components are used in $\mathop{\rm Alg}(\Sigma)$, so it is finite
and unique up to isomorphism.

The idea is that \ $\|m,\rho,n\|$ \ transfers the
value of the $m$-th component of the vector with path $\rho$ in the
term $s$ to the $n$-th component of the result of $s$, with as
few side effects as possible. We are assuming that none of the indices
used to define \ $\|m,\rho,n\|$ \ is equal to any of the others, except
that possibly \ $m=n$. \ In other words, the operation \ $\|m,\rho,n\|$
\ is {\em duplicate free}. If $m_{1}$ is distinct from both $m_{2}$
and $m_{0}$, and $\mu$ and $\nu$ are strings in \ $\mathit{P}$, \ then
the operation \ $\|m_{2},\nu,m_{1}\|+\|m_{1},\mu,m_{0}\|$ \ is duplicate
free by our convention that indices are chosen to minimize collisions.
In isolation, the sum \ $\|m_{2},\nu,m_{1}\|+\|m_{1},\mu,m_{0}\|$ \ is
equivalent to \ $\|m_{2},\mu\nu,m_{0}\|$. \ The one difference is that
the former explicitly mentions the index $m_{1}$. 

\begin{lemma}\label{path lemma}
Let the algebra operation \ $\|m,\rho,n\|$ \ be duplicate free where 
$\rho \in P$.
Suppose that $t$ is a term, and let $s$ be a subterm of $t$ with path $\rho$. 
Then $t[n]=s[m]$.
\ \end{lemma} 

\begin{proof} We let \ $\rho=\rho_{0}\rho_{1}\rho_{2}\cdots \rho_{j}$,
where each of the $\rho_{i}$ is a subscripted basic operation symbol.
We will prove the lemma by induction on $j$. Our basis is when $j=0$,
making the operation \ $\|m,\rho_{0},n\|$. \ Assume that $\rho_{0}$ is
$f_{i}$ and $f$ is $k$-ary, so $s$ is 
$f(u_{1},\dots u_{i-1},t,u_{i+1},\dots u_{k})$,
where the $u_{j}$ are terms. The only assignment to $t[n]$ is then
made by $f[n]:=x_{i}[m]$\ , \ giving \ $t[n]=f[n]=x_{i}[m]=s[m]$,
\ as desired. For the induction step, assume the statement is
true for \ $j-1$, \ and that we want to show it for the path \ 
$\rho=\rho_{0}\rho_{1}\rho_{2}\cdots \rho_{j}$.
\  We write \ $\|m,\rho,n\|$ \ as \ 
$\|m,\rho_{j},b\|+\|b,\rho_{0}\rho_{1}\rho_{2}\cdots \rho_{j-1},n\|$
\ for some new index $b$, and let $\psi$ be \ 
$\rho_{0}\rho_{1}\cdots \rho_{j-1}$,
\ so \ $\rho=\psi\rho_{j}$. \ 
By the statement for \ $j-1$, \ $t[n]=u[b]$,
where $u$ is the subterm of $s$ with path $\psi$. \ We assume $\rho_{j}$
is $f_{i}$ , and have $u=f(v_{1},\dots v_{i-1},t,v_{i+1},\dots v_{k})$,\ where
$f$ is $k$-ary and the $v_{j}$ are terms. Then $u[b]=f(v_{1},\dots v_{i-1},t,v_{i+1},\dots v_{k})[b]=s[m]$,
since indices are chosen to minimize collisions and $\|m,\rho_{j},b\|$
is the only summand that assigns a value to the $b$-th component. Thus
\ $t[n]=u[b]=s[m]$, as desired. 
\end{proof} 

Given the algebra
operation $\|m,\rho,n\|$, we define the {\em tweaked} operation
$\|m,\rho,n\|'$ to be identical to $\|m,\rho,n\|$ except for
one assignment. Writing $\rho$ as $\psi\rho_{j}$, we assume that $\rho_{j}$
is $f_{i}$, for some basic operation $f$ and some $i$ less than or 
equal to the arity of $f$.  Then $\|m,\rho,n\|$ \ has an assignment of
the form \ $f[b] := x_{i}[m]$. We modify it by adding $1$, giving
\ $f[b] := (x_i[m]+1) \mod2$ in the definition of $\|m,\rho,n\|'$,
and keeping the rest of $\|m,\rho,n\|$ unchanged. 
A slight modification of the
proof of the previous lemma then establishes the following. 

\begin{lemma}\label{tweaked lemma}
Let the tweaked algebra operation $\|m,\rho,n\|'$ be duplicate
free, and let $t$ be an algebra term and let $s$ be a subterm of $t$,
where $\rho$ is the path of $s$ in $t$.  Then $t[n] = (s[m]+1) \mod2$.
\end{lemma}

\end{section}


\begin{section}{Algebras separating terms}   


\begin{lemma}\label{no s or t lemma}
If the equivalence class of $s$ and $t$ under $\equiv$ is larger than $\{ s,t \}$,
then  $s$ and $t$ are separated in a finite algebra.
\end{lemma}

\begin{proof}
Let $s$ and $t$ be given, and let $\equiv$ be the relation on terms generated from
$s \equiv t$.  Note that only terms that are subterms of $s$ or $t$ are 
equivalent to terms they are not equal to.  (This is easily proved by induction on 
the length of deductions.)

If $s$ is a proper subterm of $t$ or $t$ is a proper subterm of $s$, then we can 
separate $s$ and $t$ in a finite algebra as follows.  Without loss of generality, 
assume $s$ is a proper subterm of $t$, and let $\rho$ be the path of $s$ in $t$.
Then in $\mathop{\rm Alg}( \| 0,\rho,0 \|' )$, we have $t[0] = s[0] + 1$ by 
\ref{tweaked lemma}, showing that $s$ and $t$
are separated.  If $s = t$, then all the $\equiv$ classes are singletons, and the 
lemma also holds.

So assume neither $s$ nor $t$ is a subterm of the other, and let $E$ be the equivalence
class of $s$ and $t$ under $\equiv$.  Suppose 
$E$ is larger than $\{s,t\}$, so there is some $r \in E$ with 
$r \neq s$ and $r \neq t$, where we assume that the deduction $D$ of $r \equiv s$ or
$r \equiv t$ that shows this is of minimal length for all deductions giving 
$r \equiv s$ or $r \equiv t$ for some term $r$ in $E$ other than $s$ or $t$.

Now $D$ can not be the deduction $\langle s \equiv t \rangle$, so the deduction must end 
with $s \equiv r$ or $t \equiv r$, which is obtained by applying a deduction rule.  This 
rule must be {\em Transitive} or {\em Decompose}, since the other two rules only
produce $\mathbf{False}$.

If $r \in E$ is obtained by an application 
of {\em Transitive}, we assume without loss of generality that $s \equiv r$ is deduced,
and that the chain of equivalences used is as short as possible.
Then for some $n \geq 3$ there are $p_1, \dots p_n$ with 
$s = p_1$, $r = p_n$, and 
where the statements $p_1 \equiv p_2$, $p_2 \equiv p_3$, and so on are already deduced,
where none of these statements is trivial.  If $p_2$ is $t$, then the chain 
$p_2 \equiv p_3 \equiv \dots p_n = r$ is shorter than the original one, contradicting
our assumption.  Thus $p_2$ must not be in $\{ s,t \}$, contradicting our assumption that 
the deduction was of minimal length.

In the case where $r \in E$ is obtained by an application 
of {\em Decompose}, we assume without loss of generality that $s \equiv r$ is deduced
from some earlier statement $p \equiv q$, where $s$ is a proper subterm of $p$ and
$r$ is a proper subterm of $q$.  Now $p$ can not be a subterm of $s$, for then
$s$ would be a proper subterm of itself.  Thus $p$ must be a subterm of $t$, making $s$ a
subterm of $t$, which is also a contradiction.
\end{proof}

In view of this lemma, we will henceforth assume that the only statement involving
$s$ or $t$ that can be deduced is $s \equiv t$ itself.

Another special case is dealt with by the following lemma.

\begin{lemma}\label{s and t not variable lemma}
If $s$ or $t$ is a variable and $s$ and $t$ can not be unified, 
then  $s$ and $t$ are separated in a finite algebra.
\end{lemma}

\begin{proof}
Without loss of generality, assume that $t$ is the variable $x$.
If $x$ does not appear in $s$, then $s$ and $t$ can be unified by substituting
$s$ for $x$.  So assume that $x$ occurs in $s$, and let $\rho$ be the path of
this occurrence.  Then $s$ and $t$ are separated in 
$\mathop{\rm Alg}( \| 0,\rho,0 \|')$,
for $s[0] = x[0] + 1$ and $t[0] = x[0]$ there.
\end{proof}

We will henceforth assume that neither $s$ nor $t$ is a variable.  This is important,
because components of non-variable subterms are $0$ everywhere in $\mathop{\rm Alg}(L)$, 
except where values are explicitly assigned to them by summands of $L$.


\begin{lemma}\label{sums for k and 0 lemma}
If $p \equiv q$ can be deduced from $s \equiv t$, then there is an index $k$ such that
there is a finite sum of transformations $L$ so that $p[k] + q[k] = s[0] + t[0]$
in $\mathop{\rm Alg}(L)$.  If $p \equiv q$ is $s \equiv t$, then $k$ must be $0$, and if 
$p \equiv q$ is not $s \equiv t$, then $k$ can have any nonzero value.
\end{lemma}

\begin{proof}
We prove this by induction on the minimal length of a deduction 
of $p \equiv q$.  Our basis is where
$p \equiv q$ is $s \equiv t$.  In this case we let $L$ be the zero vector and take $k = 0$.

For the induction step, let $p \equiv q$ be different from $s \equiv t$, and let 
$D$ be a minimal deduction of $p \equiv q$.  Then $p \equiv q$ must be deduced 
in the last step of $D$ by using either {\em Decompose} or {\em Transitive}, giving us two cases.

Assume $p \equiv q$ is deduced by {\em Decompose} from the statement
$u(\dots, p, \dots) \equiv u(\dots, q, \dots)$, where $u$ is some term such that
$p$ and $q$ have the same path $\rho$ in $u$. 
If $u(\dots, p, \dots) \equiv u(\dots, q, \dots)$ is $s \equiv t$, we let 
$k \neq 0$ be given and take $L$ to be $\| k,\rho,0 \|$.  Then 
$p[k] + q[k] = s[0] + t[0]$ by Lemma \ref{path lemma}.

So assume $u(\dots, p, \dots) \equiv u(\dots, q, \dots)$ is not $s \equiv t$,
and let any nonzero index $k$ be given.  By our induction hypothesis, 
there is a nonzero index $m \neq k$
and a sum of transformations $L'$ with 
$u(\dots, p, \dots)[m] + u(\dots, q, \dots)[m] = s[0] + t[0]$ in $\mathop{\rm Alg}(L')$.
We now let $L$ be $L' + \| k, \rho,m \|$, and consider the value of 
$p[k] + q[k]$ in $\mathop{\rm Alg}(L)$.  We have 
$p[k] + q[k] = u(\dots, p, \dots)[m] + u(\dots, q, \dots)[m]$ 
there, since this is true in $\mathop{\rm Alg}(\| k, \rho,m \|)$ and summands of 
$L'$ make no assignments to $k$-th or $m$-th components.
We also have $u(\dots, p, \dots)[m] + u(\dots, q, \dots)[m] = s[0] + t[0]$
in $\mathop{\rm Alg}(L)$, since this is true in $\mathop{\rm Alg}(L')$ and because $\| k, \rho,m \|$ makes no assignments to $0$-th components.  
So $p[k] + q[k]  = u(\dots, p, \dots)[m] + u(\dots, q, \dots)[m]) =
s[0] + t[0])$ in $\mathop{\rm Alg}(L)$.

Now assume $p \equiv q$ is deduced  from
$p_1 \equiv p_2, p_2 \equiv p_3, \dots p_m \equiv p_{m+1}$
by {\em Transitive}, where 
$p_1$ is $p$, $p_{m+1}$ is $q$, and $p_i \equiv p_{i+1}$ is in $D$ for all $i$.
By our assumption after Lemma \ref{no s or t lemma}, we have that none of
the statements $p_i \equiv p_{i+1}$ is $s \equiv t$.  Thus given any nonzero
index $k$, we have the following sums of terms for $1 \leq i \leq m$.
We let $L_i$ be such that $p_i[k] + p_{i+1}[k] = s[0] + t[0]$ in 
$\mathop{\rm Alg}(L_i)$.  As usual, we assume when $i \neq j$ that $L_i$ and $L_j$ 
have no indices other than $0$ and $k$ that they both reference.
Letting $L = L_1 + L_2 + \dots L_{m}$, we have in $\mathop{\rm Alg}(L)$
that $s[0] + t[0]$ is equal to the sum
$(p_1[k] + p_2[k]) + (p_2[k] + p_3[k]) + \dots (p_{m}[k] + p_{m+1}[k])$.
This is because none of the $L_i$ assigns values to $k$-th components, so 
the only interaction between terms in the various $L_i$ will be at  
$0$-th components, where they assign values to $s[0]$ and $t[0]$.
We are working modulo $2$, so all of the middle terms cancel, 
giving  $s[0] + t[0] =
p_1[k] + p_2[k] + p_2[k] + p_3[k] + \dots p_{m}[k] + p_{m+1}[k] =
p_1[k] + p_{m+1}[k] = p[k] + q[k]$ in $\mathop{\rm Alg}(L)$.
\end{proof}

\begin{theorem}\label{separation theorem} Let $s$ and
$t$ be terms which can not be unified.  Then $s$ and $t$
are separated in a finite algebra. \end{theorem} 

\begin{proof}
Suppose that $s$ and $t$ can not be unified, and let $\equiv$
be the closure of $s \equiv t$ under the unification axiom and
transitivity.  The relation $\equiv$ must either fail to be homogeneous
or fail to be acyclic.

\textbf{Case 1:}  Suppose $\equiv$ is not homogeneous.  

Then there is a minimal deduction
$D$ of $f(\dots) \equiv g(\dots)$, where $f$ and $g$ are different 
operation symbols.  By Lemma \ref{sums for k and 0 lemma}, we have a
sum of transformations $L'$ and an index $k$ so that 
$f(\dots)[k] + g(\dots)[k] = s[0] + t[0]$ in $\mathop{\rm Alg}(L')$.
Now consider the transformation we will call $\| f,k \|'$, which sets 
the $k$-th component of its output equal to $1$ if the basic operation
is $f$, and otherwise sets it to the default value of $0$. 
Thus adding the transformation $\| f,k \|'$ to $L'$ 
adds $1$ to the $k$-th
component of the output of $f$, and has no other effect.
We let $L$ be $L' + \| f,k \|'$, and claim that $s[0] \neq t[0]$
in $\mathop{\rm Alg}(L)$, or equivalently, that $s[0] + t[0] = 1$.

If $f(\ldots) \equiv g(\ldots)$ is $s \equiv t$, then we have 
$k = 0$ and $L = \| f,k \|' = \| f,0 \|'$.
Exactly one of $s$ or $t$ is of the form $f(\ldots)$, without loss of generality we assume that $s$ is.  Then $s[0] = 1$ and $t[0] = 0$, 
giving $s[0] + t[0] = 1$.

Now assume that $f(\ldots) \equiv g(\ldots)$ is not $s \equiv t$,
so $k \neq 0$.  The only summand of $L$ that assigns a value to
the $k$-th component is $\| f,k \|'$, so $f(\ldots)[k] = 1$ and
$g(\ldots)[k] = 0$.  Thus 
$s[0] + t[0] = f(\ldots)[k] + g(\ldots)[k] = 1 + 0 = 1$, as desired.

\textbf{Case 2:} Suppose that $\equiv$ is not acyclic.  

Then writing 
$\triangleleft$ for the relation ``is a subterm of'', there is 
a chain of subterms of $s$ or $t$ with 
$p_1 \equiv q_1 \triangleleft p_2 \equiv q_2 \triangleleft p_3 \dots
q_{m-1} \triangleleft p_{m+1} = p_1$, where $m \geq 1$ and at least
one of the subterm relationships is strict.  

For each $i$, the subterm 
relationship $q_i \triangleleft p_{i+1}$ gives us
that we have some term $u_i \in \{s,t\}$, and paths $\rho$ and $\sigma$,
so that $q_i$ has path $\rho\sigma$ in $u_i$ and 
$p_{i+1}$ has path $\rho$ in $u_i$.

We may assume that 
we have the shortest such chain that shows $\equiv$ is not acyclic,
and fix $m$ as this minimal chain length.
With this assumption, all of the subterm relationships in the chain
must be strict.  This is obviously true if $m = 1$, so consider the
case where $m > 1$, and suppose $q_i = p_{i+1}$ for some $i$.  Then 
we have $p_i \equiv q_i = p_{i+1} \equiv q_{i+1}$.  Since $\equiv$
is transitive, $p_i \equiv q_{i+1}$, so we can shorten the chain, a
contradiction.

With $m$ as above, we will also assume that our chain of subterms 
$p_1 \equiv q_1 \triangleleft p_2 \equiv q_2 \triangleleft p_3 \dots
q_{m} \triangleleft p_{m+1} = p_0$ is such that the sum of the 
lengths of the paths of the $q_i$ is as large as possible.
Specifically, we let $\mathop{\rm length}(\psi)$ denote the length of any path
$\psi$, and for each $i$ let $\rho_i$ be the path of $q_i$ in
whichever of $s$ or $t$ it is a subterm of.
We are then assuming that our 
chain of length $m$ showing $\equiv$ is not acyclic is such that 
$\mathop{\rm length}(\rho_1) + \mathop{\rm length}(\rho_2) + \dots \mathop{\rm length}(\rho_{m})$
is as large as possible for any such chain of length $m$.

Since $p_1 \equiv q_1$, $p_2 \equiv q_2$, and so on up to 
$p_{m} \equiv q_{m}$, Lemma \ref{sums for k and 0 lemma}
gives us non-zero indices $k_1, k_2, \dots k_{m}$ 
and sums of transformations $L_1, L_2, \dots L_{m}$ where
for all $i$ with $1 \leq i \leq m$ we have
$p_i[k_i] + q_i[k_i] = s[0] + t[0]$ in $\mathop{\rm Alg}(L_i)$.
As usual, we are assuming that $L_i$ and $L_j$ only have the index
$0$ that they both reference when $i \neq j$.

Since $q_i \triangleleft p_{i+1}$ for $1 \leq i \leq m$,
then for each $i$ the subterm $q_i$ has path $\sigma_i$ 
in $p_{i+1}$.  Since all of the subterm relations are strict, 
none of the $\sigma_i$ 
are $\Lambda$.  Now we let $L$ be 
$L_1 + L_2 + \dots L_{m} + \| k_1,\sigma_1,k_2 \| + 
\| k_2,\sigma_2, k_3 \| + \dots
\| k_{m-1}, \sigma_{m-1},k_m \| + \| k_{m},\sigma_{m},k_1 \|'$.

Since none of $\| k_1,\sigma_1,k_2 \| + 
\| k_2,\sigma_2, k_3 \| + \dots
\| k_{m-1}, \sigma_{m-1},k_m \| + \| k_{m},\sigma_{m},k_1 \|'$ 
assign values to $0$-th 
components, the value of $s[0] + t[0]$ comes from 
$L_1 + L_2 + \dots L_{m}$, and since none of the $L_i$ share
indices other than $0$, we get $s[0] + t[0]$ by adding together the
$p_i[k_i] + q_i[k_i]$, giving
$s[0] + t[0] = p_1[k_1] + q_1[k_1] + \dots 
p_{m}[k_{m}] + q_{m}[k_{m}]$.

Now consider any $p_i[k_i] + q_i[k_i]$ for $1 \leq i \leq m$,
where we interpret $i-1$ as $m$ when $i = 1$.
For simplicity, we will work with $\| k_{m},\sigma_{m},k_1 \|$
instead of $\| k_{m},\sigma_{m},k_1 \|'$ for the moment,
and switch to using $\| k_{m},\sigma_{m},k_1 \|'$ 
at the end of the proof.
The only summand of $L$ that assigns to $k_i$-th components is
$\| k_{i-1},\sigma_{i-1}, k_i \|$.  This could in principle give 
both $p_i[k_i]$ and $q_i[k_i]$ nonzero values.  We claim that only
$p_i[k_i]$ is given a nonzero value by
$\| k_{i-1},\sigma_{i-1}, k_i \|$.

Since $q_{i-1}$ is a subterm of $p_i$ with path $\sigma_{i-1}$
for $2 \leq i \leq m$, we have $p_i[k_i] = q_{i-1}[k_{i-1}]$.  Assume 
$q_i[k_i]$ is given a nonzero value.  This must be because $q_i$ 
has a subterm $r$ with path $\sigma_{i-1}$ in $q_i$.  In this case
we have $p_i \equiv q_i$, that $q_{i-1}$ is a subterm of $p_i$ with
path $\sigma_{i-1}$, and that $r$ is a subterm of $q_i$ with path
$\sigma_{i-1}$.  Thus $q_{i-1} \equiv r$ by {\em Decompose},
which also gives us $p_{i-1} \equiv r$ by {\em Transitive}.
Now $r$ is a subterm of $q_i$ and hence a subterm of $p_{i+1}$,
so we have the chain 
$p_1 \equiv q_1 \triangleleft \dots 
p_{i-1} \equiv r \triangleleft p_{i+1} \dots
q_{m} \triangleleft p_{m+1} = p_1$.
If $m$ is greater than $1$, this is a shorter chain, which contradicts 
our assumption.  So assume $m = 1$, which makes $p_i = p_1$ and $q_i = q_1$
for all $i$.  Then our original chain was $p_1 \equiv q_1 \triangleleft p_1$,
but we also have the chain $p_1 \equiv r \triangleleft p_1$ where 
$r$ is a proper subterm of $q_1$, contradicting our assumption that the 
sum of the lengths of the paths to the $q_i$ is as large as possible.

Thus we have 
$p_i[k_i] + q_i[k_i] = q_{i-1}[k_{i-1}] + q_i[k_i]$ for 
$2 \leq i \leq m$.
For $i = 1$ the argument is the same, except that 
$\| k_m,\sigma_m,k_1 \|'$ makes 
$p_1[k_1] + q_1[k_1] = q_m[k_m] + 1 + q_1[k_1]$.
Thus we have
$s[0] + t[0] = (p_1[k_1] + q_1[k_1]) + \dots (p_{m}[k_{m}] + q_{m}[k_{m}])
= (q_{m}[k_{m}] + q_1[k_1] + 1) + (q_1[k_1] + q_2[k_2]) +
\dots (q_{m-1}[k_{m-1}] + q_{m}[k_{m}]) =
2(q_1[k_1] + q_2[k_2] + \dots q_{m}[k_{m}]) + 1 = 1$, since we calculate 
component values modulo $2$.  This shows $s[0]$ is always not equal to $t[0]$
in $\mathop{\rm Alg}(L)$.
\end{proof} 

As a corollary, we have the following.

\begin{corollary}\label{finite model corollary} 
Whenever the first order sentence $\sigma$ is a universally quantified conjunction
of negated atomic formulas, $\sigma$ is consistent iff it has a finite
model. \end{corollary} 

\begin{proof}
If $\sigma$ has a model, it is consistent.  So assume $\sigma$ is 
consistent.  We have that $\sigma$ is of the form
$(\forall v_1) \dots (\forall v_k)(\neg(\theta_1) \wedge \dots \neg(\theta_n))$,
where each of the $\theta_i$ is an atomic formula.  If $\theta_i$ is of the 
form $R(\dots)$ where $R$ is a relation symbol, we will just interpret $R$ as
always false in our finite model.  This leaves us with the case where
$\theta_i$ is $s_i(v_1, \dots v_k) = t_i(v_1, \dots v_k)$ for terms
$s_i$ and $t_i$.  If $s_i$ and $t_i$ can be unified, then $\neg(\theta_i)$
is not always true
and hence $\sigma$ has no models, and $\sigma$ is not consistent.  So 
$s_i$ and $t_i$ can not be unified, and the theorem gives a finite model 
$A_i$ where $\neg(\theta_i)$ is always true.  
Now we take the product of all these $A_i$,
and interpret all relations in the language as $\mathbf{False}$ in the product, giving a finite model of $\sigma$.
\end{proof}

\end{section}

