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