begin
theorem
canceled;
theorem Th2:
theorem Th3:
theorem Th4:
theorem
theorem Th6:
theorem Th7:
theorem
begin
:: deftheorem defines Radix RADIX_1:def 1 :
for n being Nat holds Radix n = 2 to_power n;
:: deftheorem defines -SD RADIX_1:def 2 :
for k being Nat holds k -SD = { e where e is Element of INT : ( e <= (Radix k) - 1 & e >= (- (Radix k)) + 1 ) } ;
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 :
for i, k, n being Nat
for x being Tuple of n,k -SD holds
( ( i in Seg n implies DigA x,i = x . i ) & ( i = 0 implies DigA x,i = 0 ) );
:: deftheorem defines DigB RADIX_1:def 4 :
for i, k, n being Nat
for x being Tuple of n,k -SD holds DigB x,i = DigA x,i;
theorem Th19:
theorem Th20:
:: deftheorem defines SubDigit RADIX_1:def 5 :
for i, k, n being Nat
for x being Tuple of n,k -SD holds SubDigit x,i,k = ((Radix k) |^ (i -' 1)) * (DigB x,i);
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 :
for n, k being Nat
for x being Tuple of n,k -SD
for b4 being Tuple of n, INT holds
( b4 = DigitSD x iff for i being Nat st i in Seg n holds
b4 /. i = SubDigit x,i,k );
:: deftheorem defines SDDec RADIX_1:def 7 :
for n, k being Nat
for x being Tuple of n,k -SD holds SDDec x = Sum (DigitSD x);
:: deftheorem defines DigitDC RADIX_1:def 8 :
for i, k, x being Nat holds DigitDC x,i,k = (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1));
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 :
for k, n, x being Nat
for b4 being Tuple of n,k -SD holds
( b4 = DecSD x,n,k iff for i being Nat st i in Seg n holds
DigA b4,i = DigitDC x,i,k );
begin
:: deftheorem Def10 defines SD_Add_Carry RADIX_1:def 10 :
for x being Integer holds
( ( x > 2 implies SD_Add_Carry x = 1 ) & ( x < - 2 implies SD_Add_Carry x = - 1 ) & ( not x > 2 & not x < - 2 implies SD_Add_Carry x = 0 ) );
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 :
for x being Integer
for k being Nat holds SD_Add_Data x,k = x - ((SD_Add_Carry x) * (Radix k));
theorem
theorem Th23:
begin
:: deftheorem Def12 defines is_represented_by RADIX_1:def 12 :
for n, x, k being Nat holds
( x is_represented_by n,k iff x < (Radix k) |^ n );
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 :
for n, k being Nat
for x, y, b5 being Tuple of n,k -SD holds
( b5 = x '+' y iff for i being Nat st i in Seg n holds
DigA b5,i = Add x,y,i,k );
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))))