Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

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

- In this article, a new radix-$2^k$ signed-digit number (Radix-$2^k$ sub signed-digit number) is defined and its properties for hardware realization are discussed. \par Until now, high speed calculation method with Radix-$2^k$ signed-digit numbers is proposed, but this method used ``Compares With 2" to calculate carry. ``Compares with 2'' is a very simple method, but it needs very complicated hardware especially when the value of $k$ becomes large. In this article, we propose a subset of Radix-$2^k$ signed-digit, named Radix-$2^k$ sub signed-digit numbers. Radix-$2^k$ sub signed-digit was designed so that the carry calculation use ``bit compare'' to hardware-realization simplifies more.\par In the first section of this article, we defined the concept of Radix-$2^k$ sub signed-digit numbers and proved some of their properties. In the second section, we defined the new carry calculation method in consideration of hardware-realization, and proved some of their properties. In the third section, we provide some functions for generating Radix-$2^k$ sub signed-digit numbers from Radix-$2^k$ signed-digit numbers. In the last section, we defined some functions for generation natural numbers from Radix-$2^k$ sub signed-digit, and we clarified its correctness.

- Definition for Radix-$2^k$ Sub Signed-Digit Number
- Definition for New Carry Calculation Method
- Definition for Translation from Radix-$2^k$ Signed-Digit Number
- Definiton for Translation from Radix-$2^k$ Sub Signed-Digit Number to INT

- [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]
Yoshinori Fujisawa and Yasushi Fuwa.
Definitions of radix-$2^k$ signed-digit number and its adder algorithm.
*Journal of Formalized Mathematics*, 11, 1999. - [6]
Andrzej Kondracki.
The Chinese Remainder Theorem.
*Journal of Formalized Mathematics*, 9, 1997. - [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]
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]