:: High Speed Adder Algorithm with Radix-$2^k$ SD_Sub Number
:: by Masaaki Niimura and Yasushi Fuwa
::
:: Received January 3, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

theorem Th1: :: RADIX_4:1
for k being Nat st 2 <= k holds
2 < Radix k
proofend;

Lm1:  for k being Nat
for i1 being Integer st i1 in k -SD_Sub_S holds
( i1 >= - (Radix (k -' 1)) &amp; i1 <= (Radix (k -' 1)) - 1 )
proofend;

Lm2:  for n, m, k, i being Nat st i in Seg n holds
DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD (m,n,k)),i)
proofend;

Lm3:  for k, x, n being Nat st n >= 1 holds
DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n) = DigA ((DecSD (x,n,k)),n)
proofend;

begin

theorem Th2: :: RADIX_4:2
for x, y being Integer
for k being Nat st 3 <= k holds
SDSub_Add_Carry (((SDSub_Add_Carry (x,k)) + (SDSub_Add_Carry (y,k))),k) = 0
proofend;

theorem Th3: :: RADIX_4:3
for k, m, n being Nat st 2 <= k holds
DigA_SDSub ((SD2SDSub (DecSD (m,n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (m,n,k)),n)),k)
proofend;

theorem Th4: :: RADIX_4:4
for k, m being Nat st 2 <= k &amp; m is_represented_by 1,k holds
DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),(1 + 1)) = SDSub_Add_Carry (m,k)
proofend;

theorem Th5: :: RADIX_4:5
for k, x, n being Nat st n >= 1 &amp; k >= 3 &amp; x is_represented_by n + 1,k holds
DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1)) = SDSub_Add_Carry ((DigA ((DecSD (x,n,k)),n)),k)
proofend;

theorem Th6: :: RADIX_4:6
for k, m being Nat st 2 <= k &amp; m is_represented_by 1,k holds
DigA_SDSub ((SD2SDSub (DecSD (m,1,k))),1) = m - ((SDSub_Add_Carry (m,k)) * (Radix k))
proofend;

theorem Th7: :: RADIX_4:7
for k, x, n being Nat st k >= 2 holds
((Radix k) |^ n) * (DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1))) = ((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))
proofend;

begin

definition
let i, n, k be Nat;
let x, y be Tuple of n,k -SD_Sub ;
assume that
A1: i in Seg n and
A2: k >= 2 ;
func SDSubAddDigit (x,y,i,k) ->  Element of k -SD_Sub  equals :Def1: :: RADIX_4:def 1
(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));
coherence
 (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)) is Element of k -SD_Sub
proofend;
end;

:: deftheorem Def1 defines SDSubAddDigit RADIX_4:def_1_:_
 for i, n, k being Nat
for x, y being Tuple of n,k -SD_Sub st i in Seg n &amp; k >= 2 holds
SDSubAddDigit (x,y,i,k) = (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));

definition
let n, k be Nat;
let x, y be Tuple of n,k -SD_Sub ;
funcx '+' y ->  Tuple of n,k -SD_Sub  means :Def2: :: RADIX_4:def 2
 for i being Nat st i in Seg n holds
DigA_SDSub (it,i) = SDSubAddDigit (x,y,i,k);
existence
 ex b1 being Tuple of n,k -SD_Sub st
for i being Nat st i in Seg n holds
DigA_SDSub (b1,i) = SDSubAddDigit (x,y,i,k)
proofend;
uniqueness
 for b1, b2 being Tuple of n,k -SD_Sub st ( for i being Nat st i in Seg n holds
DigA_SDSub (b1,i) = SDSubAddDigit (x,y,i,k) ) &amp; ( for i being Nat st i in Seg n holds
DigA_SDSub (b2,i) = SDSubAddDigit (x,y,i,k) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def2 defines '+' RADIX_4:def_2_:_
 for n, k being Nat
for x, y, b5 being Tuple of n,k -SD_Sub holds
( b5 = x '+' y iff for i being Nat st i in Seg n holds
DigA_SDSub (b5,i) = SDSubAddDigit (x,y,i,k) );

theorem Th8: :: RADIX_4:8
for n, k, x, y, i being Nat st i in Seg n &amp; 2 <= k holds
SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)
proofend;

theorem :: RADIX_4:9
for n being Nat st n >= 1 holds
for k, x, y being Nat st k >= 3 &amp; x is_represented_by n,k &amp; y is_represented_by n,k holds
x + y = SDSub2IntOut ((SD2SDSub (DecSD (x,n,k))) '+' (SD2SDSub (DecSD (y,n,k))))
proofend;