radix_2.miz



    begin

    reserve k for Nat;

    theorem :: RADIX_2:1

    for a be Nat holds (a mod 1) = 0

    proof

      let a be Nat;

      a = ((1 * a) + 0 );

      hence thesis by NAT_D:def 2;

    end;

    theorem :: RADIX_2:2

    

     Th2: for a,b be Integer, n be Nat holds (((a mod n) + (b mod n)) mod n) = ((a + (b mod n)) mod n)

    proof

      let a,b be Integer;

      let n be Nat;

      per cases ;

        suppose 0 < n;

        

        then ((a mod n) + ((a div n) * n)) = ((a - ((a div n) * n)) + ((a div n) * n)) by INT_1:def 10

        .= (a + 0 );

        then n divides ((a + (b mod n)) - ((a mod n) + (b mod n))) by INT_1:def 3;

        then ((a + (b mod n)),((a mod n) + (b mod n))) are_congruent_mod n by INT_2: 15;

        hence thesis by NAT_D: 64;

      end;

        suppose

         A1: n = 0 ;

        

        hence (((a mod n) + (b mod n)) mod n) = 0 by INT_1:def 10

        .= ((a + (b mod n)) mod n) by A1, INT_1:def 10;

      end;

    end;

    theorem :: RADIX_2:3

    

     Th3: for a,b be Integer, n be Nat holds ((a * b) mod n) = ((a * (b mod n)) mod n)

    proof

      let a,b be Integer;

      let n be Nat;

      per cases ;

        suppose n > 0 ;

        

        then ((b mod n) + ((b div n) * n)) = ((b - ((b div n) * n)) + ((b div n) * n)) by INT_1:def 10

        .= (b + 0 );

        then ((a * b) - (a * (b mod n))) = ((a * (b div n)) * n);

        then n divides ((a * b) - (a * (b mod n))) by INT_1:def 3;

        then ((a * b),(a * (b mod n))) are_congruent_mod n by INT_2: 15;

        hence thesis by NAT_D: 64;

      end;

        suppose

         A1: n = 0 ;

        

        hence ((a * b) mod n) = 0 by INT_1:def 10

        .= ((a * (b mod n)) mod n) by A1, INT_1:def 10;

      end;

    end;

    theorem :: RADIX_2:4

    

     Th4: for a,b,i be Nat st 1 <= i & 0 < b holds ((a mod (b |^ i)) div (b |^ (i -' 1))) = ((a div (b |^ (i -' 1))) mod b)

    proof

      let a,b,i be Nat;

      assume that

       A1: 1 <= i and

       A2: 0 < b;

      set j = (i -' 1);

      set B0 = (b |^ j);

      

       A3: B0 > 0 by A2, PREPOWER: 6;

      set B1 = (b |^ (j + 1));

      

       A4: (a mod B1) = (a - (B1 * (a div B1))) by A2, NEWTON: 63, PREPOWER: 6;

      reconsider Z = (b * ( - (a div B1))) as Integer;

      (j + 1) = ((i - 1) + 1) by A1, XREAL_1: 233

      .= i;

      

      then ((a mod (b |^ i)) div (b |^ (i -' 1))) = ((a + (B1 * ( - (a div B1)))) div B0) by A4

      .= ((a + ((B0 * b) * ( - (a div B1)))) div B0) by NEWTON: 6

      .= [\((a + (B0 * Z)) / B0)/] by INT_1:def 9

      .= [\((a / B0) + Z)/] by A3, XCMPLX_1: 113

      .= ( [\(a / B0)/] + Z) by INT_1: 28

      .= ((a div B0) + ( - (b * (a div B1)))) by INT_1:def 9

      .= ((a div B0) - (b * (a div B1)))

      .= ((a div B0) - (b * (a div (B0 * b)))) by NEWTON: 6

      .= ((a div B0) - (b * ((a div B0) div b))) by NAT_2: 27;

      hence thesis by A2, NEWTON: 63;

    end;

    theorem :: RADIX_2:5

    

     Th5: for i,n be Nat st i in ( Seg n) holds (i + 1) in ( Seg (n + 1))

    proof

      let i,n be Nat;

      assume

       A1: i in ( Seg n);

      then 1 <= i by FINSEQ_1: 1;

      then (1 + 1) <= (i + 1) by XREAL_1: 6;

      then

       A2: 1 <= (i + 1) by XXREAL_0: 2;

      i <= n by A1, FINSEQ_1: 1;

      then (i + 1) <= (n + 1) by XREAL_1: 6;

      hence thesis by A2, FINSEQ_1: 1;

    end;

    begin

    theorem :: RADIX_2:6

    

     Th6: for k be Nat holds ( Radix k) > 0

    proof

      let k be Nat;

      ( Radix k) = (2 to_power k) by RADIX_1:def 1;

      hence thesis by POWER: 34;

    end;

    theorem :: RADIX_2:7

    

     Th7: for x be Tuple of 1, (k -SD ) holds ( SDDec x) = ( DigA (x,1))

    proof

      (1 - 1) = 0 ;

      then

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

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

      

       A2: 1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

      then

       A3: (( DigitSD x) /. 1) = ( SubDigit (x,1,k)) by RADIX_1:def 6;

      

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

      then 1 in ( dom ( DigitSD x)) by A2, FINSEQ_1:def 3;

      then

       A5: (( DigitSD x) . 1) = ( SubDigit (x,1,k)) by A3, PARTFUN1:def 6;

      

      thus ( SDDec x) = ( Sum ( DigitSD x)) by RADIX_1:def 7

      .= ( Sum <*( SubDigit (x,1,k))*>) by A4, A5, FINSEQ_1: 40

      .= ( SubDigit (x,1,k)) by RVSUM_1: 73

      .= ((( Radix k) |^ 0 ) * ( DigB (x,1))) by A1, RADIX_1:def 5

      .= (1 * ( DigB (x,1))) by NEWTON: 4

      .= ( DigA (x,1)) by RADIX_1:def 4;

    end;

    theorem :: RADIX_2:8

    

     Th8: for x be Integer holds (( SD_Add_Data (x,k)) + (( SD_Add_Carry x) * ( Radix k))) = x

    proof

      let x be Integer;

      (( SD_Add_Data (x,k)) + (( SD_Add_Carry x) * ( Radix k))) = ((x - (( SD_Add_Carry x) * ( Radix k))) + (( SD_Add_Carry x) * ( Radix k))) by RADIX_1:def 11;

      hence thesis;

    end;

    theorem :: RADIX_2:9

    

     Th9: for n be Nat holds for x be Tuple of (n + 1), (k -SD ), xn be Tuple of n, (k -SD ) st (for i be Nat st i in ( Seg n) holds (x . i) = (xn . i)) holds ( Sum ( DigitSD x)) = ( Sum (( DigitSD xn) ^ <*( SubDigit (x,(n + 1),k))*>))

    proof

      let n be Nat;

      let x be Tuple of (n + 1), (k -SD ), xn be Tuple of n, (k -SD );

      

       A1: ( len ( DigitSD x)) = (n + 1) by CARD_1:def 7;

      assume

       A2: for i be Nat st i in ( Seg n) holds (x . i) = (xn . i);

      

       A3: for i be Element of NAT st i in ( Seg n) holds ( DigA (x,i)) = ( DigA (xn,i))

      proof

        let i be Element of NAT ;

        assume

         A4: i in ( Seg n);

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

        

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

        .= (xn . i) by A2, A4;

        hence thesis by A4, RADIX_1:def 3;

      end;

      

       A5: ( len ( DigitSD xn)) = n by CARD_1:def 7;

      

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

      proof

        let i be Nat;

        assume that

         A7: 1 <= i and

         A8: i <= ( len ( DigitSD x));

        

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

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

        then

         A10: i in ( Seg (n + 1)) by A7, FINSEQ_1: 1;

        now

          per cases by A10, FINSEQ_2: 7;

            suppose

             A11: i in ( Seg n);

            then

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

            then

             A13: i in ( dom ( DigitSD x)) by A1, FINSEQ_1:def 3;

            

             A14: i in ( dom ( DigitSD xn)) by A5, A11, FINSEQ_1:def 3;

            

            then ((( DigitSD xn) ^ <*( SubDigit (x,(n + 1),k))*>) . i) = (( DigitSD xn) . i) by FINSEQ_1:def 7

            .= (( DigitSD xn) /. i) by A14, PARTFUN1:def 6

            .= ( SubDigit (xn,i,k)) by A11, RADIX_1:def 6

            .= ((( Radix k) |^ (i -' 1)) * ( DigB (xn,i))) by RADIX_1:def 5

            .= ((( Radix k) |^ (i -' 1)) * ( DigA (xn,i))) by RADIX_1:def 4

            .= ((( Radix k) |^ (i -' 1)) * ( DigA (x,i))) by A3, A11

            .= ((( Radix k) |^ (i -' 1)) * ( DigB (x,i))) by RADIX_1:def 4

            .= ( SubDigit (x,i,k)) by RADIX_1:def 5

            .= (( DigitSD x) /. i) by A12, RADIX_1:def 6;

            hence thesis by A13, PARTFUN1:def 6;

          end;

            suppose

             A15: i = (n + 1);

            then

             A16: i in ( dom ( DigitSD x)) by A1, A9, FINSEQ_1:def 3;

            ((( DigitSD xn) ^ <*( SubDigit (x,(n + 1),k))*>) . i) = ((( DigitSD xn) ^ <*( SubDigit (x,(n + 1),k))*>) . (( len ( DigitSD xn)) + 1)) by A15, CARD_1:def 7

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

            .= (( DigitSD x) /. (n + 1)) by A9, RADIX_1:def 6

            .= (( DigitSD x) . (n + 1)) by A15, A16, PARTFUN1:def 6;

            hence thesis by A15;

          end;

        end;

        hence thesis;

      end;

      

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

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

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

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

      hence thesis by A6, FINSEQ_1: 14;

    end;

    theorem :: RADIX_2:10

    

     Th10: for n be Nat holds for x be Tuple of (n + 1), (k -SD ), xn be Tuple of n, (k -SD ) st (for i be Nat st i in ( Seg n) holds (x . i) = (xn . i)) holds (( SDDec xn) + ((( Radix k) |^ n) * ( DigA (x,(n + 1))))) = ( SDDec x)

    proof

      let n be Nat;

      let x be Tuple of (n + 1), (k -SD ), xn be Tuple of n, (k -SD );

      assume

       A1: for i be Nat st i in ( Seg n) holds (x . i) = (xn . i);

      ( SDDec x) = ( Sum ( DigitSD x)) by RADIX_1:def 7

      .= ( Sum (( DigitSD xn) ^ <*( SubDigit (x,(n + 1),k))*>)) by A1, Th9

      .= (( Sum ( DigitSD xn)) + ( SubDigit (x,(n + 1),k))) by RVSUM_1: 74

      .= (( Sum ( DigitSD xn)) + ((( Radix k) |^ ((n + 1) -' 1)) * ( DigB (x,(n + 1))))) by RADIX_1:def 5

      .= (( Sum ( DigitSD xn)) + ((( Radix k) |^ n) * ( DigB (x,(n + 1))))) by NAT_D: 34

      .= (( Sum ( DigitSD xn)) + ((( Radix k) |^ n) * ( DigA (x,(n + 1))))) by RADIX_1:def 4;

      hence thesis by RADIX_1:def 7;

    end;

    theorem :: RADIX_2:11

    for n be Nat st n >= 1 holds for x,y be Tuple of n, (k -SD ) st k >= 2 holds (( SDDec (x '+' y)) + (( SD_Add_Carry (( DigA (x,n)) + ( DigA (y,n)))) * (( Radix k) |^ n))) = (( SDDec x) + ( SDDec y))

    proof

      defpred PP[ Nat] means for x,y be Tuple of $1, (k -SD ) st k >= 2 holds (( SDDec (x '+' y)) + (( SD_Add_Carry (( DigA (x,$1)) + ( DigA (y,$1)))) * (( Radix k) |^ $1))) = (( SDDec x) + ( SDDec y));

      

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

      proof

        let n be Nat;

        assume that

         A2: n >= 1 and

         A3: PP[n];

        

         A4: n in ( Seg n) by A2, FINSEQ_1: 3;

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

        assume

         A5: k >= 2;

        deffunc F( Nat) = ( DigB (x,$1));

        consider xn be FinSequence of INT such that

         A6: ( len xn) = n and

         A7: for i be Nat st i in ( dom xn) holds (xn . i) = F(i) from FINSEQ_2:sch 1;

        

         A8: ( dom xn) = ( Seg n) by A6, FINSEQ_1:def 3;

        ( rng xn) c= (k -SD )

        proof

          let z be object;

          assume z in ( rng xn);

          then

          consider xx be object such that

           A9: xx in ( dom xn) and

           A10: z = (xn . xx) by FUNCT_1:def 3;

          reconsider xx as Element of NAT by A9;

          ( dom xn) = ( Seg n) by A6, FINSEQ_1:def 3;

          then xx in ( Seg (n + 1)) by A9, FINSEQ_2: 8;

          then

           A11: ( DigA (x,xx)) is Element of (k -SD ) by RADIX_1: 16;

          z = ( DigB (x,xx)) by A7, A9, A10

          .= ( DigA (x,xx)) by RADIX_1:def 4;

          hence thesis by A11;

        end;

        then

        reconsider xn as FinSequence of (k -SD ) by FINSEQ_1:def 4;

        

         A12: for i be Nat st i in ( Seg n) holds (xn . i) = (x . i)

        proof

          let i be Nat;

          assume

           A13: i in ( Seg n);

          then

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

          (xn . i) = ( DigB (x,i)) by A7, A8, A13

          .= ( DigA (x,i)) by RADIX_1:def 4;

          hence thesis by A14, RADIX_1:def 3;

        end;

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

        deffunc F( Nat) = ( DigB (y,$1));

        consider yn be FinSequence of INT such that

         A15: ( len yn) = n and

         A16: for i be Nat st i in ( dom yn) holds (yn . i) = F(i) from FINSEQ_2:sch 1;

        

         A17: ( dom yn) = ( Seg n) by A15, FINSEQ_1:def 3;

        ( rng yn) c= (k -SD )

        proof

          let z be object;

          assume z in ( rng yn);

          then

          consider yy be object such that

           A18: yy in ( dom yn) and

           A19: z = (yn . yy) by FUNCT_1:def 3;

          reconsider yy as Element of NAT by A18;

          ( dom yn) = ( Seg n) by A15, FINSEQ_1:def 3;

          then yy in ( Seg (n + 1)) by A18, FINSEQ_2: 8;

          then

           A20: ( DigA (y,yy)) is Element of (k -SD ) by RADIX_1: 16;

          z = ( DigB (y,yy)) by A16, A18, A19

          .= ( DigA (y,yy)) by RADIX_1:def 4;

          hence thesis by A20;

        end;

        then

        reconsider yn as FinSequence of (k -SD ) by FINSEQ_1:def 4;

        

         A21: for i be Nat st i in ( Seg n) holds (yn . i) = (y . i)

        proof

          let i be Nat;

          assume

           A22: i in ( Seg n);

          then

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

          (yn . i) = ( DigB (y,i)) by A16, A17, A22

          .= ( DigA (y,i)) by RADIX_1:def 4;

          hence thesis by A23, RADIX_1:def 3;

        end;

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

        

         A24: for i be Nat st i in ( Seg n) holds ( DigA (y,i)) = ( DigA (yn,i))

        proof

          let i be Nat;

          assume

           A25: i in ( Seg n);

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

          

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

          .= (yn . i) by A21, A25;

          hence thesis by A25, RADIX_1:def 3;

        end;

        

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

        

         A27: for i be Element of NAT st i in ( Seg n) holds ( DigA (x,i)) = ( DigA (xn,i))

        proof

          let i be Element of NAT ;

          assume

           A28: i in ( Seg n);

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

          

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

          .= (xn . i) by A12, A28;

          hence thesis by A28, RADIX_1:def 3;

        end;

        for i be Nat st i in ( Seg n) holds ((x '+' y) . i) = ((xn '+' yn) . i)

        proof

          let i be Nat;

          assume

           A29: i in ( Seg n);

          then

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

          ((x '+' y) . i) = ((xn '+' yn) . i)

          proof

            

             A31: i <= (n + 1) by A30, FINSEQ_1: 1;

            

             A32: i >= 1 by A29, FINSEQ_1: 1;

            now

              per cases by A32, XXREAL_0: 1;

                suppose

                 A33: i > 1;

                then (i - 1) > (1 - 1) by XREAL_1: 9;

                then

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

                (i -' 1) > (1 -' 1) by A33, NAT_D: 57;

                then

                 A35: (i -' 1) >= 1 by NAT_1: 14;

                (i - 1) <= ((n + 1) - 1) by A31, XREAL_1: 9;

                then

                 A36: (i -' 1) in ( Seg n) by A35, A34, FINSEQ_1: 1;

                ((x '+' y) . i) = ( DigA ((x '+' y),i)) by A30, RADIX_1:def 3

                .= ( Add (x,y,i,k)) by A30, RADIX_1:def 14

                .= (( SD_Add_Data ((( DigA (x,i)) + ( DigA (y,i))),k)) + ( SD_Add_Carry (( DigA (x,(i -' 1))) + ( DigA (y,(i -' 1)))))) by A5, A30, RADIX_1:def 13

                .= (( SD_Add_Data ((( DigA (xn,i)) + ( DigA (y,i))),k)) + ( SD_Add_Carry (( DigA (x,(i -' 1))) + ( DigA (y,(i -' 1)))))) by A27, A29

                .= (( SD_Add_Data ((( DigA (xn,i)) + ( DigA (y,i))),k)) + ( SD_Add_Carry (( DigA (xn,(i -' 1))) + ( DigA (y,(i -' 1)))))) by A27, A36

                .= (( SD_Add_Data ((( DigA (xn,i)) + ( DigA (yn,i))),k)) + ( SD_Add_Carry (( DigA (xn,(i -' 1))) + ( DigA (y,(i -' 1)))))) by A24, A29

                .= (( SD_Add_Data ((( DigA (xn,i)) + ( DigA (yn,i))),k)) + ( SD_Add_Carry (( DigA (xn,(i -' 1))) + ( DigA (yn,(i -' 1)))))) by A24, A36

                .= ( Add (xn,yn,i,k)) by A5, A29, RADIX_1:def 13

                .= ( DigA ((xn '+' yn),i)) by A29, RADIX_1:def 14;

                hence thesis by A29, RADIX_1:def 3;

              end;

                suppose

                 A37: i = 1;

                ((x '+' y) . i) = ( DigA ((x '+' y),i)) by A30, RADIX_1:def 3

                .= ( Add (x,y,i,k)) by A30, RADIX_1:def 14

                .= (( SD_Add_Data ((( DigA (x,i)) + ( DigA (y,i))),k)) + ( SD_Add_Carry (( DigA (x,(1 -' 1))) + ( DigA (y,(1 -' 1)))))) by A5, A30, A37, RADIX_1:def 13

                .= (( SD_Add_Data ((( DigA (x,i)) + ( DigA (y,i))),k)) + ( SD_Add_Carry (( DigA (x, 0 )) + ( DigA (y,(1 -' 1)))))) by XREAL_1: 232

                .= (( SD_Add_Data ((( DigA (x,i)) + ( DigA (y,i))),k)) + ( SD_Add_Carry (( DigA (x, 0 )) + ( DigA (y, 0 ))))) by XREAL_1: 232

                .= (( SD_Add_Data ((( DigA (x,i)) + ( DigA (y,i))),k)) + ( SD_Add_Carry ( 0 + ( DigA (y, 0 ))))) by RADIX_1:def 3

                .= (( SD_Add_Data ((( DigA (x,i)) + ( DigA (y,i))),k)) + ( SD_Add_Carry ( 0 + 0 ))) by RADIX_1:def 3

                .= (( SD_Add_Data ((( DigA (x,i)) + ( DigA (y,i))),k)) + ( SD_Add_Carry (( DigA (xn, 0 )) + 0 ))) by RADIX_1:def 3

                .= (( SD_Add_Data ((( DigA (x,i)) + ( DigA (y,i))),k)) + ( SD_Add_Carry (( DigA (xn, 0 )) + ( DigA (yn, 0 ))))) by RADIX_1:def 3

                .= (( SD_Add_Data ((( DigA (xn,i)) + ( DigA (y,i))),k)) + ( SD_Add_Carry (( DigA (xn, 0 )) + ( DigA (yn, 0 ))))) by A27, A29

                .= (( SD_Add_Data ((( DigA (xn,i)) + ( DigA (yn,i))),k)) + ( SD_Add_Carry (( DigA (xn, 0 )) + ( DigA (yn, 0 ))))) by A24, A29

                .= (( SD_Add_Data ((( DigA (xn,i)) + ( DigA (yn,i))),k)) + ( SD_Add_Carry (( DigA (xn,(1 -' 1))) + ( DigA (yn, 0 ))))) by XREAL_1: 232

                .= (( SD_Add_Data ((( DigA (xn,i)) + ( DigA (yn,i))),k)) + ( SD_Add_Carry (( DigA (xn,(i -' 1))) + ( DigA (yn,(i -' 1)))))) by A37, XREAL_1: 232

                .= ( Add (xn,yn,i,k)) by A5, A29, RADIX_1:def 13

                .= ( DigA ((xn '+' yn),i)) by A29, RADIX_1:def 14;

                hence thesis by A29, RADIX_1:def 3;

              end;

            end;

            hence thesis;

          end;

          hence thesis;

        end;

        then ( Sum ( DigitSD (x '+' y))) = ( Sum (( DigitSD (xn '+' yn)) ^ <*( SubDigit ((x '+' y),(n + 1),k))*>)) by Th9;

        

        then ( SDDec (x '+' y)) = ( Sum (( DigitSD (xn '+' yn)) ^ <*( SubDigit ((x '+' y),(n + 1),k))*>)) by RADIX_1:def 7

        .= (( Sum ( DigitSD (xn '+' yn))) + ( SubDigit ((x '+' y),(n + 1),k))) by RVSUM_1: 74

        .= (( Sum ( DigitSD (xn '+' yn))) + ((( Radix k) |^ ((n + 1) -' 1)) * ( DigB ((x '+' y),(n + 1))))) by RADIX_1:def 5

        .= (( Sum ( DigitSD (xn '+' yn))) + ((( Radix k) |^ n) * ( DigB ((x '+' y),(n + 1))))) by NAT_D: 34

        .= (( Sum ( DigitSD (xn '+' yn))) + ((( Radix k) |^ n) * ( DigA ((x '+' y),(n + 1))))) by RADIX_1:def 4

        .= (( Sum ( DigitSD (xn '+' yn))) + ((( Radix k) |^ n) * ( Add (x,y,(n + 1),k)))) by A26, RADIX_1:def 14

        .= (( Sum ( DigitSD (xn '+' yn))) + ((( Radix k) |^ n) * (( SD_Add_Data ((( DigA (x,(n + 1))) + ( DigA (y,(n + 1)))),k)) + ( SD_Add_Carry (( DigA (x,((n + 1) -' 1))) + ( DigA (y,((n + 1) -' 1)))))))) by A5, A26, RADIX_1:def 13

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

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

        .= ((( Sum ( DigitSD (xn '+' yn))) + ((( Radix k) |^ n) * ( SD_Add_Carry (( DigA (x,n)) + ( DigA (y,n)))))) + ((( Radix k) |^ n) * ( SD_Add_Data ((( DigA (x,(n + 1))) + ( DigA (y,(n + 1)))),k))))

        .= ((( SDDec (xn '+' yn)) + ((( Radix k) |^ n) * ( SD_Add_Carry (( DigA (x,n)) + ( DigA (y,n)))))) + ((( Radix k) |^ n) * ( SD_Add_Data ((( DigA (x,(n + 1))) + ( DigA (y,(n + 1)))),k)))) by RADIX_1:def 7

        .= ((( SDDec (xn '+' yn)) + ((( Radix k) |^ n) * ( SD_Add_Carry (( DigA (xn,n)) + ( DigA (y,n)))))) + ((( Radix k) |^ n) * ( SD_Add_Data ((( DigA (x,(n + 1))) + ( DigA (y,(n + 1)))),k)))) by A27, A4

        .= ((( SDDec (xn '+' yn)) + ((( Radix k) |^ n) * ( SD_Add_Carry (( DigA (xn,n)) + ( DigA (yn,n)))))) + ((( Radix k) |^ n) * ( SD_Add_Data ((( DigA (x,(n + 1))) + ( DigA (y,(n + 1)))),k)))) by A2, A24, FINSEQ_1: 3

        .= ((( SDDec xn) + ( SDDec yn)) + ((( Radix k) |^ n) * ( SD_Add_Data ((( DigA (x,(n + 1))) + ( DigA (y,(n + 1)))),k)))) by A3, A5;

        

        then (( SDDec (x '+' y)) + (( SD_Add_Carry (( DigA (x,(n + 1))) + ( DigA (y,(n + 1))))) * (( Radix k) |^ (n + 1)))) = ((( SDDec xn) + ( SDDec yn)) + (((( Radix k) |^ n) * ( SD_Add_Data ((( DigA (x,(n + 1))) + ( DigA (y,(n + 1)))),k))) + (( SD_Add_Carry (( DigA (x,(n + 1))) + ( DigA (y,(n + 1))))) * (( Radix k) |^ (n + 1)))))

        .= ((( SDDec xn) + ( SDDec yn)) + (((( Radix k) |^ n) * ( SD_Add_Data ((( DigA (x,(n + 1))) + ( DigA (y,(n + 1)))),k))) + (( SD_Add_Carry (( DigA (x,(n + 1))) + ( DigA (y,(n + 1))))) * ((( Radix k) |^ n) * ( Radix k))))) by NEWTON: 6

        .= ((( SDDec xn) + ( SDDec yn)) + ((( Radix k) |^ n) * (( SD_Add_Data ((( DigA (x,(n + 1))) + ( DigA (y,(n + 1)))),k)) + (( SD_Add_Carry (( DigA (x,(n + 1))) + ( DigA (y,(n + 1))))) * ( Radix k)))))

        .= ((( SDDec xn) + ( SDDec yn)) + ((( Radix k) |^ n) * (( DigA (x,(n + 1))) + ( DigA (y,(n + 1)))))) by Th8

        .= ((( SDDec xn) + ((( Radix k) |^ n) * ( DigA (x,(n + 1))))) + (( SDDec yn) + ((( Radix k) |^ n) * ( DigA (y,(n + 1))))))

        .= (( SDDec x) + (( SDDec yn) + ((( Radix k) |^ n) * ( DigA (y,(n + 1)))))) by A12, Th10;

        hence thesis by A21, Th10;

      end;

      

       A38: PP[1]

      proof

        (1 - 1) = 0 ;

        then

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

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

        assume

         A40: k >= 2;

        

         A41: ( SDDec y) = ( DigA (y,1)) & ( SD_Add_Data ((( DigA (x,1)) + ( DigA (y,1))),k)) = ((( DigA (x,1)) + ( DigA (y,1))) - (( SD_Add_Carry (( DigA (x,1)) + ( DigA (y,1)))) * ( Radix k))) by Th7, RADIX_1:def 11;

        

         A42: 1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

        

        then ( DigA ((x '+' y),1)) = ( Add (x,y,1,k)) by RADIX_1:def 14

        .= (( SD_Add_Data ((( DigA (x,1)) + ( DigA (y,1))),k)) + ( SD_Add_Carry (( DigA (x, 0 )) + ( DigA (y, 0 ))))) by A40, A42, A39, RADIX_1:def 13

        .= (( SD_Add_Data ((( DigA (x,1)) + ( DigA (y,1))),k)) + ( SD_Add_Carry ( 0 + ( DigA (y, 0 ))))) by RADIX_1:def 3

        .= (( SD_Add_Data ((( DigA (x,1)) + ( DigA (y,1))),k)) + 0 ) by RADIX_1: 18, RADIX_1:def 3;

        then ( SDDec (x '+' y)) = ( SD_Add_Data ((( DigA (x,1)) + ( DigA (y,1))),k)) by Th7;

        

        hence (( SDDec (x '+' y)) + (( SD_Add_Carry (( DigA (x,1)) + ( DigA (y,1)))) * (( Radix k) |^ 1))) = (( SD_Add_Data ((( DigA (x,1)) + ( DigA (y,1))),k)) + (( SD_Add_Carry (( DigA (x,1)) + ( DigA (y,1)))) * ( Radix k)))

        .= (( SDDec x) + ( SDDec y)) by A41, Th7;

      end;

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

      hence thesis;

    end;

    begin

    definition

      let i,k,n be Nat, x be Tuple of n, NAT ;

      :: RADIX_2:def1

      func SubDigit2 (x,i,k) -> Element of NAT equals ((( Radix k) |^ (i -' 1)) * (x . i));

      coherence ;

    end

    definition

      let n,k be Nat, x be Tuple of n, NAT ;

      :: RADIX_2:def2

      func DigitSD2 (x,k) -> Tuple of n, NAT means

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

      existence

      proof

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

        consider z be FinSequence of NAT 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, NAT 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

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

      end;

      uniqueness

      proof

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

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

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

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

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

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

        end;

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    definition

      let n,k be Nat, x be Tuple of n, NAT ;

      :: RADIX_2:def3

      func SDDec2 (x,k) -> Element of NAT equals ( Sum ( DigitSD2 (x,k)));

      coherence ;

    end

    definition

      let i,k,x be Nat;

      :: RADIX_2:def4

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

      coherence ;

    end

    definition

      let k,n,x be Nat;

      :: RADIX_2:def5

      func DecSD2 (x,n,k) -> Tuple of n, NAT means

      : Def5: for i be Nat st i in ( Seg n) holds (it . i) = ( DigitDC2 (x,i,k));

      existence

      proof

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

        consider z be FinSequence of NAT 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, NAT by A1, CARD_1:def 7;

        take z;

        let i be Nat;

        assume i in ( Seg n);

        hence thesis by A2, A3;

      end;

      uniqueness

      proof

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

         A4: for i be Nat st i in ( Seg n) holds (k1 . i) = ( DigitDC2 (x,i,k)) and

         A5: for i be Nat st i in ( Seg n) holds (k2 . i) = ( DigitDC2 (x,i,k));

        

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

        then

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

         A8:

        now

          let j be Nat;

          assume

           A9: j in ( dom k1);

          then (k1 . j) = ( DigitDC2 (x,j,k)) by A4, A7;

          hence (k1 . j) = (k2 . j) by A5, A7, A9;

        end;

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

        hence thesis by A6, A8, FINSEQ_2: 9;

      end;

    end

    theorem :: RADIX_2:12

    

     Th12: for n,k be Nat, x be Tuple of n, NAT , y be Tuple of n, (k -SD ) st x = y holds ( DigitSD2 (x,k)) = ( DigitSD y)

    proof

      let n,k be Nat;

      let x be Tuple of n, NAT ;

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

      

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

      

       A2: ( len ( DigitSD2 (x,k))) = n by CARD_1:def 7;

      then

       A3: ( dom ( DigitSD2 (x,k))) = ( Seg n) by FINSEQ_1:def 3;

      assume

       A4: x = y;

       A5:

      now

        let i be Element of NAT ;

        assume i in ( Seg n);

        

        then (x . i) = ( DigA (y,i)) by A4, RADIX_1:def 3

        .= ( DigB (y,i)) by RADIX_1:def 4;

        hence (x . i) = ( DigB (y,i));

      end;

      now

        let j be Nat;

        assume

         A6: j in ( dom ( DigitSD2 (x,k)));

        then

         A7: j in ( dom ( DigitSD y)) by A1, A3, FINSEQ_1:def 3;

        (( DigitSD2 (x,k)) . j) = (( DigitSD2 (x,k)) /. j) by A6, PARTFUN1:def 6

        .= ( SubDigit2 (x,j,k)) by A3, A6, Def2

        .= ((( Radix k) |^ (j -' 1)) * ( DigB (y,j))) by A5, A3, A6

        .= ( SubDigit (y,j,k)) by RADIX_1:def 5

        .= (( DigitSD y) /. j) by A3, A6, RADIX_1:def 6

        .= (( DigitSD y) . j) by A7, PARTFUN1:def 6;

        hence (( DigitSD2 (x,k)) . j) = (( DigitSD y) . j);

      end;

      hence thesis by A2, A1, FINSEQ_2: 9;

    end;

    theorem :: RADIX_2:13

    

     Th13: for n,k be Nat, x be Tuple of n, NAT , y be Tuple of n, (k -SD ) st x = y holds ( SDDec2 (x,k)) = ( SDDec y)

    proof

      let n,k be Nat;

      let x be Tuple of n, NAT ;

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

      assume x = y;

      then ( SDDec2 (x,k)) = ( Sum ( DigitSD y)) by Th12;

      hence thesis by RADIX_1:def 7;

    end;

    theorem :: RADIX_2:14

    

     Th14: for x,n,k be Nat holds ( DecSD2 (x,n,k)) = ( DecSD (x,n,k))

    proof

      let x,n,k be Nat;

      

       A1: ( len ( DecSD2 (x,n,k))) = n by CARD_1:def 7;

      then

       A2: ( dom ( DecSD2 (x,n,k))) = ( Seg n) by FINSEQ_1:def 3;

       A3:

      now

        let j be Nat;

        assume

         A4: j in ( dom ( DecSD2 (x,n,k)));

        

        then (( DecSD2 (x,n,k)) . j) = ( DigitDC2 (x,j,k)) by A2, Def5

        .= ( DigitDC (x,j,k)) by RADIX_1:def 8

        .= ( DigA (( DecSD (x,n,k)),j)) by A2, A4, RADIX_1:def 9

        .= (( DecSD (x,n,k)) . j) by A2, A4, RADIX_1:def 3;

        hence (( DecSD2 (x,n,k)) . j) = (( DecSD (x,n,k)) . j);

      end;

      ( len ( DecSD (x,n,k))) = n by CARD_1:def 7;

      hence thesis by A1, A3, FINSEQ_2: 9;

    end;

    theorem :: RADIX_2:15

    

     Th15: for n be Nat st n >= 1 holds for m,k be Nat st m is_represented_by (n,k) holds m = ( SDDec2 (( DecSD2 (m,n,k)),k))

    proof

      let n be Nat;

      assume

       A1: n >= 1;

      let m,k be Nat;

      assume

       A2: m is_represented_by (n,k);

      ( SDDec2 (( DecSD2 (m,n,k)),k)) = ( SDDec ( DecSD (m,n,k))) by Th13, Th14;

      hence thesis by A1, A2, RADIX_1: 22;

    end;

    begin

    definition

      let q be Integer, f,j,k,n be Nat, c be Tuple of n, (k -SD );

      :: RADIX_2:def6

      func Table1 (q,c,f,j) -> Integer equals ((q * ( DigA (c,j))) mod f);

      correctness ;

    end

    definition

      let q be Integer, k,f,n be Nat, c be Tuple of n, (k -SD );

      assume

       A1: n >= 1;

      :: RADIX_2:def7

      func Mul_mod (q,c,f,k) -> Tuple of n, INT means

      : Def7: (it . 1) = ( Table1 (q,c,f,n)) & for i be Nat st 1 <= i & i <= (n - 1) holds ex I1,I2 be Integer st I1 = (it . i) & I2 = (it . (i + 1)) & I2 = (((( Radix k) * I1) + ( Table1 (q,c,f,(n -' i)))) mod f);

      existence

      proof

        defpred PP[ Nat, set, set] means ex i1,i2 be Integer st i1 = $2 & i2 = $3 & i2 = (((( Radix k) * i1) + ( Table1 (q,c,f,(n -' $1)))) mod f);

        reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

        reconsider T = ( Table1 (q,c,f,n)) as Element of INT by INT_1:def 2;

        

         A2: for i be Nat st 1 <= i & i < n1 holds for x be Element of INT holds ex y be Element of INT st PP[i, x, y]

        proof

          let i be Nat;

          assume that 1 <= i and i < n1;

          let x be Element of INT ;

          reconsider x as Integer;

          consider y be Integer such that

           A3: y = (((( Radix k) * x) + ( Table1 (q,c,f,(n -' i)))) mod f);

          reconsider z = y as Element of INT by INT_1:def 2;

          take z;

          thus thesis by A3;

        end;

        consider r be FinSequence of INT such that

         A4: ( len r) = n1 & ((r . 1) = T or n1 = 0 ) and

         A5: for i be Nat st 1 <= i & i < n1 holds PP[i, (r . i), (r . (i + 1))] from RECDEF_1:sch 4( A2);

        reconsider r as Tuple of n, INT by A4, CARD_1:def 7;

        take r;

        thus (r . 1) = ( Table1 (q,c,f,n)) by A1, A4;

        let i be Nat;

        assume

         A6: 1 <= i & i <= (n - 1);

        thus thesis by A5, A6, XREAL_1: 147;

      end;

      uniqueness

      proof

        let s1,s2 be Tuple of n, INT such that

         A7: (s1 . 1) = ( Table1 (q,c,f,n)) and

         A8: for i be Nat st 1 <= i & i <= (n - 1) holds ex I1,I2 be Integer st I1 = (s1 . i) & I2 = (s1 . (i + 1)) & I2 = (((( Radix k) * I1) + ( Table1 (q,c,f,(n -' i)))) mod f) and

         A9: (s2 . 1) = ( Table1 (q,c,f,n)) and

         A10: for i be Nat st 1 <= i & i <= (n - 1) holds ex I1,I2 be Integer st I1 = (s2 . i) & I2 = (s2 . (i + 1)) & I2 = (((( Radix k) * I1) + ( Table1 (q,c,f,(n -' i)))) mod f);

        defpred P[ Nat] means 1 <= $1 & $1 <= (n - 1) implies (s1 . $1) = (s2 . $1);

        

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

        proof

          let kk be Nat;

          assume

           A12: 1 <= kk & kk <= (n - 1) implies (s1 . kk) = (s2 . kk);

          

           A13: 0 = kk or 0 < kk & ( 0 + 1) = 1;

          assume that 1 <= (kk + 1) and

           A14: (kk + 1) <= (n - 1);

          per cases by A13, NAT_1: 13;

            suppose 0 = kk;

            hence thesis by A7, A9;

          end;

            suppose

             A15: 1 <= kk;

            

             A16: kk <= (kk + 1) by NAT_1: 11;

            then kk <= (n - 1) by A14, XXREAL_0: 2;

            then (ex I1,I2 be Integer st I1 = (s1 . kk) & I2 = (s1 . (kk + 1)) & I2 = (((( Radix k) * I1) + ( Table1 (q,c,f,(n -' kk)))) mod f)) & ex i1,i2 be Integer st i1 = (s2 . kk) & i2 = (s2 . (kk + 1)) & i2 = (((( Radix k) * i1) + ( Table1 (q,c,f,(n -' kk)))) mod f) by A8, A10, A15;

            hence thesis by A12, A14, A15, A16, XXREAL_0: 2;

          end;

        end;

        

         A17: ( len s1) = n by CARD_1:def 7;

        

         A18: P[ 0 ];

        

         A19: for kk be Nat holds P[kk] from NAT_1:sch 2( A18, A11);

        

         A20: (s1 . n) = (s2 . n)

        proof

          (n - 1) >= (1 - 1) by A1, XREAL_1: 9;

          then

          reconsider U1 = (n - 1) as Element of NAT by INT_1: 3;

          now

            per cases ;

              suppose U1 = 0 ;

              hence thesis by A7, A9;

            end;

              suppose 0 < U1;

              then

               A21: 1 <= U1 by NAT_1: 14;

              then (ex i1,i2 be Integer st i1 = (s1 . U1) & i2 = (s1 . (U1 + 1)) & i2 = (((( Radix k) * i1) + ( Table1 (q,c,f,(n -' U1)))) mod f)) & ex j1,j2 be Integer st j1 = (s2 . U1) & j2 = (s2 . (U1 + 1)) & j2 = (((( Radix k) * j1) + ( Table1 (q,c,f,(n -' U1)))) mod f) by A8, A10;

              hence thesis by A19, A21;

            end;

          end;

          hence thesis;

        end;

        

         A22: for kk be Nat st 1 <= kk & kk <= ( len s1) holds (s1 . kk) = (s2 . kk)

        proof

          let kk be Nat;

          assume that

           A23: 1 <= kk and

           A24: kk <= ( len s1);

          now

            per cases by A24, XXREAL_0: 1;

              suppose

               A25: kk < ( len s1);

              (n - 1) >= (1 - 1) by A1, XREAL_1: 9;

              then

              reconsider U1 = (( len s1) - 1) as Element of NAT by A17, INT_1: 3;

              (U1 + 1) = ( len s1);

              then kk <= U1 by A25, NAT_1: 13;

              hence thesis by A17, A19, A23;

            end;

              suppose kk = ( len s1);

              hence thesis by A17, A20;

            end;

          end;

          hence thesis;

        end;

        ( len s1) = ( len s2) by A17, CARD_1:def 7;

        hence thesis by A22, FINSEQ_1: 14;

      end;

    end

    theorem :: RADIX_2:16

    for n be Nat st n >= 1 holds for q be Integer, ic,f,k be Nat st ic is_represented_by (n,k) & f > 0 holds for c be Tuple of n, (k -SD ) st c = ( DecSD (ic,n,k)) holds (( Mul_mod (q,c,f,k)) . n) = ((q * ic) mod f)

    proof

      defpred PP[ Nat] means for q be Integer, ic,f,k be Nat st ic is_represented_by ($1,k) & f > 0 holds for c be Tuple of $1, (k -SD ) st c = ( DecSD (ic,$1,k)) holds (( Mul_mod (q,c,f,k)) . $1) = ((q * ic) mod f);

      

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

      proof

        let n be Nat;

        assume that

         A2: n >= 1 and

         A3: PP[n];

        let q be Integer;

        let ic,f,k be Nat;

        assume that

         A4: ic is_represented_by ((n + 1),k) and

         A5: f > 0 ;

        let c be Tuple of (n + 1), (k -SD );

        deffunc F( Nat) = ( DigB (c,($1 + 1)));

        consider cn be FinSequence of INT such that

         A6: ( len cn) = n and

         A7: for i be Nat st i in ( dom cn) holds (cn . i) = F(i) from FINSEQ_2:sch 1;

        

         A8: ( dom cn) = ( Seg n) by A6, FINSEQ_1:def 3;

        ( rng cn) c= (k -SD )

        proof

          let z be object;

          assume z in ( rng cn);

          then

          consider xx be object such that

           A9: xx in ( dom cn) and

           A10: z = (cn . xx) by FUNCT_1:def 3;

          reconsider xx as Element of NAT by A9;

          ( dom cn) = ( Seg n) by A6, FINSEQ_1:def 3;

          then (xx + 1) in ( Seg (n + 1)) by A9, Th5;

          then

           A11: ( DigA (c,(xx + 1))) is Element of (k -SD ) by RADIX_1: 16;

          z = ( DigB (c,(xx + 1))) by A7, A9, A10

          .= ( DigA (c,(xx + 1))) by RADIX_1:def 4;

          hence thesis by A11;

        end;

        then

        reconsider cn as FinSequence of (k -SD ) by FINSEQ_1:def 4;

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

        

         A12: (n + 1) >= 1 by NAT_1: 12;

        set c2 = ( DecSD2 (ic,(n + 1),k));

        

         A13: ( Radix k) > 0 by Th6;

        deffunc F( Nat) = (c2 . ($1 + 1));

        consider cn2 be FinSequence of NAT such that

         A14: ( len cn2) = n and

         A15: for i be Nat st i in ( dom cn2) holds (cn2 . i) = F(i) from FINSEQ_2:sch 1;

        

         A16: ( dom cn2) = ( Seg n) by A14, FINSEQ_1:def 3;

        reconsider cn2 as Tuple of n, NAT by A14, CARD_1:def 7;

        set icn2 = ( SDDec2 (cn2,k));

        

         A17: ic < (( Radix k) |^ (n + 1)) by A4, RADIX_1:def 12;

        set icn = ( SDDec cn);

        assume

         A18: c = ( DecSD (ic,(n + 1),k));

        then

         A19: c2 = c by Th14;

        

         A20: for i be Nat st 1 <= i & i <= ( len cn) holds (cn . i) = (cn2 . i)

        proof

          let i be Nat;

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

          then

           A21: i in ( Seg n) by A6, FINSEQ_1: 1;

          then

           A22: (i + 1) in ( Seg (n + 1)) by Th5;

          (cn . i) = ( DigB (c,(i + 1))) by A7, A8, A21

          .= ( DigA (c,(i + 1))) by RADIX_1:def 4

          .= (c . (i + 1)) by A22, RADIX_1:def 3

          .= (c2 . (i + 1)) by A18, Th14;

          hence thesis by A15, A16, A21;

        end;

        then

         A23: icn = icn2 by A6, A14, Th13, FINSEQ_1: 14;

        1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

        then

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

        

         A25: ic = ((( Radix k) * icn2) + (c2 . 1))

        proof

          

           A26: ( len <*( SubDigit2 (c2,1,k))*>) = 1 by FINSEQ_1: 39;

          

           A27: (1 - 1) = 0 ;

          deffunc F( Nat) = ( In ((( DigitSD2 (cn2,k)) . $1), REAL ));

          reconsider r2 = ( Radix k) as Element of REAL by XREAL_0:def 1;

          consider rD be FinSequence of REAL such that

           A28: ( len rD) = n and

           A29: for i be Nat st i in ( dom rD) holds (rD . i) = F(i) from FINSEQ_2:sch 1;

          

           A30: for i be Nat st i in ( dom rD) holds (rD . i) = (( DigitSD2 (cn2,k)) . i)

          proof

            let i be Nat;

            assume i in ( dom rD);

            then (rD . i) = F(i) by A29;

            hence thesis;

          end;

          reconsider rD as Tuple of n, REAL by A28, CARD_1:def 7;

          

           A31: ( dom ( DigitSD2 (cn2,k))) = ( Seg ( len ( DigitSD2 (cn2,k)))) by FINSEQ_1:def 3

          .= ( Seg n) by CARD_1:def 7;

          reconsider rD1 = rD as Element of (n -tuples_on REAL ) by FINSEQ_2: 131;

          

           A32: ( dom rD) = ( Seg n) by A28, FINSEQ_1:def 3;

          

          then

           A33: ( len (( Radix k) * ( DigitSD2 (cn2,k)))) = ( len (r2 * rD1)) by A30, A31, FINSEQ_1: 13

          .= n by CARD_1:def 7;

          

           A34: ( len ( <*( SubDigit2 (c2,1,k))*> ^ (( Radix k) * ( DigitSD2 (cn2,k))))) = (( len <*( SubDigit2 (c2,1,k))*>) + ( len (( Radix k) * ( DigitSD2 (cn2,k))))) by FINSEQ_1: 22

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

          

           A35: ( len ( DigitSD2 (c2,k))) = (n + 1) by CARD_1:def 7;

          

           A36: for i be Nat st 1 <= i & i <= ( len ( DigitSD2 (c2,k))) holds (( DigitSD2 (c2,k)) . i) = (( <*( SubDigit2 (c2,1,k))*> ^ (( Radix k) * ( DigitSD2 (cn2,k)))) . i)

          proof

            let i be Nat;

            assume that

             A37: 1 <= i and

             A38: i <= ( len ( DigitSD2 (c2,k)));

            

             A39: i <= (n + 1) by A38, CARD_1:def 7;

            then

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

            then

             A41: i in ( dom ( DigitSD2 (c2,k))) by A35, FINSEQ_1:def 3;

            per cases ;

              suppose

               A42: i = 1;

              

              then (( <*( SubDigit2 (c2,1,k))*> ^ (( Radix k) * ( DigitSD2 (cn2,k)))) . i) = ( SubDigit2 (c2,1,k)) by FINSEQ_1: 41

              .= (( DigitSD2 (c2,k)) /. 1) by A24, Def2

              .= (( DigitSD2 (c2,k)) . 1) by A41, A42, PARTFUN1:def 6;

              hence thesis by A42;

            end;

              suppose

               A43: i <> 1;

              reconsider rs2 = (( DigitSD2 (cn2,k)) . (i - 1)) as Element of NAT ;

              reconsider rs = (rD . (i - 1)) as Real;

              (1 - 1) <= (i - 1) by A37, XREAL_1: 9;

              then

              reconsider i1 = (i - 1) as Element of NAT by INT_1: 3;

              1 < i by A37, A43, XXREAL_0: 1;

              then (1 + 1) <= i by INT_1: 7;

              then

               A44: ((1 + 1) - 1) <= (i - 1) by XREAL_1: 9;

              (i - 1) <= ((n + 1) - 1) by A39, XREAL_1: 9;

              then

               A45: i1 in ( Seg n) by A44, FINSEQ_1: 1;

              1 < i by A37, A43, XXREAL_0: 1;

              

              then (( <*( SubDigit2 (c2,1,k))*> ^ (( Radix k) * ( DigitSD2 (cn2,k)))) . i) = ((( Radix k) * ( DigitSD2 (cn2,k))) . (i - 1)) by A26, A34, A39, FINSEQ_1: 24

              .= ((r2 * rD) . (i - 1)) by A30, A31, A32, FINSEQ_1: 13

              .= (r2 * rs) by RVSUM_1: 45

              .= (( Radix k) * rs2) by A30, A31, A32, FINSEQ_1: 13

              .= (( Radix k) * (( DigitSD2 (cn2,k)) /. i1)) by A31, A45, PARTFUN1:def 6

              .= (( Radix k) * ( SubDigit2 (cn2,i1,k))) by A45, Def2

              .= ((( Radix k) * (( Radix k) |^ (i1 -' 1))) * (cn2 . i1))

              .= ((( Radix k) |^ ((i1 -' 1) + 1)) * (cn2 . i1)) by NEWTON: 6

              .= ((( Radix k) |^ i1) * (cn2 . i1)) by A44, XREAL_1: 235

              .= ((( Radix k) |^ i1) * (c2 . (i1 + 1))) by A15, A16, A45

              .= ( SubDigit2 (c2,i,k)) by A37, XREAL_1: 233

              .= (( DigitSD2 (c2,k)) /. i) by A40, Def2;

              hence thesis by A41, PARTFUN1:def 6;

            end;

          end;

          ( len ( DigitSD2 (c2,k))) = ( len ( <*( SubDigit2 (c2,1,k))*> ^ (( Radix k) * ( DigitSD2 (cn2,k))))) by A34, CARD_1:def 7;

          then

           A46: ( DigitSD2 (c2,k)) = ( <*( SubDigit2 (c2,1,k))*> ^ (( Radix k) * ( DigitSD2 (cn2,k)))) by A36, FINSEQ_1: 14;

          ic = ( SDDec2 (( DecSD2 (ic,(n + 1),k)),k)) by A4, Th15, NAT_1: 12

          .= (( SubDigit2 (c2,1,k)) + ( Sum (( Radix k) * ( DigitSD2 (cn2,k))))) by A46, RVSUM_1: 76

          .= (( SubDigit2 (c2,1,k)) + ( Sum (r2 * rD))) by A30, A31, A32, FINSEQ_1: 13

          .= (( SubDigit2 (c2,1,k)) + (r2 * ( Sum rD))) by RVSUM_1: 87

          .= (( SubDigit2 (c2,1,k)) + (( Radix k) * icn2)) by A30, A31, A32, FINSEQ_1: 13

          .= (((( Radix k) |^ 0 ) * (c2 . 1)) + (( Radix k) * icn2)) by A27, XREAL_0:def 2

          .= ((1 * (c2 . 1)) + (( Radix k) * icn2)) by NEWTON: 4;

          hence thesis;

        end;

        

        then

         A47: ((q * ic) mod f) = ((((q * ( Radix k)) * icn2) + (q * (c2 . 1))) mod f)

        .= ((((( Radix k) * (q * icn2)) mod f) + ((q * (c2 . 1)) mod f)) mod f) by NAT_D: 66

        .= ((((( Radix k) * ((q * icn2) mod f)) mod f) + ((q * (c2 . 1)) mod f)) mod f) by Th3

        .= (((( Radix k) * ((q * icn2) mod f)) + ((q * (c2 . 1)) mod f)) mod f) by Th2;

        

         A48: cn = cn2 by A6, A14, A20, FINSEQ_1: 14;

        

         A49: for i be Nat st 1 <= i & i <= ( len cn) holds (cn . i) = (( DecSD2 (icn2,n,k)) . i)

        proof

          

           A50: (c2 . 1) = ( DigitDC2 (ic,1,k)) by A24, Def5

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

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

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

          .= (ic mod ( Radix k));

          

           A51: 0 < ( Radix k) by Th6;

          

           A52: (((c2 . 1) + (icn2 * ( Radix k))) div ( Radix k)) = [\(((c2 . 1) + (icn2 * ( Radix k))) / ( Radix k))/] by INT_1:def 9

          .= [\(((c2 . 1) / ( Radix k)) + icn2)/] by A51, XCMPLX_1: 113

          .= ( [\((c2 . 1) / ( Radix k))/] + icn2) by INT_1: 28

          .= (((c2 . 1) div ( Radix k)) + icn2) by INT_1:def 9

          .= ( 0 + icn2) by A13, A50, NAT_D: 1, NAT_D: 27;

          

           A53: ( Radix k) <> 0 by Th6;

          let i be Nat;

          assume that

           A54: 1 <= i and

           A55: i <= ( len cn);

          

           A56: i in ( Seg n) by A6, A54, A55, FINSEQ_1: 1;

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

          

           A57: 1 <= (i + 1) by A54, XREAL_1: 29;

          1 <= (i + 1) & (i + 1) <= (n + 1) by A6, A54, A55, XREAL_1: 6, XREAL_1: 29;

          then

           A58: (i + 1) in ( Seg (n + 1)) by FINSEQ_1: 1;

          (cn . i) = (c2 . (i + 1)) by A15, A16, A48, A56

          .= ( DigitDC2 (ic,(i + 1),k)) by A58, Def5

          .= ((((icn2 * ( Radix k)) + (c2 . 1)) div (( Radix k) |^ ((i + 1) -' 1))) mod ( Radix k)) by A25, A57, Th4, Th6

          .= ((((icn2 * ( Radix k)) + (c2 . 1)) div (( Radix k) |^ i)) mod ( Radix k)) by NAT_D: 34

          .= ((((icn2 * ( Radix k)) + (c2 . 1)) div (( Radix k) * (( Radix k) |^ (i -' 1)))) mod ( Radix k)) by A54, A53, PEPIN: 26

          .= ((icn2 div (( Radix k) |^ (i -' 1))) mod ( Radix k)) by A52, NAT_2: 27

          .= ( DigitDC2 (icn2,i,k)) by A54, Th4, Th6;

          hence thesis by A56, Def5;

        end;

        reconsider icn as Element of NAT by A23;

        ( len cn) = ( len ( DecSD2 (icn2,n,k))) by A6, CARD_1:def 7;

        then cn = ( DecSD2 (icn2,n,k)) by A49, FINSEQ_1: 14;

        then

         A59: cn = ( DecSD (icn,n,k)) by A23, Th14;

        ic >= (( Radix k) * icn2) by A25, INT_1: 6;

        then (icn2 * ( Radix k)) < (( Radix k) |^ (n + 1)) by A17, XXREAL_0: 2;

        then (icn2 * ( Radix k)) < ((( Radix k) |^ n) * ( Radix k)) by NEWTON: 6;

        then icn < (( Radix k) |^ n) by A23, XREAL_1: 64;

        then

         A60: icn is_represented_by (n,k) by RADIX_1:def 12;

        

         A61: for i be Element of NAT st i in ( Seg n) holds ( DigA (cn,i)) = ( DigA (c,(i + 1)))

        proof

          let i be Element of NAT ;

          assume

           A62: i in ( Seg n);

          ( DigA (c,(i + 1))) = ( DigB (c,(i + 1))) by RADIX_1:def 4

          .= (cn . i) by A7, A8, A62;

          hence thesis by A62, RADIX_1:def 3;

        end;

        

         A63: for i be Element of NAT st i in ( Seg n) holds (( Mul_mod (q,cn,f,k)) . i) = (( Mul_mod (q,c,f,k)) . i)

        proof

          defpred P[ Nat] means $1 in ( Seg n) implies (( Mul_mod (q,cn,f,k)) . $1) = (( Mul_mod (q,c,f,k)) . $1);

          

           A64: for i be Nat st P[i] holds P[(i + 1)]

          proof

            let i be Nat;

            assume

             A65: i in ( Seg n) implies (( Mul_mod (q,cn,f,k)) . i) = (( Mul_mod (q,c,f,k)) . i);

            

             A66: i = 0 or (i + 1) > (1 + 0 ) by XREAL_1: 6;

            assume (i + 1) in ( Seg n);

            then

             A67: (i + 1) <= n by FINSEQ_1: 1;

            then

             A68: ((i + 1) - 1) <= (n - 1) by XREAL_1: 9;

            

             A69: n in ( Seg n) by A2, FINSEQ_1: 1;

            now

              per cases by A66, NAT_1: 13;

                case

                 A70: i = 0 ;

                

                then (( Mul_mod (q,cn,f,k)) . (i + 1)) = ( Table1 (q,cn,f,n)) by A2, Def7

                .= ( Table1 (q,c,f,(n + 1))) by A61, A69

                .= (( Mul_mod (q,c,f,k)) . 1) by A12, Def7;

                hence thesis by A70;

              end;

                case

                 A71: i >= 1;

                reconsider nn = (n - 1) as Element of NAT by A2, INT_1: 5;

                

                 A72: i <= (nn + 1) by A68, NAT_1: 12;

                then i <= ((n + 1) - 1);

                then

                 A73: ex I1,I2 be Integer st I1 = (( Mul_mod (q,c,f,k)) . i) & I2 = (( Mul_mod (q,c,f,k)) . (i + 1)) & I2 = (((( Radix k) * I1) + ( Table1 (q,c,f,((n + 1) -' i)))) mod f) by A12, A71, Def7;

                

                 A74: (n -' i) <= n by NAT_D: 35;

                ((1 + i) - i) <= (n - i) by A67, XREAL_1: 9;

                then 1 <= (n -' i) by A72, XREAL_1: 233;

                then

                 A75: (n -' i) in ( Seg n) by A74, FINSEQ_1: 1;

                ex I1,I2 be Integer st I1 = (( Mul_mod (q,cn,f,k)) . i) & I2 = (( Mul_mod (q,cn,f,k)) . (i + 1)) & I2 = (((( Radix k) * I1) + ( Table1 (q,cn,f,(n -' i)))) mod f) by A2, A68, A71, Def7;

                

                then (( Mul_mod (q,cn,f,k)) . (i + 1)) = (((( Radix k) * (( Mul_mod (q,c,f,k)) . i)) + ((q * ( DigA (c,((n -' i) + 1)))) mod f)) mod f) by A61, A65, A71, A72, A75, FINSEQ_1: 1

                .= (( Mul_mod (q,c,f,k)) . (i + 1)) by A72, A73, NAT_D: 38;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

          

           A76: P[ 0 ] by FINSEQ_1: 1;

          for i be Nat holds P[i] from NAT_1:sch 2( A76, A64);

          hence thesis;

        end;

        n <= ((n + 1) - 1) & (n + 1) >= 1 by NAT_1: 11;

        then

         A77: ex I1,I2 be Integer st I1 = (( Mul_mod (q,c,f,k)) . n) & I2 = (( Mul_mod (q,c,f,k)) . (n + 1)) & I2 = (((( Radix k) * I1) + ( Table1 (q,c,f,((n + 1) -' n)))) mod f) by A2, Def7;

        n in ( Seg n) by A2, FINSEQ_1: 3;

        

        then (( Mul_mod (q,c,f,k)) . (n + 1)) = (((( Radix k) * (( Mul_mod (q,cn,f,k)) . n)) + ( Table1 (q,c,f,((n + 1) -' n)))) mod f) by A63, A77

        .= (((( Radix k) * ((q * icn) mod f)) + ( Table1 (q,c,f,((n + 1) -' n)))) mod f) by A3, A5, A60, A59

        .= (((( Radix k) * ((q * icn2) mod f)) + ( Table1 (q,c,f,((n + 1) -' n)))) mod f) by A6, A14, A20, Th13, FINSEQ_1: 14

        .= (((( Radix k) * ((q * icn2) mod f)) + ((q * ( DigA (c,1))) mod f)) mod f) by NAT_D: 34

        .= (((( Radix k) * ((q * icn2) mod f)) + ((q * (c2 . 1)) mod f)) mod f) by A19, A24, RADIX_1:def 3;

        hence thesis by A47;

      end;

      

       A78: PP[1]

      proof

        let q be Integer;

        let ic,f,k be Nat;

        assume that

         A79: ic is_represented_by (1,k) and f > 0 ;

        let c be Tuple of 1, (k -SD );

        assume

         A80: c = ( DecSD (ic,1,k));

        (( Mul_mod (q,c,f,k)) . 1) = ( Table1 (q,c,f,1)) by Def7

        .= ((q * ( SDDec ( DecSD (ic,1,k)))) mod f) by A80, Th7;

        hence thesis by A79, RADIX_1: 22;

      end;

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

      hence thesis;

    end;

    begin

    definition

      let n,f,j,m be Nat, e be Tuple of n, NAT ;

      :: RADIX_2:def8

      func Table2 (m,e,f,j) -> Element of NAT equals ((m |^ (e /. j)) mod f);

      correctness ;

    end

    definition

      let k,f,m,n be Nat, e be Tuple of n, NAT ;

      assume

       A1: n >= 1;

      :: RADIX_2:def9

      func Pow_mod (m,e,f,k) -> Tuple of n, NAT means

      : Def9: (it . 1) = ( Table2 (m,e,f,n)) & for i be Nat st 1 <= i & i <= (n - 1) holds ex i1,i2 be Nat st i1 = (it . i) & i2 = (it . (i + 1)) & i2 = ((((i1 |^ ( Radix k)) mod f) * ( Table2 (m,e,f,(n -' i)))) mod f);

      existence

      proof

        reconsider n1 = n as Element of NAT by ORDINAL1:def 12;

        reconsider T = ( Table2 (m,e,f,n)) as Element of NAT ;

        defpred PP[ Nat, set, set] means ex i1,i2 be Nat st i1 = $2 & i2 = $3 & i2 = ((((i1 |^ ( Radix k)) mod f) * ( Table2 (m,e,f,(n1 -' $1)))) mod f);

        

         A2: for i be Nat st 1 <= i & i < n1 holds for x be Element of NAT holds ex y be Element of NAT st PP[i, x, y]

        proof

          let i be Nat;

          assume that 1 <= i and i < n1;

          let x be Element of NAT ;

          reconsider x as Element of NAT ;

          consider y be Element of NAT such that

           A3: y = ((((x |^ ( Radix k)) mod f) * ( Table2 (m,e,f,(n -' i)))) mod f);

          reconsider z = y as Element of NAT ;

          take z;

          thus thesis by A3;

        end;

        consider r be FinSequence of NAT such that

         A4: ( len r) = n1 & ((r . 1) = T or n1 = 0 ) and

         A5: for i be Nat st 1 <= i & i < n1 holds PP[i, (r . i), (r . (i + 1))] from RECDEF_1:sch 4( A2);

        reconsider r as Tuple of n, NAT by A4, CARD_1:def 7;

        take r;

        thus (r . 1) = ( Table2 (m,e,f,n)) by A1, A4;

        let i be Nat;

        assume

         A6: 1 <= i & i <= (n - 1);

        thus thesis by A5, A6, XREAL_1: 147;

      end;

      uniqueness

      proof

        let s1,s2 be Tuple of n, NAT such that

         A7: (s1 . 1) = ( Table2 (m,e,f,n)) and

         A8: for i be Nat st 1 <= i & i <= (n - 1) holds ex I1,I2 be Nat st I1 = (s1 . i) & I2 = (s1 . (i + 1)) & I2 = ((((I1 |^ ( Radix k)) mod f) * ( Table2 (m,e,f,(n -' i)))) mod f) and

         A9: (s2 . 1) = ( Table2 (m,e,f,n)) and

         A10: for i be Nat st 1 <= i & i <= (n - 1) holds ex I1,I2 be Nat st I1 = (s2 . i) & I2 = (s2 . (i + 1)) & I2 = ((((I1 |^ ( Radix k)) mod f) * ( Table2 (m,e,f,(n -' i)))) mod f);

        defpred P[ Nat] means 1 <= $1 & $1 <= (n - 1) implies (s1 . $1) = (s2 . $1);

        

         A11: for i be Nat st P[i] holds P[(i + 1)]

        proof

          let kk be Nat;

          assume

           A12: 1 <= kk & kk <= (n - 1) implies (s1 . kk) = (s2 . kk);

          

           A13: 0 = kk or 0 < kk & ( 0 + 1) = 1;

          assume that 1 <= (kk + 1) and

           A14: (kk + 1) <= (n - 1);

          per cases by A13, NAT_1: 13;

            suppose 0 = kk;

            hence thesis by A7, A9;

          end;

            suppose

             A15: 1 <= kk;

            

             A16: kk <= (kk + 1) by NAT_1: 11;

            then kk <= (n - 1) by A14, XXREAL_0: 2;

            then (ex i1,i2 be Nat st i1 = (s1 . kk) & i2 = (s1 . (kk + 1)) & i2 = ((((i1 |^ ( Radix k)) mod f) * ( Table2 (m,e,f,(n -' kk)))) mod f)) & ex i1,i2 be Nat st i1 = (s2 . kk) & i2 = (s2 . (kk + 1)) & i2 = ((((i1 |^ ( Radix k)) mod f) * ( Table2 (m,e,f,(n -' kk)))) mod f) by A8, A10, A15;

            hence thesis by A12, A14, A15, A16, XXREAL_0: 2;

          end;

        end;

        

         A17: ( len s1) = n by CARD_1:def 7;

        

         A18: P[ 0 ];

        

         A19: for kk be Nat holds P[kk] from NAT_1:sch 2( A18, A11);

        

         A20: (s1 . n) = (s2 . n)

        proof

          (n - 1) >= (1 - 1) by A1, XREAL_1: 9;

          then

          reconsider U1 = (n - 1) as Element of NAT by INT_1: 3;

          now

            per cases ;

              suppose U1 = 0 ;

              hence thesis by A7, A9;

            end;

              suppose 0 < U1;

              then

               A21: 1 <= U1 by NAT_1: 14;

              then (ex i1,i2 be Nat st i1 = (s1 . U1) & i2 = (s1 . (U1 + 1)) & i2 = ((((i1 |^ ( Radix k)) mod f) * ( Table2 (m,e,f,(n -' U1)))) mod f)) & ex j1,j2 be Nat st j1 = (s2 . U1) & j2 = (s2 . (U1 + 1)) & j2 = ((((j1 |^ ( Radix k)) mod f) * ( Table2 (m,e,f,(n -' U1)))) mod f) by A8, A10;

              hence thesis by A19, A21;

            end;

          end;

          hence thesis;

        end;

        

         A22: for kk be Nat st 1 <= kk & kk <= ( len s1) holds (s1 . kk) = (s2 . kk)

        proof

          let kk be Nat;

          assume that

           A23: 1 <= kk and

           A24: kk <= ( len s1);

          now

            per cases by A24, XXREAL_0: 1;

              suppose

               A25: kk < ( len s1);

              (n - 1) >= (1 - 1) by A1, XREAL_1: 9;

              then

              reconsider U1 = (( len s1) - 1) as Element of NAT by A17, INT_1: 3;

              (U1 + 1) = ( len s1);

              then kk <= U1 by A25, NAT_1: 13;

              hence thesis by A17, A19, A23;

            end;

              suppose kk = ( len s1);

              hence thesis by A17, A20;

            end;

          end;

          hence thesis;

        end;

        ( len s1) = ( len s2) by A17, CARD_1:def 7;

        hence thesis by A22, FINSEQ_1: 14;

      end;

    end

    theorem :: RADIX_2:17

    for n be Nat st n >= 1 holds for m,k,f,ie be Nat st ie is_represented_by (n,k) & f > 0 holds for e be Tuple of n, NAT st e = ( DecSD2 (ie,n,k)) holds (( Pow_mod (m,e,f,k)) . n) = ((m |^ ie) mod f)

    proof

      defpred PP[ Nat] means for m,k,f,ie be Nat st ie is_represented_by ($1,k) & f > 0 holds for e be Tuple of $1, NAT st e = ( DecSD2 (ie,$1,k)) holds (( Pow_mod (m,e,f,k)) . $1) = ((m |^ ie) mod f);

      

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

      proof

        let n be Nat;

        assume that

         A2: n >= 1 and

         A3: PP[n];

        let m,k,f,ie be Nat;

        

         A4: (n + 1) >= 1 by NAT_1: 12;

        assume that

         A5: ie is_represented_by ((n + 1),k) and

         A6: f > 0 ;

        let e be Tuple of (n + 1), NAT ;

        assume

         A7: e = ( DecSD2 (ie,(n + 1),k));

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

        deffunc F( Nat) = (e . ($1 + 1));

        consider en be FinSequence of NAT such that

         A8: ( len en) = n and

         A9: for i be Nat st i in ( dom en) holds (en . i) = F(i) from FINSEQ_2:sch 1;

        

         A10: ( dom en) = ( Seg n) by A8, FINSEQ_1:def 3;

        reconsider en as Tuple of n, NAT by A8, CARD_1:def 7;

        

         A11: n in ( Seg n) by A2, FINSEQ_1: 1;

        

         A12: ie < (( Radix k) |^ (n + 1)) by A5, RADIX_1:def 12;

        set ien = ( SDDec2 (en,k));

        

         A13: 1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

        then

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

        

         A15: ie = ((ien * ( Radix k)) + (e /. 1))

        proof

          

           A16: ( len <*( SubDigit2 (e,1,k))*>) = 1 by FINSEQ_1: 39;

          deffunc F( Nat) = ( In ((( DigitSD2 (en,k)) . $1), REAL ));

          reconsider r2 = ( Radix k) as Element of REAL by XREAL_0:def 1;

          consider rD be FinSequence of REAL such that

           A17: ( len rD) = n and

           A18: for i be Nat st i in ( dom rD) holds (rD . i) = F(i) from FINSEQ_2:sch 1;

          

           A19: for i be Nat st i in ( dom rD) holds (rD . i) = (( DigitSD2 (en,k)) . i)

          proof

            let i be Nat;

            assume i in ( dom rD);

            then (rD . i) = F(i) by A18;

            hence thesis;

          end;

          reconsider rD as Tuple of n, REAL by A17, CARD_1:def 7;

          

           A20: ( dom rD) = ( Seg n) by A17, FINSEQ_1:def 3;

          reconsider rD1 = rD as Element of (n -tuples_on REAL ) by FINSEQ_2: 131;

          

           A21: ( dom ( DigitSD2 (en,k))) = ( Seg ( len ( DigitSD2 (en,k)))) by FINSEQ_1:def 3

          .= ( Seg n) by CARD_1:def 7;

          

          then

           A22: ( len (( Radix k) * ( DigitSD2 (en,k)))) = ( len (r2 * rD1)) by A19, A20, FINSEQ_1: 13

          .= n by CARD_1:def 7;

          

           A23: ( len ( <*( SubDigit2 (e,1,k))*> ^ (( Radix k) * ( DigitSD2 (en,k))))) = (( len <*( SubDigit2 (e,1,k))*>) + ( len (( Radix k) * ( DigitSD2 (en,k))))) by FINSEQ_1: 22

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

          

           A24: ( len ( DigitSD2 (e,k))) = (n + 1) by CARD_1:def 7;

          

           A25: for i be Nat st 1 <= i & i <= ( len ( DigitSD2 (e,k))) holds (( DigitSD2 (e,k)) . i) = (( <*( SubDigit2 (e,1,k))*> ^ (( Radix k) * ( DigitSD2 (en,k)))) . i)

          proof

            let i be Nat;

            assume that

             A26: 1 <= i and

             A27: i <= ( len ( DigitSD2 (e,k)));

            

             A28: i <= (n + 1) by A27, CARD_1:def 7;

            then

             A29: i in ( Seg (n + 1)) by A26, FINSEQ_1: 1;

            then

             A30: i in ( dom ( DigitSD2 (e,k))) by A24, FINSEQ_1:def 3;

            per cases ;

              suppose

               A31: i = 1;

              

              then (( <*( SubDigit2 (e,1,k))*> ^ (( Radix k) * ( DigitSD2 (en,k)))) . i) = ( SubDigit2 (e,1,k)) by FINSEQ_1: 41

              .= (( DigitSD2 (e,k)) /. 1) by A14, Def2

              .= (( DigitSD2 (e,k)) . 1) by A30, A31, PARTFUN1:def 6;

              hence thesis by A31;

            end;

              suppose

               A32: i <> 1;

              reconsider rs2 = (( DigitSD2 (en,k)) . (i - 1)) as Element of NAT ;

              reconsider rs = (rD . (i - 1)) as Real;

              (1 - 1) <= (i - 1) by A26, XREAL_1: 9;

              then

              reconsider i1 = (i - 1) as Element of NAT by INT_1: 3;

              1 < i by A26, A32, XXREAL_0: 1;

              then (1 + 1) <= i by INT_1: 7;

              then

               A33: ((1 + 1) - 1) <= (i - 1) by XREAL_1: 9;

              

               A34: (i - 1) <= ((n + 1) - 1) by A28, XREAL_1: 9;

              then

               A35: i1 in ( Seg n) by A33, FINSEQ_1: 1;

              

               A36: i1 in ( dom rD) by A20, A33, A34, FINSEQ_1: 1;

              1 < i by A26, A32, XXREAL_0: 1;

              

              then (( <*( SubDigit2 (e,1,k))*> ^ (( Radix k) * ( DigitSD2 (en,k)))) . i) = ((( Radix k) * ( DigitSD2 (en,k))) . (i - 1)) by A16, A23, A28, FINSEQ_1: 24

              .= ((r2 * rD) . (i - 1)) by A19, A21, A20, FINSEQ_1: 13

              .= (r2 * rs) by RVSUM_1: 45

              .= (( Radix k) * rs2) by A19, A21, A20, FINSEQ_1: 13

              .= (( Radix k) * (( DigitSD2 (en,k)) /. i1)) by A21, A20, A36, PARTFUN1:def 6

              .= (( Radix k) * ( SubDigit2 (en,i1,k))) by A35, Def2

              .= ((( Radix k) * (( Radix k) |^ (i1 -' 1))) * (en . i1))

              .= ((( Radix k) |^ ((i1 -' 1) + 1)) * (en . i1)) by NEWTON: 6

              .= ((( Radix k) |^ i1) * (en . i1)) by A33, XREAL_1: 235

              .= ((( Radix k) |^ i1) * (e . (i1 + 1))) by A9, A10, A35

              .= ( SubDigit2 (e,i,k)) by A26, XREAL_1: 233

              .= (( DigitSD2 (e,k)) /. i) by A29, Def2;

              hence thesis by A30, PARTFUN1:def 6;

            end;

          end;

          ( len ( DigitSD2 (e,k))) = ( len ( <*( SubDigit2 (e,1,k))*> ^ (( Radix k) * ( DigitSD2 (en,k))))) by A23, CARD_1:def 7;

          then

           A37: ( DigitSD2 (e,k)) = ( <*( SubDigit2 (e,1,k))*> ^ (( Radix k) * ( DigitSD2 (en,k)))) by A25, FINSEQ_1: 14;

          ( dom e) = ( Seg ( len e)) by FINSEQ_1:def 3;

          then

           A38: 1 in ( dom e) by A14, CARD_1:def 7;

          

           A39: (1 - 1) = 0 ;

          ie = ( SDDec2 (e,k)) by A5, A7, Th15, NAT_1: 12

          .= (( SubDigit2 (e,1,k)) + ( Sum (( Radix k) * ( DigitSD2 (en,k))))) by A37, RVSUM_1: 76

          .= (( SubDigit2 (e,1,k)) + ( Sum (r2 * rD))) by A19, A21, A20, FINSEQ_1: 13

          .= (( SubDigit2 (e,1,k)) + (r2 * ( Sum rD))) by RVSUM_1: 87

          .= (( SubDigit2 (e,1,k)) + (( Radix k) * ( SDDec2 (en,k)))) by A19, A21, A20, FINSEQ_1: 13

          .= (((( Radix k) |^ 0 ) * (e . 1)) + (( Radix k) * ien)) by A39, XREAL_0:def 2

          .= ((1 * (e . 1)) + (( Radix k) * ien)) by NEWTON: 4;

          hence thesis by A38, PARTFUN1:def 6;

        end;

        then ie >= (ien * ( Radix k)) by INT_1: 6;

        then (ien * ( Radix k)) < (( Radix k) |^ (n + 1)) by A12, XXREAL_0: 2;

        then (ien * ( Radix k)) < ((( Radix k) |^ n) * ( Radix k)) by NEWTON: 6;

        then ien < (( Radix k) |^ n) by XREAL_1: 64;

        then

         A40: ien is_represented_by (n,k) by RADIX_1:def 12;

        

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

        

         A42: for i be Element of NAT st i in ( Seg n) holds (( Pow_mod (m,en,f,k)) . i) = (( Pow_mod (m,e,f,k)) . i)

        proof

          defpred Z[ Nat] means $1 in ( Seg n) implies (( Pow_mod (m,en,f,k)) . $1) = (( Pow_mod (m,e,f,k)) . $1);

          

           A43: for i be Nat st Z[i] holds Z[(i + 1)]

          proof

            let i be Nat;

            assume

             A44: i in ( Seg n) implies (( Pow_mod (m,en,f,k)) . i) = (( Pow_mod (m,e,f,k)) . i);

            

             A45: i = 0 or (i + 1) > (1 + 0 ) by XREAL_1: 6;

            

             A46: ( dom en) = ( Seg n) by A8, FINSEQ_1:def 3;

            assume

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

            then

             A48: (i + 1) <= n by FINSEQ_1: 1;

            then

             A49: ((i + 1) - 1) <= (n - 1) by XREAL_1: 9;

            

             A50: ( dom e) = ( Seg ( len e)) by FINSEQ_1:def 3;

            then

             A51: ( dom e) = ( Seg (n + 1)) by CARD_1:def 7;

            now

              per cases by A45, NAT_1: 13;

                case

                 A52: i = 0 ;

                

                then (( Pow_mod (m,en,f,k)) . (i + 1)) = ( Table2 (m,en,f,n)) by A2, Def9

                .= ((m |^ (en . n)) mod f) by A11, A46, PARTFUN1:def 6

                .= ((m |^ (e . (n + 1))) mod f) by A9, A10, A11

                .= ( Table2 (m,e,f,(n + 1))) by A41, A51, PARTFUN1:def 6

                .= (( Pow_mod (m,e,f,k)) . 1) by A4, Def9;

                hence thesis by A52;

              end;

                case

                 A53: i >= 1;

                reconsider nn = (n - 1) as Element of NAT by A2, INT_1: 5;

                

                 A54: i <= (nn + 1) by A49, NAT_1: 12;

                then i <= ((n + 1) - 1);

                then

                 A55: ex I1,I2 be Nat st I1 = (( Pow_mod (m,e,f,k)) . i) & I2 = (( Pow_mod (m,e,f,k)) . (i + 1)) & I2 = ((((I1 |^ ( Radix k)) mod f) * ( Table2 (m,e,f,((n + 1) -' i)))) mod f) by A4, A53, Def9;

                

                 A56: ex I1,I2 be Nat st I1 = (( Pow_mod (m,en,f,k)) . i) & I2 = (( Pow_mod (m,en,f,k)) . (i + 1)) & I2 = ((((I1 |^ ( Radix k)) mod f) * ( Table2 (m,en,f,(n -' i)))) mod f) by A2, A49, A53, Def9;

                

                 A57: (n -' i) <= n by NAT_D: 35;

                (i + 1) <= n by A47, FINSEQ_1: 1;

                then ((i + 1) - 1) <= (n - 1) by XREAL_1: 9;

                then ((n + 1) -' i) >= ((n + 1) -' nn) by NAT_D: 41;

                then ((n + 1) -' i) >= ((n + 1) - (n - 1)) by XREAL_0:def 2;

                then ((n + 1) -' i) <= (n + 1) & 1 <= ((n + 1) -' i) by NAT_D: 35, XXREAL_0: 2;

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

                then

                 A58: ((n + 1) -' i) in ( dom e) by A50, CARD_1:def 7;

                ((1 + i) - i) <= (n - i) by A48, XREAL_1: 9;

                then 1 <= (n -' i) by A54, XREAL_1: 233;

                then

                 A59: (n -' i) in ( Seg n) by A57, FINSEQ_1: 1;

                then (n -' i) in ( dom en) by A8, FINSEQ_1:def 3;

                

                then (( Pow_mod (m,en,f,k)) . (i + 1)) = (((((( Pow_mod (m,e,f,k)) . i) |^ ( Radix k)) mod f) * ((m |^ (en . (n -' i))) mod f)) mod f) by A44, A53, A54, A56, FINSEQ_1: 1, PARTFUN1:def 6

                .= (((((( Pow_mod (m,e,f,k)) . i) |^ ( Radix k)) mod f) * ((m |^ (e . ((n -' i) + 1))) mod f)) mod f) by A9, A10, A59

                .= (((((( Pow_mod (m,e,f,k)) . i) |^ ( Radix k)) mod f) * ((m |^ (e . ((n + 1) -' i))) mod f)) mod f) by A54, NAT_D: 38

                .= (((((( Pow_mod (m,e,f,k)) . i) |^ ( Radix k)) mod f) * ( Table2 (m,e,f,((n + 1) -' i)))) mod f) by A58, PARTFUN1:def 6;

                hence thesis by A55;

              end;

            end;

            hence thesis;

          end;

          

           A60: Z[ 0 ] by FINSEQ_1: 1;

          for i be Nat holds Z[i] from NAT_1:sch 2( A60, A43);

          hence thesis;

        end;

        

         A61: ( Radix k) > 0 by Th6;

        

         A62: for i be Nat st 1 <= i & i <= ( len en) holds (en . i) = (( DecSD2 (ien,n,k)) . i)

        proof

          ( dom e) = ( Seg ( len e)) by FINSEQ_1:def 3;

          then

           A63: ( dom e) = ( Seg (n + 1)) by CARD_1:def 7;

          

           A64: (e . 1) = ( DigitDC2 (ie,1,k)) by A7, A14, Def5

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

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

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

          .= (ie mod ( Radix k));

          

           A65: 0 < ( Radix k) by Th6;

          

           A66: (((e . 1) + (ien * ( Radix k))) div ( Radix k)) = [\(((e . 1) + (ien * ( Radix k))) / ( Radix k))/] by INT_1:def 9

          .= [\(((e . 1) / ( Radix k)) + ien)/] by A65, XCMPLX_1: 113

          .= ( [\((e . 1) / ( Radix k))/] + ien) by INT_1: 28

          .= (((e . 1) div ( Radix k)) + ien) by INT_1:def 9

          .= ( 0 + ien) by A61, A64, NAT_D: 1, NAT_D: 27;

          

           A67: ( Radix k) <> 0 by Th6;

          let i be Nat;

          assume that

           A68: 1 <= i and

           A69: i <= ( len en);

          

           A70: 1 <= (i + 1) by A68, XREAL_1: 29;

          1 <= (i + 1) & (i + 1) <= (n + 1) by A8, A68, A69, XREAL_1: 6, XREAL_1: 29;

          then

           A71: (i + 1) in ( Seg (n + 1)) by FINSEQ_1: 1;

          

           A72: i in ( Seg n) by A8, A68, A69, FINSEQ_1: 1;

          

          then (en . i) = (e . (i + 1)) by A9, A10

          .= ( DigitDC2 (ie,(i + 1),k)) by A7, A71, Def5

          .= ((((ien * ( Radix k)) + (e /. 1)) div (( Radix k) |^ ((i + 1) -' 1))) mod ( Radix k)) by A15, A70, Th4, Th6

          .= ((((ien * ( Radix k)) + (e . 1)) div (( Radix k) |^ ((i + 1) -' 1))) mod ( Radix k)) by A13, A63, FINSEQ_2: 8, PARTFUN1:def 6

          .= ((((ien * ( Radix k)) + (e . 1)) div (( Radix k) |^ i)) mod ( Radix k)) by NAT_D: 34

          .= ((((ien * ( Radix k)) + (e . 1)) div (( Radix k) * (( Radix k) |^ (i -' 1)))) mod ( Radix k)) by A68, A67, PEPIN: 26

          .= (((((e . 1) + (ien * ( Radix k))) div ( Radix k)) div (( Radix k) |^ (i -' 1))) mod ( Radix k)) by NAT_2: 27

          .= ( DigitDC2 (ien,i,k)) by A68, A66, Th4, Th6;

          hence thesis by A72, Def5;

        end;

        ( len en) = ( len ( DecSD2 (ien,n,k))) by A8, CARD_1:def 7;

        then

         A73: en = ( DecSD2 (ien,n,k)) by A62, FINSEQ_1: 14;

        n <= ((n + 1) - 1) & (n + 1) >= 1 by NAT_1: 11;

        then ex I1,I2 be Nat st I1 = (( Pow_mod (m,e,f,k)) . n) & I2 = (( Pow_mod (m,e,f,k)) . (n + 1)) & I2 = ((((I1 |^ ( Radix k)) mod f) * ( Table2 (m,e,f,((n + 1) -' n)))) mod f) by A2, Def9;

        

        then (( Pow_mod (m,e,f,k)) . (n + 1)) = (((((( Pow_mod (m,en,f,k)) . n) |^ ( Radix k)) mod f) * ( Table2 (m,e,f,((n + 1) -' n)))) mod f) by A2, A42, FINSEQ_1: 3

        .= ((((((m |^ ien) mod f) |^ ( Radix k)) mod f) * ( Table2 (m,e,f,((n + 1) -' n)))) mod f) by A3, A6, A40, A73

        .= (((((m |^ ien) |^ ( Radix k)) mod f) * ( Table2 (m,e,f,((n + 1) -' n)))) mod f) by PEPIN: 12

        .= ((((m |^ ien) |^ ( Radix k)) * ( Table2 (m,e,f,((n + 1) -' n)))) mod f) by EULER_2: 8

        .= (((m |^ (ien * ( Radix k))) * ( Table2 (m,e,f,((n + 1) -' n)))) mod f) by NEWTON: 9

        .= (((m |^ (ien * ( Radix k))) * ((m |^ (e /. 1)) mod f)) mod f) by NAT_D: 34

        .= (((m |^ (ien * ( Radix k))) * (m |^ (e /. 1))) mod f) by EULER_2: 7

        .= ((m |^ ((ien * ( Radix k)) + (e /. 1))) mod f) by NEWTON: 8;

        hence thesis by A15;

      end;

      

       A74: PP[1]

      proof

        let m,k,f,ie be Nat;

        assume that

         A75: ie is_represented_by (1,k) and f > 0 ;

        ie < (( Radix k) |^ 1) by A75, RADIX_1:def 12;

        then

         A76: ie < ( Radix k);

        let e be Tuple of 1, NAT ;

        

         A77: (1 - 1) = 0 ;

        

         A78: 1 in ( Seg 1) by FINSEQ_1: 2, TARSKI:def 1;

        ( len ( DecSD2 (ie,1,k))) = 1 by CARD_1:def 7;

        then

         A79: 1 in ( dom ( DecSD2 (ie,1,k))) by A78, FINSEQ_1:def 3;

        assume e = ( DecSD2 (ie,1,k));

        

        then (e /. 1) = (( DecSD2 (ie,1,k)) . 1) by A79, PARTFUN1:def 6

        .= ( DigitDC2 (ie,1,k)) by A78, Def5

        .= ((ie mod (( Radix k) |^ 1)) div (( Radix k) |^ 0 )) by A77, XREAL_0:def 2

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

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

        .= (ie mod ( Radix k))

        .= ie by A76, NAT_D: 24;

        then ((m |^ ie) mod f) = ( Table2 (m,e,f,1));

        hence thesis by Def9;

      end;

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

      hence thesis;

    end;