radix_6.miz



    begin

    

     Lm1: for m be Nat st m >= 1 holds (m + 2) > 1

    proof

      let m be Nat;

      (m + 2) > m by XREAL_1: 29;

      hence thesis by XXREAL_0: 2;

    end;

    theorem :: RADIX_6:1

    

     Th1: for n be Nat st n >= 1 holds for m,k be Nat st m >= 1 & k >= 2 holds ( SDDec ( Fmin ((m + n),m,k))) = ( SDDec ( Fmin (m,m,k)))

    proof

      defpred P[ Nat] means for m,k be Nat st m >= 1 & k >= 2 holds ( SDDec ( Fmin ((m + $1),m,k))) = ( SDDec ( Fmin (m,m,k)));

      

       A1: for n be Nat st n >= 1 & P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume that n >= 1 and

         A2: P[n];

        let m,k be Nat;

        assume that

         A3: m >= 1 and

         A4: k >= 2;

        (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 be 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;

          assume

           A7: i in ( Seg (m + n));

          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 thesis by A7, RADIX_1:def 3;

        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 thesis;

      end;

      

       A9: P[1]

      proof

        let m,k be Nat;

        assume that m >= 1 and

         A10: k >= 2;

        

         A11: (m + 1) > m by NAT_1: 13;

        for i be Nat st i in ( Seg m) holds (( Fmin ((m + 1),m,k)) . i) = (( Fmin (m,m,k)) . i)

        proof

          let i be Nat;

          assume

           A12: i in ( Seg m);

          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 thesis by A12, RADIX_1:def 3;

        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 thesis by A14;

      end;

      for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8( A9, A1);

      hence thesis;

    end;

    theorem :: RADIX_6:2

    for m,k be Nat st m >= 1 & k >= 2 holds ( SDDec ( Fmin (m,m,k))) > 0

    proof

      defpred P[ Nat] means for k be Nat st k >= 2 holds ( SDDec ( Fmin ($1,$1,k))) > 0 ;

      

       A1: for m be Nat st m >= 1 & P[m] holds P[(m + 1)]

      proof

        let m be Nat;

        assume that

         A2: m >= 1 and P[m];

        let k be Nat;

        assume

         A3: k >= 2;

        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 be Nat st i in ( Seg m) holds (( Fmin ((m + 1),(m + 1),k)) . i) = (( DecSD ( 0 ,m,k)) . i)

        proof

          let i be Nat;

          assume

           A6: i in ( Seg m);

          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 thesis by A6, RADIX_1:def 3;

        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 thesis by A4, PREPOWER: 11;

      end;

      

       A9: P[1]

      proof

        let k be Nat;

        assume

         A10: k >= 2;

        

         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 thesis;

      end;

      for m be Nat st m >= 1 holds P[m] from NAT_1:sch 8( A9, A1);

      hence thesis;

    end;

    begin

    definition

      let i,m,k be Nat, r be Tuple of (m + 2), (k -SD );

      assume

       A1: i in ( Seg (m + 2));

      :: RADIX_6:def1

      func M0Digit (r,i) -> Element of (k -SD ) equals

      : Def1: (r . i) if i >= m

      otherwise 0 ;

      coherence

      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 thesis by RADIX_1: 14;

      end;

      consistency ;

    end

    definition

      let m,k be Nat, r be Tuple of (m + 2), (k -SD );

      :: RADIX_6:def2

      func M0 (r) -> Tuple of (m + 2), (k -SD ) means

      : Def2: for i be Nat st i in ( Seg (m + 2)) holds ( DigA (it ,i)) = ( M0Digit (r,i));

      existence

      proof

        deffunc F1( Nat) = ( M0Digit (r,$1));

        consider z be FinSequence of (k -SD ) such that

         A1: ( len z) = (m + 2) and

         A2: for j be Nat st j in ( dom z) holds (z . j) = F1(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 as Tuple of (m + 2), (k -SD );

        take z;

        let i be Nat;

        assume

         A4: i in ( Seg (m + 2));

        

        hence ( DigA (z,i)) = (z . i) by RADIX_1:def 3

        .= ( M0Digit (r,i)) by A2, A3, A4;

      end;

      uniqueness

      proof

        let k1,k2 be Tuple of (m + 2), (k -SD ) such that

         A5: for i be Nat st i in ( Seg (m + 2)) holds ( DigA (k1,i)) = ( M0Digit (r,i)) and

         A6: for i be Nat st i in ( Seg (m + 2)) holds ( DigA (k2,i)) = ( M0Digit (r,i));

        

         A7: ( len k1) = (m + 2) by CARD_1:def 7;

        then

         A8: ( dom k1) = ( Seg (m + 2)) by FINSEQ_1:def 3;

         A9:

        now

          let j be Nat;

          assume

           A10: j in ( dom k1);

          

          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);

        end;

        ( len k2) = (m + 2) by CARD_1:def 7;

        hence k1 = k2 by A7, A9, FINSEQ_2: 9;

      end;

    end

    definition

      let i,m,k be Nat, r be Tuple of (m + 2), (k -SD );

      assume that

       A1: k >= 2 and

       A2: i in ( Seg (m + 2));

      :: RADIX_6:def3

      func MmaxDigit (r,i) -> Element of (k -SD ) equals

      : Def3: (r . i) if i >= m

      otherwise (( Radix k) - 1);

      coherence

      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 thesis by A1, RADIX_5: 1;

      end;

      consistency ;

    end

    definition

      let m,k be Nat, r be Tuple of (m + 2), (k -SD );

      :: RADIX_6:def4

      func Mmax (r) -> Tuple of (m + 2), (k -SD ) means

      : Def4: for i be Nat st i in ( Seg (m + 2)) holds ( DigA (it ,i)) = ( MmaxDigit (r,i));

      existence

      proof

        deffunc F( Nat) = ( MmaxDigit (r,$1));

        consider z be FinSequence of (k -SD ) such that

         A1: ( len z) = (m + 2) and

         A2: for j be Nat st j in ( dom z) holds (z . j) = F(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 as Tuple of (m + 2), (k -SD );

        take z;

        let i be Nat;

        assume

         A4: i in ( Seg (m + 2));

        

        hence ( DigA (z,i)) = (z . i) by RADIX_1:def 3

        .= ( MmaxDigit (r,i)) by A2, A3, A4;

      end;

      uniqueness

      proof

        let k1,k2 be Tuple of (m + 2), (k -SD ) such that

         A5: for i be Nat st i in ( Seg (m + 2)) holds ( DigA (k1,i)) = ( MmaxDigit (r,i)) and

         A6: for i be Nat st i in ( Seg (m + 2)) holds ( DigA (k2,i)) = ( MmaxDigit (r,i));

        

         A7: ( len k1) = (m + 2) by CARD_1:def 7;

        then

         A8: ( dom k1) = ( Seg (m + 2)) by FINSEQ_1:def 3;

         A9:

        now

          let j be Nat;

          assume

           A10: j in ( dom k1);

          

          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);

        end;

        ( len k2) = (m + 2) by CARD_1:def 7;

        hence k1 = k2 by A7, A9, FINSEQ_2: 9;

      end;

    end

    definition

      let i,m,k be Nat, r be Tuple of (m + 2), (k -SD );

      assume that

       A1: k >= 2 and

       A2: i in ( Seg (m + 2));

      :: RADIX_6:def5

      func MminDigit (r,i) -> Element of (k -SD ) equals

      : Def5: (r . i) if i >= m

      otherwise (( - ( Radix k)) + 1);

      coherence

      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 be 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 thesis by A3;

      end;

      consistency ;

    end

    definition

      let m,k be Nat, r be Tuple of (m + 2), (k -SD );

      :: RADIX_6:def6

      func Mmin (r) -> Tuple of (m + 2), (k -SD ) means

      : Def6: for i be Nat st i in ( Seg (m + 2)) holds ( DigA (it ,i)) = ( MminDigit (r,i));

      existence

      proof

        deffunc F( Nat) = ( MminDigit (r,$1));

        consider z be FinSequence of (k -SD ) such that

         A1: ( len z) = (m + 2) and

         A2: for j be Nat st j in ( dom z) holds (z . j) = F(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 as Tuple of (m + 2), (k -SD );

        take z;

        let i be Nat;

        assume

         A4: i in ( Seg (m + 2));

        

        hence ( DigA (z,i)) = (z . i) by RADIX_1:def 3

        .= F(i) by A2, A3, A4;

      end;

      uniqueness

      proof

        let k1,k2 be Tuple of (m + 2), (k -SD ) such that

         A5: for i be Nat st i in ( Seg (m + 2)) holds ( DigA (k1,i)) = ( MminDigit (r,i)) and

         A6: for i be Nat st i in ( Seg (m + 2)) holds ( DigA (k2,i)) = ( MminDigit (r,i));

        

         A7: ( len k1) = (m + 2) by CARD_1:def 7;

        then

         A8: ( dom k1) = ( Seg (m + 2)) by FINSEQ_1:def 3;

         A9:

        now

          let j be Nat;

          assume

           A10: j in ( dom k1);

          

          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);

        end;

        ( len k2) = (m + 2) by CARD_1:def 7;

        hence k1 = k2 by A7, A9, FINSEQ_2: 9;

      end;

    end

    theorem :: RADIX_6:3

    

     Th3: for m,k be Nat st k >= 2 holds for r be Tuple of (m + 2), (k -SD ) holds ( SDDec ( Mmax r)) >= ( SDDec r)

    proof

      let m,k be Nat;

      assume that

       A1: k >= 2;

      let r be Tuple of (m + 2), (k -SD );

      for i be Nat st i in ( Seg (m + 2)) holds ( DigA (( Mmax r),i)) >= ( DigA (r,i))

      proof

        let i be Nat;

        assume

         A2: i in ( Seg (m + 2));

        then

         A3: ( DigA (( Mmax r),i)) = ( MmaxDigit (r,i)) by Def4;

        now

          per cases ;

            suppose i >= m;

            

            then ( DigA (( Mmax r),i)) = (r . i) by A1, A2, A3, Def3

            .= ( DigA (r,i)) by A2, RADIX_1:def 3;

            hence thesis;

          end;

            suppose

             A4: i < m;

            

             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 thesis by A5, A6, RADIX_1: 13;

          end;

        end;

        hence thesis;

      end;

      hence thesis by NAT_1: 12, RADIX_5: 13;

    end;

    theorem :: RADIX_6:4

    

     Th4: for m,k be Nat st k >= 2 holds for r be Tuple of (m + 2), (k -SD ) holds ( SDDec r) >= ( SDDec ( Mmin r))

    proof

      let m,k be Nat;

      assume that

       A1: k >= 2;

      let r be Tuple of (m + 2), (k -SD );

      for i be Nat st i in ( Seg (m + 2)) holds ( DigA (r,i)) >= ( DigA (( Mmin r),i))

      proof

        let i be Nat;

        assume

         A2: i in ( Seg (m + 2));

        then

         A3: ( DigA (( Mmin r),i)) = ( MminDigit (r,i)) by Def6;

        now

          per cases ;

            suppose i >= m;

            

            then ( DigA (( Mmin r),i)) = (r . i) by A1, A2, A3, Def5

            .= ( DigA (r,i)) by A2, RADIX_1:def 3;

            hence thesis;

          end;

            suppose

             A4: i < m;

            

             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 thesis by A5, A6, RADIX_1: 13;

          end;

        end;

        hence thesis;

      end;

      hence thesis by NAT_1: 12, RADIX_5: 13;

    end;

    begin

    definition

      let n,k be Nat, x be Integer;

      :: RADIX_6:def7

      pred x needs_digits_of n,k means x < (( Radix k) |^ n) & x >= (( Radix k) |^ (n -' 1));

    end

    theorem :: RADIX_6:5

    

     Th5: for x,n,k,i be Nat st i in ( Seg n) holds ( DigA (( DecSD (x,n,k)),i)) >= 0

    proof

      let x,n,k,i be Nat;

      assume

       A1: i in ( Seg n);

      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 thesis;

    end;

    theorem :: RADIX_6:6

    

     Th6: for n,k,x be 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;

      assume that

       A1: n >= 1 and

       A2: x needs_digits_of (n,k);

      x < (( Radix k) |^ n) by A2;

      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;

      hence thesis by A4, A5, NAT_2: 13;

    end;

    theorem :: RADIX_6:7

    

     Th7: for f,m,k be 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;

      assume that

       A1: m >= 1 and

       A2: k >= 2 and

       A3: f needs_digits_of (m,k);

      for i be Nat st i in ( Seg m) holds ( DigA (( DecSD (f,m,k)),i)) >= ( DigA (( Fmin (m,m,k)),i))

      proof

        let i be Nat;

        assume

         A4: i in ( Seg m);

        then

         A5: i <= m by FINSEQ_1: 1;

        now

          per cases by A5, XXREAL_0: 1;

            suppose

             A6: i = m;

            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 thesis by A7;

          end;

            suppose

             A8: i < m;

            ( 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 thesis by A4, Th5;

          end;

        end;

        hence thesis;

      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;

      then f is_represented_by (m,k) by RADIX_1:def 12;

      hence thesis by A1, A9, RADIX_1: 22;

    end;

    begin

    theorem :: RADIX_6:8

    

     Th8: for mlow,mhigh,f be Integer st mhigh < (mlow + f) & f > 0 holds ex s be Integer st ( - f) < (mlow - (s * f)) & (mhigh - (s * f)) < f

    proof

      let mlow,mhigh,f be Integer;

      assume that

       A1: mhigh < (mlow + f) and

       A2: f > 0 ;

      reconsider 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 thesis by A2, A4, NAT_D: 62;

    end;

    theorem :: RADIX_6:9

    

     Th9: for m,k be Nat st k >= 2 holds for r be 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;

      assume that

       A1: k >= 2;

      let r be Tuple of (m + 2), (k -SD );

      

       A2: for i be Nat st i in ( Seg (m + 2)) holds ( 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;

        assume

         A3: i in ( Seg (m + 2));

        then

         A4: ( DigA (( Mmax r),i)) = ( MmaxDigit (r,i)) by Def4;

        

         A5: i >= 1 by A3, FINSEQ_1: 1;

        now

          per cases ;

            suppose

             A6: i < m;

            

             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 thesis by A7;

          end;

            suppose

             A8: i >= m;

            

             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 thesis by A9;

          end;

        end;

        hence thesis;

      end;

      (m + 2) >= 1 by NAT_1: 12;

      hence thesis by A1, A2, RADIX_5: 15;

    end;

    theorem :: RADIX_6:10

    

     Th10: for m,k be Nat st m >= 1 & k >= 2 holds for r be 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;

      assume that

       A1: m >= 1 and

       A2: k >= 2;

      

       A3: (m + 2) > 1 by A1, Lm1;

      let r be Tuple of (m + 2), (k -SD );

      

       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 thesis by A5, A4;

    end;

    theorem :: RADIX_6:11

    

     Th11: for m,k be Nat st k >= 2 holds for r be 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;

      assume that

       A1: k >= 2;

      let r be Tuple of (m + 2), (k -SD );

      

       A2: for i be Nat st i in ( Seg (m + 2)) holds ( 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;

        assume

         A3: i in ( Seg (m + 2));

        then

         A4: ( DigA (( Mmin r),i)) = ( MminDigit (r,i)) by Def6;

        

         A5: i >= 1 by A3, FINSEQ_1: 1;

        now

          per cases ;

            suppose

             A6: i < m;

            

             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 thesis by A7;

          end;

            suppose

             A8: i >= m;

            

             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 thesis by A9;

          end;

        end;

        hence thesis;

      end;

      (m + 2) >= 1 by NAT_1: 12;

      hence thesis by A1, A2, RADIX_5: 15;

    end;

    theorem :: RADIX_6:12

    

     Th12: for m,k be Nat, r be 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, r be Tuple of (m + 2), (k -SD );

      assume that

       A1: m >= 1 and

       A2: k >= 2;

      

       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 thesis;

    end;

    theorem :: RADIX_6:13

    

     Th13: for m,k be Nat st m >= 1 & k >= 2 holds for r be 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;

      assume that

       A1: m >= 1 and

       A2: k >= 2;

      let r be Tuple of (m + 2), (k -SD );

      

       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 thesis by A4, A5;

    end;

    theorem :: RADIX_6:14

    for m,k,f be Nat, r be Tuple of (m + 2), (k -SD ) st m >= 1 & k >= 2 & f needs_digits_of (m,k) holds ex s be Integer st ( - f) < (( SDDec ( M0 r)) - (s * f)) & (( SDDec ( Mmax r)) - (s * f)) < f

    proof

      let m,k,f be Nat, r be Tuple of (m + 2), (k -SD );

      assume that

       A1: m >= 1 and

       A2: k >= 2 and

       A3: f needs_digits_of (m,k);

      ( 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;

      hence thesis by A5, Th8;

    end;

    theorem :: RADIX_6:15

    for m,k,f be Nat, r be Tuple of (m + 2), (k -SD ) st m >= 1 & k >= 2 & f needs_digits_of (m,k) holds ex s be Integer st ( - f) < (( SDDec ( Mmin r)) - (s * f)) & (( SDDec ( M0 r)) - (s * f)) < f

    proof

      let m,k,f be Nat, r be Tuple of (m + 2), (k -SD );

      assume that

       A1: m >= 1 and

       A2: k >= 2 and

       A3: f needs_digits_of (m,k);

      ( 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;

      hence thesis by A5, Th8;

    end;

    theorem :: RADIX_6:16

    for m,k be Nat, r be Tuple of (m + 2), (k -SD ) st k >= 2 holds ( 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;

      let r be Tuple of (m + 2), (k -SD );

      set MZero = ( SDDec ( M0 r));

      set R = ( SDDec r);

      assume that

       A1: k >= 2;

      now

        per cases ;

          suppose R < MZero;

          hence thesis by A1, Th4;

        end;

          suppose R >= MZero;

          hence thesis by A1, Th3;

        end;

      end;

      hence thesis;

    end;

    begin

    definition

      let i,m,k be Nat, r be Tuple of (m + 2), (k -SD );

      assume

       A1: i in ( Seg (m + 2));

      :: RADIX_6:def8

      func MmaskDigit (r,i) -> Element of (k -SD ) equals

      : Def8: (r . i) if i < m

      otherwise 0 ;

      coherence

      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 thesis by RADIX_1: 14;

      end;

      consistency ;

    end

    definition

      let m,k be Nat, r be Tuple of (m + 2), (k -SD );

      :: RADIX_6:def9

      func Mmask (r) -> Tuple of (m + 2), (k -SD ) means

      : Def9: for i be Nat st i in ( Seg (m + 2)) holds ( DigA (it ,i)) = ( MmaskDigit (r,i));

      existence

      proof

        deffunc F( Nat) = ( MmaskDigit (r,$1));

        consider z be FinSequence of (k -SD ) such that

         A1: ( len z) = (m + 2) and

         A2: for j be Nat st j in ( dom z) holds (z . j) = F(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 as Tuple of (m + 2), (k -SD );

        take z;

        let i be Nat;

        assume

         A4: i in ( Seg (m + 2));

        

        hence ( DigA (z,i)) = (z . i) by RADIX_1:def 3

        .= ( MmaskDigit (r,i)) by A2, A3, A4;

      end;

      uniqueness

      proof

        let k1,k2 be Tuple of (m + 2), (k -SD ) such that

         A5: for i be Nat st i in ( Seg (m + 2)) holds ( DigA (k1,i)) = ( MmaskDigit (r,i)) and

         A6: for i be Nat st i in ( Seg (m + 2)) holds ( DigA (k2,i)) = ( MmaskDigit (r,i));

        

         A7: ( len k1) = (m + 2) by CARD_1:def 7;

        then

         A8: ( dom k1) = ( Seg (m + 2)) by FINSEQ_1:def 3;

         A9:

        now

          let j be Nat;

          assume

           A10: j in ( dom k1);

          

          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);

        end;

        ( len k2) = (m + 2) by CARD_1:def 7;

        hence k1 = k2 by A7, A9, FINSEQ_2: 9;

      end;

    end

    theorem :: RADIX_6:17

    

     Th17: for m,k be Nat, r be 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, r be Tuple of (m + 2), (k -SD );

      

       A1: (m + 2) >= 1 by NAT_1: 12;

      

       A2: for i be Nat st i in ( Seg (m + 2)) holds ( 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;

        assume

         A3: i in ( Seg (m + 2));

        now

          per cases ;

            suppose

             A4: i < m;

            

             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 thesis by A5;

          end;

            suppose

             A6: i >= m;

            

             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 thesis by A7;

          end;

        end;

        hence thesis;

      end;

      assume k >= 2;

      hence thesis by A1, A2, RADIX_5: 15;

    end;

    theorem :: RADIX_6:18

    for m,k be Nat, r be Tuple of (m + 2), (k -SD ) st m >= 1 & k >= 2 holds ( SDDec ( Mmask r)) > 0 implies ( SDDec r) > ( SDDec ( M0 r))

    proof

      let m,k be Nat, r be Tuple of (m + 2), (k -SD );

      assume that

       A1: m >= 1 and

       A2: k >= 2;

      

       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 ;

      hence thesis by A4, XREAL_1: 47;

    end;

    definition

      let i,m,k be Nat;

      assume

       A1: k >= 2;

      :: RADIX_6:def10

      func FSDMinDigit (m,k,i) -> Element of (k -SD ) equals

      : Def10: 0 if i > m,

1 if i = m

      otherwise (( - ( Radix k)) + 1);

      coherence

      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 be 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 thesis by A6, RADIX_1: 14;

      end;

      consistency ;

    end

    definition

      let n,m,k be Nat;

      :: RADIX_6:def11

      func FSDMin (n,m,k) -> Tuple of n, (k -SD ) means

      : Def11: for i be Nat st i in ( Seg n) holds ( DigA (it ,i)) = ( FSDMinDigit (m,k,i));

      existence

      proof

        deffunc F( Nat) = ( FSDMinDigit (m,k,$1));

        consider z be FinSequence of (k -SD ) such that

         A1: ( len z) = n and

         A2: for j be Nat st j in ( dom z) holds (z . j) = F(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 as Tuple of n, (k -SD );

        take z;

        let i be Nat;

        assume

         A4: i in ( Seg n);

        then ( DigA (z,i)) = (z . i) by RADIX_1:def 3;

        hence thesis by A2, A3, A4;

      end;

      uniqueness

      proof

        let k1,k2 be Tuple of n, (k -SD ) such that

         A5: for i be Nat st i in ( Seg n) holds ( DigA (k1,i)) = ( FSDMinDigit (m,k,i)) and

         A6: for i be Nat st i in ( Seg n) holds ( DigA (k2,i)) = ( FSDMinDigit (m,k,i));

        

         A7: ( len k1) = n by CARD_1:def 7;

        then

         A8: ( dom k1) = ( Seg n) by FINSEQ_1:def 3;

         A9:

        now

          let j be Nat;

          assume

           A10: j in ( dom k1);

          

          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);

        end;

        ( len k2) = n by CARD_1:def 7;

        hence k1 = k2 by A7, A9, FINSEQ_2: 9;

      end;

    end

    theorem :: RADIX_6:19

    

     Th19: for n be Nat st n >= 1 holds for m,k be Nat st m in ( Seg n) & k >= 2 holds ( SDDec ( FSDMin (n,m,k))) = 1

    proof

      let n be Nat;

      assume

       A1: n >= 1;

      let m,k be Nat;

      assume that

       A2: m in ( Seg n) and

       A3: k >= 2;

      for i be Nat st i in ( Seg n) holds ( 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;

        assume

         A4: i in ( Seg n);

        then

         A5: i >= 1 by FINSEQ_1: 1;

        now

          per cases ;

            suppose

             A6: i > m;

            

             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 thesis by A8, A7;

          end;

            suppose

             A9: i <= m;

            now

              per cases by A9, XXREAL_0: 1;

                suppose

                 A10: i = m;

                

                 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 thesis by A12, A11;

              end;

                suppose

                 A13: i < m;

                

                 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 thesis by A15, A14;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      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 thesis by A1, A3, RADIX_5: 9;

    end;

    definition

      let n,m,k be Nat, r be Tuple of (m + 2), (k -SD );

      :: RADIX_6:def12

      pred r is_Zero_over n means for i be Nat st i > n holds ( DigA (r,i)) = 0 ;

    end

    theorem :: RADIX_6:20

    for m be Nat st m >= 1 holds for n,k be Nat, r be 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;

      assume m >= 1;

      then

       A1: (m + 2) >= 1 by Lm1;

      let n,k be Nat, r be Tuple of (m + 2), (k -SD );

      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 ;

      for i be Nat st i in ( Seg (m + 2)) holds ( DigA (( Mmask r),i)) >= ( DigA (( FSDMin ((m + 2),n,k)),i))

      proof

        let i be Nat;

        assume

         A6: i in ( Seg (m + 2));

        now

          per cases ;

            suppose

             A7: i > n;

            ( DigA (( FSDMin ((m + 2),n,k)),i)) = ( FSDMinDigit (n,k,i)) by A6, Def11

            .= 0 by A2, A7, Def10;

            hence thesis by A4, A7;

          end;

            suppose

             A8: i <= n;

            now

              per cases by A8, XXREAL_0: 1;

                suppose

                 A9: i = n;

                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 thesis by A10;

              end;

                suppose

                 A11: i < n;

                

                 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 thesis by A12, A13, RADIX_1: 13;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      then ( SDDec ( Mmask r)) >= ( SDDec ( FSDMin ((m + 2),n,k))) by A1, RADIX_5: 13;

      hence thesis by A2, A3, A1, Th19;

    end;