Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

High Speed Modulo Calculation Algorithm with Radix-$2^k$ SD Number

Masaaki Niimura
Shinshu University, Nagano
Yasushi Fuwa
Shinshu University, Nagano


In RSA Cryptograms, many modulo calculations are used, but modulo calculation is based on many subtractions and it takes long time to calculate. In this article, we explain about a new modulo calculation algorithm using table. And we proof that upper 3 digits of Radix-$2^k$ SD numbers is enough to specify the answer. In the first section, we prepared some useful theorems for operations of Radix-$2^k$ SD Number. In the second section, we defined Upper 3 Digits of Radix-$2^k$ SD number and proved that property. In the third section, we proved some property about the minimum digits of Radix-$2^k$ SD number. In the fourth section, we identified the range of modulo arithmetic result and proved that the Upper 3 Digits indicate two possible answers. And in the last section, we defined a function to select true answer from the results of Upper 3 Digits.

MML Identifier: RADIX_6

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

Contents (PDF format)

  1. Some Useful Theorems
  2. Definitions of Upper 3 Digits of Radix-$2^k$ SD Number and Its Property
  3. Properties of Minimum Digits of Radix-$2^k$ SD Number
  4. Modulo Calculation Algorithm Using Upper 3 Digits of Radix-$2^k$ SD Number
  5. How to Identify the Range of Modulo Arithmetic Result


[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] Yoshinori Fujisawa and Yasushi Fuwa. Definitions of radix-$2^k$ signed-digit number and its adder algorithm. Journal of Formalized Mathematics, 11, 1999.
[5] Andrzej Kondracki. The Chinese Remainder Theorem. Journal of Formalized Mathematics, 9, 1997.
[6] Masaaki Niimura and Yasushi Fuwa. Magnitude relation properties of radix-$2^k$ sd number. Journal of Formalized Mathematics, 15, 2003.
[7] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.
[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] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.
[11] Edmund Woronowicz. Relations defined on sets. Journal of Formalized Mathematics, 1, 1989.

Received November 7, 2003

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