Journal of Formalized Mathematics
Volume 11, 1999
University of Bialystok
Copyright (c) 1999 Association of Mizar Users

### The abstract of the Mizar article:

by
Yoshinori Fujisawa, and
Yasushi Fuwa

[ Mizar article, MML identifier index ]

```environ

vocabulary INT_1, NAT_1, ARYTM_1, ARYTM_3, POWER, MIDSP_3, FINSEQ_1, FUNCT_1,
notation TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, XREAL_0, INT_1, NAT_1, FUNCT_1,
POWER, FINSEQ_1, FINSEQ_4, BINARITH, TREES_4, WSIERP_1, MIDSP_3;
constructors REAL_1, POWER, BINARITH, FINSEQ_4, EULER_2, WSIERP_1, MEMBERED,
INT_1;
clusters INT_1, RELSET_1, GROUP_2, NAT_1, XREAL_0, MEMBERED;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

begin :: Some Useful Theorems

reserve i,k,m,n,p,x,y for Nat,
i1,i2,i3 for Integer,
e for set;

canceled;

n mod k = k - 1 implies (n+1) mod k = 0;

k <> 0 & n mod k < k - 1 implies (n+1) mod k = (n mod k) + 1;

m <> 0 implies (k mod (m*n)) mod n = k mod n;

k <> 0 implies (n+1) mod k = 0 or (n+1) mod k = (n mod k) + 1;

i <> 0 & k <> 0 implies (n mod (i |^ k)) div (i |^ (k -'1)) < i;

k <= n implies m |^ k divides m |^ n;

i2 > 0 & i3 >= 0 implies (i1 mod (i2*i3)) mod i3 = i1 mod i3;

begin :: Definition for Radix-2^k, k-SD

definition let n;

2 to_power n;
end;

definition let k;
func k-SD -> set equals

{e where e is Element of INT:e <= Radix(k)-1 & e >= -Radix(k)+1};
end;

for e holds e in 0-SD iff e = 0;

0-SD = {0};

k-SD c= (k+1)-SD;

e in k-SD implies e is Integer;

k-SD c= INT;

0 in k-SD;

definition let k;
cluster k-SD -> non empty;
end;

definition let k;
redefine func k-SD -> non empty Subset of INT;
end;

begin :: Functions for generating Radix-2^k SD numbers from natural numbers
:: and natural numbers from Radix-2^k SD numbers

reserve a for Tuple of n,(k-SD);

canceled;

i in Seg n implies a.i is Element of k-SD;

definition let i,k,n be Nat, x be Tuple of n,(k-SD);
func DigA(x,i) -> Integer equals

x.i if i in Seg n,
0 if i = 0;
end;

definition let i,k,n be Nat, x be Tuple of n,(k-SD);
func DigB(x,i) -> Element of INT equals

DigA(x,i);
end;

i in Seg n implies DigA(a,i) is Element of k-SD;

for x be Tuple of 1,INT st x/.1 = m holds x = <*m*>;

definition let i,k,n be Nat, x be Tuple of n,(k-SD);
func SubDigit(x,i,k) -> Element of INT equals

end;

definition let n,k be Nat, x be Tuple of n,(k-SD);
func DigitSD(x) -> Tuple of n,INT means

for i be Nat st i in Seg n holds it/.i = SubDigit(x,i,k);
end;

definition let n,k be Nat, x be Tuple of n,(k-SD);
func SDDec(x) -> Integer equals

Sum DigitSD(x);
end;

definition let i,k,x be Nat;
func DigitDC(x,i,k) -> Element of k-SD equals

end;

definition let k,n,x be Nat;
func DecSD(x,n,k) -> Tuple of n,(k-SD) means

for i be Nat st i in Seg n holds DigA(it,i) = DigitDC(x,i,k);
end;

begin :: Definition for carry & data components of Addition

definition let x be Integer;

1 if x > 2,
-1 if x < -2
otherwise 0;
end;

definition let x be Integer, k be Nat;

end;

k >= 2 & i1 in k-SD & i2 in k-SD implies

begin :: Definition for checking whether or not a natural number can be
:: expressed as n digits Radix-2^k SD number

definition let n,x,k be Nat;
pred x is_represented_by n,k means

end;

m is_represented_by 1,k implies DigA(DecSD(m,1,k),1) = m;

for n st n >= 1 holds
for m st m is_represented_by n,k holds m = SDDec(DecSD(m,n,k));

k >= 2 & m is_represented_by 1,k & n is_represented_by 1,k implies
;

m is_represented_by (n+1),k implies
DigA(DecSD(m,(n+1),k),n+1) = m div (Radix(k) |^ n);

definition let k,i,n be Nat, x,y be Tuple of n,(k-SD);
assume i in Seg n & k >= 2;
func Add(x,y,i,k) -> Element of k-SD equals

end;

definition let n,k be Nat,x,y be Tuple of n,(k-SD);
func x '+' y -> Tuple of n,(k-SD) means

for i st i in Seg n holds DigA(it,i) = Add(x,y,i,k);
end;

k >= 2 & m is_represented_by 1,k & n is_represented_by 1,k implies