environ
vocabularies HIDDEN, NUMBERS, NAT_1, INT_1, XXREAL_0, ARYTM_3, RADIX_1, POWER, RELAT_1, RADIX_3, ARYTM_1, SUBSET_1, FINSEQ_1, NEWTON, CARD_1, FINSEQ_2, TARSKI, FUNCT_1, ORDINAL4, PARTFUN1, CARD_3, RADIX_4;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, NAT_D, FUNCT_1, PARTFUN1, NEWTON, POWER, XXREAL_0, FINSEQ_1, FINSEQ_2, GR_CY_1, RADIX_1, RADIX_3;
definitions ;
theorems RADIX_1, POWER, NAT_1, INT_1, FINSEQ_1, FINSEQ_2, NEWTON, RVSUM_1, PREPOWER, JORDAN12, EULER_2, RADIX_3, XREAL_1, XXREAL_0, NAT_D, ORDINAL1, PARTFUN1, XREAL_0, CARD_1;
schemes FINSEQ_2, NAT_1;
registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, VALUED_0, FINSEQ_2, ORDINAL1;
constructors HIDDEN, REAL_1, NAT_D, NEWTON, POWER, BINARITH, GR_CY_1, RADIX_3;
requirements HIDDEN, REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
equalities RADIX_1;
expansions RADIX_1;
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)
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 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)))
definition
let i,
n,
k be
Nat;
let x,
y be
Tuple of
n,
k -SD_Sub ;
assume that A1:
i in Seg n
and A2:
k >= 2
;
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,k -SD_Sub 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,
k -SD_Sub ;
existence
ex b1 being Tuple of n,k -SD_Sub 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,k -SD_Sub 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;
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)