@MISC{ASYMPT_0.MIZ,
  AUTHOR = {Krueger, Richard and Rudnicki, Piotr and Shelley, Paul},
  TITLE = {Asymptotic Notation. {P}art {I}: {T}heory},
  NOTE = {This work has been supported by NSERC Grant OGP9207.},
  SECTION1 = {Preliminaries},
  SECTION2 = {A Notation for ``the order of"},
  SECTION3 = {Other Asymptotic Notation},
  SECTION4 = {Conditional Asymptotic Notation},
  SECTION5 = {Operations on Asymptotic Notation},
  DAY = {04},
  MONTH = {November},
  YEAR = {1999},
  ADDRESS1 = {University of Alberta\\Edmonton},
  ADDRESS2 = {University of Alberta\\Edmonton},
  ADDRESS3 = {University of Alberta\\Edmonton},
  SUMMARY = {The widely used textbook by Brassard and Bratley \cite{BraBra96}
includes a chapter devoted to asymptotic notation (Chapter 3, pp. 79--97).
We have attempted to test how suitable the current version of Mizar is for
recording this type of material in its entirety.  A more detailed report
on this experiment will be available separately.
This article presents the development of notions and a follow-up
article \cite{ASYMPT_1.ABS} includes examples and solutions to problems.
The preliminaries introduce a number of properties of real sequences,
some operations on real sequences, and a characterization of
convergence.  The remaining sections in this article correspond to sections
of Chapter 3 of \cite{BraBra96}.  Section 2 defines the $O$ notation
and proves the threshold, maximum, and limit rules.  Section 3 introduces
the $\Omega$ and $\Theta$ notations and their analogous rules.
Conditional asymptotic notation is defined in Section 4 where smooth
functions are also discussed.  Section 5 defines some operations
on asymptotic notation (we have decided not to introduce the asymptotic
notation for functions of several variables as it is a straightforward
generalization of notions for unary functions).}}


@BOOK{BraBra96,
       AUTHOR = {Brassard, Gilles and Bratley, Paul},
        TITLE = {Fundamentals of Algorithmics},
    PUBLISHER = {Prentice Hall},
         YEAR = {1996}}
