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

by
Masaaki Niimura, and
Yasushi Fuwa

[ Mizar article, MML identifier index ]

```environ

vocabulary ARYTM_1, NAT_1, INT_1, RADIX_1, FINSEQ_1, MIDSP_3, FINSEQ_4,
notation TARSKI, SUBSET_1, XCMPLX_0, XREAL_0, INT_1, NAT_1, BINARITH, RADIX_1,
MIDSP_3, FINSEQ_4, FINSEQ_1, FUNCT_1, RELSET_1, WSIERP_1, RADIX_5;
clusters XREAL_0, INT_1, RELSET_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin

for n be Nat st n >= 1 holds
for m,k be Nat st m >= 1 & k >= 2 holds
SDDec(Fmin(m+n,m,k)) = SDDec(Fmin(m,m,k));

for m,k be Nat st m >= 1 & k >= 2 holds
SDDec(Fmin(m,m,k)) > 0;

begin :: Definitions of Upper 3 Digits of Radix-\$2^k\$ SD number and its property

definition
let i,m,k be Nat, r be Tuple of (m+2),(k-SD);
assume
i in Seg (m+2);
func M0Digit(r,i) -> Element of k-SD equals

r.i if i >= m,
0 if i < m;
end;

definition
let m,k be Nat, r be Tuple of (m+2),(k-SD);
func M0(r) -> Tuple of (m+2),k-SD means

for i be Nat st i in Seg (m+2) holds DigA(it,i) = M0Digit(r,i);
end;

definition let i,m,k be Nat, r be Tuple of (m+2),(k-SD);
assume that
k >= 2 and
i in Seg (m+2);
func MmaxDigit(r,i) -> Element of k-SD equals

r.i if i >= m,
end;

definition let m,k be Nat, r be Tuple of (m+2),(k-SD);
func Mmax(r) -> Tuple of (m+2),k-SD means

for i be Nat st i in Seg (m+2) holds DigA(it,i) = MmaxDigit(r,i);
end;

definition let i,m,k be Nat, r be Tuple of (m+2),(k-SD);
assume that
k >= 2 and
i in Seg (m+2);
func MminDigit(r,i) -> Element of k-SD equals

r.i if i >= m,
end;

definition let m,k be Nat, r be Tuple of (m+2),(k-SD);
func Mmin(r) -> Tuple of (m+2),k-SD means

for i be Nat st i in Seg (m+2) holds DigA(it,i) = MminDigit(r,i);
end;

for m,k be Nat st m >= 1 & k >= 2 holds
for r be Tuple of (m+2),k-SD holds
SDDec(Mmax(r)) >= SDDec(r);

for m,k be Nat st m >= 1 & k >= 2 holds
for r be Tuple of (m+2),k-SD holds
SDDec(r) >= SDDec(Mmin(r));

begin :: Properties of minimum digits of Radix-\$2^k\$ SD number

definition let n,k be Nat, x be Integer;
pred x needs_digits_of n,k means

end;

for x,n,k,i be Nat st i in Seg n holds
DigA(DecSD(x,n,k),i) >= 0;

for n,k,x be Nat st
n >= 1 & k >= 2 & x needs_digits_of n,k holds
DigA(DecSD(x,n,k),n) > 0;

for f,m,k be Nat st
m >= 1 & k >= 2 & f needs_digits_of m,k holds
f >= SDDec(Fmin(m+2,m,k));

begin :: Modulo calculation algorithm using Upper 3 Digits of Radix-\$2^k\$ SD number

for mlow,mhigh,f be Integer st mhigh < mlow + f & f > 0 holds
ex s be Integer st -f < mlow - s * f & mhigh - s * f < f;

for m,k be Nat st m >= 1 & k >= 2 holds
for r be Tuple of (m+2),k-SD holds
SDDec(Mmax(r)) + SDDec(DecSD(0,m+2,k))
= SDDec(M0(r)) + SDDec(SDMax(m+2,m,k));

for m,k be Nat st m >= 1 & k >= 2 holds
for r be Tuple of (m+2),k-SD holds
SDDec(Mmax(r)) < SDDec(M0(r)) + SDDec(Fmin(m+2,m,k));

for m,k be Nat st m >= 1 & k >= 2 holds
for r be Tuple of (m+2),k-SD holds
SDDec(Mmin(r)) + SDDec(DecSD(0,m+2,k))
= SDDec(M0(r)) + SDDec(SDMin(m+2,m,k));

for m,k be Nat, r be Tuple of (m+2),k-SD st m >= 1 & k >= 2 holds
SDDec(M0(r)) + SDDec(DecSD(0,m+2,k))
= SDDec(Mmin(r)) + SDDec(SDMax(m+2,m,k));

for m,k be Nat st m >= 1 & k >= 2 holds
for r be Tuple of (m+2),k-SD holds
SDDec(M0(r)) < SDDec(Mmin(r)) + SDDec(Fmin(m+2,m,k));

for m,k,f be Nat, r be Tuple of (m+2),k-SD
st m >= 1 & k >= 2 & f needs_digits_of m,k holds
ex s be Integer st
(- f < (SDDec(M0(r)) - s*f)) &  ( SDDec(Mmax(r)) - s*f < f );

for m,k,f be Nat, r be Tuple of (m+2),k-SD
st m >= 1 & k >= 2 & f needs_digits_of m,k holds
ex s be Integer st
(- f < (SDDec(Mmin(r)) - s*f)) &  ( SDDec(M0(r)) - s*f < f );

for m,k be Nat, r be Tuple of (m+2),k-SD st m >= 1 & k >= 2 holds
SDDec(M0(r)) <= SDDec(r) & SDDec(r) <= SDDec(Mmax(r))
or
SDDec(Mmin(r)) <= SDDec(r) & SDDec(r) < SDDec(M0(r));

begin :: How to identify the range of modulo arithmetic result

definition
let i,m,k be Nat, r be Tuple of (m+2),(k-SD);
assume
i in Seg (m+2);
func MmaskDigit(r,i) -> Element of k-SD equals

r.i if i< m,
0 if i >= m;
end;

definition
let m,k be Nat, r be Tuple of (m+2),(k-SD);
func Mmask(r) -> Tuple of (m+2),k-SD means

for i be Nat st i in Seg (m+2) holds DigA(it,i) = MmaskDigit(r,i);
end;

for m,k be Nat, r be Tuple of (m+2),k-SD st m >= 1 & k >= 2 holds
SDDec(M0(r)) + SDDec(Mmask(r)) = SDDec(r) + SDDec(DecSD(0,m+2,k));

for m,k be Nat, r be Tuple of (m+2),k-SD st m >= 1 & k >= 2 holds
SDDec(Mmask(r)) > 0 implies SDDec(r) > SDDec(M0(r));

definition let i,m,k be Nat;
assume
k >= 2;
func FSDMinDigit(m,k,i) -> Element of k-SD equals

0 if i > m,
1 if i = m
end;

definition let n,m,k be Nat;
func FSDMin(n,m,k) -> Tuple of n,k-SD means

for i be Nat st i in Seg n holds DigA(it,i) = FSDMinDigit(m,k,i);
end;

for n be Nat st n >= 1 holds
for m,k be Nat st m in Seg n & k >= 2 holds
SDDec(FSDMin(n,m,k)) = 1;

definition let n,m,k be Nat, r be Tuple of m+2,k-SD;
pred r is_Zero_over n means

for i be Nat st i > n holds
DigA(r,i) = 0;
end;