begin
Lm1:
for m being Nat st m >= 1 holds
m + 2 > 1
theorem Th1:
theorem
begin
:: deftheorem Def1 defines M0Digit RADIX_6:def 1 :
for i, m, k being Nat
for r being Tuple of m + 2,k -SD st i in Seg (m + 2) holds
( ( i >= m implies M0Digit r,i = r . i ) & ( not i >= m implies M0Digit r,i = 0 ) );
definition
let m,
k be
Nat;
let r be
Tuple of
m + 2,
k -SD ;
func M0 r -> Tuple of
m + 2,
k -SD means :
Def2:
for
i being
Nat st
i in Seg (m + 2) holds
DigA it,
i = M0Digit r,
i;
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;
:: deftheorem Def2 defines M0 RADIX_6:def 2 :
for m, k being Nat
for r, b4 being Tuple of m + 2,k -SD holds
( b4 = M0 r iff for i being Nat st i in Seg (m + 2) holds
DigA b4,i = M0Digit r,i );
:: deftheorem Def3 defines MmaxDigit RADIX_6:def 3 :
for i, m, k being Nat
for r being Tuple of m + 2,k -SD st k >= 2 & i in Seg (m + 2) holds
( ( i >= m implies MmaxDigit r,i = r . i ) & ( not i >= m implies MmaxDigit r,i = (Radix k) - 1 ) );
definition
let m,
k be
Nat;
let r be
Tuple of
m + 2,
k -SD ;
func Mmax r -> Tuple of
m + 2,
k -SD means :
Def4:
for
i being
Nat st
i in Seg (m + 2) holds
DigA it,
i = MmaxDigit r,
i;
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;
:: deftheorem Def4 defines Mmax RADIX_6:def 4 :
for m, k being Nat
for r, b4 being Tuple of m + 2,k -SD holds
( b4 = Mmax r iff for i being Nat st i in Seg (m + 2) holds
DigA b4,i = MmaxDigit r,i );
:: deftheorem Def5 defines MminDigit RADIX_6:def 5 :
for i, m, k being Nat
for r being Tuple of m + 2,k -SD st k >= 2 & i in Seg (m + 2) holds
( ( i >= m implies MminDigit r,i = r . i ) & ( not i >= m implies MminDigit r,i = (- (Radix k)) + 1 ) );
definition
let m,
k be
Nat;
let r be
Tuple of
m + 2,
k -SD ;
func Mmin r -> Tuple of
m + 2,
k -SD means :
Def6:
for
i being
Nat st
i in Seg (m + 2) holds
DigA it,
i = MminDigit r,
i;
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;
:: deftheorem Def6 defines Mmin RADIX_6:def 6 :
for m, k being Nat
for r, b4 being Tuple of m + 2,k -SD holds
( b4 = Mmin r iff for i being Nat st i in Seg (m + 2) holds
DigA b4,i = MminDigit r,i );
theorem Th3:
theorem Th4:
begin
:: deftheorem Def7 defines needs_digits_of RADIX_6:def 7 :
for n, k being Nat
for x being Integer holds
( x needs_digits_of n,k iff ( x < (Radix k) |^ n & x >= (Radix k) |^ (n -' 1) ) );
theorem Th5:
theorem Th6:
theorem Th7:
begin
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 )
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem
theorem
theorem
begin
:: deftheorem Def8 defines MmaskDigit RADIX_6:def 8 :
for i, m, k being Nat
for r being Tuple of m + 2,k -SD st i in Seg (m + 2) holds
( ( i < m implies MmaskDigit r,i = r . i ) & ( not i < m implies MmaskDigit r,i = 0 ) );
definition
let m,
k be
Nat;
let r be
Tuple of
m + 2,
k -SD ;
func Mmask r -> Tuple of
m + 2,
k -SD means :
Def9:
for
i being
Nat st
i in Seg (m + 2) holds
DigA it,
i = MmaskDigit r,
i;
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;
:: deftheorem Def9 defines Mmask RADIX_6:def 9 :
for m, k being Nat
for r, b4 being Tuple of m + 2,k -SD holds
( b4 = Mmask r iff for i being Nat st i in Seg (m + 2) holds
DigA b4,i = MmaskDigit r,i );
theorem Th17:
theorem
:: deftheorem Def10 defines FSDMinDigit RADIX_6:def 10 :
for i, m, k being Nat st k >= 2 holds
( ( i > m implies FSDMinDigit m,k,i = 0 ) & ( i = m implies FSDMinDigit m,k,i = 1 ) & ( not i > m & not i = m implies FSDMinDigit m,k,i = (- (Radix k)) + 1 ) );
definition
let n,
m,
k be
Nat;
func FSDMin n,
m,
k -> Tuple of
n,
k -SD means :
Def11:
for
i being
Nat st
i in Seg n holds
DigA it,
i = FSDMinDigit m,
k,
i;
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;
:: deftheorem Def11 defines FSDMin RADIX_6:def 11 :
for n, m, k being Nat
for b4 being Tuple of n,k -SD holds
( b4 = FSDMin n,m,k iff for i being Nat st i in Seg n holds
DigA b4,i = FSDMinDigit m,k,i );
theorem Th19:
:: deftheorem Def12 defines is_Zero_over RADIX_6:def 12 :
for n, m, k being Nat
for r being Tuple of m + 2,k -SD holds
( r is_Zero_over n iff for i being Nat st i > n holds
DigA r,i = 0 );
theorem