:: Improvement of Radix-$2^k$ Signed-Digit Number for High Speed Circuit
:: by Masaaki Niimura and Yasushi Fuwa
::
:: Received January 3, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users


begin

Lm1:  for k being Nat st 1 <= k holds
Radix k = (Radix (k -' 1)) + (Radix (k -' 1))
proofend;

Lm2:  for k being Nat st 1 <= k holds
(Radix k) - (Radix (k -' 1)) = Radix (k -' 1)
proofend;

Lm3:  for k being Nat st 1 <= k holds
(- (Radix k)) + (Radix (k -' 1)) = - (Radix (k -' 1))
proofend;

Lm4:  for k being Nat st 1 <= k holds
2 <= Radix k
proofend;

Lm5:  for n, m, k, i being Nat st i in Seg n holds
DigA ((DecSD (m,(n + 1),k)),i) = DigA ((DecSD ((m mod ((Radix k) |^ n)),n,k)),i)
proofend;

definition
let k be Nat;
funck -SD_Sub_S  ->  set  equals :: RADIX_3:def 1
 {  e where e is Element of INT : ( e >= - (Radix (k -' 1)) &amp; e <= (Radix (k -' 1)) - 1 )  }  ;
correctness
coherence
{  e where e is Element of INT : ( e >= - (Radix (k -' 1)) &amp; e <= (Radix (k -' 1)) - 1 )  }  is set ;
;
funck -SD_Sub  ->  set  equals :: RADIX_3:def 2
 {  e where e is Element of INT : ( e >= (- (Radix (k -' 1))) - 1 &amp; e <= Radix (k -' 1) )  }  ;
correctness
coherence
{  e where e is Element of INT : ( e >= (- (Radix (k -' 1))) - 1 &amp; e <= Radix (k -' 1) )  }  is set ;
;
end;

:: deftheorem  defines -SD_Sub_S RADIX_3:def_1_:_
 for k being Nat holds k -SD_Sub_S =  {  e where e is Element of INT : ( e >= - (Radix (k -' 1)) &amp; e <= (Radix (k -' 1)) - 1 )  }  ;

:: deftheorem  defines -SD_Sub RADIX_3:def_2_:_
 for k being Nat holds k -SD_Sub =  {  e where e is Element of INT : ( e >= (- (Radix (k -' 1))) - 1 &amp; e <= Radix (k -' 1) )  }  ;

theorem Th1: :: RADIX_3:1
for k being Nat
for i1 being Integer st i1 in k -SD_Sub holds
( (- (Radix (k -' 1))) - 1 <= i1 &amp; i1 <= Radix (k -' 1) )
proofend;

theorem Th2: :: RADIX_3:2
for k being Nat holds k -SD_Sub_S c= k -SD_Sub
proofend;

theorem Th3: :: RADIX_3:3
for k being Nat holds k -SD_Sub_S c= (k + 1) -SD_Sub_S
proofend;

theorem :: RADIX_3:4
for k being Nat st 2 <= k holds
k -SD_Sub c= k -SD
proofend;

theorem Th5: :: RADIX_3:5
0 in 0 -SD_Sub_S
proofend;

theorem Th6: :: RADIX_3:6
for k being Nat holds 0 in k -SD_Sub_S
proofend;

theorem Th7: :: RADIX_3:7
for k being Nat holds 0 in k -SD_Sub
proofend;

theorem Th8: :: RADIX_3:8
for k being Nat
for e being set st e in k -SD_Sub holds
e is Integer
proofend;

theorem Th9: :: RADIX_3:9
for k being Nat holds k -SD_Sub c= INT
proofend;

theorem Th10: :: RADIX_3:10
for k being Nat holds k -SD_Sub_S c= INT
proofend;

registration
let k be Nat;
clusterk -SD_Sub_S  ->  non empty ;
coherence
 not k -SD_Sub_S is empty by Th6;
clusterk -SD_Sub  ->  non empty ;
coherence
 not k -SD_Sub is empty by Th7;
end;

definition
let k be Nat;
:: original:-SD_Sub_S
redefine funck -SD_Sub_S  ->  non empty Subset of INT;
coherence
 k -SD_Sub_S is non empty Subset of INT by Th10;
end;

definition
let k be Nat;
:: original:-SD_Sub
redefine funck -SD_Sub  ->  non empty Subset of INT;
coherence
 k -SD_Sub is non empty Subset of INT by Th9;
end;

theorem Th11: :: RADIX_3:11
for i, n, k being Nat
for aSub being Tuple of n,k -SD_Sub st i in Seg n holds
aSub . i is Element of k -SD_Sub
proofend;

begin

definition
let x be Integer;
let k be Nat;
func SDSub_Add_Carry (x,k) ->  Integer equals :Def3: :: RADIX_3:def 3
1 if  Radix (k -' 1) <= x
- 1 if x < - (Radix (k -' 1))
otherwise  0 ;
coherence
 ( ( Radix (k -' 1) <= x implies 1 is Integer ) &amp; ( x < - (Radix (k -' 1)) implies - 1 is Integer ) &amp; ( not Radix (k -' 1) <= x &amp; not x < - (Radix (k -' 1)) implies 0 is Integer ) ) ;
consistency
 for b1 being Integer st Radix (k -' 1) <= x &amp; x < - (Radix (k -' 1)) holds
( b1 = 1 iff b1 = - 1 ) ;
end;

:: deftheorem Def3 defines SDSub_Add_Carry RADIX_3:def_3_:_
 for x being Integer
for k being Nat holds
( ( Radix (k -' 1) <= x implies SDSub_Add_Carry (x,k) = 1 ) &amp; ( x < - (Radix (k -' 1)) implies SDSub_Add_Carry (x,k) = - 1 ) &amp; ( not Radix (k -' 1) <= x &amp; not x < - (Radix (k -' 1)) implies SDSub_Add_Carry (x,k) = 0 ) );

definition
let x be Integer;
let k be Nat;
func SDSub_Add_Data (x,k) ->  Integer equals :: RADIX_3:def 4
x - ((Radix k) * (SDSub_Add_Carry (x,k)));
coherence
 x - ((Radix k) * (SDSub_Add_Carry (x,k))) is Integer ;
end;

:: deftheorem  defines SDSub_Add_Data RADIX_3:def_4_:_
 for x being Integer
for k being Nat holds SDSub_Add_Data (x,k) = x - ((Radix k) * (SDSub_Add_Carry (x,k)));

theorem Th12: :: RADIX_3:12
for x being Integer
for k being Nat holds
( - 1 <= SDSub_Add_Carry (x,k) &amp; SDSub_Add_Carry (x,k) <= 1 )
proofend;

theorem Th13: :: RADIX_3:13
for k being Nat
for i1 being Integer st 2 <= k &amp; i1 in k -SD holds
( SDSub_Add_Data (i1,k) >= - (Radix (k -' 1)) &amp; SDSub_Add_Data (i1,k) <= (Radix (k -' 1)) - 1 )
proofend;

theorem Th14: :: RADIX_3:14
for x being Integer
for k being Nat st 2 <= k holds
SDSub_Add_Carry (x,k) in k -SD_Sub_S
proofend;

theorem Th15: :: RADIX_3:15
for k being Nat
for i1, i2 being Integer st 2 <= k &amp; i1 in k -SD holds
(SDSub_Add_Data (i1,k)) + (SDSub_Add_Carry (i2,k)) in k -SD_Sub
proofend;

theorem Th16: :: RADIX_3:16
for k being Nat holds SDSub_Add_Carry (0,k) = 0
proofend;

begin

definition
let i, k, n be Nat;
let x be Tuple of n,k -SD_Sub ;
func DigA_SDSub (x,i) ->  Integer equals :Def5: :: RADIX_3:def 5
x . i if i in Seg n
0  if i = 0
;
coherence
 ( ( i in Seg n implies x . i is Integer ) &amp; ( i = 0 implies 0 is Integer ) ) by INT_1:def_2;
consistency
 for b1 being Integer st i in Seg n &amp; i = 0 holds
( b1 = x . i iff b1 = 0 ) by FINSEQ_1:1;
end;

:: deftheorem Def5 defines DigA_SDSub RADIX_3:def_5_:_
 for i, k, n being Nat
for x being Tuple of n,k -SD_Sub holds
( ( i in Seg n implies DigA_SDSub (x,i) = x . i ) &amp; ( i = 0 implies DigA_SDSub (x,i) = 0 ) );

definition
let i, k, n be Nat;
let x be Tuple of n,k -SD ;
func SD2SDSubDigit (x,i,k) ->  Integer equals :Def6: :: RADIX_3:def 6
(SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) if i in Seg n
SDSub_Add_Carry ((DigA (x,(i -' 1))),k) if i = n + 1
otherwise  0 ;
coherence
 ( ( i in Seg n implies (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) is Integer ) &amp; ( i = n + 1 implies SDSub_Add_Carry ((DigA (x,(i -' 1))),k) is Integer ) &amp; ( not i in Seg n &amp; not i = n + 1 implies 0 is Integer ) ) ;
consistency
 for b1 being Integer st i in Seg n &amp; i = n + 1 holds
( b1 = (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) iff b1 = SDSub_Add_Carry ((DigA (x,(i -' 1))),k) )
proofend;
end;

:: deftheorem Def6 defines SD2SDSubDigit RADIX_3:def_6_:_
 for i, k, n being Nat
for x being Tuple of n,k -SD holds
( ( i in Seg n implies SD2SDSubDigit (x,i,k) = (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) ) &amp; ( i = n + 1 implies SD2SDSubDigit (x,i,k) = SDSub_Add_Carry ((DigA (x,(i -' 1))),k) ) &amp; ( not i in Seg n &amp; not i = n + 1 implies SD2SDSubDigit (x,i,k) = 0 ) );

theorem Th17: :: RADIX_3:17
for k, i, n being Nat
for a being Tuple of n,k -SD st 2 <= k &amp; i in Seg (n + 1) holds
SD2SDSubDigit (a,i,k) is Element of k -SD_Sub
proofend;

definition
let i, k, n be Nat;
let x be Tuple of n,k -SD ;
assume A1: ( 2 <= k &amp; i in Seg (n + 1) ) ;
func SD2SDSubDigitS (x,i,k) ->  Element of k -SD_Sub  equals :Def7: :: RADIX_3:def 7
 SD2SDSubDigit (x,i,k);
coherence
 SD2SDSubDigit (x,i,k) is Element of k -SD_Sub by A1, Th17;
end;

:: deftheorem Def7 defines SD2SDSubDigitS RADIX_3:def_7_:_
 for i, k, n being Nat
for x being Tuple of n,k -SD st 2 <= k &amp; i in Seg (n + 1) holds
SD2SDSubDigitS (x,i,k) = SD2SDSubDigit (x,i,k);

definition
let n, k be Nat;
let x be Tuple of n,k -SD ;
func SD2SDSub x ->  Tuple of n + 1,k -SD_Sub  means :Def8: :: RADIX_3:def 8
 for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (it,i) = SD2SDSubDigitS (x,i,k);
existence
 ex b1 being Tuple of n + 1,k -SD_Sub st
for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (b1,i) = SD2SDSubDigitS (x,i,k)
proofend;
uniqueness
 for b1, b2 being Tuple of n + 1,k -SD_Sub st ( for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (b1,i) = SD2SDSubDigitS (x,i,k) ) &amp; ( for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (b2,i) = SD2SDSubDigitS (x,i,k) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def8 defines SD2SDSub RADIX_3:def_8_:_
 for n, k being Nat
for x being Tuple of n,k -SD
for b4 being Tuple of n + 1,k -SD_Sub holds
( b4 = SD2SDSub x iff for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (b4,i) = SD2SDSubDigitS (x,i,k) );

theorem :: RADIX_3:18
for i, n, k being Nat
for aSub being Tuple of n,k -SD_Sub st i in Seg n holds
DigA_SDSub (aSub,i) is Element of k -SD_Sub
proofend;

theorem :: RADIX_3:19
for k being Nat
for i1, i2 being Integer st 2 <= k &amp; i1 in k -SD &amp; i2 in k -SD_Sub holds
SDSub_Add_Data ((i1 + i2),k) in k -SD_Sub_S
proofend;

begin

definition
let i, k, n be Nat;
let x be Tuple of n,k -SD_Sub ;
func DigB_SDSub (x,i) ->  Element of INT  equals :: RADIX_3:def 9
 DigA_SDSub (x,i);
coherence
 DigA_SDSub (x,i) is Element of INT by INT_1:def_2;
end;

:: deftheorem  defines DigB_SDSub RADIX_3:def_9_:_
 for i, k, n being Nat
for x being Tuple of n,k -SD_Sub holds DigB_SDSub (x,i) = DigA_SDSub (x,i);

definition
let i, k, n be Nat;
let x be Tuple of n,k -SD_Sub ;
func SDSub2INTDigit (x,i,k) ->  Element of INT  equals :: RADIX_3:def 10
((Radix k) |^ (i -' 1)) * (DigB_SDSub (x,i));
coherence
 ((Radix k) |^ (i -' 1)) * (DigB_SDSub (x,i)) is Element of INT by INT_1:def_2;
end;

:: deftheorem  defines SDSub2INTDigit RADIX_3:def_10_:_
 for i, k, n being Nat
for x being Tuple of n,k -SD_Sub holds SDSub2INTDigit (x,i,k) = ((Radix k) |^ (i -' 1)) * (DigB_SDSub (x,i));

definition
let n, k be Nat;
let x be Tuple of n,k -SD_Sub ;
func SDSub2INT x ->  Tuple of n, INT  means :Def11: :: RADIX_3:def 11
 for i being Nat st i in Seg n holds
it /. i = SDSub2INTDigit (x,i,k);
existence
 ex b1 being Tuple of n, INT st
for i being Nat st i in Seg n holds
b1 /. i = SDSub2INTDigit (x,i,k)
proofend;
uniqueness
 for b1, b2 being Tuple of n, INT st ( for i being Nat st i in Seg n holds
b1 /. i = SDSub2INTDigit (x,i,k) ) &amp; ( for i being Nat st i in Seg n holds
b2 /. i = SDSub2INTDigit (x,i,k) ) holds
b1 = b2
proofend;
end;

:: deftheorem Def11 defines SDSub2INT RADIX_3:def_11_:_
 for n, k being Nat
for x being Tuple of n,k -SD_Sub
for b4 being Tuple of n, INT holds
( b4 = SDSub2INT x iff for i being Nat st i in Seg n holds
b4 /. i = SDSub2INTDigit (x,i,k) );

definition
let n, k be Nat;
let x be Tuple of n,k -SD_Sub ;
func SDSub2IntOut x ->  Integer equals :: RADIX_3:def 12
 Sum (SDSub2INT x);
coherence
 Sum (SDSub2INT x) is Integer ;
end;

:: deftheorem  defines SDSub2IntOut RADIX_3:def_12_:_
 for n, k being Nat
for x being Tuple of n,k -SD_Sub holds SDSub2IntOut x = Sum (SDSub2INT x);

theorem Th20: :: RADIX_3:20
for n, k, m, i being Nat st i in Seg n &amp; 2 <= k holds
DigA_SDSub ((SD2SDSub (DecSD (m,(n + 1),k))),i) = DigA_SDSub ((SD2SDSub (DecSD ((m mod ((Radix k) |^ n)),n,k))),i)
proofend;

theorem :: RADIX_3:21
for n being Nat st n >= 1 holds
for k, x being Nat st k >= 2 &amp; x is_represented_by n,k holds
x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k)))
proofend;