.
Dann kann man die sortbase noch auf Vollst"andigkeit und
Eindeutigkeit pr"ufen (). Ist das Sortenwissen in
subsumes -Notation gegeben kann es in Hornregeln "uberf"uhrt werden
und andersrum (). Erst nach der horizontalen
Compilation kann unifiziert werden ().