:: High Speed Modulo Calculation Algorithm with Radix-$2^k$ SD Number :: by Masaaki Niimura and Yasushi Fuwa :: :: Received November 7, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin Lm1: for m being Nat st m >= 1 holds m + 2 > 1 proofend; theorem Th1: :: RADIX_6:1 for n being Nat st n >= 1 holds for m, k being Nat st m >= 1 & k >= 2 holds SDDec (Fmin ((m + n),m,k)) = SDDec (Fmin (m,m,k)) proofend; theorem :: RADIX_6:2 for m, k being Nat st m >= 1 & k >= 2 holds SDDec (Fmin (m,m,k)) > 0 proofend; begin definition let i, m, k be Nat; let r be Tuple of m + 2,k -SD ; assume A1: i in Seg (m + 2) ; func M0Digit (r,i) -> Element of k -SD equals :Def1: :: RADIX_6:def 1 r . i if i >= m otherwise 0 ; coherence ( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies 0 is Element of k -SD ) ) proofend; consistency for b1 being Element of k -SD holds verum ; end; :: deftheorem Def1 defines M0Digit RADIX_6:def_1_:_ for i, m, k being Nat for r being Tuple of m + 2,k -SD st i in Seg (m + 2) holds ( ( i >= m implies M0Digit (r,i) = r . i ) & ( not i >= m implies M0Digit (r,i) = 0 ) ); definition let m, k be Nat; let r be Tuple of m + 2,k -SD ; func M0 r -> Tuple of m + 2,k -SD means :Def2: :: RADIX_6:def 2 for i being Nat st i in Seg (m + 2) holds DigA (it,i) = M0Digit (r,i); existence ex b1 being Tuple of m + 2,k -SD st for i being Nat st i in Seg (m + 2) holds DigA (b1,i) = M0Digit (r,i) proofend; uniqueness for b1, b2 being Tuple of m + 2,k -SD st ( for i being Nat st i in Seg (m + 2) holds DigA (b1,i) = M0Digit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds DigA (b2,i) = M0Digit (r,i) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines M0 RADIX_6:def_2_:_ for m, k being Nat for r, b4 being Tuple of m + 2,k -SD holds ( b4 = M0 r iff for i being Nat st i in Seg (m + 2) holds DigA (b4,i) = M0Digit (r,i) ); definition let i, m, k be Nat; let r be Tuple of m + 2,k -SD ; assume that A1: k >= 2 and A2: i in Seg (m + 2) ; func MmaxDigit (r,i) -> Element of k -SD equals :Def3: :: RADIX_6:def 3 r . i if i >= m otherwise (Radix k) - 1; coherence ( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies (Radix k) - 1 is Element of k -SD ) ) proofend; consistency for b1 being Element of k -SD holds verum ; end; :: deftheorem Def3 defines MmaxDigit RADIX_6:def_3_:_ for i, m, k being Nat for r being Tuple of m + 2,k -SD st k >= 2 & i in Seg (m + 2) holds ( ( i >= m implies MmaxDigit (r,i) = r . i ) & ( not i >= m implies MmaxDigit (r,i) = (Radix k) - 1 ) ); definition let m, k be Nat; let r be Tuple of m + 2,k -SD ; func Mmax r -> Tuple of m + 2,k -SD means :Def4: :: RADIX_6:def 4 for i being Nat st i in Seg (m + 2) holds DigA (it,i) = MmaxDigit (r,i); existence ex b1 being Tuple of m + 2,k -SD st for i being Nat st i in Seg (m + 2) holds DigA (b1,i) = MmaxDigit (r,i) proofend; uniqueness for b1, b2 being Tuple of m + 2,k -SD st ( for i being Nat st i in Seg (m + 2) holds DigA (b1,i) = MmaxDigit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds DigA (b2,i) = MmaxDigit (r,i) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines Mmax RADIX_6:def_4_:_ for m, k being Nat for r, b4 being Tuple of m + 2,k -SD holds ( b4 = Mmax r iff for i being Nat st i in Seg (m + 2) holds DigA (b4,i) = MmaxDigit (r,i) ); definition let i, m, k be Nat; let r be Tuple of m + 2,k -SD ; assume that A1: k >= 2 and A2: i in Seg (m + 2) ; func MminDigit (r,i) -> Element of k -SD equals :Def5: :: RADIX_6:def 5 r . i if i >= m otherwise (- (Radix k)) + 1; coherence ( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies (- (Radix k)) + 1 is Element of k -SD ) ) proofend; consistency for b1 being Element of k -SD holds verum ; end; :: deftheorem Def5 defines MminDigit RADIX_6:def_5_:_ for i, m, k being Nat for r being Tuple of m + 2,k -SD st k >= 2 & i in Seg (m + 2) holds ( ( i >= m implies MminDigit (r,i) = r . i ) & ( not i >= m implies MminDigit (r,i) = (- (Radix k)) + 1 ) ); definition let m, k be Nat; let r be Tuple of m + 2,k -SD ; func Mmin r -> Tuple of m + 2,k -SD means :Def6: :: RADIX_6:def 6 for i being Nat st i in Seg (m + 2) holds DigA (it,i) = MminDigit (r,i); existence ex b1 being Tuple of m + 2,k -SD st for i being Nat st i in Seg (m + 2) holds DigA (b1,i) = MminDigit (r,i) proofend; uniqueness for b1, b2 being Tuple of m + 2,k -SD st ( for i being Nat st i in Seg (m + 2) holds DigA (b1,i) = MminDigit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds DigA (b2,i) = MminDigit (r,i) ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines Mmin RADIX_6:def_6_:_ for m, k being Nat for r, b4 being Tuple of m + 2,k -SD holds ( b4 = Mmin r iff for i being Nat st i in Seg (m + 2) holds DigA (b4,i) = MminDigit (r,i) ); theorem Th3: :: RADIX_6:3 for m, k being Nat st k >= 2 holds for r being Tuple of m + 2,k -SD holds SDDec (Mmax r) >= SDDec r proofend; theorem Th4: :: RADIX_6:4 for m, k being Nat st k >= 2 holds for r being Tuple of m + 2,k -SD holds SDDec r >= SDDec (Mmin r) proofend; begin definition let n, k be Nat; let x be Integer; predx needs_digits_of n,k means :Def7: :: RADIX_6:def 7 ( x < (Radix k) |^ n & x >= (Radix k) |^ (n -' 1) ); end; :: deftheorem Def7 defines needs_digits_of RADIX_6:def_7_:_ for n, k being Nat for x being Integer holds ( x needs_digits_of n,k iff ( x < (Radix k) |^ n & x >= (Radix k) |^ (n -' 1) ) ); theorem Th5: :: RADIX_6:5 for x, n, k, i being Nat st i in Seg n holds DigA ((DecSD (x,n,k)),i) >= 0 proofend; theorem Th6: :: RADIX_6:6 for n, k, x being Nat st n >= 1 & x needs_digits_of n,k holds DigA ((DecSD (x,n,k)),n) > 0 proofend; theorem Th7: :: RADIX_6:7 for f, m, k being Nat st m >= 1 & k >= 2 & f needs_digits_of m,k holds f >= SDDec (Fmin ((m + 2),m,k)) proofend; begin theorem Th8: :: RADIX_6:8 for mlow, mhigh, f being Integer st mhigh < mlow + f & f > 0 holds ex s being Integer st ( - f < mlow - (s * f) & mhigh - (s * f) < f ) proofend; theorem Th9: :: RADIX_6:9 for m, k being Nat st k >= 2 holds for r being 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))) proofend; theorem Th10: :: RADIX_6:10 for m, k being Nat st m >= 1 & k >= 2 holds for r being Tuple of m + 2,k -SD holds SDDec (Mmax r) < (SDDec (M0 r)) + (SDDec (Fmin ((m + 2),m,k))) proofend; theorem Th11: :: RADIX_6:11 for m, k being Nat st k >= 2 holds for r being 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))) proofend; theorem Th12: :: RADIX_6:12 for m, k being Nat for r being 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))) proofend; theorem Th13: :: RADIX_6:13 for m, k being Nat st m >= 1 & k >= 2 holds for r being Tuple of m + 2,k -SD holds SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k))) proofend; theorem :: RADIX_6:14 for m, k, f being Nat for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & f needs_digits_of m,k holds ex s being Integer st ( - f < (SDDec (M0 r)) - (s * f) & (SDDec (Mmax r)) - (s * f) < f ) proofend; theorem :: RADIX_6:15 for m, k, f being Nat for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & f needs_digits_of m,k holds ex s being Integer st ( - f < (SDDec (Mmin r)) - (s * f) & (SDDec (M0 r)) - (s * f) < f ) proofend; theorem :: RADIX_6:16 for m, k being Nat for r being Tuple of m + 2,k -SD holds ( not k >= 2 or ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) ) proofend; begin definition let i, m, k be Nat; let r be Tuple of m + 2,k -SD ; assume A1: i in Seg (m + 2) ; func MmaskDigit (r,i) -> Element of k -SD equals :Def8: :: RADIX_6:def 8 r . i if i < m otherwise 0 ; coherence ( ( i < m implies r . i is Element of k -SD ) & ( not i < m implies 0 is Element of k -SD ) ) proofend; consistency for b1 being Element of k -SD holds verum ; end; :: deftheorem Def8 defines MmaskDigit RADIX_6:def_8_:_ for i, m, k being Nat for r being Tuple of m + 2,k -SD st i in Seg (m + 2) holds ( ( i < m implies MmaskDigit (r,i) = r . i ) & ( not i < m implies MmaskDigit (r,i) = 0 ) ); definition let m, k be Nat; let r be Tuple of m + 2,k -SD ; func Mmask r -> Tuple of m + 2,k -SD means :Def9: :: RADIX_6:def 9 for i being Nat st i in Seg (m + 2) holds DigA (it,i) = MmaskDigit (r,i); existence ex b1 being Tuple of m + 2,k -SD st for i being Nat st i in Seg (m + 2) holds DigA (b1,i) = MmaskDigit (r,i) proofend; uniqueness for b1, b2 being Tuple of m + 2,k -SD st ( for i being Nat st i in Seg (m + 2) holds DigA (b1,i) = MmaskDigit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds DigA (b2,i) = MmaskDigit (r,i) ) holds b1 = b2 proofend; end; :: deftheorem Def9 defines Mmask RADIX_6:def_9_:_ for m, k being Nat for r, b4 being Tuple of m + 2,k -SD holds ( b4 = Mmask r iff for i being Nat st i in Seg (m + 2) holds DigA (b4,i) = MmaskDigit (r,i) ); theorem Th17: :: RADIX_6:17 for m, k being Nat for r being Tuple of m + 2,k -SD st k >= 2 holds (SDDec (M0 r)) + (SDDec (Mmask r)) = (SDDec r) + (SDDec (DecSD (0,(m + 2),k))) proofend; theorem :: RADIX_6:18 for m, k being Nat for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & SDDec (Mmask r) > 0 holds SDDec r > SDDec (M0 r) proofend; definition let i, m, k be Nat; assume A1: k >= 2 ; func FSDMinDigit (m,k,i) -> Element of k -SD equals :Def10: :: RADIX_6:def 10 0 if i > m 1 if i = m otherwise (- (Radix k)) + 1; coherence ( ( i > m implies 0 is Element of k -SD ) & ( i = m implies 1 is Element of k -SD ) & ( not i > m & not i = m implies (- (Radix k)) + 1 is Element of k -SD ) ) proofend; consistency for b1 being Element of k -SD st i > m & i = m holds ( b1 = 0 iff b1 = 1 ) ; end; :: deftheorem Def10 defines FSDMinDigit RADIX_6:def_10_:_ for i, m, k being Nat st k >= 2 holds ( ( i > m implies FSDMinDigit (m,k,i) = 0 ) & ( i = m implies FSDMinDigit (m,k,i) = 1 ) & ( not i > m & not i = m implies FSDMinDigit (m,k,i) = (- (Radix k)) + 1 ) ); definition let n, m, k be Nat; func FSDMin (n,m,k) -> Tuple of n,k -SD means :Def11: :: RADIX_6:def 11 for i being Nat st i in Seg n holds DigA (it,i) = FSDMinDigit (m,k,i); existence ex b1 being Tuple of n,k -SD st for i being Nat st i in Seg n holds DigA (b1,i) = FSDMinDigit (m,k,i) proofend; uniqueness for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds DigA (b1,i) = FSDMinDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds DigA (b2,i) = FSDMinDigit (m,k,i) ) holds b1 = b2 proofend; end; :: deftheorem Def11 defines FSDMin RADIX_6:def_11_:_ for n, m, k being Nat for b4 being Tuple of n,k -SD holds ( b4 = FSDMin (n,m,k) iff for i being Nat st i in Seg n holds DigA (b4,i) = FSDMinDigit (m,k,i) ); theorem Th19: :: RADIX_6:19 for n being Nat st n >= 1 holds for m, k being Nat st m in Seg n & k >= 2 holds SDDec (FSDMin (n,m,k)) = 1 proofend; definition let n, m, k be Nat; let r be Tuple of m + 2,k -SD ; predr is_Zero_over n means :Def12: :: RADIX_6:def 12 for i being Nat st i > n holds DigA (r,i) = 0 ; end; :: deftheorem Def12 defines is_Zero_over RADIX_6:def_12_:_ for n, m, k being Nat for r being Tuple of m + 2,k -SD holds ( r is_Zero_over n iff for i being Nat st i > n holds DigA (r,i) = 0 ); theorem :: RADIX_6:20 for m being Nat st m >= 1 holds for n, k being Nat for r being 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 proofend;