environ
vocabularies HIDDEN, NUMBERS, NAT_1, XXREAL_0, RADIX_1, ARYTM_1, ARYTM_3, CARD_1, SUBSET_1, FINSEQ_1, POWER, RELAT_1, FINSEQ_2, PARTFUN1, NEWTON, FUNCT_1, CARD_3, INT_1, TARSKI, RADIX_5;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_D, NEWTON, RADIX_1, POWER, FUNCT_1, PARTFUN1, FINSEQ_1, FINSEQ_2, GR_CY_1;
definitions TARSKI;
theorems RADIX_1, RADIX_4, INT_1, NAT_1, FINSEQ_1, POWER, FINSEQ_2, NEWTON, RADIX_2, NAT_2, PREPOWER, PEPIN, JORDAN5B, FUNCT_1, RVSUM_1, XREAL_1, XXREAL_0, NAT_D, PARTFUN1, ORDINAL1, XREAL_0, CARD_1;
schemes NAT_1, FINSEQ_2;
registrations RELSET_1, NUMBERS, XREAL_0, NAT_1, INT_1, ORDINAL1, NEWTON, FINSEQ_2;
constructors HIDDEN, REAL_1, NAT_D, NEWTON, POWER, GR_CY_1, RADIX_4;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ;
expansions ;
Lm1:
for k being Nat st 2 <= k holds
SD_Add_Carry ((Radix k) - 1) = 1
Lm2:
for n, k, i being Nat st k >= 2 & i in Seg n holds
SD_Add_Carry (DigA ((DecSD (1,n,k)),i)) = 0
theorem Th14:
for
n being
Nat st
n >= 1 holds
for
k being
Nat st
k >= 2 holds
for
tx,
ty,
tz,
tw being
Tuple of
n,
k -SD st ( for
i being
Nat holds
( not
i in Seg n or (
DigA (
tx,
i)
= DigA (
tz,
i) &
DigA (
ty,
i)
= DigA (
tw,
i) ) or (
DigA (
ty,
i)
= DigA (
tz,
i) &
DigA (
tx,
i)
= DigA (
tw,
i) ) ) ) holds
(SDDec tz) + (SDDec tw) = (SDDec tx) + (SDDec ty)
theorem
for
n,
k being
Nat st
n >= 1 &
k >= 2 holds
for
tx,
ty,
tz being
Tuple of
n,
k -SD st ( for
i being
Nat holds
( not
i in Seg n or (
DigA (
tx,
i)
= DigA (
tz,
i) &
DigA (
ty,
i)
= 0 ) or (
DigA (
ty,
i)
= DigA (
tz,
i) &
DigA (
tx,
i)
= 0 ) ) ) holds
(SDDec tz) + (SDDec (DecSD (0,n,k))) = (SDDec tx) + (SDDec ty)
definition
let n,
m,
k 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) = SDMinDigit (m,k,i)
uniqueness
for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (b1,i) = SDMinDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (b2,i) = SDMinDigit (m,k,i) ) holds
b1 = b2
end;
definition
let n,
m,
k 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) = SDMaxDigit (m,k,i)
uniqueness
for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (b1,i) = SDMaxDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (b2,i) = SDMaxDigit (m,k,i) ) holds
b1 = b2
end;
definition
let n,
m,
k 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) = FminDigit (m,k,i)
uniqueness
for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (b1,i) = FminDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (b2,i) = FminDigit (m,k,i) ) holds
b1 = b2
end;
definition
let n,
m,
k 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) = FmaxDigit (m,k,i)
uniqueness
for b1, b2 being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (b1,i) = FmaxDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (b2,i) = FmaxDigit (m,k,i) ) holds
b1 = b2
end;