environ
vocabularies HIDDEN, NUMBERS, NAT_1, INT_1, XXREAL_0, RADIX_1, ARYTM_1, ARYTM_3, POWER, RELAT_1, CARD_1, FINSEQ_1, NEWTON, SUBSET_1, TARSKI, XBOOLE_0, FINSEQ_2, FUNCT_1, PARTFUN1, CARD_3, ORDINAL4, RADIX_3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, NAT_D, FUNCT_1, PARTFUN1, NEWTON, POWER, FINSEQ_1, FINSEQ_2, GR_CY_1, RADIX_1;
definitions TARSKI;
theorems RADIX_1, POWER, NAT_1, INT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, PRE_FF, NEWTON, RVSUM_1, PREPOWER, JORDAN12, FINSEQ_3, RADIX_2, XREAL_1, XXREAL_0, NAT_D, ORDINAL1, PARTFUN1, XREAL_0, CARD_1;
schemes NAT_1, FINSEQ_2;
registrations RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, VALUED_0, FINSEQ_2, CARD_1, ORDINAL1;
constructors HIDDEN, REAL_1, NAT_D, NEWTON, POWER, BINARITH, GR_CY_1, RADIX_1, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities RADIX_1;
expansions RADIX_1;
Lm1:
for k being Nat st 1 <= k holds
Radix k = (Radix (k -' 1)) + (Radix (k -' 1))
Lm2:
for k being Nat st 1 <= k holds
(Radix k) - (Radix (k -' 1)) = Radix (k -' 1)
Lm3:
for k being Nat st 1 <= k holds
(- (Radix k)) + (Radix (k -' 1)) = - (Radix (k -' 1))
Lm4:
for k being Nat st 1 <= k holds
2 <= Radix k
Lm5:
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)
definition
let i,
k,
n be
Nat;
let x be
Tuple of
n,
k -SD ;
coherence
( ( i in Seg n implies (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) is Integer ) & ( i = n + 1 implies SDSub_Add_Carry ((DigA (x,(i -' 1))),k) is Integer ) & ( not i in Seg n & not i = n + 1 implies 0 is Integer ) )
;
consistency
for b1 being Integer st i in Seg n & i = n + 1 holds
( b1 = (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) iff b1 = SDSub_Add_Carry ((DigA (x,(i -' 1))),k) )
end;
::
deftheorem Def6 defines
SD2SDSubDigit RADIX_3:def 6 :
for i, k, n being Nat
for x being Tuple of n,k -SD holds
( ( i in Seg n implies SD2SDSubDigit (x,i,k) = (SDSub_Add_Data ((DigA (x,i)),k)) + (SDSub_Add_Carry ((DigA (x,(i -' 1))),k)) ) & ( i = n + 1 implies SD2SDSubDigit (x,i,k) = SDSub_Add_Carry ((DigA (x,(i -' 1))),k) ) & ( not i in Seg n & not i = n + 1 implies SD2SDSubDigit (x,i,k) = 0 ) );
definition
let n,
k be
Nat;
let x be
Tuple of
n,
k -SD ;
existence
ex b1 being Tuple of n + 1,k -SD_Sub st
for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (b1,i) = SD2SDSubDigitS (x,i,k)
uniqueness
for b1, b2 being Tuple of n + 1,k -SD_Sub st ( for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (b1,i) = SD2SDSubDigitS (x,i,k) ) & ( for i being Nat st i in Seg (n + 1) holds
DigA_SDSub (b2,i) = SD2SDSubDigitS (x,i,k) ) holds
b1 = b2
end;
definition
let n,
k be
Nat;
let x be
Tuple of
n,
k -SD_Sub ;
existence
ex b1 being Tuple of n, INT st
for i being Nat st i in Seg n holds
b1 /. i = SDSub2INTDigit (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 = SDSub2INTDigit (x,i,k) ) & ( for i being Nat st i in Seg n holds
b2 /. i = SDSub2INTDigit (x,i,k) ) holds
b1 = b2
end;