@MISC{PRE_FF.MIZ,
  AUTHOR = {Bancerek, Grzegorz and Rudnicki, Piotr},
  TITLE = {Two Programs for {\bf {SCM}}. {P}art {I} - Preliminaries},
  NOTE = {This work was partially supported by NSERC Grant OGP9207
while the first author visited University of Alberta, May--June 1993.},
  DAY = {08},
  MONTH = {October},
  YEAR = {1993},
  ADDRESS1 = {Polish Academy of Sciences\\Institute of Mathematics\\Warsaw},
  ADDRESS2 = {University of Alberta\\Department of Computing Science\\Edmonton},
  SUMMARY = {In two articles (this one and \cite{FIB_FUSC.ABS}) we discuss correctness
of two short programs for the {\bf SCM} machine:
one computes Fibonacci numbers
and the other computes the {\em fusc}
function of Dijkstra \cite{DIJKSTRA}.
The limitations of current Mizar implementation rendered it impossible
to present the correctness proofs for the programs in one article.
This part is purely technical and contains a number of very specific
lemmas about integer division, floor, exponentiation and logarithms.
The formal definitions of the Fibonacci sequence and the {\em fusc}
function may be of general interest.}}

