:: RADIX_6 semantic presentation

begin

Lm1:  for m being Nat st m >= 1 holds
m + 2 > 1
proof
let m be Nat; ::_thesis: ( m >= 1 implies m + 2 > 1 )
 m + 2 > m by XREAL_1:29;
hence  ( m >= 1 implies m + 2 > 1 ) by XXREAL_0:2; ::_thesis: verum
end;

theorem Th1: :: RADIX_6:1
for n being Nat st n >= 1 holds
for m, k being Nat st m >= 1 & k >= 2 holds
SDDec (Fmin ((m + n),m,k)) = SDDec (Fmin (m,m,k))
proof
defpred S1[ Nat] means  for m, k being Nat st m >= 1 & k >= 2 holds
SDDec (Fmin ((m + $1),m,k)) = SDDec (Fmin (m,m,k));
A1: for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( n >= 1 & S1[n] implies S1[n + 1] )
assume that
 n >= 1 and
A2: S1[n] ; ::_thesis: S1[n + 1]
let m, k be Nat; ::_thesis: ( m >= 1 & k >= 2 implies SDDec (Fmin ((m + (n + 1)),m,k)) = SDDec (Fmin (m,m,k)) )
assume that
A3: m >= 1 and
A4: k >= 2 ; ::_thesis: SDDec (Fmin ((m + (n + 1)),m,k)) = SDDec (Fmin (m,m,k))
 m + n >= m by NAT_1:11;
then A5: (m + n) + 1 > m by NAT_1:13;
 (m + n) + 1 in Seg ((m + n) + 1) by FINSEQ_1:4;
then A6: DigA ((Fmin (((m + n) + 1),m,k)),((m + n) + 1)) = FminDigit (m,k,((m + n) + 1)) by RADIX_5:def_6
.= 0 by A4, A5, RADIX_5:def_5 ;
 for i being Nat st i in Seg (m + n) holds
(Fmin (((m + n) + 1),m,k)) . i = (Fmin ((m + n),m,k)) . i
proof
let i be Nat; ::_thesis: ( i in Seg (m + n) implies (Fmin (((m + n) + 1),m,k)) . i = (Fmin ((m + n),m,k)) . i )
assume A7: i in Seg (m + n) ; ::_thesis: (Fmin (((m + n) + 1),m,k)) . i = (Fmin ((m + n),m,k)) . i
then A8: i in Seg ((m + n) + 1) by FINSEQ_2:8;
then (Fmin (((m + n) + 1),m,k)) . i = DigA ((Fmin (((m + n) + 1),m,k)),i) by RADIX_1:def_3
.= FminDigit (m,k,i) by A8, RADIX_5:def_6
.= DigA ((Fmin ((m + n),m,k)),i) by A7, RADIX_5:def_6 ;
hence  (Fmin (((m + n) + 1),m,k)) . i = (Fmin ((m + n),m,k)) . i by A7, RADIX_1:def_3; ::_thesis: verum
end;
then  SDDec (Fmin ((m + (n + 1)),m,k)) = (SDDec (Fmin ((m + n),m,k))) + (((Radix k) |^ (m + n)) * (DigA ((Fmin (((m + n) + 1),m,k)),((m + n) + 1)))) by RADIX_2:10
.= SDDec (Fmin (m,m,k)) by A2, A3, A4, A6 ;
hence  SDDec (Fmin ((m + (n + 1)),m,k)) = SDDec (Fmin (m,m,k)) ; ::_thesis: verum
end;
A9: S1[1]
proof
let m, k be Nat; ::_thesis: ( m >= 1 & k >= 2 implies SDDec (Fmin ((m + 1),m,k)) = SDDec (Fmin (m,m,k)) )
assume that
 m >= 1 and
A10: k >= 2 ; ::_thesis: SDDec (Fmin ((m + 1),m,k)) = SDDec (Fmin (m,m,k))
A11: m + 1 > m by NAT_1:13;
 for i being Nat st i in Seg m holds
(Fmin ((m + 1),m,k)) . i = (Fmin (m,m,k)) . i
proof
let i be Nat; ::_thesis: ( i in Seg m implies (Fmin ((m + 1),m,k)) . i = (Fmin (m,m,k)) . i )
assume A12: i in Seg m ; ::_thesis: (Fmin ((m + 1),m,k)) . i = (Fmin (m,m,k)) . i
then A13: i in Seg (m + 1) by FINSEQ_2:8;
then (Fmin ((m + 1),m,k)) . i = DigA ((Fmin ((m + 1),m,k)),i) by RADIX_1:def_3
.= FminDigit (m,k,i) by A13, RADIX_5:def_6
.= DigA ((Fmin (m,m,k)),i) by A12, RADIX_5:def_6 ;
hence  (Fmin ((m + 1),m,k)) . i = (Fmin (m,m,k)) . i by A12, RADIX_1:def_3; ::_thesis: verum
end;
then A14: SDDec (Fmin ((m + 1),m,k)) = (SDDec (Fmin (m,m,k))) + (((Radix k) |^ m) * (DigA ((Fmin ((m + 1),m,k)),(m + 1)))) by RADIX_2:10;
 m + 1 in Seg (m + 1) by FINSEQ_1:4;
then  DigA ((Fmin ((m + 1),m,k)),(m + 1)) = FminDigit (m,k,(m + 1)) by RADIX_5:def_6
.= 0 by A10, A11, RADIX_5:def_5 ;
hence  SDDec (Fmin ((m + 1),m,k)) = SDDec (Fmin (m,m,k)) by A14; ::_thesis: verum
end;
 for n being Nat st n >= 1 holds
S1[n] from NAT_1:sch_8(A9, A1);
hence  for n being Nat st n >= 1 holds
for m, k being Nat st m >= 1 & k >= 2 holds
SDDec (Fmin ((m + n),m,k)) = SDDec (Fmin (m,m,k)) ; ::_thesis: verum
end;

theorem :: RADIX_6:2
for m, k being Nat st m >= 1 & k >= 2 holds
SDDec (Fmin (m,m,k)) > 0
proof
defpred S1[ Nat] means  for k being Nat st k >= 2 holds
SDDec (Fmin ($1,$1,k)) > 0 ;
A1: for m being Nat st m >= 1 & S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( m >= 1 & S1[m] implies S1[m + 1] )
assume that
A2: m >= 1 and
 S1[m] ; ::_thesis: S1[m + 1]
let k be Nat; ::_thesis: ( k >= 2 implies SDDec (Fmin ((m + 1),(m + 1),k)) > 0 )
assume A3: k >= 2 ; ::_thesis: SDDec (Fmin ((m + 1),(m + 1),k)) > 0
then  Radix k > 2 by RADIX_4:1;
then A4: Radix k > 1 by XXREAL_0:2;
 m + 1 in Seg (m + 1) by FINSEQ_1:4;
then A5: DigA ((Fmin ((m + 1),(m + 1),k)),(m + 1)) = FminDigit ((m + 1),k,(m + 1)) by RADIX_5:def_6
.= 1 by A3, RADIX_5:def_5 ;
 for i being Nat st i in Seg m holds
(Fmin ((m + 1),(m + 1),k)) . i = (DecSD (0,m,k)) . i
proof
let i be Nat; ::_thesis: ( i in Seg m implies (Fmin ((m + 1),(m + 1),k)) . i = (DecSD (0,m,k)) . i )
assume A6: i in Seg m ; ::_thesis: (Fmin ((m + 1),(m + 1),k)) . i = (DecSD (0,m,k)) . i
then  i <= m by FINSEQ_1:1;
then A7: i < m + 1 by NAT_1:13;
A8: i in Seg (m + 1) by A6, FINSEQ_2:8;
then (Fmin ((m + 1),(m + 1),k)) . i = DigA ((Fmin ((m + 1),(m + 1),k)),i) by RADIX_1:def_3
.= FminDigit ((m + 1),k,i) by A8, RADIX_5:def_6
.= 0 by A3, A7, RADIX_5:def_5
.= DigA ((DecSD (0,m,k)),i) by A6, RADIX_5:5 ;
hence  (Fmin ((m + 1),(m + 1),k)) . i = (DecSD (0,m,k)) . i by A6, RADIX_1:def_3; ::_thesis: verum
end;
then  SDDec (Fmin ((m + 1),(m + 1),k)) = (SDDec (DecSD (0,m,k))) + (((Radix k) |^ m) * (DigA ((Fmin ((m + 1),(m + 1),k)),(m + 1)))) by RADIX_2:10
.= 0 + ((Radix k) |^ m) by A2, A5, RADIX_5:6 ;
hence  SDDec (Fmin ((m + 1),(m + 1),k)) > 0 by A4, PREPOWER:11; ::_thesis: verum
end;
A9: S1[1]
proof
let k be Nat; ::_thesis: ( k >= 2 implies SDDec (Fmin (1,1,k)) > 0 )
assume A10: k >= 2 ; ::_thesis: SDDec (Fmin (1,1,k)) > 0
A11: 1 in Seg 1 by FINSEQ_1:1;
then (DigitSD (Fmin (1,1,k))) /. 1 = SubDigit ((Fmin (1,1,k)),1,k) by RADIX_1:def_6
.= ((Radix k) |^ (1 -' 1)) * (DigB ((Fmin (1,1,k)),1)) by RADIX_1:def_5
.= ((Radix k) |^ (1 -' 1)) * (DigA ((Fmin (1,1,k)),1)) by RADIX_1:def_4
.= ((Radix k) |^ 0) * (DigA ((Fmin (1,1,k)),1)) by XREAL_1:232
.= 1 * (DigA ((Fmin (1,1,k)),1)) by NEWTON:4
.= FminDigit (1,k,1) by A11, RADIX_5:def_6
.= 1 by A10, RADIX_5:def_5 ;
then A12: DigitSD (Fmin (1,1,k)) = <*1*> by RADIX_1:17;
SDDec (Fmin (1,1,k)) = Sum (DigitSD (Fmin (1,1,k))) by RADIX_1:def_7
.= 1 by A12, RVSUM_1:73 ;
hence  SDDec (Fmin (1,1,k)) > 0 ; ::_thesis: verum
end;
 for m being Nat st m >= 1 holds
S1[m] from NAT_1:sch_8(A9, A1);
hence  for m, k being Nat st m >= 1 & k >= 2 holds
SDDec (Fmin (m,m,k)) > 0 ; ::_thesis: verum
end;

begin

definition
let i, m, k be Nat;
let r be Tuple of m + 2,k -SD ;
assume A1: i in Seg (m + 2) ;
func M0Digit (r,i) ->  Element of k -SD  equals :Def1: :: RADIX_6:def 1
r . i if i >= m
otherwise  0 ;
coherence
 ( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies 0 is Element of k -SD ) )
proof
 len r = m + 2 by CARD_1:def_7;
then  i in dom r by A1, FINSEQ_1:def_3;
then  r . i in rng r by FUNCT_1:def_3;
hence  ( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies 0 is Element of k -SD ) ) by RADIX_1:14; ::_thesis: verum
end;
consistency
 for b1 being Element of k -SD holds verum ;
end;

:: 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: :: RADIX_6:def 2
 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)
proof
deffunc H1( Nat) ->  Element of k -SD = M0Digit (r,$1);
consider z being FinSequence of k -SD  such that
A1: len z = m + 2 and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg (m + 2) by A1, FINSEQ_1:def_3;
 z is Element of (m + 2) -tuples_on (k -SD) by A1, FINSEQ_2:92;
then reconsider z = z as Tuple of m + 2,k -SD ;
take  z ; ::_thesis: for i being Nat st i in Seg (m + 2) holds
DigA (z,i) = M0Digit (r,i)
let i be Nat; ::_thesis: ( i in Seg (m + 2) implies DigA (z,i) = M0Digit (r,i) )
assume A4: i in Seg (m + 2) ; ::_thesis: DigA (z,i) = M0Digit (r,i)
hence  DigA (z,i) = z . i by RADIX_1:def_3
.= M0Digit (r,i) by A2, A3, A4 ;
::_thesis: verum
end;
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
proof
let k1, k2 be Tuple of m + 2,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg (m + 2) holds
DigA (k1,i) = M0Digit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds
DigA (k2,i) = M0Digit (r,i) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg (m + 2) holds
DigA (k1,i) = M0Digit (r,i) and
A6: for i being Nat st i in Seg (m + 2) holds
DigA (k2,i) = M0Digit (r,i) ; ::_thesis: k1 = k2
A7: len k1 = m + 2 by CARD_1:def_7;
then A8: dom k1 = Seg (m + 2) by FINSEQ_1:def_3;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then k1 . j = DigA (k1,j) by A8, RADIX_1:def_3
.= M0Digit (r,j) by A5, A8, A10
.= DigA (k2,j) by A6, A8, A10
.= k2 . j by A8, A10, RADIX_1:def_3 ;
hence  k1 . j = k2 . j ; ::_thesis: verum
end;
 len k2 = m + 2 by CARD_1:def_7;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
end;
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) );

definition
let i, m, k be Nat;
let r be Tuple of m + 2,k -SD ;
assume that
A1: k >= 2 and
A2: i in Seg (m + 2) ;
func MmaxDigit (r,i) ->  Element of k -SD  equals :Def3: :: RADIX_6:def 3
r . i if i >= m
otherwise (Radix k) - 1;
coherence
 ( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies (Radix k) - 1 is Element of k -SD ) )
proof
 len r = m + 2 by CARD_1:def_7;
then  i in dom r by A2, FINSEQ_1:def_3;
then  r . i in rng r by FUNCT_1:def_3;
hence  ( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies (Radix k) - 1 is Element of k -SD ) ) by A1, RADIX_5:1; ::_thesis: verum
end;
consistency
 for b1 being Element of k -SD holds verum ;
end;

:: 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: :: RADIX_6:def 4
 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)
proof
deffunc H1( Nat) ->  Element of k -SD = MmaxDigit (r,$1);
consider z being FinSequence of k -SD  such that
A1: len z = m + 2 and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg (m + 2) by A1, FINSEQ_1:def_3;
 z is Element of (m + 2) -tuples_on (k -SD) by A1, FINSEQ_2:92;
then reconsider z = z as Tuple of m + 2,k -SD ;
take  z ; ::_thesis: for i being Nat st i in Seg (m + 2) holds
DigA (z,i) = MmaxDigit (r,i)
let i be Nat; ::_thesis: ( i in Seg (m + 2) implies DigA (z,i) = MmaxDigit (r,i) )
assume A4: i in Seg (m + 2) ; ::_thesis: DigA (z,i) = MmaxDigit (r,i)
hence  DigA (z,i) = z . i by RADIX_1:def_3
.= MmaxDigit (r,i) by A2, A3, A4 ;
::_thesis: verum
end;
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
proof
let k1, k2 be Tuple of m + 2,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg (m + 2) holds
DigA (k1,i) = MmaxDigit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds
DigA (k2,i) = MmaxDigit (r,i) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg (m + 2) holds
DigA (k1,i) = MmaxDigit (r,i) and
A6: for i being Nat st i in Seg (m + 2) holds
DigA (k2,i) = MmaxDigit (r,i) ; ::_thesis: k1 = k2
A7: len k1 = m + 2 by CARD_1:def_7;
then A8: dom k1 = Seg (m + 2) by FINSEQ_1:def_3;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then k1 . j = DigA (k1,j) by A8, RADIX_1:def_3
.= MmaxDigit (r,j) by A5, A8, A10
.= DigA (k2,j) by A6, A8, A10
.= k2 . j by A8, A10, RADIX_1:def_3 ;
hence  k1 . j = k2 . j ; ::_thesis: verum
end;
 len k2 = m + 2 by CARD_1:def_7;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
end;
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) );

definition
let i, m, k be Nat;
let r be Tuple of m + 2,k -SD ;
assume that
A1: k >= 2 and
A2: i in Seg (m + 2) ;
func MminDigit (r,i) ->  Element of k -SD  equals :Def5: :: RADIX_6:def 5
r . i if i >= m
otherwise (- (Radix k)) + 1;
coherence
 ( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies (- (Radix k)) + 1 is Element of k -SD ) )
proof
 len r = m + 2 by CARD_1:def_7;
then  i in dom r by A2, FINSEQ_1:def_3;
then A3: r . i in rng r by FUNCT_1:def_3;
 Radix k > 2 by A1, RADIX_4:1;
then  Radix k > 1 by XXREAL_0:2;
then  (Radix k) + (Radix k) > 1 + 1 by XREAL_1:8;
then A4: (Radix k) - 1 > 1 - (Radix k) by XREAL_1:21;
A5: (- (Radix k)) + 1 is Element of INT by INT_1:def_2;
 k -SD =  {  w where w is Element of INT : ( w <= (Radix k) - 1 & w >= (- (Radix k)) + 1 )  }  by RADIX_1:def_2;
then  (- (Radix k)) + 1 in k -SD by A4, A5;
hence  ( ( i >= m implies r . i is Element of k -SD ) & ( not i >= m implies (- (Radix k)) + 1 is Element of k -SD ) ) by A3; ::_thesis: verum
end;
consistency
 for b1 being Element of k -SD holds verum ;
end;

:: 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: :: RADIX_6:def 6
 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)
proof
deffunc H1( Nat) ->  Element of k -SD = MminDigit (r,$1);
consider z being FinSequence of k -SD  such that
A1: len z = m + 2 and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg (m + 2) by A1, FINSEQ_1:def_3;
 z is Element of (m + 2) -tuples_on (k -SD) by A1, FINSEQ_2:92;
then reconsider z = z as Tuple of m + 2,k -SD ;
take  z ; ::_thesis: for i being Nat st i in Seg (m + 2) holds
DigA (z,i) = MminDigit (r,i)
let i be Nat; ::_thesis: ( i in Seg (m + 2) implies DigA (z,i) = MminDigit (r,i) )
assume A4: i in Seg (m + 2) ; ::_thesis: DigA (z,i) = MminDigit (r,i)
hence  DigA (z,i) = z . i by RADIX_1:def_3
.= H1(i) by A2, A3, A4 ;
::_thesis: verum
end;
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
proof
let k1, k2 be Tuple of m + 2,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg (m + 2) holds
DigA (k1,i) = MminDigit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds
DigA (k2,i) = MminDigit (r,i) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg (m + 2) holds
DigA (k1,i) = MminDigit (r,i) and
A6: for i being Nat st i in Seg (m + 2) holds
DigA (k2,i) = MminDigit (r,i) ; ::_thesis: k1 = k2
A7: len k1 = m + 2 by CARD_1:def_7;
then A8: dom k1 = Seg (m + 2) by FINSEQ_1:def_3;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then k1 . j = DigA (k1,j) by A8, RADIX_1:def_3
.= MminDigit (r,j) by A5, A8, A10
.= DigA (k2,j) by A6, A8, A10
.= k2 . j by A8, A10, RADIX_1:def_3 ;
hence  k1 . j = k2 . j ; ::_thesis: verum
end;
 len k2 = m + 2 by CARD_1:def_7;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
end;
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: :: RADIX_6:3
for m, k being Nat st k >= 2 holds
for r being Tuple of m + 2,k -SD holds SDDec (Mmax r) >= SDDec r
proof
let m, k be Nat; ::_thesis: ( k >= 2 implies for r being Tuple of m + 2,k -SD holds SDDec (Mmax r) >= SDDec r )
assume A1: k >= 2 ; ::_thesis: for r being Tuple of m + 2,k -SD holds SDDec (Mmax r) >= SDDec r
let r be Tuple of m + 2,k -SD ; ::_thesis: SDDec (Mmax r) >= SDDec r
 for i being Nat st i in Seg (m + 2) holds
DigA ((Mmax r),i) >= DigA (r,i)
proof
let i be Nat; ::_thesis: ( i in Seg (m + 2) implies DigA ((Mmax r),i) >= DigA (r,i) )
assume A2: i in Seg (m + 2) ; ::_thesis: DigA ((Mmax r),i) >= DigA (r,i)
then A3: DigA ((Mmax r),i) = MmaxDigit (r,i) by Def4;
now__::_thesis:_DigA_((Mmax_r),i)_>=_DigA_(r,i)
percases ( i >= m or i < m ) ;
suppose i >= m ; ::_thesis: DigA ((Mmax r),i) >= DigA (r,i)
then  DigA ((Mmax r),i) = r . i by A1, A2, A3, Def3
.= DigA (r,i) by A2, RADIX_1:def_3 ;
hence  DigA ((Mmax r),i) >= DigA (r,i) ; ::_thesis: verum
end;
supposeA4: i < m ; ::_thesis: DigA ((Mmax r),i) >= DigA (r,i)
A5: DigA (r,i) = r . i by A2, RADIX_1:def_3;
A6: r . i is Element of k -SD by A2, RADIX_1:15;
 DigA ((Mmax r),i) = (Radix k) - 1 by A1, A2, A3, A4, Def3;
hence  DigA ((Mmax r),i) >= DigA (r,i) by A5, A6, RADIX_1:13; ::_thesis: verum
end;
end;
end;
hence  DigA ((Mmax r),i) >= DigA (r,i) ; ::_thesis: verum
end;
hence  SDDec (Mmax r) >= SDDec r by NAT_1:12, RADIX_5:13; ::_thesis: verum
end;

theorem Th4: :: RADIX_6:4
for m, k being Nat st k >= 2 holds
for r being Tuple of m + 2,k -SD holds SDDec r >= SDDec (Mmin r)
proof
let m, k be Nat; ::_thesis: ( k >= 2 implies for r being Tuple of m + 2,k -SD holds SDDec r >= SDDec (Mmin r) )
assume A1: k >= 2 ; ::_thesis: for r being Tuple of m + 2,k -SD holds SDDec r >= SDDec (Mmin r)
let r be Tuple of m + 2,k -SD ; ::_thesis: SDDec r >= SDDec (Mmin r)
 for i being Nat st i in Seg (m + 2) holds
DigA (r,i) >= DigA ((Mmin r),i)
proof
let i be Nat; ::_thesis: ( i in Seg (m + 2) implies DigA (r,i) >= DigA ((Mmin r),i) )
assume A2: i in Seg (m + 2) ; ::_thesis: DigA (r,i) >= DigA ((Mmin r),i)
then A3: DigA ((Mmin r),i) = MminDigit (r,i) by Def6;
now__::_thesis:_DigA_(r,i)_>=_DigA_((Mmin_r),i)
percases ( i >= m or i < m ) ;
suppose i >= m ; ::_thesis: DigA (r,i) >= DigA ((Mmin r),i)
then  DigA ((Mmin r),i) = r . i by A1, A2, A3, Def5
.= DigA (r,i) by A2, RADIX_1:def_3 ;
hence  DigA (r,i) >= DigA ((Mmin r),i) ; ::_thesis: verum
end;
supposeA4: i < m ; ::_thesis: DigA (r,i) >= DigA ((Mmin r),i)
A5: DigA (r,i) = r . i by A2, RADIX_1:def_3;
A6: r . i is Element of k -SD by A2, RADIX_1:15;
 DigA ((Mmin r),i) = (- (Radix k)) + 1 by A1, A2, A3, A4, Def5;
hence  DigA (r,i) >= DigA ((Mmin r),i) by A5, A6, RADIX_1:13; ::_thesis: verum
end;
end;
end;
hence  DigA (r,i) >= DigA ((Mmin r),i) ; ::_thesis: verum
end;
hence  SDDec r >= SDDec (Mmin r) by NAT_1:12, RADIX_5:13; ::_thesis: verum
end;

begin

definition
let n, k be Nat;
let x be Integer;
predx needs_digits_of n,k means :Def7: :: RADIX_6:def 7
( x < (Radix k) |^ n & x >= (Radix k) |^ (n -' 1) );
end;

:: 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: :: RADIX_6:5
for x, n, k, i being Nat st i in Seg n holds
DigA ((DecSD (x,n,k)),i) >= 0
proof
let x, n, k, i be Nat; ::_thesis: ( i in Seg n implies DigA ((DecSD (x,n,k)),i) >= 0 )
assume A1: i in Seg n ; ::_thesis: DigA ((DecSD (x,n,k)),i) >= 0
then A2: i >= 1 by FINSEQ_1:1;
DigA ((DecSD (x,n,k)),i) = DigitDC (x,i,k) by A1, RADIX_1:def_9
.= (x mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)) by RADIX_1:def_8
.= (x div ((Radix k) |^ (i -' 1))) mod (Radix k) by A2, RADIX_2:4, RADIX_2:6 ;
hence  DigA ((DecSD (x,n,k)),i) >= 0 ; ::_thesis: verum
end;

theorem Th6: :: RADIX_6:6
for n, k, x being Nat st n >= 1 & x needs_digits_of n,k holds
DigA ((DecSD (x,n,k)),n) > 0
proof
let n, k, x be Nat; ::_thesis: ( n >= 1 & x needs_digits_of n,k implies DigA ((DecSD (x,n,k)),n) > 0 )
assume that
A1: n >= 1 and
A2: x needs_digits_of n,k ; ::_thesis: DigA ((DecSD (x,n,k)),n) > 0
 x < (Radix k) |^ n by A2, Def7;
then A3: x mod ((Radix k) |^ n) = x by NAT_D:24;
 n in Seg n by A1, FINSEQ_1:3;
then A4: DigA ((DecSD (x,n,k)),n) = DigitDC (x,n,k) by RADIX_1:def_9
.= x div ((Radix k) |^ (n -' 1)) by A3, RADIX_1:def_8 ;
A5: (Radix k) |^ (n -' 1) > 0 by PREPOWER:6, RADIX_2:6;
 x >= (Radix k) |^ (n -' 1) by A2, Def7;
hence  DigA ((DecSD (x,n,k)),n) > 0 by A4, A5, NAT_2:13; ::_thesis: verum
end;

theorem Th7: :: RADIX_6:7
for f, m, k being Nat st m >= 1 & k >= 2 & f needs_digits_of m,k holds
f >= SDDec (Fmin ((m + 2),m,k))
proof
let f, m, k be Nat; ::_thesis: ( m >= 1 & k >= 2 & f needs_digits_of m,k implies f >= SDDec (Fmin ((m + 2),m,k)) )
assume that
A1: m >= 1 and
A2: k >= 2 and
A3: f needs_digits_of m,k ; ::_thesis: f >= SDDec (Fmin ((m + 2),m,k))
 for i being Nat st i in Seg m holds
DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i)
proof
let i be Nat; ::_thesis: ( i in Seg m implies DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i) )
assume A4: i in Seg m ; ::_thesis: DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i)
then A5: i <= m by FINSEQ_1:1;
now__::_thesis:_DigA_((DecSD_(f,m,k)),i)_>=_DigA_((Fmin_(m,m,k)),i)
percases ( i = m or i < m ) by A5, XXREAL_0:1;
supposeA6: i = m ; ::_thesis: DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i)
then  DigA ((DecSD (f,m,k)),i) > 0 by A1, A3, Th6;
then A7: DigA ((DecSD (f,m,k)),i) >= 0 + 1 by INT_1:7;
DigA ((Fmin (m,m,k)),i) = FminDigit (m,k,i) by A4, RADIX_5:def_6
.= 1 by A2, A6, RADIX_5:def_5 ;
hence  DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i) by A7; ::_thesis: verum
end;
supposeA8: i < m ; ::_thesis: DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i)
DigA ((Fmin (m,m,k)),i) = FminDigit (m,k,i) by A4, RADIX_5:def_6
.= 0 by A2, A8, RADIX_5:def_5 ;
hence  DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i) by A4, Th5; ::_thesis: verum
end;
end;
end;
hence  DigA ((DecSD (f,m,k)),i) >= DigA ((Fmin (m,m,k)),i) ; ::_thesis: verum
end;
then  SDDec (DecSD (f,m,k)) >= SDDec (Fmin (m,m,k)) by A1, RADIX_5:13;
then A9: SDDec (DecSD (f,m,k)) >= SDDec (Fmin ((m + 2),m,k)) by A1, A2, Th1;
 f < (Radix k) |^ m by A3, Def7;
then  f is_represented_by m,k by RADIX_1:def_12;
hence  f >= SDDec (Fmin ((m + 2),m,k)) by A1, A9, RADIX_1:22; ::_thesis: verum
end;

begin

theorem Th8: :: RADIX_6:8
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 )
proof
let mlow, mhigh, f be Integer; ::_thesis: ( mhigh < mlow + f & f > 0 implies ex s being Integer st
( - f < mlow - (s * f) & mhigh - (s * f) < f ) )
assume that
A1: mhigh < mlow + f and
A2: f > 0 ; ::_thesis: ex s being Integer st
( - f < mlow - (s * f) & mhigh - (s * f) < f )
reconsider f = f as Element of NAT by A2, INT_1:3;
A3: mhigh + (- ((mhigh div f) * f)) < (mlow + f) + (- ((mhigh div f) * f)) by A1, XREAL_1:6;
A4: mhigh mod f = mhigh - ((mhigh div f) * f) by A2, INT_1:def_10;
then  0 <= mhigh - ((mhigh div f) * f) by A2, NAT_D:62;
then  0 + (- f) < ((mlow + (- ((mhigh div f) * f))) + f) + (- f) by A3, XREAL_1:6;
then  - f < mlow - ((mhigh div f) * f) ;
hence  ex s being Integer st
( - f < mlow - (s * f) & mhigh - (s * f) < f ) by A2, A4, NAT_D:62; ::_thesis: verum
end;

theorem Th9: :: RADIX_6:9
for m, k being Nat st k >= 2 holds
for r being Tuple of m + 2,k -SD holds (SDDec (Mmax r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMax ((m + 2),m,k)))
proof
let m, k be Nat; ::_thesis: ( k >= 2 implies for r being Tuple of m + 2,k -SD holds (SDDec (Mmax r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMax ((m + 2),m,k))) )
assume A1: k >= 2 ; ::_thesis: for r being Tuple of m + 2,k -SD holds (SDDec (Mmax r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMax ((m + 2),m,k)))
let r be Tuple of m + 2,k -SD ; ::_thesis: (SDDec (Mmax r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMax ((m + 2),m,k)))
A2: for i being Nat holds
( not i in Seg (m + 2) or ( DigA ((M0 r),i) = DigA ((Mmax r),i) & DigA ((SDMax ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMax ((m + 2),m,k)),i) = DigA ((Mmax r),i) & DigA ((M0 r),i) = 0 ) )
proof
let i be Nat; ::_thesis: ( not i in Seg (m + 2) or ( DigA ((M0 r),i) = DigA ((Mmax r),i) & DigA ((SDMax ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMax ((m + 2),m,k)),i) = DigA ((Mmax r),i) & DigA ((M0 r),i) = 0 ) )
assume A3: i in Seg (m + 2) ; ::_thesis: ( ( DigA ((M0 r),i) = DigA ((Mmax r),i) & DigA ((SDMax ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMax ((m + 2),m,k)),i) = DigA ((Mmax r),i) & DigA ((M0 r),i) = 0 ) )
then A4: DigA ((Mmax r),i) = MmaxDigit (r,i) by Def4;
A5: i >= 1 by A3, FINSEQ_1:1;
now__::_thesis:_(_(_DigA_((M0_r),i)_=_DigA_((Mmax_r),i)_&_DigA_((SDMax_((m_+_2),m,k)),i)_=_0_)_or_(_DigA_((SDMax_((m_+_2),m,k)),i)_=_DigA_((Mmax_r),i)_&_DigA_((M0_r),i)_=_0_)_)
percases ( i < m or i >= m ) ;
supposeA6: i < m ; ::_thesis: ( ( DigA ((M0 r),i) = DigA ((Mmax r),i) & DigA ((SDMax ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMax ((m + 2),m,k)),i) = DigA ((Mmax r),i) & DigA ((M0 r),i) = 0 ) )
A7: DigA ((M0 r),i) = M0Digit (r,i) by A3, Def2
.= 0 by A3, A6, Def1 ;
DigA ((Mmax r),i) = (Radix k) - 1 by A1, A3, A4, A6, Def3
.= SDMaxDigit (m,k,i) by A1, A5, A6, RADIX_5:def_3
.= DigA ((SDMax ((m + 2),m,k)),i) by A3, RADIX_5:def_4 ;
hence  ( ( DigA ((M0 r),i) = DigA ((Mmax r),i) & DigA ((SDMax ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMax ((m + 2),m,k)),i) = DigA ((Mmax r),i) & DigA ((M0 r),i) = 0 ) ) by A7; ::_thesis: verum
end;
supposeA8: i >= m ; ::_thesis: ( ( DigA ((M0 r),i) = DigA ((Mmax r),i) & DigA ((SDMax ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMax ((m + 2),m,k)),i) = DigA ((Mmax r),i) & DigA ((M0 r),i) = 0 ) )
A9: DigA ((SDMax ((m + 2),m,k)),i) = SDMaxDigit (m,k,i) by A3, RADIX_5:def_4
.= 0 by A1, A8, RADIX_5:def_3 ;
DigA ((Mmax r),i) = r . i by A1, A3, A4, A8, Def3
.= M0Digit (r,i) by A3, A8, Def1
.= DigA ((M0 r),i) by A3, Def2 ;
hence  ( ( DigA ((M0 r),i) = DigA ((Mmax r),i) & DigA ((SDMax ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMax ((m + 2),m,k)),i) = DigA ((Mmax r),i) & DigA ((M0 r),i) = 0 ) ) by A9; ::_thesis: verum
end;
end;
end;
hence  ( ( DigA ((M0 r),i) = DigA ((Mmax r),i) & DigA ((SDMax ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMax ((m + 2),m,k)),i) = DigA ((Mmax r),i) & DigA ((M0 r),i) = 0 ) ) ; ::_thesis: verum
end;
 m + 2 >= 1 by NAT_1:12;
hence  (SDDec (Mmax r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMax ((m + 2),m,k))) by A1, A2, RADIX_5:15; ::_thesis: verum
end;

theorem Th10: :: RADIX_6:10
for m, k being Nat st m >= 1 & k >= 2 holds
for r being Tuple of m + 2,k -SD holds SDDec (Mmax r) < (SDDec (M0 r)) + (SDDec (Fmin ((m + 2),m,k)))
proof
let m, k be Nat; ::_thesis: ( m >= 1 & k >= 2 implies for r being Tuple of m + 2,k -SD holds SDDec (Mmax r) < (SDDec (M0 r)) + (SDDec (Fmin ((m + 2),m,k))) )
assume that
A1: m >= 1 and
A2: k >= 2 ; ::_thesis: for r being Tuple of m + 2,k -SD holds SDDec (Mmax r) < (SDDec (M0 r)) + (SDDec (Fmin ((m + 2),m,k)))
A3: m + 2 > 1 by A1, Lm1;
let r be Tuple of m + 2,k -SD ; ::_thesis: SDDec (Mmax r) < (SDDec (M0 r)) + (SDDec (Fmin ((m + 2),m,k)))
A4: (SDDec (Mmax r)) + 1 > (SDDec (Mmax r)) + 0 by XREAL_1:8;
A5: (SDDec (M0 r)) + (SDDec (SDMax ((m + 2),m,k))) = (SDDec (Mmax r)) + (SDDec (DecSD (0,(m + 2),k))) by A2, Th9
.= (SDDec (Mmax r)) + 0 by A3, RADIX_5:6 ;
 m in Seg (m + 2) by A1, FINSEQ_3:9;
then  SDDec (Fmin ((m + 2),m,k)) = (SDDec (SDMax ((m + 2),m,k))) + (SDDec (DecSD (1,(m + 2),k))) by A2, A3, RADIX_5:18
.= (SDDec (SDMax ((m + 2),m,k))) + 1 by A2, A3, RADIX_5:9 ;
hence  SDDec (Mmax r) < (SDDec (M0 r)) + (SDDec (Fmin ((m + 2),m,k))) by A5, A4; ::_thesis: verum
end;

theorem Th11: :: RADIX_6:11
for m, k being Nat st k >= 2 holds
for r being Tuple of m + 2,k -SD holds (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k)))
proof
let m, k be Nat; ::_thesis: ( k >= 2 implies for r being Tuple of m + 2,k -SD holds (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k))) )
assume A1: k >= 2 ; ::_thesis: for r being Tuple of m + 2,k -SD holds (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k)))
let r be Tuple of m + 2,k -SD ; ::_thesis: (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k)))
A2: for i being Nat holds
( not i in Seg (m + 2) or ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) )
proof
let i be Nat; ::_thesis: ( not i in Seg (m + 2) or ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) )
assume A3: i in Seg (m + 2) ; ::_thesis: ( ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) )
then A4: DigA ((Mmin r),i) = MminDigit (r,i) by Def6;
A5: i >= 1 by A3, FINSEQ_1:1;
now__::_thesis:_(_(_DigA_((M0_r),i)_=_DigA_((Mmin_r),i)_&_DigA_((SDMin_((m_+_2),m,k)),i)_=_0_)_or_(_DigA_((SDMin_((m_+_2),m,k)),i)_=_DigA_((Mmin_r),i)_&_DigA_((M0_r),i)_=_0_)_)
percases ( i < m or i >= m ) ;
supposeA6: i < m ; ::_thesis: ( ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) )
A7: DigA ((M0 r),i) = M0Digit (r,i) by A3, Def2
.= 0 by A3, A6, Def1 ;
DigA ((Mmin r),i) = (- (Radix k)) + 1 by A1, A3, A4, A6, Def5
.= SDMinDigit (m,k,i) by A1, A5, A6, RADIX_5:def_1
.= DigA ((SDMin ((m + 2),m,k)),i) by A3, RADIX_5:def_2 ;
hence  ( ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) ) by A7; ::_thesis: verum
end;
supposeA8: i >= m ; ::_thesis: ( ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) )
A9: DigA ((SDMin ((m + 2),m,k)),i) = SDMinDigit (m,k,i) by A3, RADIX_5:def_2
.= 0 by A1, A8, RADIX_5:def_1 ;
DigA ((Mmin r),i) = r . i by A1, A3, A4, A8, Def5
.= M0Digit (r,i) by A3, A8, Def1
.= DigA ((M0 r),i) by A3, Def2 ;
hence  ( ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) ) by A9; ::_thesis: verum
end;
end;
end;
hence  ( ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) ) ; ::_thesis: verum
end;
 m + 2 >= 1 by NAT_1:12;
hence  (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k))) by A1, A2, RADIX_5:15; ::_thesis: verum
end;

theorem Th12: :: RADIX_6:12
for m, k being Nat
for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 holds
(SDDec (M0 r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (Mmin r)) + (SDDec (SDMax ((m + 2),m,k)))
proof
let m, k be Nat; ::_thesis: for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 holds
(SDDec (M0 r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (Mmin r)) + (SDDec (SDMax ((m + 2),m,k)))
let r be Tuple of m + 2,k -SD ; ::_thesis: ( m >= 1 & k >= 2 implies (SDDec (M0 r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (Mmin r)) + (SDDec (SDMax ((m + 2),m,k))) )
assume that
A1: m >= 1 and
A2: k >= 2 ; ::_thesis: (SDDec (M0 r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (Mmin r)) + (SDDec (SDMax ((m + 2),m,k)))
A3: m + 2 > 1 by A1, Lm1;
(SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k))) = (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) by A2, Th11
.= (SDDec (Mmin r)) + 0 by A3, RADIX_5:6 ;
then (SDDec (Mmin r)) + (SDDec (SDMax ((m + 2),m,k))) = (SDDec (M0 r)) + ((SDDec (SDMax ((m + 2),m,k))) + (SDDec (SDMin ((m + 2),m,k))))
.= (SDDec (M0 r)) + (SDDec (DecSD (0,(m + 2),k))) by A2, A3, RADIX_5:17 ;
hence  (SDDec (M0 r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (Mmin r)) + (SDDec (SDMax ((m + 2),m,k))) ; ::_thesis: verum
end;

theorem Th13: :: RADIX_6:13
for m, k being Nat st m >= 1 & k >= 2 holds
for r being Tuple of m + 2,k -SD holds SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k)))
proof
let m, k be Nat; ::_thesis: ( m >= 1 & k >= 2 implies for r being Tuple of m + 2,k -SD holds SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k))) )
assume that
A1: m >= 1 and
A2: k >= 2 ; ::_thesis: for r being Tuple of m + 2,k -SD holds SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k)))
let r be Tuple of m + 2,k -SD ; ::_thesis: SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k)))
A3: m + 2 > 1 by A1, Lm1;
A4: (SDDec (Mmin r)) + (SDDec (SDMax ((m + 2),m,k))) = (SDDec (M0 r)) + (SDDec (DecSD (0,(m + 2),k))) by A1, A2, Th12
.= (SDDec (M0 r)) + 0 by A3, RADIX_5:6 ;
A5: (SDDec (M0 r)) + 1 > (SDDec (M0 r)) + 0 by XREAL_1:8;
 m in Seg (m + 2) by A1, FINSEQ_3:9;
then  SDDec (Fmin ((m + 2),m,k)) = (SDDec (SDMax ((m + 2),m,k))) + (SDDec (DecSD (1,(m + 2),k))) by A2, A3, RADIX_5:18
.= (SDDec (SDMax ((m + 2),m,k))) + 1 by A2, A3, RADIX_5:9 ;
hence  SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k))) by A4, A5; ::_thesis: verum
end;

theorem :: RADIX_6:14
for m, k, f being Nat
for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & f needs_digits_of m,k holds
ex s being Integer st
( - f < (SDDec (M0 r)) - (s * f) & (SDDec (Mmax r)) - (s * f) < f )
proof
let m, k, f be Nat; ::_thesis: for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & f needs_digits_of m,k holds
ex s being Integer st
( - f < (SDDec (M0 r)) - (s * f) & (SDDec (Mmax r)) - (s * f) < f )
let r be Tuple of m + 2,k -SD ; ::_thesis: ( m >= 1 & k >= 2 & f needs_digits_of m,k implies ex s being Integer st
( - f < (SDDec (M0 r)) - (s * f) & (SDDec (Mmax r)) - (s * f) < f ) )
assume that
A1: m >= 1 and
A2: k >= 2 and
A3: f needs_digits_of m,k ; ::_thesis: ex s being Integer st
( - f < (SDDec (M0 r)) - (s * f) & (SDDec (Mmax r)) - (s * f) < f )
 SDDec (Fmin ((m + 2),m,k)) <= f by A1, A2, A3, Th7;
then A4: (SDDec (M0 r)) + (SDDec (Fmin ((m + 2),m,k))) <= (SDDec (M0 r)) + f by XREAL_1:7;
 SDDec (Mmax r) < (SDDec (M0 r)) + (SDDec (Fmin ((m + 2),m,k))) by A1, A2, Th10;
then A5: SDDec (Mmax r) < (SDDec (M0 r)) + f by A4, XXREAL_0:2;
 (Radix k) |^ (m -' 1) > 0 by NEWTON:83, RADIX_2:6;
then  f > 0 by A3, Def7;
hence  ex s being Integer st
( - f < (SDDec (M0 r)) - (s * f) & (SDDec (Mmax r)) - (s * f) < f ) by A5, Th8; ::_thesis: verum
end;

theorem :: RADIX_6:15
for m, k, f being Nat
for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & f needs_digits_of m,k holds
ex s being Integer st
( - f < (SDDec (Mmin r)) - (s * f) & (SDDec (M0 r)) - (s * f) < f )
proof
let m, k, f be Nat; ::_thesis: for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & f needs_digits_of m,k holds
ex s being Integer st
( - f < (SDDec (Mmin r)) - (s * f) & (SDDec (M0 r)) - (s * f) < f )
let r be Tuple of m + 2,k -SD ; ::_thesis: ( m >= 1 & k >= 2 & f needs_digits_of m,k implies ex s being Integer st
( - f < (SDDec (Mmin r)) - (s * f) & (SDDec (M0 r)) - (s * f) < f ) )
assume that
A1: m >= 1 and
A2: k >= 2 and
A3: f needs_digits_of m,k ; ::_thesis: ex s being Integer st
( - f < (SDDec (Mmin r)) - (s * f) & (SDDec (M0 r)) - (s * f) < f )
 SDDec (Fmin ((m + 2),m,k)) <= f by A1, A2, A3, Th7;
then A4: (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k))) <= (SDDec (Mmin r)) + f by XREAL_1:7;
 SDDec (M0 r) < (SDDec (Mmin r)) + (SDDec (Fmin ((m + 2),m,k))) by A1, A2, Th13;
then A5: SDDec (M0 r) < (SDDec (Mmin r)) + f by A4, XXREAL_0:2;
 (Radix k) |^ (m -' 1) > 0 by NEWTON:83, RADIX_2:6;
then  f > 0 by A3, Def7;
hence  ex s being Integer st
( - f < (SDDec (Mmin r)) - (s * f) & (SDDec (M0 r)) - (s * f) < f ) by A5, Th8; ::_thesis: verum
end;

theorem :: RADIX_6:16
for m, k being Nat
for r being Tuple of m + 2,k -SD holds
( not k >= 2 or ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )
proof
let m, k be Nat; ::_thesis: for r being Tuple of m + 2,k -SD holds
( not k >= 2 or ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )
let r be Tuple of m + 2,k -SD ; ::_thesis: ( not k >= 2 or ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )
set MZero = SDDec (M0 r);
set R = SDDec r;
assume A1: k >= 2 ; ::_thesis: ( ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )
now__::_thesis:_(_(_SDDec_(M0_r)_<=_SDDec_r_&_SDDec_r_<=_SDDec_(Mmax_r)_)_or_(_SDDec_(Mmin_r)_<=_SDDec_r_&_SDDec_r_<_SDDec_(M0_r)_)_)
percases ( SDDec r < SDDec (M0 r) or SDDec r >= SDDec (M0 r) ) ;
suppose SDDec r < SDDec (M0 r) ; ::_thesis: ( ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )
hence  ( ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) ) by A1, Th4; ::_thesis: verum
end;
suppose SDDec r >= SDDec (M0 r) ; ::_thesis: ( ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) )
hence  ( ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) ) by A1, Th3; ::_thesis: verum
end;
end;
end;
hence  ( ( SDDec (M0 r) <= SDDec r & SDDec r <= SDDec (Mmax r) ) or ( SDDec (Mmin r) <= SDDec r & SDDec r < SDDec (M0 r) ) ) ; ::_thesis: verum
end;

begin

definition
let i, m, k be Nat;
let r be Tuple of m + 2,k -SD ;
assume A1: i in Seg (m + 2) ;
func MmaskDigit (r,i) ->  Element of k -SD  equals :Def8: :: RADIX_6:def 8
r . i if i < m
otherwise  0 ;
coherence
 ( ( i < m implies r . i is Element of k -SD ) & ( not i < m implies 0 is Element of k -SD ) )
proof
 len r = m + 2 by CARD_1:def_7;
then  i in dom r by A1, FINSEQ_1:def_3;
then  r . i in rng r by FUNCT_1:def_3;
hence  ( ( i < m implies r . i is Element of k -SD ) & ( not i < m implies 0 is Element of k -SD ) ) by RADIX_1:14; ::_thesis: verum
end;
consistency
 for b1 being Element of k -SD holds verum ;
end;

:: 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: :: RADIX_6:def 9
 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)
proof
deffunc H1( Nat) ->  Element of k -SD = MmaskDigit (r,$1);
consider z being FinSequence of k -SD  such that
A1: len z = m + 2 and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg (m + 2) by A1, FINSEQ_1:def_3;
 z is Element of (m + 2) -tuples_on (k -SD) by A1, FINSEQ_2:92;
then reconsider z = z as Tuple of m + 2,k -SD ;
take  z ; ::_thesis: for i being Nat st i in Seg (m + 2) holds
DigA (z,i) = MmaskDigit (r,i)
let i be Nat; ::_thesis: ( i in Seg (m + 2) implies DigA (z,i) = MmaskDigit (r,i) )
assume A4: i in Seg (m + 2) ; ::_thesis: DigA (z,i) = MmaskDigit (r,i)
hence  DigA (z,i) = z . i by RADIX_1:def_3
.= MmaskDigit (r,i) by A2, A3, A4 ;
::_thesis: verum
end;
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
proof
let k1, k2 be Tuple of m + 2,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg (m + 2) holds
DigA (k1,i) = MmaskDigit (r,i) ) & ( for i being Nat st i in Seg (m + 2) holds
DigA (k2,i) = MmaskDigit (r,i) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg (m + 2) holds
DigA (k1,i) = MmaskDigit (r,i) and
A6: for i being Nat st i in Seg (m + 2) holds
DigA (k2,i) = MmaskDigit (r,i) ; ::_thesis: k1 = k2
A7: len k1 = m + 2 by CARD_1:def_7;
then A8: dom k1 = Seg (m + 2) by FINSEQ_1:def_3;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then k1 . j = DigA (k1,j) by A8, RADIX_1:def_3
.= MmaskDigit (r,j) by A5, A8, A10
.= DigA (k2,j) by A6, A8, A10
.= k2 . j by A8, A10, RADIX_1:def_3 ;
hence  k1 . j = k2 . j ; ::_thesis: verum
end;
 len k2 = m + 2 by CARD_1:def_7;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
end;
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: :: RADIX_6:17
for m, k being Nat
for r being Tuple of m + 2,k -SD st k >= 2 holds
(SDDec (M0 r)) + (SDDec (Mmask r)) = (SDDec r) + (SDDec (DecSD (0,(m + 2),k)))
proof
let m, k be Nat; ::_thesis: for r being Tuple of m + 2,k -SD st k >= 2 holds
(SDDec (M0 r)) + (SDDec (Mmask r)) = (SDDec r) + (SDDec (DecSD (0,(m + 2),k)))
let r be Tuple of m + 2,k -SD ; ::_thesis: ( k >= 2 implies (SDDec (M0 r)) + (SDDec (Mmask r)) = (SDDec r) + (SDDec (DecSD (0,(m + 2),k))) )
A1: m + 2 >= 1 by NAT_1:12;
A2: for i being Nat holds
( not i in Seg (m + 2) or ( DigA ((M0 r),i) = DigA (r,i) & DigA ((Mmask r),i) = 0 ) or ( DigA ((Mmask r),i) = DigA (r,i) & DigA ((M0 r),i) = 0 ) )
proof
let i be Nat; ::_thesis: ( not i in Seg (m + 2) or ( DigA ((M0 r),i) = DigA (r,i) & DigA ((Mmask r),i) = 0 ) or ( DigA ((Mmask r),i) = DigA (r,i) & DigA ((M0 r),i) = 0 ) )
assume A3: i in Seg (m + 2) ; ::_thesis: ( ( DigA ((M0 r),i) = DigA (r,i) & DigA ((Mmask r),i) = 0 ) or ( DigA ((Mmask r),i) = DigA (r,i) & DigA ((M0 r),i) = 0 ) )
now__::_thesis:_(_(_DigA_((M0_r),i)_=_DigA_(r,i)_&_DigA_((Mmask_r),i)_=_0_)_or_(_DigA_((Mmask_r),i)_=_DigA_(r,i)_&_DigA_((M0_r),i)_=_0_)_)
percases ( i < m or i >= m ) ;
supposeA4: i < m ; ::_thesis: ( ( DigA ((M0 r),i) = DigA (r,i) & DigA ((Mmask r),i) = 0 ) or ( DigA ((Mmask r),i) = DigA (r,i) & DigA ((M0 r),i) = 0 ) )
A5: DigA ((M0 r),i) = M0Digit (r,i) by A3, Def2
.= 0 by A3, A4, Def1 ;
DigA ((Mmask r),i) = MmaskDigit (r,i) by A3, Def9
.= r . i by A3, A4, Def8
.= DigA (r,i) by A3, RADIX_1:def_3 ;
hence  ( ( DigA ((M0 r),i) = DigA (r,i) & DigA ((Mmask r),i) = 0 ) or ( DigA ((Mmask r),i) = DigA (r,i) & DigA ((M0 r),i) = 0 ) ) by A5; ::_thesis: verum
end;
supposeA6: i >= m ; ::_thesis: ( ( DigA ((M0 r),i) = DigA (r,i) & DigA ((Mmask r),i) = 0 ) or ( DigA ((Mmask r),i) = DigA (r,i) & DigA ((M0 r),i) = 0 ) )
A7: DigA ((Mmask r),i) = MmaskDigit (r,i) by A3, Def9
.= 0 by A3, A6, Def8 ;
DigA ((M0 r),i) = M0Digit (r,i) by A3, Def2
.= r . i by A3, A6, Def1
.= DigA (r,i) by A3, RADIX_1:def_3 ;
hence  ( ( DigA ((M0 r),i) = DigA (r,i) & DigA ((Mmask r),i) = 0 ) or ( DigA ((Mmask r),i) = DigA (r,i) & DigA ((M0 r),i) = 0 ) ) by A7; ::_thesis: verum
end;
end;
end;
hence  ( ( DigA ((M0 r),i) = DigA (r,i) & DigA ((Mmask r),i) = 0 ) or ( DigA ((Mmask r),i) = DigA (r,i) & DigA ((M0 r),i) = 0 ) ) ; ::_thesis: verum
end;
assume  k >= 2 ; ::_thesis: (SDDec (M0 r)) + (SDDec (Mmask r)) = (SDDec r) + (SDDec (DecSD (0,(m + 2),k)))
hence  (SDDec (M0 r)) + (SDDec (Mmask r)) = (SDDec r) + (SDDec (DecSD (0,(m + 2),k))) by A1, A2, RADIX_5:15; ::_thesis: verum
end;

theorem :: RADIX_6:18
for m, k being Nat
for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & SDDec (Mmask r) > 0 holds
SDDec r > SDDec (M0 r)
proof
let m, k be Nat; ::_thesis: for r being Tuple of m + 2,k -SD st m >= 1 & k >= 2 & SDDec (Mmask r) > 0 holds
SDDec r > SDDec (M0 r)
let r be Tuple of m + 2,k -SD ; ::_thesis: ( m >= 1 & k >= 2 & SDDec (Mmask r) > 0 implies SDDec r > SDDec (M0 r) )
assume that
A1: m >= 1 and
A2: k >= 2 ; ::_thesis: ( not SDDec (Mmask r) > 0 or SDDec r > SDDec (M0 r) )
A3: m + 2 > 1 by A1, Lm1;
(SDDec (M0 r)) + (SDDec (Mmask r)) = (SDDec r) + (SDDec (DecSD (0,(m + 2),k))) by A2, Th17
.= (SDDec r) + 0 by A3, RADIX_5:6 ;
then A4: (SDDec r) - (SDDec (M0 r)) = (SDDec (Mmask r)) - 0 ;
assume  SDDec (Mmask r) > 0 ; ::_thesis: SDDec r > SDDec (M0 r)
hence  SDDec r > SDDec (M0 r) by A4, XREAL_1:47; ::_thesis: verum
end;

definition
let i, m, k be Nat;
assume A1: k >= 2 ;
func FSDMinDigit (m,k,i) ->  Element of k -SD  equals :Def10: :: RADIX_6:def 10
 0  if i > m
1 if i = m
otherwise (- (Radix k)) + 1;
coherence
 ( ( i > m implies 0 is Element of k -SD ) & ( i = m implies 1 is Element of k -SD ) & ( not i > m & not i = m implies (- (Radix k)) + 1 is Element of k -SD ) )
proof
 Radix k > 2 by A1, RADIX_4:1;
then  Radix k > 1 by XXREAL_0:2;
then  (Radix k) + (Radix k) > 1 + 1 by XREAL_1:8;
then A2: (Radix k) - 1 > 1 - (Radix k) by XREAL_1:21;
A3: k -SD =  {  w where w is Element of INT : ( w <= (Radix k) - 1 & w >= (- (Radix k)) + 1 )  }  by RADIX_1:def_2;
A4: Radix k > 2 by A1, RADIX_4:1;
then  - (Radix k) < - 2 by XREAL_1:24;
then A5: (- (Radix k)) + 1 < (- 2) + 1 by XREAL_1:6;
 (- (Radix k)) + 1 is Element of INT by INT_1:def_2;
then A6: (- (Radix k)) + 1 in k -SD by A3, A2;
A7: 1 is Element of INT by INT_1:def_2;
 (Radix k) + (- 1) > 2 + (- 1) by A4, XREAL_1:6;
then  1 in k -SD by A3, A5, A7;
hence  ( ( i > m implies 0 is Element of k -SD ) & ( i = m implies 1 is Element of k -SD ) & ( not i > m & not i = m implies (- (Radix k)) + 1 is Element of k -SD ) ) by A6, RADIX_1:14; ::_thesis: verum
end;
consistency
 for b1 being Element of k -SD st i > m & i = m holds
( b1 = 0 iff b1 = 1 ) ;
end;

:: 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: :: RADIX_6:def 11
 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)
proof
deffunc H1( Nat) ->  Element of k -SD = FSDMinDigit (m,k,$1);
consider z being FinSequence of k -SD  such that
A1: len z = n and
A2: for j being Nat st j in dom z holds
z . j = H1(j) from FINSEQ_2:sch_1();
A3: dom z = Seg n by A1, FINSEQ_1:def_3;
 z is Element of n -tuples_on (k -SD) by A1, FINSEQ_2:92;
then reconsider z = z as Tuple of n,k -SD ;
take  z ; ::_thesis: for i being Nat st i in Seg n holds
DigA (z,i) = FSDMinDigit (m,k,i)
let i be Nat; ::_thesis: ( i in Seg n implies DigA (z,i) = FSDMinDigit (m,k,i) )
assume A4: i in Seg n ; ::_thesis: DigA (z,i) = FSDMinDigit (m,k,i)
then  DigA (z,i) = z . i by RADIX_1:def_3;
hence  DigA (z,i) = FSDMinDigit (m,k,i) by A2, A3, A4; ::_thesis: verum
end;
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
proof
let k1, k2 be Tuple of n,k -SD ; ::_thesis: ( ( for i being Nat st i in Seg n holds
DigA (k1,i) = FSDMinDigit (m,k,i) ) & ( for i being Nat st i in Seg n holds
DigA (k2,i) = FSDMinDigit (m,k,i) ) implies k1 = k2 )
assume that
A5: for i being Nat st i in Seg n holds
DigA (k1,i) = FSDMinDigit (m,k,i) and
A6: for i being Nat st i in Seg n holds
DigA (k2,i) = FSDMinDigit (m,k,i) ; ::_thesis: k1 = k2
A7: len k1 = n by CARD_1:def_7;
then A8: dom k1 = Seg n by FINSEQ_1:def_3;
A9: now__::_thesis:_for_j_being_Nat_st_j_in_dom_k1_holds_
k1_._j_=_k2_._j
let j be Nat; ::_thesis: ( j in dom k1 implies k1 . j = k2 . j )
assume A10: j in dom k1 ; ::_thesis: k1 . j = k2 . j
then k1 . j = DigA (k1,j) by A8, RADIX_1:def_3
.= FSDMinDigit (m,k,j) by A5, A8, A10
.= DigA (k2,j) by A6, A8, A10
.= k2 . j by A8, A10, RADIX_1:def_3 ;
hence  k1 . j = k2 . j ; ::_thesis: verum
end;
 len k2 = n by CARD_1:def_7;
hence  k1 = k2 by A7, A9, FINSEQ_2:9; ::_thesis: verum
end;
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: :: RADIX_6:19
for n being Nat st n >= 1 holds
for m, k being Nat st m in Seg n & k >= 2 holds
SDDec (FSDMin (n,m,k)) = 1
proof
let n be Nat; ::_thesis: ( n >= 1 implies for m, k being Nat st m in Seg n & k >= 2 holds
SDDec (FSDMin (n,m,k)) = 1 )
assume A1: n >= 1 ; ::_thesis: for m, k being Nat st m in Seg n & k >= 2 holds
SDDec (FSDMin (n,m,k)) = 1
let m, k be Nat; ::_thesis: ( m in Seg n & k >= 2 implies SDDec (FSDMin (n,m,k)) = 1 )
assume that
A2: m in Seg n and
A3: k >= 2 ; ::_thesis: SDDec (FSDMin (n,m,k)) = 1
 for i being Nat holds
( not i in Seg n or ( DigA ((FSDMin (n,m,k)),i) = DigA ((Fmin (n,m,k)),i) & DigA ((SDMin (n,m,k)),i) = 0 ) or ( DigA ((FSDMin (n,m,k)),i) = DigA ((SDMin (n,m,k)),i) & DigA ((Fmin (n,m,k)),i) = 0 ) )
proof
let i be Nat; ::_thesis: ( not i in Seg n or ( DigA ((FSDMin (n,m,k)),i) = DigA ((Fmin (n,m,k)),i) & DigA ((SDMin (n,m,k)),i) = 0 ) or ( DigA ((FSDMin (n,m,k)),i) = DigA ((SDMin (n,m,k)),i) & DigA ((Fmin (n,m,k)),i) = 0 ) )
assume A4: i in Seg n ; ::_thesis: ( ( DigA ((FSDMin (n,m,k)),i) = DigA ((Fmin (n,m,k)),i) & DigA ((SDMin (n,m,k)),i) = 0 ) or ( DigA ((FSDMin (n,m,k)),i) = DigA ((SDMin (n,m,k)),i) & DigA ((Fmin (n,m,k)),i) = 0 ) )
then A5: i >= 1 by FINSEQ_1:1;
now__::_thesis:_(_(_DigA_((FSDMin_(n,m,k)),i)_=_DigA_((Fmin_(n,m,k)),i)_&_DigA_((SDMin_(n,m,k)),i)_=_0_)_or_(_DigA_((FSDMin_(n,m,k)),i)_=_DigA_((SDMin_(n,m,k)),i)_&_DigA_((Fmin_(n,m,k)),i)_=_0_)_)
percases ( i > m or i <= m ) ;
supposeA6: i > m ; ::_thesis: ( ( DigA ((FSDMin (n,m,k)),i) = DigA ((Fmin (n,m,k)),i) & DigA ((SDMin (n,m,k)),i) = 0 ) or ( DigA ((FSDMin (n,m,k)),i) = DigA ((SDMin (n,m,k)),i) & DigA ((Fmin (n,m,k)),i) = 0 ) )
A7: DigA ((Fmin (n,m,k)),i) = FminDigit (m,k,i) by A4, RADIX_5:def_6
.= 0 by A3, A6, RADIX_5:def_5 ;
A8: DigA ((SDMin (n,m,k)),i) = SDMinDigit (m,k,i) by A4, RADIX_5:def_2
.= 0 by A3, A6, RADIX_5:def_1 ;
DigA ((FSDMin (n,m,k)),i) = FSDMinDigit (m,k,i) by A4, Def11
.= 0 by A3, A6, Def10 ;
hence  ( ( DigA ((FSDMin (n,m,k)),i) = DigA ((Fmin (n,m,k)),i) & DigA ((SDMin (n,m,k)),i) = 0 ) or ( DigA ((FSDMin (n,m,k)),i) = DigA ((SDMin (n,m,k)),i) & DigA ((Fmin (n,m,k)),i) = 0 ) ) by A8, A7; ::_thesis: verum
end;
supposeA9: i <= m ; ::_thesis: ( ( DigA ((FSDMin (n,m,k)),i) = DigA ((Fmin (n,m,k)),i) & DigA ((SDMin (n,m,k)),i) = 0 ) or ( DigA ((FSDMin (n,m,k)),i) = DigA ((SDMin (n,m,k)),i) & DigA ((Fmin (n,m,k)),i) = 0 ) )
now__::_thesis:_(_(_DigA_((FSDMin_(n,m,k)),i)_=_DigA_((Fmin_(n,m,k)),i)_&_DigA_((SDMin_(n,m,k)),i)_=_0_)_or_(_DigA_((FSDMin_(n,m,k)),i)_=_DigA_((SDMin_(n,m,k)),i)_&_DigA_((Fmin_(n,m,k)),i)_=_0_)_)
percases ( i = m or i < m ) by A9, XXREAL_0:1;
supposeA10: i = m ; ::_thesis: ( ( DigA ((FSDMin (n,m,k)),i) = DigA ((Fmin (n,m,k)),i) & DigA ((SDMin (n,m,k)),i) = 0 ) or ( DigA ((FSDMin (n,m,k)),i) = DigA ((SDMin (n,m,k)),i) & DigA ((Fmin (n,m,k)),i) = 0 ) )
A11: DigA ((Fmin (n,m,k)),i) = FminDigit (m,k,i) by A4, RADIX_5:def_6
.= 1 by A3, A10, RADIX_5:def_5 ;
A12: DigA ((SDMin (n,m,k)),i) = SDMinDigit (m,k,i) by A4, RADIX_5:def_2
.= 0 by A3, A10, RADIX_5:def_1 ;
DigA ((FSDMin (n,m,k)),i) = FSDMinDigit (m,k,i) by A4, Def11
.= 1 by A3, A10, Def10 ;
hence  ( ( DigA ((FSDMin (n,m,k)),i) = DigA ((Fmin (n,m,k)),i) & DigA ((SDMin (n,m,k)),i) = 0 ) or ( DigA ((FSDMin (n,m,k)),i) = DigA ((SDMin (n,m,k)),i) & DigA ((Fmin (n,m,k)),i) = 0 ) ) by A12, A11; ::_thesis: verum
end;
supposeA13: i < m ; ::_thesis: ( ( DigA ((FSDMin (n,m,k)),i) = DigA ((Fmin (n,m,k)),i) & DigA ((SDMin (n,m,k)),i) = 0 ) or ( DigA ((FSDMin (n,m,k)),i) = DigA ((SDMin (n,m,k)),i) & DigA ((Fmin (n,m,k)),i) = 0 ) )
A14: DigA ((Fmin (n,m,k)),i) = FminDigit (m,k,i) by A4, RADIX_5:def_6
.= 0 by A3, A13, RADIX_5:def_5 ;
A15: DigA ((SDMin (n,m,k)),i) = SDMinDigit (m,k,i) by A4, RADIX_5:def_2
.= (- (Radix k)) + 1 by A3, A5, A13, RADIX_5:def_1 ;
DigA ((FSDMin (n,m,k)),i) = FSDMinDigit (m,k,i) by A4, Def11
.= (- (Radix k)) + 1 by A3, A13, Def10 ;
hence  ( ( DigA ((FSDMin (n,m,k)),i) = DigA ((Fmin (n,m,k)),i) & DigA ((SDMin (n,m,k)),i) = 0 ) or ( DigA ((FSDMin (n,m,k)),i) = DigA ((SDMin (n,m,k)),i) & DigA ((Fmin (n,m,k)),i) = 0 ) ) by A15, A14; ::_thesis: verum
end;
end;
end;
hence  ( ( DigA ((FSDMin (n,m,k)),i) = DigA ((Fmin (n,m,k)),i) & DigA ((SDMin (n,m,k)),i) = 0 ) or ( DigA ((FSDMin (n,m,k)),i) = DigA ((SDMin (n,m,k)),i) & DigA ((Fmin (n,m,k)),i) = 0 ) ) ; ::_thesis: verum
end;
end;
end;
hence  ( ( DigA ((FSDMin (n,m,k)),i) = DigA ((Fmin (n,m,k)),i) & DigA ((SDMin (n,m,k)),i) = 0 ) or ( DigA ((FSDMin (n,m,k)),i) = DigA ((SDMin (n,m,k)),i) & DigA ((Fmin (n,m,k)),i) = 0 ) ) ; ::_thesis: verum
end;
then  (SDDec (FSDMin (n,m,k))) + (SDDec (DecSD (0,n,k))) = (SDDec (Fmin (n,m,k))) + (SDDec (SDMin (n,m,k))) by A1, A3, RADIX_5:15;
then (SDDec (FSDMin (n,m,k))) + 0 = (SDDec (Fmin (n,m,k))) + (SDDec (SDMin (n,m,k))) by A1, RADIX_5:6
.= ((SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k)))) + (SDDec (SDMin (n,m,k))) by A1, A2, A3, RADIX_5:18
.= ((SDDec (SDMax (n,m,k))) + (SDDec (SDMin (n,m,k)))) + (SDDec (DecSD (1,n,k)))
.= (SDDec (DecSD (0,n,k))) + (SDDec (DecSD (1,n,k))) by A1, A3, RADIX_5:17
.= 0 + (SDDec (DecSD (1,n,k))) by A1, RADIX_5:6 ;
hence  SDDec (FSDMin (n,m,k)) = 1 by A1, A3, RADIX_5:9; ::_thesis: verum
end;

definition
let n, m, k be Nat;
let r be Tuple of m + 2,k -SD ;
predr is_Zero_over n means :Def12: :: RADIX_6:def 12
 for i being Nat st i > n holds
DigA (r,i) = 0 ;
end;

:: 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 :: RADIX_6:20
for m being Nat st m >= 1 holds
for n, k being Nat
for r being Tuple of m + 2,k -SD st k >= 2 & n in Seg (m + 2) & Mmask r is_Zero_over n & DigA ((Mmask r),n) > 0 holds
SDDec (Mmask r) > 0
proof
let m be Nat; ::_thesis: ( m >= 1 implies for n, k being Nat
for r being Tuple of m + 2,k -SD st k >= 2 & n in Seg (m + 2) & Mmask r is_Zero_over n & DigA ((Mmask r),n) > 0 holds
SDDec (Mmask r) > 0 )
assume  m >= 1 ; ::_thesis: for n, k being Nat
for r being Tuple of m + 2,k -SD st k >= 2 & n in Seg (m + 2) & Mmask r is_Zero_over n & DigA ((Mmask r),n) > 0 holds
SDDec (Mmask r) > 0
then A1: m + 2 >= 1 by Lm1;
let n, k be Nat; ::_thesis: for r being Tuple of m + 2,k -SD st k >= 2 & n in Seg (m + 2) & Mmask r is_Zero_over n & DigA ((Mmask r),n) > 0 holds
SDDec (Mmask r) > 0
let r be Tuple of m + 2,k -SD ; ::_thesis: ( k >= 2 & n in Seg (m + 2) & Mmask r is_Zero_over n & DigA ((Mmask r),n) > 0 implies SDDec (Mmask r) > 0 )
assume that
A2: k >= 2 and
A3: n in Seg (m + 2) and
A4: Mmask r is_Zero_over n and
A5: DigA ((Mmask r),n) > 0 ; ::_thesis: SDDec (Mmask r) > 0
 for i being Nat st i in Seg (m + 2) holds
DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i)
proof
let i be Nat; ::_thesis: ( i in Seg (m + 2) implies DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i) )
assume A6: i in Seg (m + 2) ; ::_thesis: DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i)
now__::_thesis:_DigA_((Mmask_r),i)_>=_DigA_((FSDMin_((m_+_2),n,k)),i)
percases ( i > n or i <= n ) ;
supposeA7: i > n ; ::_thesis: DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i)
DigA ((FSDMin ((m + 2),n,k)),i) = FSDMinDigit (n,k,i) by A6, Def11
.= 0 by A2, A7, Def10 ;
hence  DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i) by A4, A7, Def12; ::_thesis: verum
end;
supposeA8: i <= n ; ::_thesis: DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i)
now__::_thesis:_DigA_((Mmask_r),i)_>=_DigA_((FSDMin_((m_+_2),n,k)),i)
percases ( i = n or i < n ) by A8, XXREAL_0:1;
supposeA9: i = n ; ::_thesis: DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i)
then A10: DigA ((Mmask r),i) >= 0 + 1 by A5, INT_1:7;
DigA ((FSDMin ((m + 2),n,k)),i) = FSDMinDigit (n,k,i) by A6, Def11
.= 1 by A2, A9, Def10 ;
hence  DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i) by A10; ::_thesis: verum
end;
supposeA11: i < n ; ::_thesis: DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i)
A12: DigA ((Mmask r),i) = (Mmask r) . i by A6, RADIX_1:def_3;
A13: (Mmask r) . i is Element of k -SD by A6, RADIX_1:15;
DigA ((FSDMin ((m + 2),n,k)),i) = FSDMinDigit (n,k,i) by A6, Def11
.= (- (Radix k)) + 1 by A2, A11, Def10 ;
hence  DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i) by A12, A13, RADIX_1:13; ::_thesis: verum
end;
end;
end;
hence  DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i) ; ::_thesis: verum
end;
end;
end;
hence  DigA ((Mmask r),i) >= DigA ((FSDMin ((m + 2),n,k)),i) ; ::_thesis: verum
end;
then  SDDec (Mmask r) >= SDDec (FSDMin ((m + 2),n,k)) by A1, RADIX_5:13;
hence  SDDec (Mmask r) > 0 by A2, A3, A1, Th19; ::_thesis: verum
end;