**(1)**- University of Bremen
**(2)**- That means that no ground term is an instance of more than one left hand-side.
**(3)**- Uniqueness follows from the freeness constraints. Note that the free datatype declarations are equivalent to some free specification.
**(4)**- Usually, the semantics of constructor-generated data types in programming languages is given in a domain-theoretic fashion. But from this, we usually can build a partial algebra in a canonical way.
**(5)**- That is, any ground term consisting of the head operation symbol applied to constructor terms must match one of the left hand-sides.
**(6)**- It is also possible to include complete
specifications of partial functions. The complement of
the domain of such a function must completely be specified
with axioms of form
*not def f(t*._{1},...,t_{n})

CoFI Note: L-9 --Version 1.0-- 21 March 1998.

Comments to till@informatik.uni-bremen.de