environ
vocabularies HIDDEN, NUMBERS, NAT_1, INT_1, ARYTM_1, ARYTM_3, CARD_1, XXREAL_0, SUBSET_1, RELAT_1, NEWTON, POWER, TARSKI, XBOOLE_0, FINSEQ_2, FINSEQ_1, FUNCT_1, PARTFUN1, CARD_3, ORDINAL4, RADIX_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, NAT_D, FUNCT_1, PARTFUN1, NEWTON, POWER, FINSEQ_1, RVSUM_1, FINSEQ_2, GR_CY_1, XXREAL_0;
definitions TARSKI;
theorems NAT_1, NAT_2, INT_1, FINSEQ_1, EULER_1, PREPOWER, POWER, RVSUM_1, FINSEQ_2, FINSEQ_4, TARSKI, FUNCT_1, PEPIN, FINSEQ_5, NEWTON, XCMPLX_1, XREAL_1, XXREAL_0, FINSOP_1, ORDINAL1, NAT_D, PARTFUN1, CARD_1, XREAL_0;
schemes NAT_1, FINSEQ_2;
registrations RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, VALUED_0, POWER, CARD_1, FINSEQ_1, ORDINAL1;
constructors HIDDEN, REAL_1, NAT_D, FINSOP_1, NEWTON, POWER, GR_CY_1, BINOP_2;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities RVSUM_1;
expansions ;
Lm1:
for k being Nat st k >= 2 holds
Radix k >= 2 + 2
definition
let n,
k be
Nat;
let x be
Tuple of
n,
k -SD ;
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;
definition
let k,
n,
x be
Nat;
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;
Lm2:
for x being Integer holds
( - 1 <= SD_Add_Carry x & SD_Add_Carry x <= 1 )
theorem Th22:
for
k,
m,
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 k, m, n, 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)
::
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 ;
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;
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)))))