Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

Definitions of Radix-$2^k$ Signed-Digit Number and its Adder Algorithm

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.

MML Identifier: RADIX_1

The terminology and notation used in this paper have been introduced in the following articles [8] [11] [9] [1] [4] [7] [3] [10] [6] [2] [5]

Contents (PDF format)

  1. Some Useful Theorems
  2. Definition for Radix-$2^k$, $k$-SD
  3. Functions for Generating Radix-$2^k$ SD Numbers from Natural Numbers and Natural Numbers from Radix-$2^k$ SD Numbers
  4. Definition for Carry and Data Components of Addition
  5. Definition for Checking whether or not a Natural Number can be Expressed as n Digits Radix-$2^k$ SD Number
  6. 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.

Received September 7, 1999

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