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