@misc{AOFA_000.MIZ,
  AUTHOR = {Bancerek, Grzegorz},
  TITLE = {Mizar Analysis of Algorithms: Preliminaries},
  SECTION1 = {Binary Operations, Orbits, and Iterations},
  SECTION2 = {Free Universal Algebras},
  SECTION3 = {If-while Algebra},
  SECTION4 = {Execution Function},
  SECTION5 = {Existence and Uniqueness of Execution Function and Termination},
  ADDRESS1 = {Bia{\l}ystok Technical University},
  YEAR = {2007},
  MONTH = {July},
  DAY = {9},
  SUMMARY = {Algorithms and its parts -- instructions -- are introduced
  as elements of if-while algebras. An if-while algebra is a (1-sorted)
  universal algebra which has 4 operations:
   a constant -- the empty instruction,
   a binary catenation of instructions,
   a ternary conditional instruction, and
   a binary while instruction.
   An execution function is defined on pairs $(s,I)$, where $s$
   is a state (an element of certain set of states) and $I$ is
   an instruction, and results in states. The execution function
   obeys control structures using the set of distinguished
   true states. I.e., a condition instruction is executed and
   the continuation of execution depends on if the resulting state
   is in true states or not.
   Termination is also defined for pairs $(s,I)$ and depends
   on the execution function. The existence of execution function
   determined on elementary instructions and the uniqueness of
   it for terminating instructions are shown.}}
