@MISC{SCMFSA9A.MIZ,
  AUTHOR = {Rudnicki, Piotr},
  TITLE = {The {\tt while} Macro Instructions of {\SCMFSA}. {P}art {II}},
  SECTION1 = {Arithmetic Preliminaries},
  SECTION2 = {{\SCMFSA} Preliminaries},
  SECTION3 = {The {\tt while=0} Macro Instruction},
  SECTION4 = {The {\tt while>0} Macro Instruction},
  SECTION5 = {A Macro for the {\tt fusc} Function},
  DAY = {03},
  MONTH = {June},
  YEAR = {1998},
  ADDRESS1 = {University of Alberta\\Edmonton},
  SUMMARY = {An attempt to use the {\tt while} macro, \cite{SCMFSA_9.ABS},
was the origin of writing this article.
The {\tt while} semantics, as given by J.-C.~Chen, is slightly extended by
weakening its correctness conditions and this forced a quite straightforward
remake of a number of theorems from \cite{SCMFSA_9.ABS}.
Numerous additional properties of the {\tt while} macro are then proven.
In the last section, we define a macro instruction computing the
{\tt fusc} function
(see the SCM program computing the same function in \cite{FIB_FUSC.ABS})
and prove its correctness.}}

