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

### Summary.

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

#### 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] 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]