@misc{AOFA_I00.MIZ,
  AUTHOR = {Bancerek, Grzegorz},
  TITLE = {Mizar Analysis of Algorithms: Algorithms over Integers},
  ACKNOWLEDGEMENT = {This work has been partially supported by the
  Bia{\l}ystok Technical University grant W/WI/1/06},
  SECTION1 = {Preliminaries},
  SECTION2 = {If-while Algebra over Integers},
  SECTION3 = {Termination in If-while Algebras over Integers },
  SECTION4 = {Examples},
  ADDRESS1 = {Bia{\l}ystok Technical University},
  YEAR = {2008},
  MONTH = {March},
  DAY = {18},
  SUMMARY = {This paper is a continuation of \cite{AOFA_000.ABS}
  and concerns if-while algebras over integers.
  In these algebras the only elementary instructions are assignment instructions.
  The instruction assigns to a (program) variable a value
  which is calculated for the current state according to some
  arithmetic expression. The expression may include variables,
  constants, and a limited number of arithmetic operations.
  States are functions from a given set of locations
  into integers. A variable is a function from the states into the locations
  and an expression is a function from the states into integers.
  Additional conditions (computability) limit the set of variables and expressions and,
  simultaneously, allow to write algorithms in a natural way
  (and to prove their correctness).\par
  As examples the proofs of full correctness of two Euclid algorithms
  (with modulo operation and subtraction) and
  algorithm of exponentiation by squaring are given.
  }}
