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

Magnitude Relation Properties of Radix-$2^k$ SD Number

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


In this article, magnitude relation properties of Radix-$2^k$ SD number are discussed.\par Until now, the Radix-$2^k$ SD Number is proposed for the high-speed calculations for RSA Cryptograms. In RSA Cryptograms, many modulo calculations are used, and modulo calculations need a comparison between two numbers.\par In this article, we discussed about a magnitude relation of Radix-$2^k$ SD Number. In the first section, we prepared some useful theorems for operations of Radix-$2^k$ SD Number. In the second section, we proved some properties about the primary numbers expressed by Radix-$2^k$ SD Number such as 0, 1, and Radix(k). In the third section, we proved primary magnitude relations between two Radix-$2^k$ SD Numbers. In the fourth section, we defined Max/Min numbers in some cases. And in the last section, we proved some relations about the addition of Max/Min numbers.

MML Identifier: RADIX_5

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

Contents (PDF format)

  1. Some Useful Theorems
  2. Properties of Primary Radix-$2^k$ SD Number
  3. Primary Magnitude Relation of Radix-$2^k$ SD Number
  4. Definition of Max/Min Radix-$2^k$ SD Numbers in Some Digits
  5. Properties of Max/Min Radix-$2^k$ SD Numbers


[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] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.
[7] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.
[8] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

Received November 7, 2003

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