@MISC{AMI_4.MIZ,
  AUTHOR = {Trybulec, Andrzej and Nakamura, Yatsuka},
  TITLE = {Euclid's Algorithm},
  SECTION1 = {Preliminaries},
  SECTION2 = {Euclid's Algorithm},
  SECTION3 = {The Natural Semantics of the Euclid's Algorithm},
  DAY = {08},
  MONTH = {October},
  YEAR = {1993},
  ADDRESS1 = {Warsaw University\\Bia{\l}ystok},
  ADDRESS2 = {Shinshu University\\Nagano},
  SUMMARY = {The main goal of the paper is to prove the correctness of
the Euclid's algorithm for {\bf SCM}. We define the Euclid's
algorithm and describe the natural semantics of it. Eventually we prove
that the Euclid's algorithm computes the Euclid's function.
Let us observe that the Euclid's function is defined as a function
mapping finite partial states to finite partial states of {\bf SCM}
rather than pairs of integers to integers.}}

