:: High Speed Adder Algorithm with Radix-$2^k$ SD_Sub Number :: by Masaaki Niimura and Yasushi Fuwa :: :: Received January 3, 2003 :: Copyright (c) 2003-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, NAT_1, INT_1, XXREAL_0, ARYTM_3, RADIX_1, POWER, RELAT_1, RADIX_3, ARYTM_1, SUBSET_1, FINSEQ_1, NEWTON, CARD_1, FINSEQ_2, TARSKI, FUNCT_1, ORDINAL4, PARTFUN1, CARD_3, RADIX_4; notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, NAT_D, FUNCT_1, PARTFUN1, NEWTON, POWER, XXREAL_0, FINSEQ_1, FINSEQ_2, GR_CY_1, RADIX_1, RADIX_3; constructors REAL_1, NAT_D, NEWTON, POWER, BINARITH, GR_CY_1, RADIX_3; registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, VALUED_0, FINSEQ_2, ORDINAL1; 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 2 <= k implies 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 k >= 2 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 that i in Seg n and 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)) );