@@ -4,7 +4,7 @@ To run a proper unficiation algorithm is in our situation infeasible, since the
\paragraph{} We do so by first transforming each constant $C$ in a theory to an \emph{encoding}$(\cn{h}(C),\cn{syms}(C))$ the following way:
Consider the syntax tree of the type $t$ of a constant $C$. We first systematically replace the leaves by an abstract representation, yielding a data structure $\cn{tree}(C)$. We can eliminate variables by replacing them by their De Bruijn index, and symbol references by considering them like a separate set of variables, replacing them by their De Brujin indices and storing the symbol's names in a list $\cn{syms}(C)$.
Consider the syntax tree of the type $t$ of a constant $C$. We first systematically replace the leaves by an abstract representation, yielding a data structure $\cn{tree}(C)$. We can eliminate variables by replacing them by their De Bruijn index, and symbol references by enumerating them and storing the symbol's names in a list $\cn{syms}(C)$.
As a result, we get a pair $(\cn{tree}(C),\cn{syms}(C))$. Now an assignment $V(C)=D$ is valid, iff $\cn{tree}(C)=\cn{tree}(D)$, the lists $\cn{syms}(C)$ and $\cn{syms}(D)$ have the same length and their pairwise assignments $V(\cn{syms}(C)_i)=\cn{syms}(D)_i$ are all valid.
