begin
theorem Th1:
Lm1:
for k being Nat
for i1 being Integer st i1 in k -SD_Sub_S holds
( i1 >= - (Radix (k -' 1)) & i1 <= (Radix (k -' 1)) - 1 )
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
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
begin
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
for
k,
x,
n being
Nat st
n >= 1 &
k >= 3 &
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
theorem Th6:
theorem Th7:
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))
begin
definition
let i,
n,
k be
Nat;
let x,
y be
Tuple of
n, ;
assume that A1:
i in Seg n
and A2:
k >= 2
;
func SDSubAddDigit x,
y,
i,
k -> Element of
k -SD_Sub equals :
Def1:
(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
end;
:: deftheorem Def1 defines SDSubAddDigit RADIX_4:def 1 :
for
i,
n,
k being
Nat for
x,
y being
Tuple of
n, st
i in Seg n &
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, ;
func x '+' y -> Tuple of
n,
means :
Def2:
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, st
for i being Nat st i in Seg n holds
DigA_SDSub b1,i = SDSubAddDigit x,y,i,k
uniqueness
for b1, b2 being Tuple of n, st ( for i being Nat st i in Seg n holds
DigA_SDSub b1,i = SDSubAddDigit x,y,i,k ) & ( for i being Nat st i in Seg n holds
DigA_SDSub b2,i = SDSubAddDigit x,y,i,k ) holds
b1 = b2
end;
:: deftheorem Def2 defines '+' RADIX_4:def 2 :
theorem Th8:
for
n,
k,
x,
y,
i being
Nat st
i in Seg n & 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
theorem