The abstract of the Mizar article:

High Speed Modulo Calculation Algorithm with Radix-$2^k$ SD Number

by

Masaaki Niimura, and

Yasushi Fuwa

Received November 7, 2003

MML identifier: RADIX_6

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM_1, NAT_1, INT_1, RADIX_1, FINSEQ_1, MIDSP_3, FINSEQ_4,
      GROUP_1, RELAT_1, RLVECT_1, FUNCT_1, RADIX_5, RADIX_6;
 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;
 constructors REAL_1, BINARITH, FINSEQ_4, RADIX_5;
 clusters XREAL_0, INT_1, RELSET_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin

theorem :: RADIX_6:1
  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));

theorem :: RADIX_6:2
  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
:: RADIX_6:def 1

    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
:: RADIX_6:def 2

    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
:: RADIX_6:def 3

    r.i if i >= m,
    Radix(k)-1 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
:: RADIX_6:def 4

    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
:: RADIX_6:def 5

    r.i if i >= m,
    -Radix(k)+1 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
:: RADIX_6:def 6

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

theorem :: RADIX_6:3
  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);

theorem :: RADIX_6:4
  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
:: RADIX_6:def 7

    x < (Radix(k) |^ n) & x >= (Radix(k) |^ (n-'1));
end;

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

theorem :: RADIX_6:6
  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;

theorem :: RADIX_6:7
  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

theorem :: RADIX_6:8
  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;

theorem :: RADIX_6:9
  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));

theorem :: RADIX_6:10
  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));

theorem :: RADIX_6:11
  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));

theorem :: RADIX_6:12
  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));

theorem :: RADIX_6:13
  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));

theorem :: RADIX_6:14
  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 );

theorem :: RADIX_6:15
  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 );

theorem :: RADIX_6:16
  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
:: RADIX_6:def 8

    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
:: RADIX_6:def 9

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

theorem :: RADIX_6:17
  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));

theorem :: RADIX_6:18
  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
:: RADIX_6:def 10

    0 if i > m,
    1 if i = m
    otherwise -Radix(k)+1;
end;

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

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

theorem :: RADIX_6:19
  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
:: RADIX_6:def 12

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

theorem :: RADIX_6:20
  for m be Nat st m >= 1 holds
    for n,k be Nat, r be Tuple of m+2,k-SD st
      k >= 2 & n in Seg (m+2) &
        Mmask(r) is_Zero_over n & DigA(Mmask(r),n) > 0 holds
          SDDec(Mmask(r)) > 0;