begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem Th6:
theorem Th7:
theorem
begin
:: 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
canceled;
theorem Th10:
theorem
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
begin
theorem
canceled;
theorem Th18:
:: deftheorem Def3 defines DigA RADIX_1:def 3 :
:: deftheorem defines DigB RADIX_1:def 4 :
theorem Th19:
theorem Th20:
:: 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:
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:
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 :
begin
:: deftheorem Def10 defines SD_Add_Carry RADIX_1:def 10 :
theorem Th21:
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
theorem Th23:
begin
:: deftheorem Def12 defines is_represented_by RADIX_1:def 12 :
theorem Th24:
theorem
theorem Th26:
for
m,
k,
n being
Nat st
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:
begin
definition
let k,
i,
n be
Nat;
let x,
y be
Tuple of
n,
k -SD ;
assume that A1:
i in Seg n
and A2:
k >= 2
;
func Add x,
y,
i,
k -> Element of
k -SD equals :
Def13:
(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:
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:
theorem
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))))