:: High Speed Modulo Calculation Algorithm with Radix-$2^k$ SD Number :: by Masaaki Niimura and Yasushi Fuwa :: :: Received November 7, 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, XXREAL_0, ARYTM_3, RADIX_1, RADIX_5, FINSEQ_1, CARD_1, FUNCT_1, NEWTON, RELAT_1, PARTFUN1, ARYTM_1, CARD_3, FINSEQ_2, SUBSET_1, INT_1, RADIX_6; notations SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, NAT_D, NEWTON, RADIX_1, FINSEQ_1, FINSEQ_2, FUNCT_1, RELSET_1, PARTFUN1, GR_CY_1, RADIX_5; constructors REAL_1, NAT_D, NEWTON, GR_CY_1, RADIX_5, RELSET_1; registrations RELSET_1, XREAL_0, NAT_1, INT_1, ORDINAL1, NEWTON, FINSEQ_2; 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 otherwise 0; 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 otherwise Radix(k)-1; 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 otherwise -Radix(k)+1; 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 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 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 & 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 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 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 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 otherwise 0; 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 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;