:: Definitions of Radix-2k Signed-Digit number and its adder algorithm
:: by Yoshinori Fujisawa and Yasushi Fuwa
::
:: Received September 7, 1999
:: Copyright (c) 1999 Association of Mizar Users
theorem :: RADIX_1:1
canceled;
theorem Th2: :: RADIX_1:2
theorem Th3: :: RADIX_1:3
theorem Th4: :: RADIX_1:4
theorem :: RADIX_1:5
theorem Th6: :: RADIX_1:6
theorem Th7: :: RADIX_1:7
theorem :: RADIX_1:8
:: deftheorem defines Radix RADIX_1:def 1 :
:: deftheorem defines -SD RADIX_1:def 2 :
Lm1:
for k being Nat st k >= 2 holds
Radix k >= 2 + 2
theorem :: RADIX_1:9
canceled;
theorem Th10: :: RADIX_1:10
theorem :: RADIX_1:11
theorem Th12: :: RADIX_1:12
theorem Th13: :: RADIX_1:13
theorem Th14: :: RADIX_1:14
theorem Th15: :: RADIX_1:15
theorem Th16: :: RADIX_1:16
theorem :: RADIX_1:17
canceled;
theorem Th18: :: RADIX_1:18
:: deftheorem Def3 defines DigA RADIX_1:def 3 :
:: deftheorem defines DigB RADIX_1:def 4 :
theorem Th19: :: RADIX_1:19
theorem Th20: :: RADIX_1:20
:: deftheorem defines SubDigit RADIX_1:def 5 :
definition
let n,
k be
Nat;
let x be
Tuple of
n,
(k -SD );
func DigitSD x -> Tuple of
n,
INT means :
Def6:
:: RADIX_1:def 6
for
i being
Nat st
i in Seg n holds
it /. i = SubDigit x,
i,
k;
existence
ex b1 being Tuple of n,INT st
for i being Nat st i in Seg n holds
b1 /. i = SubDigit x,i,k
uniqueness
for b1, b2 being Tuple of n,INT st ( for i being Nat st i in Seg n holds
b1 /. i = SubDigit x,i,k ) & ( for i being Nat st i in Seg n holds
b2 /. i = SubDigit x,i,k ) holds
b1 = b2
end;
:: deftheorem Def6 defines DigitSD RADIX_1:def 6 :
:: deftheorem defines SDDec RADIX_1:def 7 :
:: deftheorem defines DigitDC RADIX_1:def 8 :
definition
let k,
n,
x be
Nat;
func DecSD x,
n,
k -> Tuple of
n,
(k -SD ) means :
Def9:
:: RADIX_1:def 9
for
i being
Nat st
i in Seg n holds
DigA it,
i = DigitDC x,
i,
k;
existence
ex b1 being Tuple of n,(k -SD ) st
for i being Nat st i in Seg n holds
DigA b1,i = DigitDC x,i,k
uniqueness
for b1, b2 being Tuple of n,(k -SD ) st ( for i being Nat st i in Seg n holds
DigA b1,i = DigitDC x,i,k ) & ( for i being Nat st i in Seg n holds
DigA b2,i = DigitDC x,i,k ) holds
b1 = b2
end;
:: deftheorem Def9 defines DecSD RADIX_1:def 9 :
:: deftheorem Def10 defines SD_Add_Carry RADIX_1:def 10 :
theorem Th21: :: RADIX_1:21
Lm2:
for x being Integer holds
( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 )
:: deftheorem defines SD_Add_Data RADIX_1:def 11 :
theorem :: RADIX_1:22
theorem Th23: :: RADIX_1:23
:: deftheorem Def12 defines is_represented_by RADIX_1:def 12 :
theorem Th24: :: RADIX_1:24
theorem :: RADIX_1:25
theorem Th26: :: RADIX_1:26
for
k,
m,
n being
Nat st
k >= 2 &
m is_represented_by 1,
k &
n is_represented_by 1,
k holds
SD_Add_Carry ((DigA (DecSD m,1,k),1) + (DigA (DecSD n,1,k),1)) = SD_Add_Carry (m + n)
Lm3:
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
theorem Th27: :: RADIX_1:27
definition
let k,
i,
n be
Nat;
let x,
y be
Tuple of
n,
(k -SD );
assume A1:
(
i in Seg n &
k >= 2 )
;
func Add x,
y,
i,
k -> Element of
k -SD equals :
Def13:
:: RADIX_1:def 13
(SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1))));
coherence
(SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1)))) is Element of k -SD
end;
:: deftheorem Def13 defines Add RADIX_1:def 13 :
for
k,
i,
n being
Nat for
x,
y being
Tuple of
n,
(k -SD ) st
i in Seg n &
k >= 2 holds
Add x,
y,
i,
k = (SD_Add_Data ((DigA x,i) + (DigA y,i)),k) + (SD_Add_Carry ((DigA x,(i -' 1)) + (DigA y,(i -' 1))));
definition
let n,
k be
Nat;
let x,
y be
Tuple of
n,
(k -SD );
func x '+' y -> Tuple of
n,
(k -SD ) means :
Def14:
:: RADIX_1:def 14
for
i being
Nat st
i in Seg n holds
DigA it,
i = Add x,
y,
i,
k;
existence
ex b1 being Tuple of n,(k -SD ) st
for i being Nat st i in Seg n holds
DigA b1,i = Add x,y,i,k
uniqueness
for b1, b2 being Tuple of n,(k -SD ) st ( for i being Nat st i in Seg n holds
DigA b1,i = Add x,y,i,k ) & ( for i being Nat st i in Seg n holds
DigA b2,i = Add x,y,i,k ) holds
b1 = b2
end;
:: deftheorem Def14 defines '+' RADIX_1:def 14 :
theorem Th28: :: RADIX_1:28
theorem :: RADIX_1:29
for
n being
Nat st
n >= 1 holds
for
k,
x,
y being
Nat st
k >= 2 &
x is_represented_by n,
k &
y is_represented_by n,
k holds
x + y = (SDDec ((DecSD x,n,k) '+' (DecSD y,n,k))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA (DecSD x,n,k),n) + (DigA (DecSD y,n,k),n))))