:: Magnitude Relation Properties of Radix-$2^k$ SD Number :: by Masaaki Niimura and Yasushi Fuwa :: :: Received November 7, 2003 :: Copyright (c) 2003-2012 Association of Mizar Users begin theorem Th1: :: RADIX_5:1 for k being Nat st k >= 2 holds (Radix k) - 1 in k -SD proofend; theorem Th2: :: RADIX_5:2 for i, n being Nat st i > 1 & i in Seg n holds i -' 1 in Seg n proofend; theorem Th3: :: RADIX_5:3 for k being Nat st 2 <= k holds 4 <= Radix k proofend; theorem Th4: :: RADIX_5:4 for k being Nat for tx being Tuple of 1,k -SD holds SDDec tx = DigA (tx,1) proofend; begin theorem Th5: :: RADIX_5:5 for i, k, n being Nat st i in Seg n holds DigA ((DecSD (0,n,k)),i) = 0 proofend; theorem :: RADIX_5:6 for n, k being Nat st n >= 1 holds SDDec (DecSD (0,n,k)) = 0 proofend; theorem Th7: :: RADIX_5:7 for k, n being Nat st 1 in Seg n & k >= 2 holds DigA ((DecSD (1,n,k)),1) = 1 proofend; theorem Th8: :: RADIX_5:8 for i, k, n being Nat st i in Seg n & i > 1 & k >= 2 holds DigA ((DecSD (1,n,k)),i) = 0 proofend; theorem :: RADIX_5:9 for n, k being Nat st n >= 1 & k >= 2 holds SDDec (DecSD (1,n,k)) = 1 proofend; theorem Th10: :: RADIX_5:10 for k being Nat st k >= 2 holds SD_Add_Carry (Radix k) = 1 proofend; theorem Th11: :: RADIX_5:11 for k being Nat st k >= 2 holds SD_Add_Data ((Radix k),k) = 0 proofend; begin Lm1: for k being Nat st 2 <= k holds SD_Add_Carry ((Radix k) - 1) = 1 proofend; Lm2: for n, k, i being Nat st k >= 2 & i in Seg n holds SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = 0 proofend; theorem Th12: :: RADIX_5:12 for n being Nat st n >= 1 holds for k being Nat for tx, ty being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds DigA (tx,i) = DigA (ty,i) ) holds SDDec tx = SDDec ty proofend; theorem :: RADIX_5:13 for n being Nat st n >= 1 holds for k being Nat for tx, ty being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds DigA (tx,i) >= DigA (ty,i) ) holds SDDec tx >= SDDec ty proofend; theorem Th14: :: RADIX_5:14 for n being Nat st n >= 1 holds for k being Nat st k >= 2 holds for tx, ty, tz, tw being Tuple of n,k -SD st ( for i being Nat holds ( not i in Seg n or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = DigA (tw,i) ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = DigA (tw,i) ) ) ) holds (SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty) proofend; theorem :: RADIX_5:15 for n, k being Nat st n >= 1 & k >= 2 holds for tx, ty, tz being Tuple of n,k -SD st ( for i being Nat holds ( not i in Seg n or ( DigA (tx,i) = DigA (tz,i) & DigA (ty,i) = 0 ) or ( DigA (ty,i) = DigA (tz,i) & DigA (tx,i) = 0 ) ) ) holds (SDDec tz) + (SDDec (DecSD (0,n,k))) = (SDDec tx) + (SDDec ty) proofend; begin definition let i, m, k be Nat; assume A1: k >= 2 ; func SDMinDigit (m,k,i) -> Element of k -SD equals :Def1: :: RADIX_5:def 1 (- (Radix k)) + 1 if ( 1 <= i & i < m ) otherwise 0 ; coherence ( ( 1 <= i & i < m implies (- (Radix k)) + 1 is Element of k -SD ) & ( ( not 1 <= i or 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 SDMinDigit RADIX_5:def_1_:_ for i, m, k being Nat st k >= 2 holds ( ( 1 <= i & i < m implies SDMinDigit (m,k,i) = (- (Radix k)) + 1 ) & ( ( not 1 <= i or not i < m ) implies SDMinDigit (m,k,i) = 0 ) ); definition let n, m, k be Nat; func SDMin (n,m,k) -> Tuple of n,k -SD means :Def2: :: RADIX_5:def 2 for i being Nat st i in Seg n holds DigA (it,i) = SDMinDigit (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) = SDMinDigit (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) = SDMinDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds DigA (b2,i) = SDMinDigit (m,k,i) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines SDMin RADIX_5:def_2_:_ for n, m, k being Nat for b4 being Tuple of n,k -SD holds ( b4 = SDMin (n,m,k) iff for i being Nat st i in Seg n holds DigA (b4,i) = SDMinDigit (m,k,i) ); definition let i, m, k be Nat; assume A1: k >= 2 ; func SDMaxDigit (m,k,i) -> Element of k -SD equals :Def3: :: RADIX_5:def 3 (Radix k) - 1 if ( 1 <= i & i < m ) otherwise 0 ; coherence ( ( 1 <= i & i < m implies (Radix k) - 1 is Element of k -SD ) & ( ( not 1 <= i or not i < m ) implies 0 is Element of k -SD ) ) by A1, Th1, RADIX_1:14; consistency for b1 being Element of k -SD holds verum ; end; :: deftheorem Def3 defines SDMaxDigit RADIX_5:def_3_:_ for i, m, k being Nat st k >= 2 holds ( ( 1 <= i & i < m implies SDMaxDigit (m,k,i) = (Radix k) - 1 ) & ( ( not 1 <= i or not i < m ) implies SDMaxDigit (m,k,i) = 0 ) ); definition let n, m, k be Nat; func SDMax (n,m,k) -> Tuple of n,k -SD means :Def4: :: RADIX_5:def 4 for i being Nat st i in Seg n holds DigA (it,i) = SDMaxDigit (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) = SDMaxDigit (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) = SDMaxDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds DigA (b2,i) = SDMaxDigit (m,k,i) ) holds b1 = b2 proofend; end; :: deftheorem Def4 defines SDMax RADIX_5:def_4_:_ for n, m, k being Nat for b4 being Tuple of n,k -SD holds ( b4 = SDMax (n,m,k) iff for i being Nat st i in Seg n holds DigA (b4,i) = SDMaxDigit (m,k,i) ); definition let i, m, k be Nat; assume A1: k >= 2 ; func FminDigit (m,k,i) -> Element of k -SD equals :Def5: :: RADIX_5:def 5 1 if i = m otherwise 0 ; coherence ( ( i = m implies 1 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 Def5 defines FminDigit RADIX_5:def_5_:_ for i, m, k being Nat st k >= 2 holds ( ( i = m implies FminDigit (m,k,i) = 1 ) & ( not i = m implies FminDigit (m,k,i) = 0 ) ); definition let n, m, k be Nat; func Fmin (n,m,k) -> Tuple of n,k -SD means :Def6: :: RADIX_5:def 6 for i being Nat st i in Seg n holds DigA (it,i) = FminDigit (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) = FminDigit (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) = FminDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds DigA (b2,i) = FminDigit (m,k,i) ) holds b1 = b2 proofend; end; :: deftheorem Def6 defines Fmin RADIX_5:def_6_:_ for n, m, k being Nat for b4 being Tuple of n,k -SD holds ( b4 = Fmin (n,m,k) iff for i being Nat st i in Seg n holds DigA (b4,i) = FminDigit (m,k,i) ); definition let i, m, k be Nat; assume A1: k >= 2 ; func FmaxDigit (m,k,i) -> Element of k -SD equals :Def7: :: RADIX_5:def 7 (Radix k) - 1 if i = m otherwise 0 ; coherence ( ( i = m implies (Radix k) - 1 is Element of k -SD ) & ( not i = m implies 0 is Element of k -SD ) ) by A1, Th1, RADIX_1:14; consistency for b1 being Element of k -SD holds verum ; end; :: deftheorem Def7 defines FmaxDigit RADIX_5:def_7_:_ for i, m, k being Nat st k >= 2 holds ( ( i = m implies FmaxDigit (m,k,i) = (Radix k) - 1 ) & ( not i = m implies FmaxDigit (m,k,i) = 0 ) ); definition let n, m, k be Nat; func Fmax (n,m,k) -> Tuple of n,k -SD means :Def8: :: RADIX_5:def 8 for i being Nat st i in Seg n holds DigA (it,i) = FmaxDigit (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) = FmaxDigit (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) = FmaxDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds DigA (b2,i) = FmaxDigit (m,k,i) ) holds b1 = b2 proofend; end; :: deftheorem Def8 defines Fmax RADIX_5:def_8_:_ for n, m, k being Nat for b4 being Tuple of n,k -SD holds ( b4 = Fmax (n,m,k) iff for i being Nat st i in Seg n holds DigA (b4,i) = FmaxDigit (m,k,i) ); begin theorem Th16: :: RADIX_5:16 for n, m, k being Nat st k >= 2 holds for i being Nat st i in Seg n holds (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 proofend; theorem :: RADIX_5:17 for n being Nat st n >= 1 holds for m, k being Nat st k >= 2 holds (SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k))) = SDDec (DecSD (0,n,k)) proofend; theorem :: RADIX_5:18 for n being Nat st n >= 1 holds for m, k being Nat st m in Seg n & k >= 2 holds SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k))) proofend; theorem :: RADIX_5:19 for n, m, k being Nat st m in Seg n & k >= 2 holds SDDec (Fmin ((n + 1),(m + 1),k)) = (SDDec (Fmin ((n + 1),m,k))) + (SDDec (Fmax ((n + 1),m,k))) proofend;