@MISC{AMI_3.MIZ,
  AUTHOR = {Trybulec, Andrzej and Nakamura, Yatsuka},
  TITLE = {Some Remarks on the Simple Concrete Model of Computer},
  SECTION1 = {A small concrete machine},
  SECTION2 = {Users guide},
  SECTION3 = {Preliminaries},
  SECTION4 = {Some Remarks on AMI-Struct},
  SECTION5 = {Instruction Locations and Data Locations},
  SECTION6 = {Halt Instruction},
  DAY = {08},
  MONTH = {October},
  YEAR = {1993},
  ADDRESS1 = {Warsaw University\\Bia{\l}ystok},
  ADDRESS2 = {Shinshu University\\Nagano},
  SUMMARY = {We prove some results on {\bf SCM} needed for the proof
of the correctness
of Euclid's algorithm. We introduce the following concepts:
 \begin{itemize}
 \item[-] starting finite partial state (Start-At$(l)$), then assigns to
 the instruction counter an instruction location (and consists only of
 this assignment),
 \item[-] programmed finite partial state, that consists of the instructions
  (to be more precise, a finite partial state with the domain consisting
   of instruction locations).
 \end{itemize}
We define for a total state $s$ what it means that
 $s$ starts at $l$ (the value of the instruction counter in the state $s$ 
is $l$) and
 $s$ halts at $l$ (the halt instruction is assigned to $l$ in the state $s$).
Similar notions are defined for finite partial states.}}