radix_1.miz



    begin

    reserve k,m,n for Nat,

i1,i2,i3 for Integer,

e for set;

    theorem :: RADIX_1:1

    

     Th1: (n mod k) = (k - 1) implies ((n + 1) mod k) = 0 by NAT_D: 69;

    theorem :: RADIX_1:2

    

     Th2: (n mod k) < (k - 1) implies ((n + 1) mod k) = ((n mod k) + 1) by NAT_D: 70;

    theorem :: RADIX_1:3

    

     Th3: m <> 0 implies ((k mod (m * n)) mod n) = (k mod n)

    proof

      assume

       A1: m <> 0 ;

      per cases ;

        suppose

         A2: n <> 0 ;

        reconsider k9 = k, m9 = m, n9 = n as Integer;

        (m9 * n9) <> 0 by A1, A2, XCMPLX_1: 6;

        

        hence ((k mod (m * n)) mod n) = ((k9 - ((k9 div (m9 * n9)) * (m9 * n9))) mod n9) by INT_1:def 10

        .= ((k9 + (( - (m9 * (k9 div (m9 * n9)))) * n9)) mod n9)

        .= (k mod n) by EULER_1: 12;

      end;

        suppose

         A3: n = 0 ;

        

        hence ((k mod (m * n)) mod n) = 0 by NAT_D:def 2

        .= (k mod n) by A3, NAT_D:def 2;

      end;

    end;

    theorem :: RADIX_1:4

    k <> 0 implies ((n + 1) mod k) = 0 or ((n + 1) mod k) = ((n mod k) + 1)

    proof

      assume

       A1: k <> 0 ;

      then k >= 1 by NAT_1: 14;

      then

      reconsider K = (k - 1) as Element of NAT by INT_1: 3, XREAL_1: 48;

      (n mod k) < ((k - 1) + 1) by A1, NAT_D: 1;

      then

       A2: (n mod k) <= K by NAT_1: 13;

      per cases by A2, XXREAL_0: 1;

        suppose (n mod k) < (k - 1);

        hence thesis by Th2;

      end;

        suppose (n mod k) = (k - 1);

        hence thesis by Th1;

      end;

    end;

    reserve i,k,m,n,p,x,y for Nat;

    theorem :: RADIX_1:5

    

     Th5: i <> 0 & k <> 0 implies ((n mod (i |^ k)) div (i |^ (k -' 1))) < i

    proof

      assume that

       A1: i <> 0 and

       A2: k <> 0 ;

      

       A3: (n mod (i |^ k)) < (i |^ k) by A1, NAT_D: 1, PREPOWER: 6;

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

      set I1 = (i |^ (k -' 1));

      set T = (n mod (i |^ k));

      (i |^ k) = (i * (i |^ (k -' 1))) by A1, A2, PEPIN: 26;

      

      then (T mod I1) = (n mod I1) by A1, Th3

      .= (n - (I1 * (n div I1))) by A1, NEWTON: 63, PREPOWER: 6;

      then T = ((I1 * (T div I1)) + (n - (I1 * (n div I1)))) by A1, NAT_D: 2, PREPOWER: 6;

      then

       A4: ((I1 * (T div I1)) + (n - (I1 * (n div I1)))) < (i * I1) by A1, A2, A3, PEPIN: 26;

      

       A5: I1 <> 0 by A1, PREPOWER: 6;

       [\(n / I1)/] <= (n / I1) by INT_1:def 6;

      then (n div I1) = [\(n / I1)/] & ((T div I1) + [\(n / I1)/]) <= ((T div I1) + (n / I1)) by INT_1:def 9, XREAL_1: 6;

      then

       A6: (((T div I1) + [\(n / I1)/]) - [\(n / I1)/]) <= (((T div I1) + (n / I1)) - (n div I1)) by XREAL_1: 9;

      I1 > 0 by A1, PREPOWER: 6;

      then ((((I1 * (T div I1)) + n) - (I1 * (n div I1))) / I1) < ((i * I1) / I1) by A4, XREAL_1: 74;

      then ((((I1 * (T div I1)) / I1) + (n / I1)) - ((I1 * (n div I1)) / I1)) < ((i * I1) / I1) by XCMPLX_1: 124;

      then (((T div I1) + (n / I1)) - ((I1 * (n div I1)) / I1)) < ((i * I1) / I1) by A5, XCMPLX_1: 89;

      then (((T div I1) + (n / I1)) - (n div I1)) < ((i * I1) / I1) by A5, XCMPLX_1: 89;

      then (((T div I1) + (n / I1)) - (n div I1)) < i by A5, XCMPLX_1: 89;

      hence thesis by A6, XXREAL_0: 2;

    end;

    ::$Canceled

    theorem :: RADIX_1:7

    i2 > 0 & i3 >= 0 implies ((i1 mod (i2 * i3)) mod i3) = (i1 mod i3)

    proof

      assume that

       A1: i2 > 0 and

       A2: i3 >= 0 ;

      per cases by A2;

        suppose i3 > 0 ;

        then (i2 * i3) <> 0 by A1, XCMPLX_1: 6;

        

        then ((i1 mod (i2 * i3)) mod i3) = ((i1 - ((i1 div (i2 * i3)) * (i2 * i3))) mod i3) by INT_1:def 10

        .= ((i1 + (( - (i2 * (i1 div (i2 * i3)))) * i3)) mod i3);

        hence thesis by EULER_1: 12;

      end;

        suppose

         A3: i3 = 0 ;

        then ((i1 mod (i2 * i3)) mod i3) = 0 by INT_1:def 10;

        hence thesis by A3, INT_1:def 10;

      end;

    end;

    begin

    definition

      let n be Nat;

      :: RADIX_1:def1

      func Radix (n) -> Element of NAT equals (2 to_power n);

      correctness by ORDINAL1:def 12;

    end

    definition

      let k be Nat;

      :: RADIX_1:def2

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

      correctness ;

    end

    

     Lm1: for k be Nat st k >= 2 holds ( Radix k) >= (2 + 2)

    proof

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

      let k;

      

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

      proof

        let kk be Nat;

        assume kk >= 2;

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

        .= (( Radix kk) * 2);

        then

         A2: ( Radix (kk + 1)) >= ( Radix kk) by XREAL_1: 155;

        assume ( Radix kk) >= (2 + 2);

        hence thesis by A2, XXREAL_0: 2;

      end;

      ( Radix 2) = (2 to_power (1 + 1))

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

      .= (2 * (2 to_power 1))

      .= (2 * 2);

      then

       A3: P[2];

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

      hence thesis;

    end;

    theorem :: RADIX_1:8

    

     Th7: for e be object holds e in ( 0 -SD ) iff e = 0

    proof

      let e be object;

      

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

      hereby

        assume e in ( 0 -SD );

        then ex b be Element of INT st e = b & b <= 0 & b >= 0 by A1;

        hence e = 0 ;

      end;

      assume

       A2: e = 0 ;

      then e is Element of INT by INT_1:def 2;

      hence thesis by A1, A2;

    end;

    theorem :: RADIX_1:9

    ( 0 -SD ) = { 0 } by Th7, TARSKI:def 1;

    theorem :: RADIX_1:10

    

     Th9: (k -SD ) c= ((k + 1) -SD )

    proof

      let e be object;

      assume e in (k -SD );

      then

      consider g be Element of INT such that

       A1: e = g and

       A2: g <= (( Radix k) - 1) and

       A3: g >= (( - ( Radix k)) + 1);

      k < (k + 1) by NAT_1: 13;

      then

       A4: (2 to_power k) < (2 to_power (k + 1)) by POWER: 39;

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

      then (( - ( Radix k)) + 1) > (( - ( Radix (k + 1))) + 1) by XREAL_1: 6;

      then

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

      (( Radix k) - 1) < (( Radix (k + 1)) - 1) by A4, XREAL_1: 9;

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

      hence thesis by A1, A5;

    end;

    theorem :: RADIX_1:11

    

     Th10: e in (k -SD ) implies e is Integer

    proof

      assume e in (k -SD );

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

      hence thesis;

    end;

    theorem :: RADIX_1:12

    

     Th11: (k -SD ) c= INT

    proof

      let e be object;

      assume e in (k -SD );

      then e is Integer by Th10;

      hence thesis by INT_1:def 2;

    end;

    theorem :: RADIX_1:13

    

     Th12: i1 in (k -SD ) implies i1 <= (( Radix k) - 1) & i1 >= (( - ( Radix k)) + 1)

    proof

      assume i1 in (k -SD );

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

      hence thesis;

    end;

    theorem :: RADIX_1:14

    

     Th13: 0 in (k -SD )

    proof

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

      

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

      proof

        let kk be Nat;

        assume

         A2: 0 in (kk -SD );

        (kk -SD ) c= ((kk + 1) -SD ) by Th9;

        hence thesis by A2;

      end;

      

       A3: P[ 0 ] by Th7;

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

      hence thesis;

    end;

    registration

      let k be Nat;

      cluster (k -SD ) -> non empty;

      coherence by Th13;

    end

    definition

      let k be Nat;

      :: original: -SD

      redefine

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

      coherence by Th11;

    end

    begin

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

    theorem :: RADIX_1:15

    

     Th14: i in ( Seg n) implies (a . i) is Element of (k -SD )

    proof

      

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

      assume i in ( Seg n);

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

      then

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

      ( rng a) c= (k -SD ) by FINSEQ_1:def 4;

      hence thesis by A2;

    end;

    definition

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

      :: RADIX_1:def3

      func DigA (x,i) -> Integer equals

      : Def3: (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_1:def4

      func DigB (x,i) -> Element of INT equals ( DigA (x,i));

      coherence by INT_1:def 2;

    end

    theorem :: RADIX_1:16

    

     Th15: i in ( Seg n) implies ( DigA (a,i)) is Element of (k -SD )

    proof

      assume

       A1: i in ( Seg n);

      then (a . i) = ( DigA (a,i)) by Def3;

      hence thesis by A1, Th14;

    end;

    theorem :: RADIX_1:17

    

     Th16: for x be Tuple of 1, INT st (x /. 1) = m holds x = <*m*>

    proof

      let x be Tuple of 1, INT ;

      assume

       A1: (x /. 1) = m;

      

       A2: ( len x) = 1 by CARD_1:def 7;

      then (x /. 1) = (x . 1) by FINSEQ_4: 15;

      hence thesis by A1, A2, FINSEQ_1: 40;

    end;

    definition

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

      :: RADIX_1:def5

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

      coherence by INT_1:def 2;

    end

    definition

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

      :: RADIX_1:def6

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

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

      existence

      proof

        deffunc F( Nat) = ( SubDigit (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;

        reconsider z as Tuple of n, INT by A1, CARD_1:def 7;

        take z;

        let i be Nat;

        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

        .= ( SubDigit (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) = ( SubDigit (x,i,k)) and

         A6: for i be Nat st i in ( Seg n) holds (k2 /. i) = ( SubDigit (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

          .= ( SubDigit (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 );

      :: RADIX_1:def7

      func SDDec (x) -> Integer equals ( Sum ( DigitSD x));

      coherence ;

    end

    definition

      let i,k,x be Nat;

      :: RADIX_1:def8

      func DigitDC (x,i,k) -> Element of (k -SD ) equals ((x mod (( Radix k) |^ i)) div (( Radix k) |^ (i -' 1)));

      coherence

      proof

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

        set T = (( Radix k) |^ i);

        set S = (( Radix k) |^ (i -' 1));

        defpred P[ Nat] means (($1 mod T) div S) is Element of (k -SD );

        

         A1: 0 in (k -SD ) by Th13;

        

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

        then

         A3: S > 0 by NAT_1: 14, PREPOWER: 11;

        then

         A4: ( 0 div S) = 0 by NAT_D: 27;

        

         A5: ( Radix k) >= 1 by A2, NAT_1: 14;

        

         A6: for x be Nat st P[x] holds P[(x + 1)]

        proof

          reconsider R = (( Radix k) - 1) as Element of NAT by A5, INT_1: 3, XREAL_1: 48;

          let xx be Nat;

          assume ((xx mod T) div S) is Element of (k -SD );

          set X = (((xx + 1) mod T) div S);

          per cases ;

            suppose

             A7: i = 0 ;

            (( Radix k) |^ i) = (( Radix k) to_power i)

            .= 1 by A7, POWER: 24;

            

            then ((xx + 1) mod T) = (((xx + 1) * 1) mod 1)

            .= 0 by NAT_D: 13;

            then X = 0 by A3, NAT_D: 27;

            hence thesis by Th13;

          end;

            suppose

             A8: i > 0 ;

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

            then

             A9: X is Element of INT & 0 >= (( - ( Radix k)) + 1) by INT_1:def 2, XREAL_1: 59;

            X < ((( Radix k) - 1) + 1) by A2, A8, Th5;

            then X <= R by NAT_1: 13;

            then X in (k -SD ) by A9;

            hence thesis;

          end;

        end;

        T > 0 by A2, NAT_1: 14, PREPOWER: 11;

        then

         A10: P[ 0 ] by A4, A1, NAT_D: 24;

        for x be Nat holds P[x] from NAT_1:sch 2( A10, A6);

        hence thesis;

      end;

    end

    definition

      let k,n,x be Nat;

      :: RADIX_1:def9

      func DecSD (x,n,k) -> Tuple of n, (k -SD ) means

      : Def9: for i be Nat st i in ( Seg n) holds ( DigA (it ,i)) = ( DigitDC (x,i,k));

      existence

      proof

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

        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;

        reconsider z as Tuple of n, (k -SD ) by A1, CARD_1:def 7;

        take z;

        let i;

        assume

         A4: i in ( Seg n);

        

        hence ( DigA (z,i)) = (z . i) by Def3

        .= ( DigitDC (x,i,k)) 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)) = ( DigitDC (x,i,k)) and

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

        

         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, Def3

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

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

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

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

        end;

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

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    begin

    definition

      let x be Integer;

      :: RADIX_1:def10

      func SD_Add_Carry (x) -> Integer equals

      : Def10: 1 if x > 2,

( - 1) if x < ( - 2)

      otherwise 0 ;

      coherence ;

      consistency ;

    end

    theorem :: RADIX_1:18

    

     Th17: ( SD_Add_Carry 0 ) = 0 by Def10;

    

     Lm2: for x be Integer holds ( - 1) <= ( SD_Add_Carry x) & ( SD_Add_Carry x) <= 1

    proof

      let x be Integer;

      per cases ;

        suppose x < ( - 2);

        hence thesis by Def10;

      end;

        suppose ( - 2) <= x & x <= 2;

        hence thesis by Def10;

      end;

        suppose x > 2;

        hence thesis by Def10;

      end;

    end;

    definition

      let x be Integer, k be Nat;

      :: RADIX_1:def11

      func SD_Add_Data (x,k) -> Integer equals (x - (( SD_Add_Carry x) * ( Radix k)));

      coherence ;

    end

    theorem :: RADIX_1:19

    ( SD_Add_Data ( 0 ,k)) = 0 by Th17;

    theorem :: RADIX_1:20

    

     Th19: k >= 2 & i1 in (k -SD ) & i2 in (k -SD ) implies (( - ( Radix k)) + 2) <= ( SD_Add_Data ((i1 + i2),k)) & ( SD_Add_Data ((i1 + i2),k)) <= (( Radix k) - 2)

    proof

      assume that

       A1: k >= 2 and

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

      

       A3: (( - ( Radix k)) + 1) <= i1 & (( - ( Radix k)) + 1) <= i2 by A2, Th12;

      set z = (i1 + i2);

      i1 <= (( Radix k) - 1) & i2 <= (( Radix k) - 1) by A2, Th12;

      then

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

      per cases ;

        suppose

         A5: z < ( - 2);

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

        then

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

        ( SD_Add_Carry z) = ( - 1) & (z + ( Radix k)) < (( - 2) + ( Radix k)) by A5, Def10, XREAL_1: 6;

        hence thesis by A6, XREAL_1: 20;

      end;

        suppose

         A7: ( - 2) <= z & z <= 2;

        

         A8: ( Radix k) >= (2 + 2) by A1, Lm1;

        then

         A9: (( Radix k) - 2) >= 2 by XREAL_1: 19;

        ( - ( Radix k)) <= ( - (2 + 2)) by A8, XREAL_1: 24;

        then ( - ( Radix k)) <= (( - 2) + ( - 2));

        then

         A10: (( - ( Radix k)) - ( - 2)) <= ( - 2) by XREAL_1: 20;

        ( SD_Add_Carry z) = 0 by A7, Def10;

        hence thesis by A7, A9, A10, XXREAL_0: 2;

      end;

        suppose

         A11: z > 2;

        

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

        ( SD_Add_Carry z) = 1 & (z - ( Radix k)) > (2 - ( Radix k)) by A11, Def10, XREAL_1: 9;

        hence thesis by A12, XREAL_1: 20;

      end;

    end;

    begin

    definition

      let n,x,k be Nat;

      :: RADIX_1:def12

      pred x is_represented_by n,k means x < (( Radix k) |^ n);

    end

    theorem :: RADIX_1:21

    

     Th20: m is_represented_by (1,k) implies ( DigA (( DecSD (m,1,k)),1)) = m

    proof

      assume m is_represented_by (1,k);

      then

       A1: m < (( Radix k) |^ 1);

      1 in ( Seg 1) by FINSEQ_1: 1;

      

      hence ( DigA (( DecSD (m,1,k)),1)) = ( DigitDC (m,1,k)) by Def9

      .= ((m mod (( Radix k) |^ 1)) div (( Radix k) |^ 0 )) by XREAL_1: 232

      .= ((m mod (( Radix k) |^ 1)) div 1) by NEWTON: 4

      .= (m mod (( Radix k) |^ 1)) by NAT_2: 4

      .= m by A1, NAT_D: 24;

    end;

    theorem :: RADIX_1:22

    for n st n >= 1 holds for m st m is_represented_by (n,k) holds m = ( SDDec ( DecSD (m,n,k)))

    proof

      let n;

      defpred P[ Nat] means for m st m is_represented_by ($1,k) holds m = ( SDDec ( DecSD (m,$1,k)));

      

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

      proof

        let u be Nat;

        assume that u >= 1 and

         A2: P[u];

        p is_represented_by ((u + 1),k) implies p = ( SDDec ( DecSD (p,(u + 1),k)))

        proof

          set I = (u + 1);

          set R = (( Radix k) |^ u);

          set M = (p mod R);

          set N = (R * (p div R));

          

           A3: (I -' 1) = u by NAT_D: 34;

          

           A4: (u + 1) <= ( len ( DigitSD ( DecSD (p,(u + 1),k)))) by CARD_1:def 7;

          

           A5: 1 <= (u + 1) by NAT_1: 12;

          then

           A6: (u + 1) in ( Seg (u + 1)) by FINSEQ_1: 1;

          assume p is_represented_by ((u + 1),k);

          then p < (( Radix k) |^ (u + 1));

          then (p div R) = ( DigitDC (p,(u + 1),k)) by A3, NAT_D: 24;

          

          then

           A7: N = ( SubDigit (( DecSD (p,(u + 1),k)),(u + 1),k)) by A3, A6, Def9

          .= (( DigitSD ( DecSD (p,(u + 1),k))) /. (u + 1)) by A6, Def6

          .= (( DigitSD ( DecSD (p,(u + 1),k))) . (u + 1)) by A4, FINSEQ_4: 15, NAT_1: 12;

          

           A8: (( DigitSD ( DecSD (M,u,k))) ^ <*N*>) = ( DigitSD ( DecSD (p,(u + 1),k)))

          proof

            N is Element of INT by INT_1:def 2;

            then

            reconsider z1 = <*N*> as FinSequence of INT by FINSEQ_1: 74;

            reconsider DD = ( DigitSD ( DecSD (p,(u + 1),k))) as FinSequence of INT ;

            set z0 = ( DigitSD ( DecSD (M,u,k)));

            reconsider z = (z0 ^ z1) as FinSequence of INT ;

            

             A9: ( len z) = (( len ( DigitSD ( DecSD (M,u,k)))) + ( len <*N*>)) by FINSEQ_1: 22

            .= (u + ( len <*N*>)) by CARD_1:def 7

            .= (u + 1) by FINSEQ_1: 39;

            

             A10: for i be Nat st 1 <= i & i <= ( len z) holds (z /. i) = (DD /. i)

            proof

              let i be Nat;

              assume 1 <= i & i <= ( len z);

              then

               A11: i in ( Seg (u + 1)) by A9, FINSEQ_1: 1;

              per cases by A11, FINSEQ_2: 7;

                suppose

                 A12: i in ( Seg u);

                

                 A13: (M mod (( Radix k) |^ i)) = (p mod (( Radix k) |^ i))

                proof

                  i <= u by A12, FINSEQ_1: 1;

                  then (( Radix k) |^ i) divides (( Radix k) |^ u) by NEWTON: 89;

                  then

                  consider t be Nat such that

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

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

                  then t <> 0 by A14, PREPOWER: 5;

                  hence thesis by A14, Th3;

                end;

                

                 A15: i in ( dom (z0 ^ z1)) by A9, A11, FINSEQ_1:def 3;

                ( len DD) = (u + 1) by CARD_1:def 7;

                then

                 A16: i in ( dom DD) by A11, FINSEQ_1:def 3;

                then

                 A17: (DD . i) = (DD /. i) by PARTFUN1:def 6;

                

                 A18: (DD . i) = (( DigitSD ( DecSD (p,(u + 1),k))) /. i) by A16, PARTFUN1:def 6

                .= ( SubDigit (( DecSD (p,(u + 1),k)),i,k)) by A11, Def6

                .= ((( Radix k) |^ (i -' 1)) * ( DigitDC (p,i,k))) by A11, Def9

                .= ((( Radix k) |^ (i -' 1)) * ((p mod (( Radix k) |^ i)) div (( Radix k) |^ (i -' 1))));

                ( len z0) = u by CARD_1:def 7;

                then

                 A19: i in ( dom z0) by A12, FINSEQ_1:def 3;

                

                then ((z0 ^ z1) . i) = (( DigitSD ( DecSD (M,u,k))) . i) by FINSEQ_1:def 7

                .= (( DigitSD ( DecSD (M,u,k))) /. i) by A19, PARTFUN1:def 6

                .= ( SubDigit (( DecSD (M,u,k)),i,k)) by A12, Def6

                .= ((( Radix k) |^ (i -' 1)) * ( DigitDC (M,i,k))) by A12, Def9

                .= ((( Radix k) |^ (i -' 1)) * ((p mod (( Radix k) |^ i)) div (( Radix k) |^ (i -' 1)))) by A13;

                hence thesis by A18, A17, A15, PARTFUN1:def 6;

              end;

                suppose

                 A20: i = (u + 1);

                

                hence (z /. i) = (z . (u + 1)) by A5, A9, FINSEQ_4: 15

                .= ((z0 ^ z1) . (( len z0) + 1)) by CARD_1:def 7

                .= (( DigitSD ( DecSD (p,(u + 1),k))) . (u + 1)) by A7, FINSEQ_1: 42

                .= (DD /. i) by A4, A20, FINSEQ_4: 15, NAT_1: 12;

              end;

            end;

            ( len DD) = (u + 1) by CARD_1:def 7;

            hence thesis by A9, A10, FINSEQ_5: 13;

          end;

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

          then

           A21: R <> 0 by PREPOWER: 5;

          then M < R by NAT_D: 1;

          then

           A22: M is_represented_by (u,k);

          p = ((R * (p div R)) + (p mod R)) by A21, NAT_D: 2;

          then p = (( SDDec ( DecSD (M,u,k))) + N) by A2, A22;

          hence thesis by A8, RVSUM_1: 74;

        end;

        hence thesis;

      end;

      

       A23: P[1]

      proof

        let m;

        assume

         A24: m is_represented_by (1,k);

        reconsider i = m as Element of REAL by XREAL_0:def 1;

        reconsider M = <*i*> as FinSequence of REAL ;

        

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

        ( SubDigit (( DecSD (m,1,k)),1,k)) = ((( Radix k) |^ 0 ) * ( DigB (( DecSD (m,1,k)),1))) by XREAL_1: 232

        .= (1 * ( DigB (( DecSD (m,1,k)),1))) by NEWTON: 4

        .= m by A24, Th20;

        then (( DigitSD ( DecSD (m,1,k))) /. 1) = m by A25, Def6;

        

        hence ( SDDec ( DecSD (m,1,k))) = ( Sum M) by Th16

        .= m by FINSOP_1: 11;

      end;

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

      hence thesis;

    end;

    theorem :: RADIX_1:23

    

     Th22: m is_represented_by (1,k) & n is_represented_by (1,k) implies ( SD_Add_Carry (( DigA (( DecSD (m,1,k)),1)) + ( DigA (( DecSD (n,1,k)),1)))) = ( SD_Add_Carry (m + n))

    proof

      assume that

       A1: m is_represented_by (1,k) and

       A2: n is_represented_by (1,k);

      ( SD_Add_Carry (( DigA (( DecSD (m,1,k)),1)) + ( DigA (( DecSD (n,1,k)),1)))) = ( SD_Add_Carry (m + ( DigA (( DecSD (n,1,k)),1)))) by A1, Th20

      .= ( SD_Add_Carry (m + n)) by A2, Th20;

      hence thesis;

    end;

    

     Lm3: 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, Def9

      .= ( DigitDC (m,i,k)) by A5, A6, Th3

      .= ( DigA (( DecSD (m,(n + 1),k)),i)) by A4, Def9;

      hence thesis;

    end;

    theorem :: RADIX_1:24

    

     Th23: m is_represented_by ((n + 1),k) implies ( DigA (( DecSD (m,(n + 1),k)),(n + 1))) = (m div (( Radix k) |^ n))

    proof

      assume m is_represented_by ((n + 1),k);

      then

       A1: m < (( Radix k) |^ (n + 1));

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

      

      then ( DigA (( DecSD (m,(n + 1),k)),(n + 1))) = ( DigitDC (m,(n + 1),k)) by Def9

      .= (m div (( Radix k) |^ ((n + 1) -' 1))) by A1, NAT_D: 24

      .= (m div (( Radix k) |^ n)) by NAT_D: 34;

      hence thesis;

    end;

    begin

    definition

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

      assume that

       A1: i in ( Seg n) and

       A2: k >= 2;

      :: RADIX_1:def13

      func Add (x,y,i,k) -> Element of (k -SD ) equals

      : Def13: (( SD_Add_Data ((( DigA (x,i)) + ( DigA (y,i))),k)) + ( SD_Add_Carry (( DigA (x,(i -' 1))) + ( DigA (y,(i -' 1))))));

      coherence

      proof

        set SDC = ( SD_Add_Carry (( DigA (x,(i -' 1))) + ( DigA (y,(i -' 1)))));

        set SDD = ( SD_Add_Data ((( DigA (x,i)) + ( DigA (y,i))),k));

        

         A3: ( - 1) <= SDC by Lm2;

        

         A4: SDC <= 1 by Lm2;

        

         A5: ( DigA (x,i)) is Element of (k -SD ) & ( DigA (y,i)) is Element of (k -SD ) by A1, Th15;

        then SDD <= (( Radix k) - 2) by A2, Th19;

        then

         A6: (SDD + SDC) <= ((( Radix k) - 2) + 1) by A4, XREAL_1: 7;

        (( - ( Radix k)) + 2) <= SDD by A2, A5, Th19;

        then (SDD + SDC) is Element of INT & ((( - ( Radix k)) + 2) + ( - 1)) <= (SDD + SDC) by A3, INT_1:def 2, XREAL_1: 7;

        then (SDD + SDC) in (k -SD ) by A6;

        hence thesis;

      end;

    end

    definition

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

      :: RADIX_1:def14

      func x '+' y -> Tuple of n, (k -SD ) means

      : Def14: for i st i in ( Seg n) holds ( DigA (it ,i)) = ( Add (x,y,i,k));

      existence

      proof

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

        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;

        reconsider z as Tuple of n, (k -SD ) by A1, CARD_1:def 7;

        take z;

        let i;

        assume

         A4: i in ( Seg n);

        

        hence ( DigA (z,i)) = (z . i) by Def3

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

      end;

      uniqueness

      proof

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

         A5: for i st i in ( Seg n) holds ( DigA (k1,i)) = ( Add (x,y,i,k)) and

         A6: for i st i in ( Seg n) holds ( DigA (k2,i)) = ( Add (x,y,i,k));

        

         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, Def3

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

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

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

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

        end;

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

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    theorem :: RADIX_1:25

    

     Th24: k >= 2 & m is_represented_by (1,k) & n is_represented_by (1,k) implies ( SDDec (( DecSD (m,1,k)) '+' ( DecSD (n,1,k)))) = ( SD_Add_Data ((m + n),k))

    proof

      assume that

       A1: k >= 2 and

       A2: m is_represented_by (1,k) and

       A3: n is_represented_by (1,k);

      set N = ( DecSD (n,1,k));

      set M = ( DecSD (m,1,k));

      

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

      

      then

       A5: ( DigA ((M '+' N),1)) = ( Add (M,N,1,k)) by Def14

      .= (( SD_Add_Data ((( DigA (M,1)) + ( DigA (N,1))),k)) + ( SD_Add_Carry (( DigA (M,(1 -' 1))) + ( DigA (N,(1 -' 1)))))) by A1, A4, Def13

      .= (( SD_Add_Data ((( DigA (M,1)) + ( DigA (N,1))),k)) + ( SD_Add_Carry (( DigA (M, 0 )) + ( DigA (N,(1 -' 1)))))) by XREAL_1: 232

      .= (( SD_Add_Data ((( DigA (M,1)) + ( DigA (N,1))),k)) + ( SD_Add_Carry (( DigA (M, 0 )) + ( DigA (N, 0 ))))) by XREAL_1: 232

      .= (( SD_Add_Data ((( DigA (M,1)) + ( DigA (N,1))),k)) + ( SD_Add_Carry ( 0 + ( DigA (N, 0 ))))) by Def3

      .= (( SD_Add_Data ((( DigA (M,1)) + ( DigA (N,1))),k)) + 0 ) by Def3, Th17

      .= ( SD_Add_Data ((m + ( DigA (N,1))),k)) by A2, Th20

      .= ( SD_Add_Data ((m + n),k)) by A3, Th20;

      

       A6: (( DigitSD (M '+' N)) /. 1) = ( SubDigit ((M '+' N),1,k)) by A4, Def6

      .= ((( Radix k) |^ 0 ) * ( DigA ((M '+' N),1))) by XREAL_1: 232

      .= (1 * ( DigA ((M '+' N),1))) by NEWTON: 4

      .= ( SD_Add_Data ((m + n),k)) by A5;

      reconsider w = ( SD_Add_Data ((m + n),k)) as Element of INT by INT_1:def 2;

      

       A7: ( len ( DigitSD (M '+' N))) = 1 by CARD_1:def 7;

      1 in ( Seg 1) by FINSEQ_1: 1;

      then 1 in ( dom ( DigitSD (M '+' N))) by A7, FINSEQ_1:def 3;

      then (( DigitSD (M '+' N)) . 1) = ( SD_Add_Data ((m + n),k)) by A6, PARTFUN1:def 6;

      

      then ( SDDec (M '+' N)) = ( Sum <*w*>) by A7, FINSEQ_1: 40

      .= ( SD_Add_Data ((m + n),k)) by RVSUM_1: 73;

      hence thesis;

    end;

    theorem :: RADIX_1:26

    for n st n >= 1 holds for k, x, y st k >= 2 & x is_represented_by (n,k) & y is_represented_by (n,k) holds (x + y) = (( SDDec (( DecSD (x,n,k)) '+' ( DecSD (y,n,k)))) + ((( Radix k) |^ n) * ( SD_Add_Carry (( DigA (( DecSD (x,n,k)),n)) + ( DigA (( DecSD (y,n,k)),n))))))

    proof

      defpred P[ Nat] means for k,x,y be Nat st k >= 2 & x is_represented_by ($1,k) & y is_represented_by ($1,k) holds (x + y) = (( SDDec (( DecSD (x,$1,k)) '+' ( DecSD (y,$1,k)))) + ((( Radix k) |^ $1) * ( SD_Add_Carry (( DigA (( DecSD (x,$1,k)),$1)) + ( DigA (( DecSD (y,$1,k)),$1))))));

      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,y be Nat;

        

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

        set z = (( DecSD (x,(n + 1),k)) '+' ( DecSD (y,(n + 1),k)));

        set yn = (y mod (( Radix k) |^ n));

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

        assume that

         A7: k >= 2 and

         A8: x is_represented_by ((n + 1),k) and

         A9: y is_represented_by ((n + 1),k);

        set zn = (( DecSD (xn,n,k)) '+' ( DecSD (yn,n,k)));

        

         A10: ( len ( DigitSD zn)) = n by CARD_1:def 7;

        

         A11: ( len ( DigitSD z)) = (n + 1) by CARD_1:def 7;

        

         A12: for i be Nat st 1 <= i & i <= ( len ( DigitSD z)) holds (( DigitSD z) . i) = ((( DigitSD zn) ^ <*( SubDigit (z,(n + 1),k))*>) . i)

        proof

          let i be Nat;

          assume that

           A13: 1 <= i and

           A14: i <= ( len ( DigitSD z));

          

           A15: (i -' 1) = (i - 1) by A13, XREAL_1: 233;

          

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

          then

           A17: i in ( Seg (n + 1)) by A13, FINSEQ_1: 1;

          then

           A18: i in ( dom ( DigitSD z)) by A11, FINSEQ_1:def 3;

          per cases by A17, FINSEQ_2: 7;

            suppose

             A19: i in ( Seg n);

            then

             A20: i in ( dom ( DigitSD zn)) by A10, FINSEQ_1:def 3;

            

            then

             A21: ((( DigitSD zn) ^ <*( SubDigit (z,(n + 1),k))*>) . i) = (( DigitSD zn) . i) by FINSEQ_1:def 7

            .= (( DigitSD zn) /. i) by A20, PARTFUN1:def 6

            .= ( SubDigit (zn,i,k)) by A19, Def6

            .= ((( Radix k) |^ (i -' 1)) * ( Add (( DecSD (xn,n,k)),( DecSD (yn,n,k)),i,k))) by A19, Def14

            .= ((( Radix k) |^ (i -' 1)) * (( SD_Add_Data ((( DigA (( DecSD (xn,n,k)),i)) + ( DigA (( DecSD (yn,n,k)),i))),k)) + ( SD_Add_Carry (( DigA (( DecSD (xn,n,k)),(i -' 1))) + ( DigA (( DecSD (yn,n,k)),(i -' 1))))))) by A7, A19, Def13;

            

             A22: (( DigitSD z) . i) = (( DigitSD z) /. i) by A18, PARTFUN1:def 6

            .= ( SubDigit (z,i,k)) by A17, Def6

            .= ((( Radix k) |^ (i -' 1)) * ( Add (( DecSD (x,(n + 1),k)),( DecSD (y,(n + 1),k)),i,k))) by A17, Def14

            .= ((( Radix k) |^ (i -' 1)) * (( SD_Add_Data ((( DigA (( DecSD (x,(n + 1),k)),i)) + ( DigA (( DecSD (y,(n + 1),k)),i))),k)) + ( SD_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),(i -' 1))) + ( DigA (( DecSD (y,(n + 1),k)),(i -' 1))))))) by A7, A17, Def13;

            now

              per cases by A13, XXREAL_0: 1;

                suppose

                 A23: i = 1;

                

                then

                 A24: ((( DigitSD zn) ^ <*( SubDigit (z,(n + 1),k))*>) . i) = ((( Radix k) |^ (i -' 1)) * (( SD_Add_Data ((( DigA (( DecSD (xn,n,k)),i)) + ( DigA (( DecSD (yn,n,k)),i))),k)) + ( SD_Add_Carry (( DigA (( DecSD (xn,n,k)),(i -' 1))) + ( DigA (( DecSD (yn,n,k)), 0 )))))) by A21, XREAL_1: 232

                .= ((( Radix k) |^ (i -' 1)) * (( SD_Add_Data ((( DigA (( DecSD (xn,n,k)),i)) + ( DigA (( DecSD (yn,n,k)),i))),k)) + ( SD_Add_Carry (( DigA (( DecSD (xn,n,k)), 0 )) + ( DigA (( DecSD (yn,n,k)), 0 )))))) by A23, XREAL_1: 232

                .= ((( Radix k) |^ (i -' 1)) * (( SD_Add_Data ((( DigA (( DecSD (xn,n,k)),i)) + ( DigA (( DecSD (yn,n,k)),i))),k)) + ( SD_Add_Carry (( DigA (( DecSD (xn,n,k)), 0 )) + 0 )))) by Def3

                .= ((( Radix k) |^ (i -' 1)) * (( SD_Add_Data ((( DigA (( DecSD (xn,n,k)),i)) + ( DigA (( DecSD (yn,n,k)),i))),k)) + 0 )) by Def3, Th17;

                (( DigitSD z) . i) = ((( Radix k) |^ (i -' 1)) * (( SD_Add_Data ((( DigA (( DecSD (x,(n + 1),k)),i)) + ( DigA (( DecSD (y,(n + 1),k)),i))),k)) + ( SD_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),(i -' 1))) + ( DigA (( DecSD (y,(n + 1),k)), 0 )))))) by A22, A23, XREAL_1: 232

                .= ((( Radix k) |^ (i -' 1)) * (( SD_Add_Data ((( DigA (( DecSD (x,(n + 1),k)),i)) + ( DigA (( DecSD (y,(n + 1),k)),i))),k)) + ( SD_Add_Carry (( DigA (( DecSD (x,(n + 1),k)), 0 )) + ( DigA (( DecSD (y,(n + 1),k)), 0 )))))) by A23, XREAL_1: 232

                .= ((( Radix k) |^ (i -' 1)) * (( SD_Add_Data ((( DigA (( DecSD (x,(n + 1),k)),i)) + ( DigA (( DecSD (y,(n + 1),k)),i))),k)) + ( SD_Add_Carry (( DigA (( DecSD (x,(n + 1),k)), 0 )) + 0 )))) by Def3

                .= ((( Radix k) |^ (i -' 1)) * (( SD_Add_Data ((( DigA (( DecSD (x,(n + 1),k)),i)) + ( DigA (( DecSD (y,(n + 1),k)),i))),k)) + 0 )) by Def3, Th17

                .= ((( Radix k) |^ (i -' 1)) * ( SD_Add_Data ((( DigA (( DecSD (xn,n,k)),i)) + ( DigA (( DecSD (y,(n + 1),k)),i))),k))) by A19, Lm3

                .= ((( Radix k) |^ (i -' 1)) * ( SD_Add_Data ((( DigA (( DecSD (xn,n,k)),i)) + ( DigA (( DecSD (yn,n,k)),i))),k))) by A19, Lm3;

                hence thesis by A24;

              end;

                suppose

                 A25: i > 1;

                

                 A26: (i - 1) <= n by A16, XREAL_1: 20;

                (i -' 1) >= 1 by A25, NAT_D: 49;

                then

                 A27: (i -' 1) in ( Seg n) by A15, A26, FINSEQ_1: 1;

                (( DigitSD z) . i) = ((( Radix k) |^ (i -' 1)) * (( SD_Add_Data ((( DigA (( DecSD (xn,n,k)),i)) + ( DigA (( DecSD (y,(n + 1),k)),i))),k)) + ( SD_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),(i -' 1))) + ( DigA (( DecSD (y,(n + 1),k)),(i -' 1))))))) by A19, A22, Lm3

                .= ((( Radix k) |^ (i -' 1)) * (( SD_Add_Data ((( DigA (( DecSD (xn,n,k)),i)) + ( DigA (( DecSD (yn,n,k)),i))),k)) + ( SD_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),(i -' 1))) + ( DigA (( DecSD (y,(n + 1),k)),(i -' 1))))))) by A19, Lm3

                .= ((( Radix k) |^ (i -' 1)) * (( SD_Add_Data ((( DigA (( DecSD (xn,n,k)),i)) + ( DigA (( DecSD (yn,n,k)),i))),k)) + ( SD_Add_Carry (( DigA (( DecSD (xn,n,k)),(i -' 1))) + ( DigA (( DecSD (y,(n + 1),k)),(i -' 1))))))) by A27, Lm3

                .= ((( Radix k) |^ (i -' 1)) * (( SD_Add_Data ((( DigA (( DecSD (xn,n,k)),i)) + ( DigA (( DecSD (yn,n,k)),i))),k)) + ( SD_Add_Carry (( DigA (( DecSD (xn,n,k)),(i -' 1))) + ( DigA (( DecSD (yn,n,k)),(i -' 1))))))) by A27, Lm3;

                hence thesis by A21;

              end;

            end;

            hence thesis;

          end;

            suppose

             A28: i = (n + 1);

            

            then ((( DigitSD zn) ^ <*( SubDigit (z,(n + 1),k))*>) . i) = ((( DigitSD zn) ^ <*( SubDigit (z,(n + 1),k))*>) . (( len ( DigitSD zn)) + 1)) by CARD_1:def 7

            .= ( SubDigit (z,(n + 1),k)) by FINSEQ_1: 42

            .= (( DigitSD z) /. (n + 1)) by A6, Def6

            .= (( DigitSD z) . (n + 1)) by A18, A28, PARTFUN1:def 6;

            hence thesis by A28;

          end;

        end;

        

         A29: ( SubDigit (z,(n + 1),k)) = ((( Radix k) |^ n) * ( DigB (z,(n + 1)))) by NAT_D: 34;

        

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

        then

         A31: x = (((x div (( Radix k) |^ n)) * (( Radix k) |^ n)) + (x mod (( Radix k) |^ n))) by NAT_D: 2, PREPOWER: 6;

        set y1 = (y div (( Radix k) |^ n));

        set x1 = (x div (( Radix k) |^ n));

        

         A32: ( len <*( SubDigit (z,(n + 1),k))*>) = 1 by FINSEQ_1: 39;

        

         A33: ( DigA (( DecSD (y,(n + 1),k)),(n + 1))) = y1 by A9, Th23;

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

        then

         A34: yn is_represented_by (n,k);

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

        then

         A35: xn is_represented_by (n,k);

        ( len (( DigitSD zn) ^ <*( SubDigit (z,(n + 1),k))*>)) = (( len ( DigitSD zn)) + ( len <*( SubDigit (z,(n + 1),k))*>)) by FINSEQ_1: 22

        .= (n + 1) by A32, CARD_1:def 7;

        then ( len ( DigitSD z)) = ( len (( DigitSD zn) ^ <*( SubDigit (z,(n + 1),k))*>)) by CARD_1:def 7;

        then ( DigitSD z) = (( DigitSD zn) ^ <*( SubDigit (z,(n + 1),k))*>) by A12, FINSEQ_1: 14;

        

        then ( SDDec z) = (((( Radix k) |^ n) * ( DigB (z,(n + 1)))) + ( Sum ( DigitSD zn))) by A29, RVSUM_1: 74

        .= ((( Add (( DecSD (x,(n + 1),k)),( DecSD (y,(n + 1),k)),(n + 1),k)) * (( Radix k) |^ n)) + ( Sum ( DigitSD zn))) by A6, Def14

        .= (((( SD_Add_Data ((( DigA (( DecSD (x,(n + 1),k)),(n + 1))) + ( DigA (( DecSD (y,(n + 1),k)),(n + 1)))),k)) + ( SD_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),((n + 1) -' 1))) + ( DigA (( DecSD (y,(n + 1),k)),((n + 1) -' 1)))))) * (( Radix k) |^ n)) + ( Sum ( DigitSD zn))) by A6, A7, Def13

        .= (((( SD_Add_Data ((( DigA (( DecSD (x,(n + 1),k)),(n + 1))) + ( DigA (( DecSD (y,(n + 1),k)),(n + 1)))),k)) + ( SD_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),((n + 1) -' 1))) + ( DigA (( DecSD (y,(n + 1),k)),n))))) * (( Radix k) |^ n)) + ( Sum ( DigitSD zn))) by NAT_D: 34

        .= (((( SD_Add_Data ((( DigA (( DecSD (x,(n + 1),k)),(n + 1))) + ( DigA (( DecSD (y,(n + 1),k)),(n + 1)))),k)) + ( SD_Add_Carry (( DigA (( DecSD (x,(n + 1),k)),n)) + ( DigA (( DecSD (y,(n + 1),k)),n))))) * (( Radix k) |^ n)) + ( Sum ( DigitSD zn))) by NAT_D: 34

        .= (((( SD_Add_Data ((( DigA (( DecSD (x,(n + 1),k)),(n + 1))) + ( DigA (( DecSD (y,(n + 1),k)),(n + 1)))),k)) + ( SD_Add_Carry (( DigA (( DecSD (xn,n,k)),n)) + ( DigA (( DecSD (y,(n + 1),k)),n))))) * (( Radix k) |^ n)) + ( Sum ( DigitSD zn))) by A5, Lm3

        .= (((( SD_Add_Data ((( DigA (( DecSD (x,(n + 1),k)),(n + 1))) + ( DigA (( DecSD (y,(n + 1),k)),(n + 1)))),k)) + ( SD_Add_Carry (( DigA (( DecSD (xn,n,k)),n)) + ( DigA (( DecSD (yn,n,k)),n))))) * (( Radix k) |^ n)) + ( Sum ( DigitSD zn))) by A5, Lm3

        .= (((( SD_Add_Data ((x1 + y1),k)) + ( SD_Add_Carry (( DigA (( DecSD (xn,n,k)),n)) + ( DigA (( DecSD (yn,n,k)),n))))) * (( Radix k) |^ n)) + ( Sum ( DigitSD zn))) by A8, A33, Th23

        .= ((( SD_Add_Data ((x1 + y1),k)) * (( Radix k) |^ n)) + ((( SD_Add_Carry (( DigA (( DecSD (xn,n,k)),n)) + ( DigA (( DecSD (yn,n,k)),n)))) * (( Radix k) |^ n)) + ( SDDec (( DecSD (xn,n,k)) '+' ( DecSD (yn,n,k))))))

        .= ((( SD_Add_Data ((x1 + y1),k)) * (( Radix k) |^ n)) + (xn + yn)) by A4, A7, A35, A34

        .= (((( SD_Add_Data ((x1 + y1),k)) * (( Radix k) |^ n)) + xn) + yn);

        

        then (( SDDec z) + (( SD_Add_Carry (x1 + y1)) * (( Radix k) |^ (n + 1)))) = ((((( SD_Add_Data ((x1 + y1),k)) * (( Radix k) |^ n)) + (( SD_Add_Carry (x1 + y1)) * (( Radix k) |^ (n + 1)))) + xn) + yn)

        .= ((((( SD_Add_Data ((x1 + y1),k)) * (( Radix k) |^ n)) + (( SD_Add_Carry (x1 + y1)) * ((( Radix k) |^ n) * ( Radix k)))) + xn) + yn) by NEWTON: 6

        .= (((x1 * (( Radix k) |^ n)) + xn) + ((y1 * (( Radix k) |^ n)) + yn))

        .= (x + y) by A30, A31, NAT_D: 2, PREPOWER: 6;

        hence thesis by A8, A33, Th23;

      end;

      

       A36: P[1]

      proof

        let k,x,y be Nat;

        assume k >= 2 & x is_represented_by (1,k) & y is_represented_by (1,k);

        then

         A37: ( SDDec (( DecSD (x,1,k)) '+' ( DecSD (y,1,k)))) = ( SD_Add_Data ((x + y),k)) & ( SD_Add_Carry (( DigA (( DecSD (x,1,k)),1)) + ( DigA (( DecSD (y,1,k)),1)))) = ( SD_Add_Carry (x + y)) by Th22, Th24;

        thus thesis by A37;

      end;

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

      hence thesis by A1;

    end;