:: Magnitude Relation Properties of 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, RADIX_1, ARYTM_1, ARYTM_3, CARD_1, SUBSET_1, FINSEQ_1, POWER, RELAT_1, FINSEQ_2, PARTFUN1, NEWTON, FUNCT_1, CARD_3, INT_1, TARSKI, RADIX_5; notations TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_D, NEWTON, RADIX_1, POWER, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, GR_CY_1; constructors REAL_1, NAT_D, NEWTON, POWER, GR_CY_1, RADIX_4; registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, ORDINAL1, NEWTON, FINSEQ_2; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin :: Some Useful Theorems theorem :: RADIX_5:1 for k be Nat st k >= 2 holds Radix(k) - 1 in k-SD; theorem :: RADIX_5:2 for i,n be Nat st i > 1 & i in Seg n holds i -' 1 in Seg n; theorem :: RADIX_5:3 for k be Nat st 2 <= k holds 4 <= Radix(k); theorem :: RADIX_5:4 for k be Nat, tx be Tuple of 1,k-SD holds SDDec(tx) = DigA(tx,1); begin :: Properties of Primary Radix-$2^k$ SD Number theorem :: RADIX_5:5 for i,k,n be Nat st i in Seg n holds DigA(DecSD(0,n,k),i) = 0; theorem :: RADIX_5:6 for n,k be Nat st n >= 1 holds SDDec(DecSD(0,n,k)) = 0; theorem :: RADIX_5:7 for k,n be Nat st 1 in Seg n & k >= 2 holds DigA(DecSD(1,n,k),1) = 1; theorem :: RADIX_5:8 for i,k,n be Nat st i in Seg n & i > 1 & k >= 2 holds DigA(DecSD( 1,n,k),i) = 0; theorem :: RADIX_5:9 for n,k be Nat st n >= 1 & k >= 2 holds SDDec(DecSD(1,n,k)) = 1; theorem :: RADIX_5:10 for k be Nat st k >= 2 holds SD_Add_Carry(Radix(k)) = 1; theorem :: RADIX_5:11 for k be Nat st k >= 2 holds SD_Add_Data(Radix(k),k) = 0; begin theorem :: RADIX_5:12 for n be Nat st n >= 1 holds for k be Nat, tx,ty be Tuple of n,k -SD st (for i be Nat st i in Seg n holds DigA(tx,i) = DigA(ty,i)) holds SDDec( tx) = SDDec(ty); theorem :: RADIX_5:13 for n be Nat st n >= 1 holds for k be Nat, tx,ty be Tuple of n,k-SD st (for i be Nat st i in Seg n holds DigA(tx,i) >= DigA(ty,i)) holds SDDec(tx) >= SDDec(ty); theorem :: RADIX_5:14 for n be Nat st n >= 1 holds for k be Nat st k >= 2 holds for tx ,ty,tz,tw be Tuple of n,k-SD st (for i be Nat st i in Seg n holds (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); theorem :: RADIX_5:15 for n,k be Nat st n >= 1 & k >= 2 holds for tx,ty,tz be Tuple of n,k -SD st (for i be Nat st i in Seg n holds (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); begin :: Definiton of Max/Min Radix-2^k SD Number in Some Digits definition let i,m,k be Nat; assume k >= 2; func SDMinDigit(m,k,i) -> Element of k-SD equals :: RADIX_5:def 1 -Radix(k)+1 if 1 <= i & i < m otherwise 0; end; definition let n,m,k be Nat; func SDMin(n,m,k) -> Tuple of n,k-SD means :: RADIX_5:def 2 for i be Nat st i in Seg n holds DigA(it,i) = SDMinDigit(m,k,i); end; definition let i,m,k be Nat; assume k >= 2; func SDMaxDigit(m,k,i) -> Element of k-SD equals :: RADIX_5:def 3 Radix(k)-1 if 1 <= i & i < m otherwise 0; end; definition let n,m,k be Nat; func SDMax(n,m,k) -> Tuple of n,k-SD means :: RADIX_5:def 4 for i be Nat st i in Seg n holds DigA(it,i) = SDMaxDigit(m,k,i); end; definition let i,m,k be Nat; assume k >= 2; func FminDigit(m,k,i) -> Element of k-SD equals :: RADIX_5:def 5 1 if i = m otherwise 0; end; definition let n,m,k be Nat; func Fmin(n,m,k) -> Tuple of n,k-SD means :: RADIX_5:def 6 for i be Nat st i in Seg n holds DigA(it,i) = FminDigit(m,k,i); end; definition let i,m,k be Nat; assume k >= 2; func FmaxDigit(m,k,i) -> Element of k-SD equals :: RADIX_5:def 7 Radix(k) - 1 if i = m otherwise 0; end; definition let n,m,k be Nat; func Fmax(n,m,k) -> Tuple of n,k-SD means :: RADIX_5:def 8 for i be Nat st i in Seg n holds DigA(it,i) = FmaxDigit(m,k,i); end; begin :: Properties of Max/Min Radix-$2^k$ SD Numbers theorem :: RADIX_5:16 for n,m,k be Nat st k >= 2 holds for i be Nat st i in Seg n holds DigA(SDMax(n,m,k),i)+DigA(SDMin(n,m,k),i) = 0; theorem :: RADIX_5:17 for n be Nat st n >= 1 holds for m,k be Nat st k >= 2 holds SDDec( SDMax(n,m,k)) + SDDec(SDMin(n,m,k)) = SDDec(DecSD(0,n,k)); theorem :: RADIX_5:18 for n be Nat st n >= 1 holds for m,k be Nat st m in Seg n & k >= 2 holds SDDec(Fmin(n,m,k)) = SDDec(SDMax(n,m,k)) + SDDec(DecSD(1,n,k)); theorem :: RADIX_5:19 for n,m,k be 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));