Volume 15, 2003

University of Bialystok

Copyright (c) 2003 Association of Mizar Users

### The abstract of the Mizar article:

### Magnitude Relation Properties of Radix-$2^k$ SD Number

**by****Masaaki Niimura, and****Yasushi Fuwa**- Received November 7, 2003
- MML identifier: RADIX_5

- [ Mizar article, MML identifier index ]

environ vocabulary ARYTM_1, NAT_1, INT_1, RADIX_1, FINSEQ_1, POWER, MIDSP_3, FINSEQ_4, GROUP_1, RELAT_1, RLVECT_1, FUNCT_1, RADIX_5; notation TARSKI, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, BINARITH, RADIX_1, POWER, MIDSP_3, FINSEQ_4, FINSEQ_1, FUNCT_1, WSIERP_1; constructors RADIX_1, BINARITH, POWER, FINSEQ_4, EULER_2; clusters REAL_1, NUMBERS, XREAL_0, INT_1, RELSET_1; 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; reserve k for Nat; 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 n >= 1 & k >= 2 & m in Seg n 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 m in Seg n & 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));

Back to top