Volume 5, 1993

University of Bialystok

Copyright (c) 1993 Association of Mizar Users

**Grzegorz Bancerek**- Polish Academy of Sciences, Institute of Mathematics, Warsaw
**Piotr Rudnicki**- University of Alberta, Department of Computing Science, Edmonton

- In two articles (this one and [4]) we discuss correctness of two short programs for the {\bf SCM} machine: one computes Fibonacci numbers and the other computes the {\em fusc} function of Dijkstra [9]. The limitations of current Mizar implementation rendered it impossible to present the correctness proofs for the programs in one article. This part is purely technical and contains a number of very specific lemmas about integer division, floor, exponentiation and logarithms. The formal definitions of the Fibonacci sequence and the {\em fusc} function may be of general interest.

This work was partially supported by NSERC Grant OGP9207 while the first author visited University of Alberta, May--June 1993.

Contents (PDF format)

- [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 and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Grzegorz Bancerek and Piotr Rudnicki.
Two programs for \bf scm. Part II - programs.
*Journal of Formalized Mathematics*, 5, 1993. - [5]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [6]
Czeslaw Bylinski.
Functions from a set to a set.
*Journal of Formalized Mathematics*, 1, 1989. - [7]
Czeslaw Bylinski.
Some basic properties of sets.
*Journal of Formalized Mathematics*, 1, 1989. - [8]
Czeslaw Bylinski.
Finite sequences and tuples of elements of a non-empty sets.
*Journal of Formalized Mathematics*, 2, 1990. - [9] Edsger W. Dijkstra. \em Selected Writings on Computing, a Personal Perspective.
- [10]
Konrad Raczkowski and Andrzej Nedzusiak.
Real exponents and logarithms.
*Journal of Formalized Mathematics*, 2, 1990. - [11]
Andrzej Trybulec.
Domains and their Cartesian products.
*Journal of Formalized Mathematics*, 1, 1989. - [12]
Andrzej Trybulec.
Tuples, projections and Cartesian products.
*Journal of Formalized Mathematics*, 1, 1989. - [13]
Andrzej Trybulec.
Subsets of real numbers.
*Journal of Formalized Mathematics*, Addenda, 2003. - [14]
Michal J. Trybulec.
Integers.
*Journal of Formalized Mathematics*, 2, 1990. - [15]
Wojciech A. Trybulec.
Pigeon hole principle.
*Journal of Formalized Mathematics*, 2, 1990. - [16]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989.

[ Download a postscript version, MML identifier index, Mizar home page]