Volume 11, 1999

University of Bialystok

Copyright (c) 1999 Association of Mizar Users

**Yoshinori Fujisawa**- Shinshu University, Nagano
**Yasushi Fuwa**- Shinshu University, Nagano

- In this article, a radix-$2^k$ signed-digit number (Radix-$2^k$ SD number) is defined and based on it a high-speed adder algorithm is discussed. \par The processes of coding and encoding for public-key cryptograms require a great deal of addition operations of natural number of many figures. This results in a~long time for the encoding and decoding processes. It is possible to reduce the processing time using the high-speed adder algorithm.\par In the first section of this article, we prepared some useful theorems for natural numbers and integers. In the second section, we defined the concept of radix-$2^k$, a set named $k$-SD and proved some properties about them. In the third section, we provide some important functions for generating Radix-$2^k$ SD numbers from natural numbers and natural numbers from Radix-$2^k$ SD numbers. In the fourth section, we defined the carry and data components of addition with Radix-$2^k$ SD numbers and some properties about them. In the fifth section, we defined a theorem for checking whether or not a natural number can be expressed as $n$ digits Radix-$2^k$ SD number. \par In the last section, a high-speed adder algorithm on Radix-$2^k$ SD numbers is proposed and we provided some properties. In this algorithm, the carry of each digit has an effect on only the next digit. Properties of the relationships of the results of this algorithm to the operations of natural numbers are also given.

- Some Useful Theorems
- Definition for Radix-$2^k$, $k$-SD
- Functions for Generating Radix-$2^k$ SD Numbers from Natural Numbers and Natural Numbers from Radix-$2^k$ SD Numbers
- Definition for Carry and Data Components of Addition
- Definition for Checking whether or not a Natural Number can be Expressed as n Digits Radix-$2^k$ SD Number
- Definition for Addition Operation for a High-Speed Adder Algorithm on Radix-$2^k$ SD Number

- [1]
Grzegorz Bancerek.
The fundamental properties of natural numbers.
*Journal of Formalized Mathematics*, 1, 1989. - [2]
Grzegorz Bancerek.
Joining of decorated trees.
*Journal of Formalized Mathematics*, 5, 1993. - [3]
Grzegorz Bancerek and Krzysztof Hryniewiecki.
Segments of natural numbers and finite sequences.
*Journal of Formalized Mathematics*, 1, 1989. - [4]
Czeslaw Bylinski.
Functions and their basic properties.
*Journal of Formalized Mathematics*, 1, 1989. - [5]
Andrzej Kondracki.
The Chinese Remainder Theorem.
*Journal of Formalized Mathematics*, 9, 1997. - [6]
Takaya Nishiyama and Yasuho Mizuhara.
Binary arithmetics.
*Journal of Formalized Mathematics*, 5, 1993. - [7]
Konrad Raczkowski and Andrzej Nedzusiak.
Real exponents and logarithms.
*Journal of Formalized Mathematics*, 2, 1990. - [8]
Andrzej Trybulec.
Tarski Grothendieck set theory.
*Journal of Formalized Mathematics*, Axiomatics, 1989. - [9]
Michal J. Trybulec.
Integers.
*Journal of Formalized Mathematics*, 2, 1990. - [10]
Wojciech A. Trybulec.
Pigeon hole principle.
*Journal of Formalized Mathematics*, 2, 1990. - [11]
Zinaida Trybulec.
Properties of subsets.
*Journal of Formalized Mathematics*, 1, 1989.

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