@MISC{ASYMPT_1.MIZ,
  AUTHOR = {Krueger, Richard and Rudnicki, Piotr and Shelley, Paul},
  TITLE = {Asymptotic Notation. {P}art {II}: {E}xamples and Problems},
  SUBTITLE = {Part {II}: {E}xamples and Problems},
  NOTE = {This work has been supported by NSERC Grant OGP9207.},
  SECTION1 = {Examples from the Text},
  SECTION2 = {Problem 3.1},
  SECTION3 = {Problem 3.5},
  SECTION4 = {Problem 3.6},
  SECTION5 = {Problem 3.7},
  SECTION6 = {Problem 3.8},
  SECTION7 = {Problem 3.11},
  SECTION8 = {Problem 3.19},
  SECTION9 = {Problem 3.21},
  SECTION10 = {Problem 3.22},
  SECTION11 = {Problem 3.23},
  SECTION12 = {Problem 3.24},
  SECTION13 = {Problem 3.26},
  SECTION14 = {Problem 3.28},
  SECTION15 = {Problem 3.30},
  SECTION16 = {Problem 3.31},
  SECTION17 = {Problem 3.34},
  SECTION18 = {Problem 3.35},
  SECTION19 = {Addition},
  SECTION20 = {Potentatially Useful},
  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.
This article is a follow-up to \cite{ASYMPT_0.ABS} in which we
introduced the basic notions and general theory.
This article presents a Mizar formalization of examples and solutions to
problems from Chapter 3 of \cite{BraBra96} (some of the
examples and solved problems are also in \cite{ASYMPT_0.ABS}).
Not all problems have been solved as some required solutions
not amenable for formalization.}}


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