:: Improvement of Radix-$2^k$ Signed-Digit Number for High Speed Circuit :: 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, RADIX_1, ARYTM_1, ARYTM_3, POWER, RELAT_1, CARD_1, FINSEQ_1, NEWTON, SUBSET_1, TARSKI, XBOOLE_0, FINSEQ_2, FUNCT_1, PARTFUN1, CARD_3, ORDINAL4, RADIX_3; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, NAT_D, FUNCT_1, PARTFUN1, NEWTON, POWER, FINSEQ_1, FINSEQ_2, GR_CY_1, RADIX_1; constructors REAL_1, NAT_D, NEWTON, POWER, BINARITH, GR_CY_1, RADIX_1, RELSET_1; registrations RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, VALUED_0, FINSEQ_2, CARD_1, ORDINAL1; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Definition for Radix-2^k SD_Sub number reserve i,n,m,k,x for Nat, i1,i2 for Integer; definition let k; func k-SD_Sub_S -> set equals :: RADIX_3:def 1 {e where e is Element of INT: e >= -Radix(k -' 1) & e <= Radix(k -' 1) - 1 }; func k-SD_Sub -> set equals :: RADIX_3:def 2 {e where e is Element of INT: e >= -Radix(k -' 1) - 1 & e <= Radix(k -' 1) }; end; theorem :: RADIX_3:1 i1 in k-SD_Sub implies -Radix(k-'1) - 1 <= i1 & i1 <= Radix(k-'1); theorem :: RADIX_3:2 k-SD_Sub_S c= k-SD_Sub; theorem :: RADIX_3:3 k-SD_Sub_S c= (k+1)-SD_Sub_S; theorem :: RADIX_3:4 2 <= k implies k-SD_Sub c= k-SD; theorem :: RADIX_3:5 0 in 0-SD_Sub_S; theorem :: RADIX_3:6 0 in k-SD_Sub_S; theorem :: RADIX_3:7 0 in k-SD_Sub; theorem :: RADIX_3:8 for e being set st e in k-SD_Sub holds e is Integer; theorem :: RADIX_3:9 k-SD_Sub c= INT; theorem :: RADIX_3:10 k-SD_Sub_S c= INT; registration let k; cluster k-SD_Sub_S -> non empty; cluster k-SD_Sub -> non empty; end; definition let k; redefine func k-SD_Sub_S -> non empty Subset of INT; end; definition let k; redefine func k-SD_Sub -> non empty Subset of INT; end; reserve a for Tuple of n,k-SD; reserve aSub for Tuple of n,k-SD_Sub; theorem :: RADIX_3:11 i in Seg n implies aSub.i is Element of k-SD_Sub; begin :: Definition for new carry calculation method definition let x be Integer, k be Nat; func SDSub_Add_Carry(x,k) -> Integer equals :: RADIX_3:def 3 1 if Radix(k -' 1) <= x, -1 if x < -Radix(k -' 1) otherwise 0; end; definition let x be Integer, k be Nat; func SDSub_Add_Data(x,k) -> Integer equals :: RADIX_3:def 4 x - Radix(k) * SDSub_Add_Carry(x, k); end; theorem :: RADIX_3:12 for x be Integer, k be Nat holds -1 <= SDSub_Add_Carry(x,k) & SDSub_Add_Carry(x,k) <= 1; theorem :: RADIX_3:13 2 <= k & i1 in k-SD implies SDSub_Add_Data(i1,k) >= -Radix(k-'1) & SDSub_Add_Data(i1,k) <= Radix(k-'1) - 1; theorem :: RADIX_3:14 for x be Integer, k be Nat st 2 <= k holds SDSub_Add_Carry(x,k) in k-SD_Sub_S ; theorem :: RADIX_3:15 2 <= k & i1 in k-SD implies SDSub_Add_Data(i1,k) + SDSub_Add_Carry(i2,k) in k-SD_Sub; theorem :: RADIX_3:16 SDSub_Add_Carry(0,k) = 0; begin :: Definition for translation from Radix-2^k SD number definition let i,k,n be Nat, x be Tuple of n,(k-SD_Sub); func DigA_SDSub(x,i) -> Integer equals :: RADIX_3:def 5 x.i if i in Seg n, 0 if i = 0; end; definition let i,k,n be Nat, x be Tuple of n,(k-SD); func SD2SDSubDigit(x,i,k) -> Integer equals :: RADIX_3:def 6 SDSub_Add_Data(DigA(x,i), k)+SDSub_Add_Carry(DigA(x,i-'1),k) if i in Seg n, SDSub_Add_Carry(DigA(x,i-'1), k) if i = n + 1 otherwise 0; end; theorem :: RADIX_3:17 2 <= k & i in Seg (n+1) implies SD2SDSubDigit(a,i,k) is Element of k-SD_Sub; definition let i,k,n be Nat, x be Tuple of n,(k-SD); assume 2 <= k & i in Seg (n+1); func SD2SDSubDigitS(x,i,k) -> Element of k-SD_Sub equals :: RADIX_3:def 7 SD2SDSubDigit(x,i,k); end; definition let n,k be Nat, x be Tuple of n,(k-SD); func SD2SDSub(x) -> Tuple of (n+1),(k-SD_Sub) means :: RADIX_3:def 8 for i be Nat st i in Seg (n+1) holds DigA_SDSub(it,i) = SD2SDSubDigitS(x,i,k); end; theorem :: RADIX_3:18 i in Seg n implies DigA_SDSub(aSub,i) is Element of k-SD_Sub; theorem :: RADIX_3:19 2 <= k & i1 in k-SD & i2 in k-SD_Sub implies SDSub_Add_Data(i1+i2,k) in k-SD_Sub_S; begin :: Definiton for Translation from Radix-2^k SD_Sub number to INT definition let i,k,n be Nat, x be Tuple of n,(k-SD_Sub); func DigB_SDSub(x,i) -> Element of INT equals :: RADIX_3:def 9 DigA_SDSub(x,i); end; definition let i,k,n be Nat, x be Tuple of n, k-SD_Sub; func SDSub2INTDigit(x,i,k) -> Element of INT equals :: RADIX_3:def 10 (Radix(k) |^ (i -'1)) * DigB_SDSub(x,i); end; definition let n,k be Nat, x be Tuple of n, k-SD_Sub; func SDSub2INT(x) -> Tuple of n,INT means :: RADIX_3:def 11 for i be Nat st i in Seg n holds it/.i = SDSub2INTDigit(x,i,k); end; definition let n,k be Nat, x be Tuple of n,(k-SD_Sub); func SDSub2IntOut(x) -> Integer equals :: RADIX_3:def 12 Sum SDSub2INT(x); end; theorem :: RADIX_3:20 for i st i in Seg n holds 2 <= k implies DigA_SDSub(SD2SDSub( DecSD(m,n+1,k)),i) = DigA_SDSub(SD2SDSub(DecSD((m mod (Radix(k) |^ n)),n,k)),i) ; theorem :: RADIX_3:21 for n st n >= 1 holds for k,x st k >= 2 & x is_represented_by n,k holds x = SDSub2IntOut( SD2SDSub(DecSD(x,n,k)) );