radix_3.miz



    begin

    reserve i,n,m,k,x for Nat,

i1,i2 for Integer;

    

     Lm1: 1 <= k implies ( Radix k) = (( Radix (k -' 1)) + ( Radix (k -' 1)))

    proof

      assume 1 <= k;

      

      then ( Radix k) = (2 to_power ((k -' 1) + 1)) by XREAL_1: 235

      .= ((2 to_power 1) * (2 to_power (k -' 1))) by POWER: 27

      .= (2 * ( Radix (k -' 1))) by POWER: 25

      .= (( Radix (k -' 1)) + ( Radix (k -' 1)));

      hence thesis;

    end;

    

     Lm2: 1 <= k implies (( Radix k) - ( Radix (k -' 1))) = ( Radix (k -' 1))

    proof

      assume 1 <= k;

      then (( Radix k) + 0 ) = (( Radix (k -' 1)) + ( Radix (k -' 1))) by Lm1;

      hence thesis;

    end;

    

     Lm3: 1 <= k implies (( - ( Radix k)) + ( Radix (k -' 1))) = ( - ( Radix (k -' 1)))

    proof

      assume 1 <= k;

      then ( - (( Radix k) - ( Radix (k -' 1)))) = ( - ( Radix (k -' 1))) by Lm2;

      hence thesis;

    end;

    

     Lm4: for k be Nat st 1 <= k holds 2 <= ( Radix k)

    proof

      defpred P[ Nat] means 2 <= ( Radix $1);

      let k;

      assume

       A1: 1 <= k;

      

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

      proof

        let kk be Nat;

        assume that 1 <= kk and

         A3: 2 <= ( Radix kk);

        

         A4: ( Radix (kk + 1)) = ((2 to_power 1) * (2 to_power kk)) by POWER: 27

        .= (2 * ( Radix kk)) by POWER: 25;

        ( Radix kk) > 1 by A3, XXREAL_0: 2;

        hence thesis by A4, XREAL_1: 155;

      end;

      

       A5: P[1] by POWER: 25;

      for k be Nat holds 1 <= k implies P[k] from NAT_1:sch 8( A5, A2);

      hence thesis by A1;

    end;

    

     Lm5: for i st i in ( Seg n) holds ( DigA (( DecSD (m,(n + 1),k)),i)) = ( DigA (( DecSD ((m mod (( Radix k) |^ n)),n,k)),i))

    proof

      let i;

      assume

       A1: i in ( Seg n);

      then

       A2: i <= n by FINSEQ_1: 1;

      then

       A3: i <= (n + 1) by NAT_1: 12;

      1 <= i by A1, FINSEQ_1: 1;

      then

       A4: i in ( Seg (n + 1)) by A3, FINSEQ_1: 1;

      (( Radix k) |^ i) divides (( Radix k) |^ n) by A2, NEWTON: 89;

      then

      consider t be Nat such that

       A5: (( Radix k) |^ n) = ((( Radix k) |^ i) * t) by NAT_D:def 3;

      ( Radix k) <> 0 by POWER: 34;

      then

       A6: t <> 0 by A5, PREPOWER: 5;

      ( DigA (( DecSD ((m mod (( Radix k) |^ n)),n,k)),i)) = ( DigitDC ((m mod (( Radix k) |^ n)),i,k)) by A1, RADIX_1:def 9

      .= ( DigitDC (m,i,k)) by A5, A6, RADIX_1: 3

      .= ( DigA (( DecSD (m,(n + 1),k)),i)) by A4, RADIX_1:def 9;

      hence thesis;

    end;

    definition

      let k;

      :: RADIX_3:def1

      func k -SD_Sub_S -> set equals { e where e be Element of INT : e >= ( - ( Radix (k -' 1))) & e <= (( Radix (k -' 1)) - 1) };

      correctness ;

      :: RADIX_3:def2

      func k -SD_Sub -> set equals { e where e be Element of INT : e >= (( - ( Radix (k -' 1))) - 1) & e <= ( Radix (k -' 1)) };

      correctness ;

    end

    theorem :: RADIX_3:1

    

     Th1: i1 in (k -SD_Sub ) implies (( - ( Radix (k -' 1))) - 1) <= i1 & i1 <= ( Radix (k -' 1))

    proof

      assume i1 in (k -SD_Sub );

      then ex i be Element of INT st i = i1 & (( - ( Radix (k -' 1))) - 1) <= i & i <= ( Radix (k -' 1));

      hence thesis;

    end;

    theorem :: RADIX_3:2

    

     Th2: (k -SD_Sub_S ) c= (k -SD_Sub )

    proof

      let e be object;

      assume e in (k -SD_Sub_S );

      then

      consider g be Element of INT such that

       A1: e = g and

       A2: g >= ( - ( Radix (k -' 1))) and

       A3: g <= (( Radix (k -' 1)) - 1);

      (( Radix (k -' 1)) + 1) >= (( Radix (k -' 1)) + 0 ) by XREAL_1: 7;

      then ( - ( Radix (k -' 1))) >= ( - (( Radix (k -' 1)) + 1)) by XREAL_1: 24;

      then

       A4: g >= (( - ( Radix (k -' 1))) - 1) by A2, XXREAL_0: 2;

      (( Radix (k -' 1)) + 0 ) >= (( Radix (k -' 1)) + ( - 1)) by XREAL_1: 7;

      then ( Radix (k -' 1)) >= g by A3, XXREAL_0: 2;

      hence thesis by A1, A4;

    end;

    theorem :: RADIX_3:3

    

     Th3: (k -SD_Sub_S ) c= ((k + 1) -SD_Sub_S )

    proof

      let e be object;

      assume e in (k -SD_Sub_S );

      then

      consider g be Element of INT such that

       A1: e = g and

       A2: g >= ( - ( Radix (k -' 1))) and

       A3: g <= (( Radix (k -' 1)) - 1);

      (k -' 1) <= k by NAT_D: 44;

      then

       A4: (2 to_power (k -' 1)) <= (2 to_power k) by PRE_FF: 8;

      then (( Radix (k -' 1)) - 1) <= (( Radix k) - 1) by XREAL_1: 9;

      then (( Radix (k -' 1)) - 1) <= (( Radix ((k + 1) -' 1)) - 1) by NAT_D: 34;

      then

       A5: g <= (( Radix ((k + 1) -' 1)) - 1) by A3, XXREAL_0: 2;

      ( - ( Radix (k -' 1))) >= ( - ( Radix k)) by A4, XREAL_1: 24;

      then ( - ( Radix (k -' 1))) >= ( - ( Radix ((k + 1) -' 1))) by NAT_D: 34;

      then g >= ( - ( Radix ((k + 1) -' 1))) by A2, XXREAL_0: 2;

      hence thesis by A1, A5;

    end;

    theorem :: RADIX_3:4

    2 <= k implies (k -SD_Sub ) c= (k -SD )

    proof

      assume

       A1: 2 <= k;

      then (1 + 1) <= k;

      then 1 <= (k -' 1) by NAT_D: 55;

      then

       A2: ( Radix (k -' 1)) >= 2 by Lm4;

      then ( Radix (k -' 1)) >= 1 by XXREAL_0: 2;

      then ( - ( Radix (k -' 1))) <= ( - 1) by XREAL_1: 24;

      then

       A3: (( Radix k) + ( - ( Radix (k -' 1)))) <= (( Radix k) + ( - 1)) by XREAL_1: 7;

      let e be object;

      assume e in (k -SD_Sub );

      then

      consider g be Element of INT such that

       A4: e = g and

       A5: g >= (( - ( Radix (k -' 1))) - 1) and

       A6: g <= ( Radix (k -' 1));

      (( Radix (k -' 1)) + ( Radix (k -' 1))) >= (( Radix (k -' 1)) + 2) by A2, XREAL_1: 6;

      then (( Radix k) + 0 ) >= ((( Radix (k -' 1)) + 1) + 1) by A1, Lm1, XXREAL_0: 2;

      then (( Radix k) - 1) >= ((( Radix (k -' 1)) + 1) - 0 ) by XREAL_1: 21;

      then ( - (( Radix (k -' 1)) + 1)) >= ( - (( Radix k) - 1)) by XREAL_1: 24;

      then

       A7: g >= (( - ( Radix k)) + 1) by A5, XXREAL_0: 2;

      (( Radix k) + 0 ) = (( Radix (k -' 1)) + ( Radix (k -' 1))) by A1, Lm1, XXREAL_0: 2;

      then g <= (( Radix k) - 1) by A6, A3, XXREAL_0: 2;

      hence thesis by A4, A7;

    end;

    theorem :: RADIX_3:5

    

     Th5: 0 in ( 0 -SD_Sub_S )

    proof

      reconsider ZERO = 0 as Integer;

       0 > ( 0 - 1);

      then ( 0 -' 1) = 0 by XREAL_0:def 2;

      then

       A1: ( Radix ( 0 -' 1)) = 1 by POWER: 24;

      ZERO is Element of INT by INT_1:def 2;

      hence thesis by A1;

    end;

    theorem :: RADIX_3:6

    

     Th6: 0 in (k -SD_Sub_S )

    proof

      defpred P[ Nat] means 0 in ($1 -SD_Sub_S );

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let kk be Nat;

        assume

         A2: 0 in (kk -SD_Sub_S );

        (kk -SD_Sub_S ) c= ((kk + 1) -SD_Sub_S ) by Th3;

        hence thesis by A2;

      end;

      

       A3: P[ 0 ] by Th5;

      for k be Nat holds P[k] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: RADIX_3:7

    

     Th7: 0 in (k -SD_Sub )

    proof

       0 in (k -SD_Sub_S ) & (k -SD_Sub_S ) c= (k -SD_Sub ) by Th2, Th6;

      hence thesis;

    end;

    theorem :: RADIX_3:8

    

     Th8: for e be set st e in (k -SD_Sub ) holds e is Integer

    proof

      let e be set;

      assume e in (k -SD_Sub );

      then ex t be Element of INT st e = t & t >= (( - ( Radix (k -' 1))) - 1) & t <= ( Radix (k -' 1));

      hence thesis;

    end;

    theorem :: RADIX_3:9

    

     Th9: (k -SD_Sub ) c= INT

    proof

      let e be object;

      assume e in (k -SD_Sub );

      then e is Integer by Th8;

      hence thesis by INT_1:def 2;

    end;

    theorem :: RADIX_3:10

    

     Th10: (k -SD_Sub_S ) c= INT

    proof

      let e be object;

      assume

       A1: e in (k -SD_Sub_S );

      (k -SD_Sub_S ) c= (k -SD_Sub ) by Th2;

      then e is Integer by A1, Th8;

      hence thesis by INT_1:def 2;

    end;

    registration

      let k;

      cluster (k -SD_Sub_S ) -> non empty;

      coherence by Th6;

      cluster (k -SD_Sub ) -> non empty;

      coherence by Th7;

    end

    definition

      let k;

      :: original: -SD_Sub_S

      redefine

      func k -SD_Sub_S -> non empty Subset of INT ;

      coherence by Th10;

    end

    definition

      let k;

      :: original: -SD_Sub

      redefine

      func k -SD_Sub -> non empty Subset of INT ;

      coherence by Th9;

    end

    reserve a for Tuple of n, (k -SD );

    reserve aSub for Tuple of n, (k -SD_Sub );

    theorem :: RADIX_3:11

    

     Th11: i in ( Seg n) implies (aSub . i) is Element of (k -SD_Sub )

    proof

      

       A1: ( len aSub) = n by CARD_1:def 7;

      assume i in ( Seg n);

      then i in ( dom aSub) by A1, FINSEQ_1:def 3;

      then

       A2: (aSub . i) in ( rng aSub) by FUNCT_1:def 3;

      ( rng aSub) c= (k -SD_Sub ) by FINSEQ_1:def 4;

      hence thesis by A2;

    end;

    begin

    definition

      let x be Integer, k be Nat;

      :: RADIX_3:def3

      func SDSub_Add_Carry (x,k) -> Integer equals

      : Def3: 1 if ( Radix (k -' 1)) <= x,

( - 1) if x < ( - ( Radix (k -' 1)))

      otherwise 0 ;

      coherence ;

      consistency ;

    end

    definition

      let x be Integer, k be Nat;

      :: RADIX_3:def4

      func SDSub_Add_Data (x,k) -> Integer equals (x - (( Radix k) * ( SDSub_Add_Carry (x,k))));

      coherence ;

    end

    theorem :: RADIX_3:12

    

     Th12: for x be Integer, k be Nat holds ( - 1) <= ( SDSub_Add_Carry (x,k)) & ( SDSub_Add_Carry (x,k)) <= 1

    proof

      let x be Integer, k be Nat;

      per cases ;

        suppose x < ( - ( Radix (k -' 1)));

        hence thesis by Def3;

      end;

        suppose ( - ( Radix (k -' 1))) <= x & x < ( Radix (k -' 1));

        hence thesis by Def3;

      end;

        suppose x >= ( Radix (k -' 1));

        hence thesis by Def3;

      end;

    end;

    theorem :: RADIX_3:13

    

     Th13: 2 <= k & i1 in (k -SD ) implies ( SDSub_Add_Data (i1,k)) >= ( - ( Radix (k -' 1))) & ( SDSub_Add_Data (i1,k)) <= (( Radix (k -' 1)) - 1)

    proof

      assume that

       A1: 2 <= k and

       A2: i1 in (k -SD );

      

       A3: (( - ( Radix k)) + 1) <= i1 & 1 <= k by A1, A2, RADIX_1: 13, XXREAL_0: 2;

      now

        per cases ;

          case

           A4: i1 < ( - ( Radix (k -' 1)));

          then (i1 + 1) <= ( - ( Radix (k -' 1))) by INT_1: 7;

          then i1 <= (( - ( Radix (k -' 1))) - 1) by XREAL_1: 19;

          then (i1 + ( Radix k)) <= (( Radix k) + (( - ( Radix (k -' 1))) - 1)) by XREAL_1: 7;

          then

           A5: (i1 + ( Radix k)) <= ((( Radix k) - ( Radix (k -' 1))) - 1);

          ( SDSub_Add_Carry (i1,k)) = ( - 1) by A4, Def3;

          hence thesis by A3, A5, Lm2, XREAL_1: 19;

        end;

          case

           A6: ( - ( Radix (k -' 1))) <= i1 & i1 < ( Radix (k -' 1));

          then ( SDSub_Add_Carry (i1,k)) = 0 & (i1 + 1) <= ( Radix (k -' 1)) by Def3, INT_1: 7;

          hence thesis by A6, XREAL_1: 19;

        end;

          case

           A7: ( Radix (k -' 1)) <= i1;

          i1 <= (( Radix k) + ( - 1)) by A2, RADIX_1: 13;

          then

           A8: ( 0 - 1) <= (( Radix (k -' 1)) - 1) & (i1 - ( Radix k)) <= ( - 1) by XREAL_1: 9, XREAL_1: 20;

          ( SDSub_Add_Carry (i1,k)) = 1 & (( Radix (k -' 1)) + ( - ( Radix k))) <= (i1 + ( - ( Radix k))) by A7, Def3, XREAL_1: 6;

          hence thesis by A1, A8, Lm3, XXREAL_0: 2;

        end;

      end;

      hence thesis;

    end;

    theorem :: RADIX_3:14

    

     Th14: for x be Integer, k be Nat st 2 <= k holds ( SDSub_Add_Carry (x,k)) in (k -SD_Sub_S )

    proof

      let x be Integer, k be Nat;

      

       A1: ( SDSub_Add_Carry (x,k)) <= 1 by Th12;

      assume k >= 2;

      then k > 1 by XXREAL_0: 2;

      then (k - 1) > (1 - 1) by XREAL_1: 14;

      then

       A2: (k -' 1) > 0 by XREAL_0:def 2;

      then (2 to_power (k -' 1)) > 1 by POWER: 35;

      then

       A3: ( - ( Radix (k -' 1))) <= ( - 1) by XREAL_1: 24;

      ( - 1) <= ( SDSub_Add_Carry (x,k)) by Th12;

      then

       A4: ( SDSub_Add_Carry (x,k)) >= ( - ( Radix (k -' 1))) by A3, XXREAL_0: 2;

      (( Radix (k -' 1)) - 1) >= 1 by A2, INT_1: 52, POWER: 35;

      then

       A5: ( SDSub_Add_Carry (x,k)) <= (( Radix (k -' 1)) - 1) by A1, XXREAL_0: 2;

      ( SDSub_Add_Carry (x,k)) is Element of INT by INT_1:def 2;

      hence thesis by A5, A4;

    end;

    theorem :: RADIX_3:15

    

     Th15: 2 <= k & i1 in (k -SD ) implies (( SDSub_Add_Data (i1,k)) + ( SDSub_Add_Carry (i2,k))) in (k -SD_Sub )

    proof

      

       A1: ( SDSub_Add_Carry (i2,k)) >= ( - 1) by Th12;

      assume

       A2: 2 <= k & i1 in (k -SD );

      then ( SDSub_Add_Data (i1,k)) >= ( - ( Radix (k -' 1))) by Th13;

      then

       A3: (( SDSub_Add_Data (i1,k)) + ( SDSub_Add_Carry (i2,k))) >= (( - ( Radix (k -' 1))) + ( - 1)) by A1, XREAL_1: 7;

      

       A4: ( SDSub_Add_Carry (i2,k)) <= 1 by Th12;

      ( SDSub_Add_Data (i1,k)) <= (( Radix (k -' 1)) - 1) by A2, Th13;

      then

       A5: (( SDSub_Add_Data (i1,k)) + ( SDSub_Add_Carry (i2,k))) <= ((( Radix (k -' 1)) - 1) + 1) by A4, XREAL_1: 7;

      (( SDSub_Add_Data (i1,k)) + ( SDSub_Add_Carry (i2,k))) is Element of INT by INT_1:def 2;

      hence thesis by A3, A5;

    end;

    theorem :: RADIX_3:16

    

     Th16: ( SDSub_Add_Carry ( 0 ,k)) = 0

    proof

      set x = 0 ;

      ( Radix (k -' 1)) <> x & ( - ( Radix (k -' 1))) <= ( 0 - 0 ) by POWER: 34;

      hence thesis by Def3;

    end;

    begin

    definition

      let i,k,n be Nat, x be Tuple of n, (k -SD_Sub );

      :: RADIX_3:def5

      func DigA_SDSub (x,i) -> Integer equals

      : Def5: (x . i) if i in ( Seg n),

0 if i = 0 ;

      coherence by INT_1:def 2;

      consistency by FINSEQ_1: 1;

    end

    definition

      let i,k,n be Nat, x be Tuple of n, (k -SD );

      :: RADIX_3:def6

      func SD2SDSubDigit (x,i,k) -> Integer equals

      : Def6: (( SDSub_Add_Data (( DigA (x,i)),k)) + ( SDSub_Add_Carry (( DigA (x,(i -' 1))),k))) if i in ( Seg n),

( SDSub_Add_Carry (( DigA (x,(i -' 1))),k)) if i = (n + 1)

      otherwise 0 ;

      coherence ;

      consistency

      proof

        i in ( Seg n) implies not i = (n + 1)

        proof

          assume i in ( Seg n);

          then

           A1: i <= n by FINSEQ_1: 1;

          assume i = (n + 1);

          hence contradiction by A1, NAT_1: 13;

        end;

        hence thesis;

      end;

    end

    theorem :: RADIX_3:17

    

     Th17: 2 <= k & i in ( Seg (n + 1)) implies ( SD2SDSubDigit (a,i,k)) is Element of (k -SD_Sub )

    proof

      assume that

       A1: 2 <= k and

       A2: i in ( Seg (n + 1));

      set SDD = (( SDSub_Add_Data (( DigA (a,i)),k)) + ( SDSub_Add_Carry (( DigA (a,(i -' 1))),k)));

      set SDC = ( SDSub_Add_Carry (( DigA (a,(i -' 1))),k));

      now

        per cases by A2, FINSEQ_2: 7;

          suppose

           A3: i in ( Seg n);

          SDD in (k -SD_Sub )

          proof

            ( DigA (a,i)) is Element of (k -SD ) by A3, RADIX_1: 16;

            hence thesis by A1, Th15;

          end;

          hence ( SD2SDSubDigit (a,i,k)) in (k -SD_Sub ) by A3, Def6;

        end;

          suppose

           A4: i = (n + 1);

          ( SDSub_Add_Carry (( DigA (a,(i -' 1))),k)) in (k -SD_Sub_S ) & (k -SD_Sub_S ) c= (k -SD_Sub ) by A1, Th2, Th14;

          then SDC in (k -SD_Sub );

          hence ( SD2SDSubDigit (a,i,k)) in (k -SD_Sub ) by A4, Def6;

        end;

      end;

      hence thesis;

    end;

    definition

      let i,k,n be Nat, x be Tuple of n, (k -SD );

      assume

       A1: 2 <= k & i in ( Seg (n + 1));

      :: RADIX_3:def7

      func SD2SDSubDigitS (x,i,k) -> Element of (k -SD_Sub ) equals

      : Def7: ( SD2SDSubDigit (x,i,k));

      coherence by A1, Th17;

    end

    definition

      let n,k be Nat, x be Tuple of n, (k -SD );

      :: RADIX_3:def8

      func SD2SDSub (x) -> Tuple of (n + 1), (k -SD_Sub ) means

      : Def8: for i be Nat st i in ( Seg (n + 1)) holds ( DigA_SDSub (it ,i)) = ( SD2SDSubDigitS (x,i,k));

      existence

      proof

        deffunc F( Nat) = ( SD2SDSubDigitS (x,$1,k));

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

         A1: ( len z) = (n + 1) 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 + 1)) by A1, FINSEQ_1:def 3;

        z is Element of ((n + 1) -tuples_on (k -SD_Sub )) by A1, FINSEQ_2: 92;

        then

        reconsider z as Tuple of (n + 1), (k -SD_Sub );

        take z;

        let i;

        assume

         A4: i in ( Seg (n + 1));

        

        hence ( DigA_SDSub (z,i)) = (z . i) by Def5

        .= ( SD2SDSubDigitS (x,i,k)) by A2, A3, A4;

      end;

      uniqueness

      proof

        let k1,k2 be Tuple of (n + 1), (k -SD_Sub ) such that

         A5: for i be Nat st i in ( Seg (n + 1)) holds ( DigA_SDSub (k1,i)) = ( SD2SDSubDigitS (x,i,k)) and

         A6: for i be Nat st i in ( Seg (n + 1)) holds ( DigA_SDSub (k2,i)) = ( SD2SDSubDigitS (x,i,k));

        

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

        then

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

         A9:

        now

          let j be Nat;

          assume

           A10: j in ( dom k1);

          

          then (k1 . j) = ( DigA_SDSub (k1,j)) by A8, Def5

          .= ( SD2SDSubDigitS (x,j,k)) by A5, A8, A10

          .= ( DigA_SDSub (k2,j)) by A6, A8, A10

          .= (k2 . j) by A8, A10, Def5;

          hence (k1 . j) = (k2 . j);

        end;

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

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    theorem :: RADIX_3:18

    i in ( Seg n) implies ( DigA_SDSub (aSub,i)) is Element of (k -SD_Sub )

    proof

      assume

       A1: i in ( Seg n);

      then (aSub . i) = ( DigA_SDSub (aSub,i)) by Def5;

      hence thesis by A1, Th11;

    end;

    theorem :: RADIX_3:19

    2 <= k & i1 in (k -SD ) & i2 in (k -SD_Sub ) implies ( SDSub_Add_Data ((i1 + i2),k)) in (k -SD_Sub_S )

    proof

      assume that

       A1: 2 <= k and

       A2: i1 in (k -SD ) & i2 in (k -SD_Sub );

      set z = (i1 + i2);

      i1 <= (( Radix k) - 1) & i2 <= ( Radix (k -' 1)) by A2, Th1, RADIX_1: 13;

      then

       A3: z <= ((( Radix k) - 1) + ( Radix (k -' 1))) by XREAL_1: 7;

      (( - ( Radix k)) + 1) <= i1 & (( - ( Radix (k -' 1))) - 1) <= i2 by A2, Th1, RADIX_1: 13;

      then

       A4: ((( - ( Radix k)) + 1) + (( - ( Radix (k -' 1))) - 1)) <= z by XREAL_1: 7;

      

       A5: ( SDSub_Add_Data (z,k)) >= ( - ( Radix (k -' 1))) & ( SDSub_Add_Data (z,k)) <= (( Radix (k -' 1)) - 1)

      proof

        now

          per cases ;

            case

             A6: z < ( - ( Radix (k -' 1)));

            then (z + 1) <= ( - ( Radix (k -' 1))) by INT_1: 7;

            then z <= (( - ( Radix (k -' 1))) - 1) by XREAL_1: 19;

            then z <= (( - ( Radix (k -' 1))) + ( - 1));

            then z <= ((( - ( Radix k)) + ( Radix (k -' 1))) + ( - 1)) by A1, Lm3, XXREAL_0: 2;

            then

             A7: z <= (( - ( Radix k)) + (( Radix (k -' 1)) + ( - 1)));

            (( - ( Radix (k -' 1))) + ( - ( Radix k))) <= (z + 0 ) by A4;

            then

             A8: (( - ( Radix (k -' 1))) - 0 ) <= (z - ( - ( Radix k))) by XREAL_1: 21;

            ( SDSub_Add_Carry (z,k)) = ( - 1) by A6, Def3;

            hence thesis by A8, A7, XREAL_1: 20;

          end;

            case

             A9: ( - ( Radix (k -' 1))) <= z & z < ( Radix (k -' 1));

            then ( SDSub_Add_Carry (z,k)) = 0 & (z + 1) <= ( Radix (k -' 1)) by Def3, INT_1: 7;

            hence thesis by A9, XREAL_1: 19;

          end;

            case

             A10: ( Radix (k -' 1)) <= z;

            then (( Radix k) - ( Radix (k -' 1))) <= z by A1, Lm2, XXREAL_0: 2;

            then

             A11: (( Radix k) + ( - ( Radix (k -' 1)))) <= z;

            

             A12: z <= (( Radix k) + (( Radix (k -' 1)) - 1)) by A3;

            ( SDSub_Add_Carry (z,k)) = 1 by A10, Def3;

            hence thesis by A11, A12, XREAL_1: 19, XREAL_1: 20;

          end;

        end;

        hence thesis;

      end;

      ( SDSub_Add_Data (z,k)) is Element of INT by INT_1:def 2;

      hence thesis by A5;

    end;

    begin

    definition

      let i,k,n be Nat, x be Tuple of n, (k -SD_Sub );

      :: RADIX_3:def9

      func DigB_SDSub (x,i) -> Element of INT equals ( DigA_SDSub (x,i));

      coherence by INT_1:def 2;

    end

    definition

      let i,k,n be Nat, x be Tuple of n, (k -SD_Sub );

      :: RADIX_3:def10

      func SDSub2INTDigit (x,i,k) -> Element of INT equals ((( Radix k) |^ (i -' 1)) * ( DigB_SDSub (x,i)));

      coherence by INT_1:def 2;

    end

    definition

      let n,k be Nat, x be Tuple of n, (k -SD_Sub );

      :: RADIX_3:def11

      func SDSub2INT (x) -> Tuple of n, INT means

      : Def11: for i be Nat st i in ( Seg n) holds (it /. i) = ( SDSub2INTDigit (x,i,k));

      existence

      proof

        deffunc F( Nat) = ( SDSub2INTDigit (x,$1,k));

        consider z be FinSequence of INT 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 INT ) by A1, FINSEQ_2: 92;

        then

        reconsider z as Tuple of n, INT ;

        take z;

        let i;

        assume

         A4: i in ( Seg n);

        then i in ( dom z) by A1, FINSEQ_1:def 3;

        

        hence (z /. i) = (z . i) by PARTFUN1:def 6

        .= ( SDSub2INTDigit (x,i,k)) by A2, A3, A4;

      end;

      uniqueness

      proof

        let k1,k2 be Tuple of n, INT such that

         A5: for i be Nat st i in ( Seg n) holds (k1 /. i) = ( SDSub2INTDigit (x,i,k)) and

         A6: for i be Nat st i in ( Seg n) holds (k2 /. i) = ( SDSub2INTDigit (x,i,k));

        

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

        then

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

        

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

        now

          let j be Nat;

          assume

           A10: j in ( dom k1);

          then

           A11: j in ( dom k2) by A9, A8, FINSEQ_1:def 3;

          (k1 . j) = (k1 /. j) by A10, PARTFUN1:def 6

          .= ( SDSub2INTDigit (x,j,k)) by A5, A8, A10

          .= (k2 /. j) by A6, A8, A10

          .= (k2 . j) by A11, PARTFUN1:def 6;

          hence (k1 . j) = (k2 . j);

        end;

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    definition

      let n,k be Nat, x be Tuple of n, (k -SD_Sub );

      :: RADIX_3:def12

      func SDSub2IntOut (x) -> Integer equals ( Sum ( SDSub2INT x));

      coherence ;

    end

    theorem :: RADIX_3:20

    

     Th20: for i st i in ( Seg n) holds 2 <= k implies ( DigA_SDSub (( SD2SDSub ( DecSD (m,(n + 1),k))),i)) = ( DigA_SDSub (( SD2SDSub ( DecSD ((m mod (( Radix k) |^ n)),n,k))),i))

    proof

      let i;

      assume

       A1: i in ( Seg n);

      reconsider i as Element of NAT by ORDINAL1:def 12;

      

       A2: 1 <= i by A1, FINSEQ_1: 1;

      i <= n by A1, FINSEQ_1: 1;

      then

       A3: i <= (n + 1) by NAT_1: 12;

      then

       A4: i in ( Seg (n + 1)) by A2, FINSEQ_1: 1;

      i <= ((n + 1) + 1) by A3, NAT_1: 12;

      then

       A5: i in ( Seg ((n + 1) + 1)) by A2, FINSEQ_1: 1;

      set M = (m mod (( Radix k) |^ n));

      assume

       A6: 2 <= k;

      

       A7: ( DigA_SDSub (( SD2SDSub ( DecSD (M,n,k))),i)) = ( SD2SDSubDigitS (( DecSD (M,n,k)),i,k)) by A4, Def8

      .= ( SD2SDSubDigit (( DecSD (M,n,k)),i,k)) by A6, A4, Def7

      .= (( SDSub_Add_Data (( DigA (( DecSD (M,n,k)),i)),k)) + ( SDSub_Add_Carry (( DigA (( DecSD (M,n,k)),(i -' 1))),k))) by A1, Def6

      .= (( SDSub_Add_Data (( DigA (( DecSD (m,(n + 1),k)),i)),k)) + ( SDSub_Add_Carry (( DigA (( DecSD (M,n,k)),(i -' 1))),k))) by A1, Lm5;

      now

        per cases ;

          suppose

           A8: i = 1;

          

          then

           A9: ( DigA_SDSub (( SD2SDSub ( DecSD (M,n,k))),i)) = (( SDSub_Add_Data (( DigA (( DecSD (m,(n + 1),k)),i)),k)) + ( SDSub_Add_Carry (( DigA (( DecSD (M,n,k)), 0 )),k))) by A7, XREAL_1: 232

          .= (( SDSub_Add_Data (( DigA (( DecSD (m,(n + 1),k)),i)),k)) + ( SDSub_Add_Carry ( 0 ,k))) by RADIX_1:def 3

          .= (( SDSub_Add_Data (( DigA (( DecSD (m,(n + 1),k)),i)),k)) + 0 ) by Th16;

          ( DigA_SDSub (( SD2SDSub ( DecSD (m,(n + 1),k))),i)) = ( SD2SDSubDigitS (( DecSD (m,(n + 1),k)),i,k)) by A5, Def8

          .= ( SD2SDSubDigit (( DecSD (m,(n + 1),k)),i,k)) by A6, A5, Def7

          .= (( SDSub_Add_Data (( DigA (( DecSD (m,(n + 1),k)),i)),k)) + ( SDSub_Add_Carry (( DigA (( DecSD (m,(n + 1),k)),(i -' 1))),k))) by A4, Def6

          .= (( SDSub_Add_Data (( DigA (( DecSD (m,(n + 1),k)),i)),k)) + ( SDSub_Add_Carry (( DigA (( DecSD (m,(n + 1),k)), 0 )),k))) by A8, XREAL_1: 232

          .= (( SDSub_Add_Data (( DigA (( DecSD (m,(n + 1),k)),i)),k)) + ( SDSub_Add_Carry ( 0 ,k))) by RADIX_1:def 3

          .= (( SDSub_Add_Data (( DigA (( DecSD (m,(n + 1),k)),i)),k)) + 0 ) by Th16;

          hence thesis by A9;

        end;

          suppose

           A10: i <> 1;

          i <= n by A1, FINSEQ_1: 1;

          then

           A11: (i -' 1) <= n by NAT_D: 44;

          1 < i by A2, A10, XXREAL_0: 1;

          then ( 0 + 1) <= (i -' 1) by INT_1: 7, JORDAN12: 1;

          then (i -' 1) in ( Seg n) by A11, FINSEQ_1: 1;

          

          then ( DigA_SDSub (( SD2SDSub ( DecSD (M,n,k))),i)) = (( SDSub_Add_Data (( DigA (( DecSD (m,(n + 1),k)),i)),k)) + ( SDSub_Add_Carry (( DigA (( DecSD (m,(n + 1),k)),(i -' 1))),k))) by A7, Lm5

          .= ( SD2SDSubDigit (( DecSD (m,(n + 1),k)),i,k)) by A4, Def6

          .= ( SD2SDSubDigitS (( DecSD (m,(n + 1),k)),i,k)) by A6, A5, Def7

          .= ( DigA_SDSub (( SD2SDSub ( DecSD (m,(n + 1),k))),i)) by A5, Def8;

          hence thesis;

        end;

      end;

      hence thesis;

    end;

    theorem :: RADIX_3:21

    for n st n >= 1 holds for k, x st k >= 2 & x is_represented_by (n,k) holds x = ( SDSub2IntOut ( SD2SDSub ( DecSD (x,n,k))))

    proof

      defpred P[ Nat] means for k,x be Nat st k >= 2 & x is_represented_by ($1,k) holds x = ( SDSub2IntOut ( SD2SDSub ( DecSD (x,$1,k))));

      let n;

      assume

       A1: n >= 1;

      

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

      proof

        let n be Nat;

        assume that

         A3: n >= 1 and

         A4: P[n];

        

         A5: n in ( Seg n) by A3, FINSEQ_1: 3;

        let k,x be Nat;

        assume that

         A6: k >= 2 and

         A7: x is_represented_by ((n + 1),k);

        reconsider k as Element of NAT by ORDINAL1:def 12;

        set xn = (x mod (( Radix k) |^ n));

        set RN1 = (( Radix k) |^ (n + 1));

        set RN = (( Radix k) |^ n);

        

         A8: ((n + 1) + 1) in ( Seg ((n + 1) + 1)) by FINSEQ_1: 3;

        

         A9: ( SDSub2INTDigit (( SD2SDSub ( DecSD (x,(n + 1),k))),((n + 1) + 1),k)) = (RN1 * ( DigB_SDSub (( SD2SDSub ( DecSD (x,(n + 1),k))),((n + 1) + 1)))) by NAT_D: 34

        .= (RN1 * ( SD2SDSubDigitS (( DecSD (x,(n + 1),k)),((n + 1) + 1),k))) by A8, Def8

        .= (RN1 * ( SD2SDSubDigit (( DecSD (x,(n + 1),k)),((n + 1) + 1),k))) by A6, A8, Def7

        .= (RN1 * ( SDSub_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),(((n + 1) + 1) -' 1))),k))) by Def6

        .= (RN1 * ( SDSub_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),(n + 1))),k))) by NAT_D: 34;

        set XN = ( SD2SDSub ( DecSD (xn,n,k)));

        set X = ( SD2SDSub ( DecSD (x,(n + 1),k)));

        deffunc Q( Nat) = ( SDSub2INTDigit (X,$1,k));

        consider xp be FinSequence of INT such that

         A10: ( len xp) = (n + 1) and

         A11: for i be Nat st i in ( dom xp) holds (xp . i) = Q(i) from FINSEQ_2:sch 1;

        

         A12: ( dom xp) = ( Seg (n + 1)) by A10, FINSEQ_1:def 3;

        

         A13: ( len ( SDSub2INT X)) = ((n + 1) + 1) by CARD_1:def 7;

        

         A14: for j be Nat st 1 <= j & j <= ( len ( SDSub2INT X)) holds (( SDSub2INT X) . j) = ((xp ^ <*( SDSub2INTDigit (X,((n + 1) + 1),k))*>) . j)

        proof

          let j be Nat;

          assume that

           A15: 1 <= j and

           A16: j <= ( len ( SDSub2INT X));

          j <= ((n + 1) + 1) by A16, CARD_1:def 7;

          then

           A17: j in ( Seg ((n + 1) + 1)) by A15, FINSEQ_1: 1;

          

           A18: j in ( dom ( SDSub2INT X)) by A15, A16, FINSEQ_3: 25;

          now

            per cases by A17, FINSEQ_2: 7;

              suppose

               A19: j in ( Seg (n + 1));

              then j in ( dom xp) by A10, FINSEQ_1:def 3;

              

              then ((xp ^ <*( SDSub2INTDigit (X,((n + 1) + 1),k))*>) . j) = (xp . j) by FINSEQ_1:def 7

              .= ( SDSub2INTDigit (X,j,k)) by A11, A12, A19

              .= (( SDSub2INT X) /. j) by A17, Def11

              .= (( SDSub2INT X) . j) by A18, PARTFUN1:def 6;

              hence thesis;

            end;

              suppose

               A20: j = ((n + 1) + 1);

              

               A21: j in ( dom ( SDSub2INT X)) by A13, A17, FINSEQ_1:def 3;

              ((xp ^ <*( SDSub2INTDigit (X,((n + 1) + 1),k))*>) . j) = ( SDSub2INTDigit (X,((n + 1) + 1),k)) by A10, A20, FINSEQ_1: 42

              .= (( SDSub2INT X) /. ((n + 1) + 1)) by A17, A20, Def11

              .= (( SDSub2INT X) . j) by A20, A21, PARTFUN1:def 6;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        ( Radix k) > 0 by RADIX_2: 6;

        then xn < (( Radix k) |^ n) by NAT_D: 1, PREPOWER: 6;

        then xn is_represented_by (n,k);

        

        then

         A22: xn = ( SDSub2IntOut ( SD2SDSub ( DecSD (xn,n,k)))) by A4, A6

        .= ( Sum ( SDSub2INT ( SD2SDSub ( DecSD (xn,n,k)))));

        

         A23: (n + 1) in ( Seg (n + 1)) by FINSEQ_1: 3;

        then

         A24: (n + 1) in ( Seg ((n + 1) + 1)) by FINSEQ_2: 8;

        consider xpp be FinSequence of INT such that

         A25: ( len xpp) = n and

         A26: for i be Nat st i in ( dom xpp) holds (xpp . i) = Q(i) from FINSEQ_2:sch 1;

        

         A27: ( dom xpp) = ( Seg n) by A25, FINSEQ_1:def 3;

        

         A28: for j be Nat st 1 <= j & j <= ( len xp) holds (xp . j) = ((xpp ^ <*( SDSub2INTDigit (X,(n + 1),k))*>) . j)

        proof

          let j be Nat;

          assume 1 <= j & j <= ( len xp);

          then

           A29: j in ( Seg (n + 1)) by A10, FINSEQ_1: 1;

          now

            per cases by A29, FINSEQ_2: 7;

              suppose

               A30: j in ( Seg n);

              then j in ( dom xpp) by A25, FINSEQ_1:def 3;

              

              then ((xpp ^ <*( SDSub2INTDigit (X,(n + 1),k))*>) . j) = (xpp . j) by FINSEQ_1:def 7

              .= ( SDSub2INTDigit (X,j,k)) by A26, A27, A30

              .= (xp . j) by A11, A12, A29;

              hence thesis;

            end;

              suppose

               A31: j = (n + 1);

              

              then ((xpp ^ <*( SDSub2INTDigit (X,(n + 1),k))*>) . j) = ( SDSub2INTDigit (X,(n + 1),k)) by A25, FINSEQ_1: 42

              .= (xp . j) by A11, A12, A29, A31;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        deffunc G( Nat) = ( SDSub2INTDigit (XN,$1,k));

        consider xnpp be FinSequence of INT such that

         A32: ( len xnpp) = n and

         A33: for i be Nat st i in ( dom xnpp) holds (xnpp . i) = G(i) from FINSEQ_2:sch 1;

        

         A34: ( dom xnpp) = ( Seg n) by A32, FINSEQ_1:def 3;

        for j be Nat st 1 <= j & j <= ( len xnpp) holds (xnpp . j) = (xpp . j)

        proof

          let j be Nat;

          assume 1 <= j & j <= ( len xnpp);

          then

           A35: j in ( Seg n) by A32, FINSEQ_1: 1;

          

          then (xpp . j) = ( SDSub2INTDigit (X,j,k)) by A26, A27

          .= ( SDSub2INTDigit (XN,j,k)) by A6, A35, Th20

          .= (xnpp . j) by A33, A34, A35;

          hence thesis;

        end;

        then

         A36: xpp = xnpp by A25, A32, FINSEQ_1: 14;

        

         A37: ( len ( SDSub2INT XN)) = (n + 1) by CARD_1:def 7;

        

         A38: for j be Nat st 1 <= j & j <= ( len ( SDSub2INT XN)) holds (( SDSub2INT XN) . j) = ((xnpp ^ <*( SDSub2INTDigit (XN,(n + 1),k))*>) . j)

        proof

          let j be Nat;

          assume

           A39: 1 <= j & j <= ( len ( SDSub2INT XN));

          then

           A40: j in ( Seg (n + 1)) by A37, FINSEQ_1: 1;

          

           A41: j in ( dom ( SDSub2INT XN)) by A39, FINSEQ_3: 25;

          now

            per cases by A40, FINSEQ_2: 7;

              suppose

               A42: j in ( Seg n);

              then j in ( dom xnpp) by A32, FINSEQ_1:def 3;

              

              then ((xnpp ^ <*( SDSub2INTDigit (XN,(n + 1),k))*>) . j) = (xnpp . j) by FINSEQ_1:def 7

              .= ( SDSub2INTDigit (XN,j,k)) by A33, A34, A42

              .= (( SDSub2INT XN) /. j) by A40, Def11

              .= (( SDSub2INT XN) . j) by A41, PARTFUN1:def 6;

              hence thesis;

            end;

              suppose

               A43: j = (n + 1);

              

               A44: j in ( dom ( SDSub2INT XN)) by A37, A40, FINSEQ_1:def 3;

              ((xnpp ^ <*( SDSub2INTDigit (XN,(n + 1),k))*>) . j) = ( SDSub2INTDigit (XN,(n + 1),k)) by A32, A43, FINSEQ_1: 42

              .= (( SDSub2INT XN) /. (n + 1)) by A40, A43, Def11

              .= (( SDSub2INT XN) . j) by A43, A44, PARTFUN1:def 6;

              hence thesis;

            end;

          end;

          hence thesis;

        end;

        ( len xp) = ( len (xpp ^ <*( SDSub2INTDigit (X,(n + 1),k))*>)) by A10, A25, FINSEQ_2: 16;

        then

         A45: xp = (xpp ^ <*( SDSub2INTDigit (X,(n + 1),k))*>) by A28, FINSEQ_1: 14;

        ( len (xp ^ <*( SDSub2INTDigit (X,((n + 1) + 1),k))*>)) = ((n + 1) + 1) by A10, FINSEQ_2: 16;

        then ( len ( SDSub2INT X)) = ( len (xp ^ <*( SDSub2INTDigit (X,((n + 1) + 1),k))*>)) by CARD_1:def 7;

        then ( SDSub2INT X) = (xp ^ <*( SDSub2INTDigit (X,((n + 1) + 1),k))*>) by A14, FINSEQ_1: 14;

        

        then

         A46: ( Sum ( SDSub2INT X)) = (( Sum xp) + ( SDSub2INTDigit (X,((n + 1) + 1),k))) by RVSUM_1: 74

        .= ((( Sum xnpp) + ( SDSub2INTDigit (X,(n + 1),k))) + ( SDSub2INTDigit (X,((n + 1) + 1),k))) by A45, A36, RVSUM_1: 74;

        set RNDIG = (RN * ( DigA (( DecSD (x,(n + 1),k)),(n + 1))));

        set RNSDC = (RN * ( SDSub_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),n)),k)));

        

         A47: ( Radix k) > 0 by RADIX_2: 6;

        ( len (xnpp ^ <*( SDSub2INTDigit (XN,(n + 1),k))*>)) = (n + 1) by A32, FINSEQ_2: 16;

        then ( SDSub2INT XN) = (xnpp ^ <*( SDSub2INTDigit (XN,(n + 1),k))*>) by A37, A38, FINSEQ_1: 14;

        then

         A48: (xn + 0 ) = (( Sum xnpp) + ( SDSub2INTDigit (XN,(n + 1),k))) by A22, RVSUM_1: 74;

        

         A49: ( SDSub2INTDigit (( SD2SDSub ( DecSD (x,(n + 1),k))),(n + 1),k)) = ((( Radix k) |^ n) * ( DigB_SDSub (( SD2SDSub ( DecSD (x,(n + 1),k))),(n + 1)))) by NAT_D: 34

        .= (RN * ( SD2SDSubDigitS (( DecSD (x,(n + 1),k)),(n + 1),k))) by A24, Def8

        .= (RN * ( SD2SDSubDigit (( DecSD (x,(n + 1),k)),(n + 1),k))) by A6, A24, Def7

        .= (RN * (( SDSub_Add_Data (( DigA (( DecSD (x,(n + 1),k)),(n + 1))),k)) + ( SDSub_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),((n + 1) -' 1))),k)))) by A23, Def6

        .= (RN * (( SDSub_Add_Data (( DigA (( DecSD (x,(n + 1),k)),(n + 1))),k)) + ( SDSub_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),n)),k)))) by NAT_D: 34

        .= (((RN * ( DigA (( DecSD (x,(n + 1),k)),(n + 1)))) - ((RN * ( Radix k)) * ( SDSub_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),(n + 1))),k)))) + (RN * ( SDSub_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),n)),k))))

        .= (((RN * ( DigA (( DecSD (x,(n + 1),k)),(n + 1)))) - (RN1 * ( SDSub_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),(n + 1))),k)))) + (RN * ( SDSub_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),n)),k)))) by NEWTON: 6;

        ( SDSub2INTDigit (( SD2SDSub ( DecSD (xn,n,k))),(n + 1),k)) = ((( Radix k) |^ n) * ( DigB_SDSub (( SD2SDSub ( DecSD (xn,n,k))),(n + 1)))) by NAT_D: 34

        .= (RN * ( SD2SDSubDigitS (( DecSD (xn,n,k)),(n + 1),k))) by A23, Def8

        .= (RN * ( SD2SDSubDigit (( DecSD (xn,n,k)),(n + 1),k))) by A23, A6, Def7

        .= (RN * ( SDSub_Add_Carry (( DigA (( DecSD (xn,n,k)),((n + 1) -' 1))),k))) by Def6

        .= (RN * ( SDSub_Add_Carry (( DigA (( DecSD (xn,n,k)),n)),k))) by NAT_D: 34

        .= (RN * ( SDSub_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),n)),k))) by A5, Lm5;

        

        then ( Sum ( SDSub2INT X)) = (((xn + RNDIG) - RNSDC) + RNSDC) by A46, A48, A49, A9

        .= (xn + (RN * (x div RN))) by A7, RADIX_1: 24;

        hence thesis by A47, NAT_D: 2, PREPOWER: 6;

      end;

      

       A50: P[1]

      proof

        

         A51: 1 in ( Seg 1) by FINSEQ_1: 1;

        (2 - 1) = 1;

        then

         A52: (2 -' 1) = 1 by XREAL_0:def 2;

        let k,x be Nat;

        assume that

         A53: k >= 2 and

         A54: x is_represented_by (1,k);

        set X = ( DecSD (x,1,k));

        reconsider CRY = (( Radix k) * ( SDSub_Add_Carry (( DigA (X,1)),k))) as Integer;

        reconsider DIG2 = CRY as Element of INT by INT_1:def 2;

        reconsider DIG1 = (( DigA (X,1)) - CRY) as Element of INT by INT_1:def 2;

        

         A55: 1 in ( Seg (1 + 1)) by FINSEQ_1: 1;

        

         A56: ( len ( SDSub2INT ( SD2SDSub X))) = (1 + 1) by CARD_1:def 7;

        then

         A57: 1 in ( dom ( SDSub2INT ( SD2SDSub X))) by A55, FINSEQ_1:def 3;

        

         A58: 2 in ( Seg (1 + 1)) by FINSEQ_1: 1;

        then

         A59: 2 in ( dom ( SDSub2INT ( SD2SDSub X))) by A56, FINSEQ_1:def 3;

        (( SDSub2INT ( SD2SDSub X)) /. 2) = ( SDSub2INTDigit (( SD2SDSub X),2,k)) by A58, Def11

        .= (( Radix k) * ( DigB_SDSub (( SD2SDSub X),2))) by A52

        .= (( Radix k) * ( SD2SDSubDigitS (X,2,k))) by A58, Def8

        .= (( Radix k) * ( SD2SDSubDigit (X,2,k))) by A53, A58, Def7

        .= (( Radix k) * ( SDSub_Add_Carry (( DigA (X,1)),k))) by A52, A58, Def6;

        then

         A60: (( SDSub2INT ( SD2SDSub X)) . 2) = CRY by A59, PARTFUN1:def 6;

        (( SDSub2INT ( SD2SDSub X)) /. 1) = ( SDSub2INTDigit (( SD2SDSub X),1,k)) by A55, Def11

        .= ((( Radix k) |^ 0 ) * ( DigB_SDSub (( SD2SDSub X),1))) by XREAL_1: 232

        .= (1 * ( DigB_SDSub (( SD2SDSub X),1))) by NEWTON: 4

        .= ( SD2SDSubDigitS (X,1,k)) by A55, Def8

        .= ( SD2SDSubDigit (X,1,k)) by A53, A55, Def7

        .= (( SDSub_Add_Data (( DigA (X,1)),k)) + ( SDSub_Add_Carry (( DigA (X,(1 -' 1))),k))) by A51, Def6

        .= (( SDSub_Add_Data (( DigA (X,1)),k)) + ( SDSub_Add_Carry (( DigA (X, 0 )),k))) by XREAL_1: 232

        .= (( SDSub_Add_Data (( DigA (X,1)),k)) + ( SDSub_Add_Carry ( 0 ,k))) by RADIX_1:def 3

        .= (( SDSub_Add_Data (( DigA (X,1)),k)) + 0 ) by Th16

        .= (( DigA (X,1)) - (( Radix k) * ( SDSub_Add_Carry (( DigA (X,1)),k))));

        then (( SDSub2INT ( SD2SDSub X)) . 1) = (( DigA (X,1)) - CRY) by A57, PARTFUN1:def 6;

        then ( SDSub2INT ( SD2SDSub X)) = <*DIG1, DIG2*> by A56, A60, FINSEQ_1: 44;

        

        then ( Sum ( SDSub2INT ( SD2SDSub X))) = (DIG1 + DIG2) by RVSUM_1: 77

        .= x by A54, RADIX_1: 21;

        hence thesis;

      end;

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

      hence thesis by A1;

    end;