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

### The abstract of the Mizar article:

by
Masaaki Niimura, and
Yasushi Fuwa

[ Mizar article, MML identifier index ]

```environ

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

begin :: Some Useful Theorems

reserve i,n,m,k,x,y for Nat,
i1 for Integer;

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

begin :: Carry operation at n+1 digits Radix-2^k SD_Sub number

for x,y be Integer, k be Nat st 3 <= k holds

2 <= k implies
DigA_SDSub(SD2SDSub(DecSD(m,n,k)),n+1)

2 <= k & m is_represented_by 1,k implies

for k,x,n be Nat st
n >= 1 & k >= 3 & x is_represented_by (n+1),k holds

2 <= k & m is_represented_by 1,k implies

for k,x,n be Nat st
n >= 1 & k >= 2 & x is_represented_by (n+1),k holds
= (Radix(k) |^ n) * DigA(DecSD(x,n+1,k),n+1)

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

SDSub_Add_Data( DigA_SDSub(x,i) + DigA_SDSub(y,i), k )
+ SDSub_Add_Carry( DigA_SDSub(x,i -'1) + DigA_SDSub(y,i -'1), k);
end;

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

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

for i st i in Seg n holds
2 <= k implies