The abstract of the Mizar article:

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)) );