Journal of Formalized Mathematics
Volume 15, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

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

by
Masaaki Niimura, and
Yasushi Fuwa

[ Mizar article, MML identifier index ]

```environ

vocabulary ARYTM_1, NAT_1, INT_1, RADIX_1, FINSEQ_1, POWER, MIDSP_3, FINSEQ_4,
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

for k be Nat st k >= 2 holds Radix(k) - 1 in k-SD;

for i,n be Nat st i > 1 & i in Seg n holds
i -' 1 in Seg n;

reserve k for Nat;

for k be Nat st 2 <= k holds 4 <= Radix(k);

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

for i,k,n be Nat st i in Seg n holds
DigA(DecSD(0,n,k),i) = 0;

for n,k be Nat st n >= 1 holds
SDDec(DecSD(0,n,k)) = 0;

for k,n be Nat st 1 in Seg n & k >= 2 holds
DigA(DecSD(1,n,k),1) = 1;

for i,k,n be Nat st i in Seg n & i > 1 & k >= 2 holds
DigA(DecSD(1,n,k),i) = 0;

for n,k be Nat st n >= 1 & k >= 2 holds
SDDec(DecSD(1,n,k)) = 1;

for k be Nat st k >= 2 holds SD_Add_Carry(Radix(k)) = 1;

for k be Nat st k >= 2 holds SD_Add_Data(Radix(k),k) = 0;

begin

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);

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);

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);

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(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

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(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

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

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

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(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

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

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;

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));