@MISC{TERMORD.MIZ,
  AUTHOR = {Schwarzweller, Christoph},
  TITLE = {Term Orders},
  ACKNOWLEDGEMENT = {I'd like to thank Piotr Rudnicki for
  valuable discussions on how to represent term orders in Mizar.},
  SECTION1 = {Preliminaries},
  SECTION2 = {Term Orders},
  SECTION3 = {Head Terms, Head Monomials, and Head Coefficients},
  SECTION4 = {Reductum of a Polynomial},
  DAY = {20},
  MONTH = {December},
  YEAR = {2002},
  ADDRESS1 = {University of Tuebingen},
  SUMMARY = {We continue the formalization of \cite{Becker93} towards Gr\"obner Bases. 
Here we deal with term orders, that is with orders on bags. We introduce the
notions of head term, head coefficient, and head monomial necessary to define
reduction for polynomials.}}

