environ
vocabularies HIDDEN, NUMBERS, NAT_1, XXREAL_0, ARYTM_3, RADIX_1, RADIX_5, FINSEQ_1, CARD_1, FUNCT_1, NEWTON, RELAT_1, PARTFUN1, ARYTM_1, CARD_3, FINSEQ_2, SUBSET_1, INT_1, RADIX_6;
notations HIDDEN, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, NAT_D, NEWTON, RADIX_1, FINSEQ_1, FINSEQ_2, FUNCT_1, RELSET_1, PARTFUN1, GR_CY_1, RADIX_5;
definitions ;
theorems RADIX_1, RADIX_2, RADIX_4, RADIX_5, INT_1, NAT_1, NAT_2, FINSEQ_1, FINSEQ_2, RVSUM_1, NEWTON, PREPOWER, FUNCT_1, FINSEQ_3, XREAL_1, XXREAL_0, NAT_D, CARD_1;
schemes FINSEQ_2, NAT_1;
registrations RELSET_1, XREAL_0, NAT_1, INT_1, ORDINAL1, NEWTON, FINSEQ_2;
constructors HIDDEN, REAL_1, NAT_D, NEWTON, GR_CY_1, RADIX_5, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities ;
expansions ;
Lm1:
for m being Nat st m >= 1 holds
m + 2 > 1
definition
let m,
k be
Nat;
let r be
Tuple of
m + 2,
k -SD ;
existence
ex b1 being Tuple of m + 2,k -SD st
for i being Nat st i in Seg (m + 2) holds
DigA (b1,i) = M0Digit (r,i)
uniqueness
for b1, b2 being Tuple of m + 2,k -SD st ( for i being Nat st i in Seg (m + 2) holds
DigA (b1,i) = M0Digit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds
DigA (b2,i) = M0Digit (r,i) ) holds
b1 = b2
end;
definition
let m,
k be
Nat;
let r be
Tuple of
m + 2,
k -SD ;
existence
ex b1 being Tuple of m + 2,k -SD st
for i being Nat st i in Seg (m + 2) holds
DigA (b1,i) = MmaxDigit (r,i)
uniqueness
for b1, b2 being Tuple of m + 2,k -SD st ( for i being Nat st i in Seg (m + 2) holds
DigA (b1,i) = MmaxDigit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds
DigA (b2,i) = MmaxDigit (r,i) ) holds
b1 = b2
end;
definition
let m,
k be
Nat;
let r be
Tuple of
m + 2,
k -SD ;
existence
ex b1 being Tuple of m + 2,k -SD st
for i being Nat st i in Seg (m + 2) holds
DigA (b1,i) = MminDigit (r,i)
uniqueness
for b1, b2 being Tuple of m + 2,k -SD st ( for i being Nat st i in Seg (m + 2) holds
DigA (b1,i) = MminDigit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds
DigA (b2,i) = MminDigit (r,i) ) holds
b1 = b2
end;
theorem Th8:
for
mlow,
mhigh,
f being
Integer st
mhigh < mlow + f &
f > 0 holds
ex
s being
Integer st
(
- f < mlow - (s * f) &
mhigh - (s * f) < f )
definition
let m,
k be
Nat;
let r be
Tuple of
m + 2,
k -SD ;
existence
ex b1 being Tuple of m + 2,k -SD st
for i being Nat st i in Seg (m + 2) holds
DigA (b1,i) = MmaskDigit (r,i)
uniqueness
for b1, b2 being Tuple of m + 2,k -SD st ( for i being Nat st i in Seg (m + 2) holds
DigA (b1,i) = MmaskDigit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds
DigA (b2,i) = MmaskDigit (r,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) = FSDMinDigit (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) = FSDMinDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (b2,i) = FSDMinDigit (m,k,i) ) holds
b1 = b2
end;