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

### High Speed Adder Algorithm with Radix-\$2^k\$ Sub Signed-Digit Number

by
Masaaki Niimura, and
Yasushi Fuwa

Received January 3, 2003

MML identifier: RADIX_4
[ Mizar article, MML identifier index ]

```environ

vocabulary INT_1, NAT_1, ARYTM_1, POWER, MIDSP_3, FINSEQ_1, FUNCT_1, RELAT_1,
RLVECT_1, RADIX_1, FINSEQ_4, RADIX_3, RADIX_4, GROUP_1;
notation TARSKI, SUBSET_1, XCMPLX_0, XREAL_0, INT_1, NAT_1, FUNCT_1, POWER,
FINSEQ_1, FINSEQ_4, BINARITH, TREES_4, WSIERP_1, MIDSP_3, RADIX_1,
RADIX_3;
constructors REAL_1, POWER, BINARITH, FINSEQ_4, EULER_2, RADIX_3, MEMBERED;
clusters INT_1, RELSET_1, NAT_1, MEMBERED;
requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;

begin :: Some Useful Theorems

reserve i,n,m,k,x,y for Nat,
i1 for Integer;

theorem :: RADIX_4:1
for k be Nat st 2 <= k holds 2 < Radix(k);

begin :: Carry operation at n+1 digits Radix-2^k SD_Sub number

theorem :: RADIX_4:2
for x,y be Integer, k be Nat st 3 <= k holds
SDSub_Add_Carry( SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k), k ) = 0;

theorem :: RADIX_4:3
2 <= k implies
DigA_SDSub(SD2SDSub(DecSD(m,n,k)),n+1)
= SDSub_Add_Carry( DigA(DecSD(m,n,k),n), k);

theorem :: RADIX_4:4
2 <= k & m is_represented_by 1,k implies
DigA_SDSub(SD2SDSub(DecSD(m,1,k)),1+1) = SDSub_Add_Carry(m, k);

theorem :: RADIX_4:5
for k,x,n be Nat st
n >= 1 & k >= 3 & x is_represented_by (n+1),k holds
DigA_SDSub(SD2SDSub(DecSD(x mod (Radix(k) |^ n),n,k)),n+1)
= SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k);

theorem :: RADIX_4:6
2 <= k & m is_represented_by 1,k implies
DigA_SDSub(SD2SDSub(DecSD(m,1,k)),1) = m - SDSub_Add_Carry(m,k)*Radix(k);

theorem :: RADIX_4:7
for k,x,n be Nat st
n >= 1 & k >= 2 & x is_represented_by (n+1),k holds
(Radix(k) |^ n) * DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1)
= (Radix(k) |^ n) * DigA(DecSD(x,n+1,k),n+1)
- (Radix(k) |^ (n+1)) * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k)
+ (Radix(k) |^ n) * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k);

begin :: Definition for adder operation on Radix-2^k SD-Sub number

definition
let i,n,k be Nat,
x be Tuple of n,(k-SD_Sub), y be Tuple of n,(k-SD_Sub);
assume i in Seg n & k >= 2;
func SDSubAddDigit(x,y,i,k) -> Element of k-SD_Sub equals
:: RADIX_4:def 1

SDSub_Add_Data( DigA_SDSub(x,i) + DigA_SDSub(y,i), k )
+ SDSub_Add_Carry( DigA_SDSub(x,i -'1) + DigA_SDSub(y,i -'1), k);
end;

definition let n,k be Nat,x,y be Tuple of n,(k-SD_Sub);
func x '+' y -> Tuple of n,(k-SD_Sub) means
:: RADIX_4:def 2

for i st i in Seg n holds DigA_SDSub(it,i) = SDSubAddDigit(x,y,i,k);
end;

theorem :: RADIX_4:8
for i st i in Seg n holds
2 <= k implies
SDSubAddDigit(SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),i,k)=
SDSubAddDigit(
SD2SDSub(DecSD((x mod (Radix(k) |^ n)),n,k)),
SD2SDSub(DecSD((y mod (Radix(k) |^ n)),n,k)),i,k);

theorem :: RADIX_4:9
for n st n >= 1 holds
for k,x,y st
k >= 3 & x is_represented_by n,k & y is_represented_by n,k holds
x + y =
SDSub2IntOut( SD2SDSub(DecSD(x,n,k)) '+' SD2SDSub(DecSD(y,n,k)) );
```

Back to top