Journal of Formalized Mathematics
Volume 5, 1993
University of Bialystok
Copyright (c) 1993 Association of Mizar Users

## Some Remarks on the Simple Concrete Model of Computer

Andrzej Trybulec
Warsaw University, Bialystok
Yatsuka Nakamura
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.

#### MML Identifier: AMI_3

The terminology and notation used in this paper have been introduced in the following articles [15] [14] [19] [3] [2] [17] [6] [7] [18] [1] [16] [8] [4] [13] [20] [9] [10] [5] [11] [12]

#### Contents (PDF format)

1. A small concrete machine
2. Users guide
3. Preliminaries
4. Some Remarks on AMI-Struct
5. Instruction Locations and Data Locations
6. Halt Instruction

#### Bibliography

[1] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.
[2] Grzegorz Bancerek. The ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[3] Grzegorz Bancerek. Sequences of ordinal numbers. Journal of Formalized Mathematics, 1, 1989.
[4] Grzegorz Bancerek. K\"onig's theorem. Journal of Formalized Mathematics, 2, 1990.
[5] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.
[6] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.
[7] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.
[8] Czeslaw Bylinski. A classical first order language. Journal of Formalized Mathematics, 2, 1990.
[9] Czeslaw Bylinski. The modification of a function by a function and the iteration of the composition of a function. Journal of Formalized Mathematics, 2, 1990.
[10] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.
[11] Yatsuka Nakamura and Andrzej Trybulec. A mathematical model of CPU. Journal of Formalized Mathematics, 4, 1992.
[12] Yatsuka Nakamura and Andrzej Trybulec. On a mathematical model of programs. Journal of Formalized Mathematics, 4, 1992.
[13] Dariusz Surowik. Cyclic groups and some of their properties --- part I. Journal of Formalized Mathematics, 3, 1991.
[14] Andrzej Trybulec. Enumerated sets. Journal of Formalized Mathematics, 1, 1989.
[15] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[16] Andrzej Trybulec. Tuples, projections and Cartesian products. Journal of Formalized Mathematics, 1, 1989.
[17] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.
[18] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.
[19] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[20] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.