Journal of Formalized Mathematics
Volume 10, 1998
University of Bialystok
Copyright (c) 1998
Association of Mizar Users
Binary Arithmetics. Binary Sequences

Robert Milewski

University of Bialystok
The terminology and notation used in this paper have been
introduced in the following articles
[14]
[8]
[1]
[11]
[12]
[15]
[3]
[5]
[2]
[13]
[6]
[4]
[10]
[9]
[7]

Binary Arithmetics

Binary Sequences
Bibliography
 [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
Journal of Formalized Mathematics,
1, 1989.
 [2]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
Journal of Formalized Mathematics,
1, 1989.
 [3]
Czeslaw Bylinski.
Functions and their basic properties.
Journal of Formalized Mathematics,
1, 1989.
 [4]
Czeslaw Bylinski.
Binary operations applied to finite sequences.
Journal of Formalized Mathematics,
2, 1990.
 [5]
Czeslaw Bylinski.
A classical first order language.
Journal of Formalized Mathematics,
2, 1990.
 [6]
Czeslaw Bylinski.
Some properties of restrictions of finite sequences.
Journal of Formalized Mathematics,
7, 1995.
 [7]
Agata Darmochwal.
The Euclidean space.
Journal of Formalized Mathematics,
3, 1991.
 [8]
Krzysztof Hryniewiecki.
Basic properties of real numbers.
Journal of Formalized Mathematics,
1, 1989.
 [9]
Yasuho Mizuhara and Takaya Nishiyama.
Binary arithmetics, addition and subtraction of integers.
Journal of Formalized Mathematics,
6, 1994.
 [10]
Takaya Nishiyama and Yasuho Mizuhara.
Binary arithmetics.
Journal of Formalized Mathematics,
5, 1993.
 [11]
Konrad Raczkowski and Andrzej Nedzusiak.
Real exponents and logarithms.
Journal of Formalized Mathematics,
2, 1990.
 [12]
Konrad Raczkowski and Andrzej Nedzusiak.
Series.
Journal of Formalized Mathematics,
3, 1991.
 [13]
Wojciech A. Trybulec.
Pigeon hole principle.
Journal of Formalized Mathematics,
2, 1990.
 [14]
Zinaida Trybulec.
Properties of subsets.
Journal of Formalized Mathematics,
1, 1989.
 [15]
Edmund Woronowicz.
Manyargument relations.
Journal of Formalized Mathematics,
2, 1990.
Received February 24, 1998
[
Download a postscript version,
MML identifier index,
Mizar home page]