radix_5.miz



    begin

    theorem :: RADIX_5:1

    

     Th1: for k be Nat st k >= 2 holds (( Radix k) - 1) in (k -SD )

    proof

      let k be Nat;

      assume k >= 2;

      then ( Radix k) > 2 by RADIX_4: 1;

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

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

      then

       A1: (( Radix k) - 1) > (( 0 + 1) - ( Radix k)) by XREAL_1: 21;

      (k -SD ) = { w where w be Element of INT : w <= (( Radix k) - 1) & w >= (( - ( Radix k)) + 1) } & (( Radix k) - 1) is Element of INT by INT_1:def 2, RADIX_1:def 2;

      hence thesis by A1;

    end;

    theorem :: RADIX_5:2

    

     Th2: for i,n be Nat st i > 1 & i in ( Seg n) holds (i -' 1) in ( Seg n)

    proof

      let i,n be Nat;

      assume that

       A1: i > 1 and

       A2: i in ( Seg n);

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

      then (i -' 1) > 0 by A1, XREAL_1: 233;

      then

       A3: (i -' 1) >= ( 0 + 1) by NAT_1: 13;

      i <= n by A2, FINSEQ_1: 1;

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

      hence thesis by A3, FINSEQ_1: 1;

    end;

    theorem :: RADIX_5:3

    

     Th3: for k be Nat st 2 <= k holds 4 <= ( Radix k)

    proof

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

      

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

      proof

        let kk be Nat;

        assume that 2 <= kk and

         A2: 4 <= ( Radix kk);

        ( Radix (kk + 1)) = (2 to_power (kk + 1)) by RADIX_1:def 1

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

        .= (2 * (2 to_power kk)) by POWER: 25

        .= (2 * ( Radix kk)) by RADIX_1:def 1;

        then ( Radix (kk + 1)) >= ( Radix kk) by XREAL_1: 151;

        hence thesis by A2, XXREAL_0: 2;

      end;

      ( Radix 2) = (2 to_power (1 + 1)) by RADIX_1:def 1

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

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

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

      then

       A3: P[2];

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

      hence thesis;

    end;

    theorem :: RADIX_5:4

    

     Th4: for k be Nat, tx be Tuple of 1, (k -SD ) holds ( SDDec tx) = ( DigA (tx,1))

    proof

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

      reconsider w = ( DigA (tx,1)) as Element of INT by INT_1:def 2;

      

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

      

      then

       A2: (( DigitSD tx) /. 1) = ( SubDigit (tx,1,k)) by RADIX_1:def 6

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

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

      .= ((( Radix k) |^ 0 ) * ( DigA (tx,1))) by XREAL_1: 232

      .= (1 * ( DigA (tx,1))) by NEWTON: 4;

      

       A3: ( len ( DigitSD tx)) = 1 by CARD_1:def 7;

      then 1 in ( dom ( DigitSD tx)) by A1, FINSEQ_1:def 3;

      then

       A4: (( DigitSD tx) . 1) = ( DigA (tx,1)) by A2, PARTFUN1:def 6;

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

      .= ( Sum <*w*>) by A3, A4, FINSEQ_1: 40

      .= ( DigA (tx,1)) by RVSUM_1: 73;

      hence thesis;

    end;

    begin

    theorem :: RADIX_5:5

    

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

    proof

      let i,k,n be Nat;

      assume

       A1: i in ( Seg n);

      then

       A2: i >= 1 by FINSEQ_1: 1;

      ( DigA (( DecSD ( 0 ,n,k)),i)) = ( DigitDC ( 0 ,i,k)) by A1, RADIX_1:def 9

      .= (( 0 mod (( Radix k) |^ i)) div (( Radix k) |^ (i -' 1))) by RADIX_1:def 8

      .= (( 0 div (( Radix k) |^ (i -' 1))) mod ( Radix k)) by A2, RADIX_2: 4, RADIX_2: 6

      .= ( 0 mod ( Radix k)) by NAT_2: 2;

      hence thesis by NAT_D: 26;

    end;

    theorem :: RADIX_5:6

    for n,k be Nat st n >= 1 holds ( SDDec ( DecSD ( 0 ,n,k))) = 0

    proof

      let n,k be Nat;

      ( Radix k) >= ( 0 + 1) by INT_1: 7, RADIX_2: 6;

      then (( Radix k) |^ n) >= 1 by PREPOWER: 11;

      then

       A1: 0 is_represented_by (n,k) by RADIX_1:def 12;

      assume n >= 1;

      hence thesis by A1, RADIX_1: 22;

    end;

    theorem :: RADIX_5:7

    

     Th7: for k,n be Nat st 1 in ( Seg n) & k >= 2 holds ( DigA (( DecSD (1,n,k)),1)) = 1

    proof

      let k,n be Nat;

      assume that

       A1: 1 in ( Seg n) and

       A2: k >= 2;

      

       A3: ( Radix k) > 2 by A2, RADIX_4: 1;

      then

       A4: ( Radix k) > 1 by XXREAL_0: 2;

      ( DigA (( DecSD (1,n,k)),1)) = ( DigitDC (1,1,k)) by A1, RADIX_1:def 9

      .= ((1 mod (( Radix k) |^ 1)) div (( Radix k) |^ (1 -' 1))) by RADIX_1:def 8

      .= ((1 div (( Radix k) |^ (1 -' 1))) mod ( Radix k)) by A3, RADIX_2: 4

      .= ((1 div (( Radix k) |^ 0 )) mod ( Radix k)) by NAT_2: 8

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

      .= (1 mod ( Radix k)) by NAT_2: 4;

      hence thesis by A4, NAT_D: 14;

    end;

    theorem :: RADIX_5:8

    

     Th8: for i,k,n be Nat st i in ( Seg n) & i > 1 & k >= 2 holds ( DigA (( DecSD (1,n,k)),i)) = 0

    proof

      let i,k,n be Nat;

      assume that

       A1: i in ( Seg n) and

       A2: i > 1 and

       A3: k >= 2;

      (i - 1) > (1 - 1) by A2, XREAL_1: 14;

      then

       A4: (i -' 1) > 0 by XREAL_0:def 2;

      

       A5: ( Radix k) > 2 by A3, RADIX_4: 1;

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

      then

       A6: (1 div (( Radix k) |^ (i -' 1))) = 0 by A4, NAT_D: 27, PEPIN: 25;

      ( DigA (( DecSD (1,n,k)),i)) = ( DigitDC (1,i,k)) by A1, RADIX_1:def 9

      .= ((1 mod (( Radix k) |^ i)) div (( Radix k) |^ (i -' 1))) by RADIX_1:def 8

      .= ((1 div (( Radix k) |^ (i -' 1))) mod ( Radix k)) by A2, A5, RADIX_2: 4;

      hence thesis by A6, NAT_D: 26;

    end;

    theorem :: RADIX_5:9

    for n,k be Nat st n >= 1 & k >= 2 holds ( SDDec ( DecSD (1,n,k))) = 1

    proof

      let n,k be Nat;

      assume that

       A1: n >= 1 and

       A2: k >= 2;

      

       A3: ( Radix k) > 2 by A2, RADIX_4: 1;

      ( Radix k) >= ( 0 + 1) by INT_1: 7, RADIX_2: 6;

      then (( Radix k) |^ n) >= ( Radix k) by A1, PREPOWER: 12;

      then (( Radix k) |^ n) >= 2 by A3, XXREAL_0: 2;

      then (( Radix k) |^ n) > 1 by XXREAL_0: 2;

      then 1 is_represented_by (n,k) by RADIX_1:def 12;

      hence thesis by A1, RADIX_1: 22;

    end;

    theorem :: RADIX_5:10

    

     Th10: for k be Nat st k >= 2 holds ( SD_Add_Carry ( Radix k)) = 1

    proof

      let k be Nat;

      assume k >= 2;

      then ( Radix k) > 2 by RADIX_4: 1;

      hence thesis by RADIX_1:def 10;

    end;

    theorem :: RADIX_5:11

    

     Th11: for k be Nat st k >= 2 holds ( SD_Add_Data (( Radix k),k)) = 0

    proof

      let k be Nat;

      assume k >= 2;

      then

       A1: ( SD_Add_Carry ( Radix k)) = 1 by Th10;

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

      .= (( Radix k) - ( Radix k)) by A1;

      hence thesis;

    end;

    begin

    

     Lm1: for k be Nat st 2 <= k holds ( SD_Add_Carry (( Radix k) - 1)) = 1

    proof

      let k be Nat;

      assume k >= 2;

      then ( Radix k) >= 4 by Th3;

      then (( Radix k) - 1) >= (4 - 1) by XREAL_1: 9;

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

      hence thesis by RADIX_1:def 10;

    end;

    

     Lm2: for n,k,i be Nat st k >= 2 & i in ( Seg n) holds ( SD_Add_Carry ( DigA (( DecSD (1,n,k)),i))) = 0

    proof

      let n,k,i be Nat;

      assume that

       A1: k >= 2 and

       A2: i in ( Seg n);

      

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

      now

        per cases by A3, XXREAL_0: 1;

          suppose i = 1;

          then ( SD_Add_Carry ( DigA (( DecSD (1,n,k)),i))) = ( SD_Add_Carry 1) by A1, A2, Th7;

          hence thesis by RADIX_1:def 10;

        end;

          suppose i > 1;

          then ( SD_Add_Carry ( DigA (( DecSD (1,n,k)),i))) = ( SD_Add_Carry 0 ) by A1, A2, Th8;

          hence thesis by RADIX_1:def 10;

        end;

      end;

      hence thesis;

    end;

    theorem :: RADIX_5:12

    

     Th12: for n be Nat st n >= 1 holds for k be Nat, tx,ty be Tuple of n, (k -SD ) st (for i be Nat st i in ( Seg n) holds ( DigA (tx,i)) = ( DigA (ty,i))) holds ( SDDec tx) = ( SDDec ty)

    proof

      defpred P[ Nat] means for k be Nat, tx,ty be Tuple of $1, (k -SD ) st (for i be Nat st i in ( Seg $1) holds ( DigA (tx,i)) = ( DigA (ty,i))) holds ( SDDec tx) = ( SDDec ty);

      

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

      proof

        let n be Nat;

        assume that n >= 1 and

         A2: P[n];

        let k be Nat, tx,ty be Tuple of (n + 1), (k -SD );

        assume

         A3: for i be Nat st i in ( Seg (n + 1)) holds ( DigA (tx,i)) = ( DigA (ty,i));

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

        consider txn be FinSequence of INT such that

         A4: ( len txn) = n and

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

        

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

        ( rng txn) c= (k -SD )

        proof

          let z be object;

          assume z in ( rng txn);

          then

          consider xx be object such that

           A7: xx in ( dom txn) and

           A8: z = (txn . xx) by FUNCT_1:def 3;

          reconsider xx as Element of NAT by A7;

          ( dom txn) = ( Seg n) by A4, FINSEQ_1:def 3;

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

          then

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

          z = ( DigB (tx,xx)) by A5, A7, A8

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

          hence thesis by A9;

        end;

        then

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

        

         A10: for i be Nat st i in ( Seg n) holds (txn . i) = (tx . i)

        proof

          let i be Nat;

          assume

           A11: i in ( Seg n);

          then

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

          (txn . i) = ( DigB (tx,i)) by A5, A6, A11

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

          hence thesis by A12, RADIX_1:def 3;

        end;

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

        consider tyn be FinSequence of INT such that

         A13: ( len tyn) = n and

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

        

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

        ( rng tyn) c= (k -SD )

        proof

          let z be object;

          assume z in ( rng tyn);

          then

          consider yy be object such that

           A16: yy in ( dom tyn) and

           A17: z = (tyn . yy) by FUNCT_1:def 3;

          reconsider yy as Element of NAT by A16;

          ( dom tyn) = ( Seg n) by A13, FINSEQ_1:def 3;

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

          then

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

          z = ( DigB (ty,yy)) by A14, A16, A17

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

          hence thesis by A18;

        end;

        then

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

        

         A19: for i be Nat st i in ( Seg n) holds (tyn . i) = (ty . i)

        proof

          let i be Nat;

          assume

           A20: i in ( Seg n);

          then

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

          (tyn . i) = ( DigB (ty,i)) by A14, A15, A20

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

          hence thesis by A21, RADIX_1:def 3;

        end;

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

        tyn is Element of (n -tuples_on (k -SD )) by A13, FINSEQ_2: 92;

        then

        reconsider tyn as Tuple of n, (k -SD );

        

         A22: (( SDDec tyn) + ((( Radix k) |^ n) * ( DigA (ty,(n + 1))))) = ( SDDec ty) by A19, RADIX_2: 10;

        txn is Element of (n -tuples_on (k -SD )) by A4, FINSEQ_2: 92;

        then

        reconsider txn as Tuple of n, (k -SD );

        for i be Nat st i in ( Seg n) holds ( DigA (txn,i)) = ( DigA (tyn,i))

        proof

          let i be Nat;

          assume

           A23: i in ( Seg n);

          

          then

           A24: ( DigA (tyn,i)) = (tyn . i) by RADIX_1:def 3

          .= ( DigB (ty,i)) by A14, A15, A23

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

          ( DigA (txn,i)) = (txn . i) by A23, RADIX_1:def 3

          .= ( DigB (tx,i)) by A5, A6, A23

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

          hence thesis by A3, A23, A24, FINSEQ_2: 8;

        end;

        then

         A25: ( SDDec txn) = ( SDDec tyn) by A2;

        (( SDDec txn) + ((( Radix k) |^ n) * ( DigA (tx,(n + 1))))) = ( SDDec tx) by A10, RADIX_2: 10;

        hence thesis by A3, A22, A25, FINSEQ_1: 4;

      end;

      

       A26: P[1]

      proof

        let k be Nat, tx,ty be Tuple of 1, (k -SD );

        assume

         A27: for i be Nat st i in ( Seg 1) holds ( DigA (tx,i)) = ( DigA (ty,i));

        

         A28: ( SDDec ty) = ( DigA (ty,1)) by Th4;

        1 in ( Seg 1) & ( SDDec tx) = ( DigA (tx,1)) by Th4, FINSEQ_1: 1;

        hence thesis by A27, A28;

      end;

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

      hence thesis;

    end;

    theorem :: RADIX_5:13

    for n be Nat st n >= 1 holds for k be Nat, tx,ty be Tuple of n, (k -SD ) st (for i be Nat st i in ( Seg n) holds ( DigA (tx,i)) >= ( DigA (ty,i))) holds ( SDDec tx) >= ( SDDec ty)

    proof

      defpred P[ Nat] means for k be Nat, tx,ty be Tuple of $1, (k -SD ) st (for i be Nat st i in ( Seg $1) holds ( DigA (tx,i)) >= ( DigA (ty,i))) holds ( SDDec tx) >= ( SDDec ty);

      

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

      proof

        let n be Nat;

        assume that n >= 1 and

         A2: P[n];

        let k be Nat, tx,ty be Tuple of (n + 1), (k -SD );

        assume

         A3: for i be Nat st i in ( Seg (n + 1)) holds ( DigA (tx,i)) >= ( DigA (ty,i));

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

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

        consider txn be FinSequence of INT such that

         A4: ( len txn) = n and

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

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

        consider tyn be FinSequence of INT such that

         A6: ( len tyn) = n and

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

        

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

        ( rng tyn) c= (k -SD )

        proof

          let z be object;

          assume z in ( rng tyn);

          then

          consider yy be object such that

           A9: yy in ( dom tyn) and

           A10: z = (tyn . yy) by FUNCT_1:def 3;

          reconsider yy as Element of NAT by A9;

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

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

          then

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

          z = ( DigB (ty,yy)) by A7, A9, A10

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

          hence thesis by A11;

        end;

        then

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

        

         A12: for i be Nat st i in ( Seg n) holds (tyn . i) = (ty . i)

        proof

          let i be Nat;

          assume

           A13: i in ( Seg n);

          then

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

          (tyn . i) = ( DigB (ty,i)) by A7, A8, A13

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

          hence thesis by A14, RADIX_1:def 3;

        end;

        tyn is Element of (n -tuples_on (k -SD )) by A6, FINSEQ_2: 92;

        then

        reconsider tyn as Tuple of n, (k -SD );

        

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

        ( rng txn) c= (k -SD )

        proof

          let z be object;

          assume z in ( rng txn);

          then

          consider xx be object such that

           A16: xx in ( dom txn) and

           A17: z = (txn . xx) by FUNCT_1:def 3;

          reconsider xx as Element of NAT by A16;

          ( dom txn) = ( Seg n) by A4, FINSEQ_1:def 3;

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

          then

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

          z = ( DigB (tx,xx)) by A5, A16, A17

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

          hence thesis by A18;

        end;

        then

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

        

         A19: for i be Nat st i in ( Seg n) holds (txn . i) = (tx . i)

        proof

          let i be Nat;

          assume

           A20: i in ( Seg n);

          then

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

          (txn . i) = ( DigB (tx,i)) by A5, A15, A20

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

          hence thesis by A21, RADIX_1:def 3;

        end;

        txn is Element of (n -tuples_on (k -SD )) by A4, FINSEQ_2: 92;

        then

        reconsider txn as Tuple of n, (k -SD );

        for i be Nat st i in ( Seg n) holds ( DigA (txn,i)) >= ( DigA (tyn,i))

        proof

          let i be Nat;

          assume

           A22: i in ( Seg n);

          

          then

           A23: ( DigA (tyn,i)) = (tyn . i) by RADIX_1:def 3

          .= ( DigB (ty,i)) by A7, A8, A22

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

          ( DigA (txn,i)) = (txn . i) by A22, RADIX_1:def 3

          .= ( DigB (tx,i)) by A5, A15, A22

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

          hence thesis by A3, A22, A23, FINSEQ_2: 8;

        end;

        then

         A24: ( SDDec txn) >= ( SDDec tyn) by A2;

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

        then

         A25: ((( Radix k) |^ n) * ( DigA (tx,(n + 1)))) >= ((( Radix k) |^ n) * ( DigA (ty,(n + 1)))) by A3, XREAL_1: 64;

        

         A26: (( SDDec tyn) + ((( Radix k) |^ n) * ( DigA (ty,(n + 1))))) = ( SDDec ty) by A12, RADIX_2: 10;

        (( SDDec txn) + ((( Radix k) |^ n) * ( DigA (tx,(n + 1))))) = ( SDDec tx) by A19, RADIX_2: 10;

        hence thesis by A26, A24, A25, XREAL_1: 7;

      end;

      

       A27: P[1]

      proof

        let k be Nat, tx,ty be Tuple of 1, (k -SD );

        assume

         A28: for i be Nat st i in ( Seg 1) holds ( DigA (tx,i)) >= ( DigA (ty,i));

        

         A29: ( SDDec ty) = ( DigA (ty,1)) by Th4;

        1 in ( Seg 1) & ( SDDec tx) = ( DigA (tx,1)) by Th4, FINSEQ_1: 1;

        hence thesis by A28, A29;

      end;

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

      hence thesis;

    end;

    theorem :: RADIX_5:14

    

     Th14: for n be Nat st n >= 1 holds for k be Nat st k >= 2 holds for tx,ty,tz,tw be Tuple of n, (k -SD ) st (for i be Nat st i in ( Seg n) holds (( DigA (tx,i)) = ( DigA (tz,i)) & ( DigA (ty,i)) = ( DigA (tw,i))) or (( DigA (ty,i)) = ( DigA (tz,i)) & ( DigA (tx,i)) = ( DigA (tw,i)))) holds (( SDDec tz) + ( SDDec tw)) = (( SDDec tx) + ( SDDec ty))

    proof

      defpred P[ Nat] means for k be Nat st k >= 2 holds for tx,ty,tz,tw be Tuple of $1, (k -SD ) st (for i be Nat st i in ( Seg $1) holds (( DigA (tx,i)) = ( DigA (tz,i)) & ( DigA (ty,i)) = ( DigA (tw,i))) or (( DigA (ty,i)) = ( DigA (tz,i)) & ( DigA (tx,i)) = ( DigA (tw,i)))) holds (( SDDec tz) + ( SDDec tw)) = (( SDDec tx) + ( SDDec ty));

      

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

      proof

        let n be Nat;

        assume that n >= 1 and

         A2: P[n];

        let k be Nat;

        assume

         A3: k >= 2;

        let tx,ty,tz,tw be Tuple of (n + 1), (k -SD );

        assume

         A4: for i be Nat st i in ( Seg (n + 1)) holds ( DigA (tx,i)) = ( DigA (tz,i)) & ( DigA (ty,i)) = ( DigA (tw,i)) or ( DigA (ty,i)) = ( DigA (tz,i)) & ( DigA (tx,i)) = ( DigA (tw,i));

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

        consider txn be FinSequence of INT such that

         A5: ( len txn) = n and

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

        

         A7: ( dom txn) = ( Seg n) by A5, FINSEQ_1:def 3;

        ( rng txn) c= (k -SD )

        proof

          let z be object;

          assume z in ( rng txn);

          then

          consider xx be object such that

           A8: xx in ( dom txn) and

           A9: z = (txn . xx) by FUNCT_1:def 3;

          reconsider xx as Element of NAT by A8;

          ( dom txn) = ( Seg n) by A5, FINSEQ_1:def 3;

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

          then

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

          z = ( DigB (tx,xx)) by A6, A8, A9

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

          hence thesis by A10;

        end;

        then

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

        

         A11: for i be Nat st i in ( Seg n) holds (txn . i) = (tx . i)

        proof

          let i be Nat;

          assume

           A12: i in ( Seg n);

          then

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

          (txn . i) = ( DigB (tx,i)) by A6, A7, A12

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

          hence thesis by A13, RADIX_1:def 3;

        end;

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

        consider tyn be FinSequence of INT such that

         A14: ( len tyn) = n and

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

        

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

        ( rng tyn) c= (k -SD )

        proof

          let z be object;

          assume z in ( rng tyn);

          then

          consider yy be object such that

           A17: yy in ( dom tyn) and

           A18: z = (tyn . yy) by FUNCT_1:def 3;

          reconsider yy as Element of NAT by A17;

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

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

          then

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

          z = ( DigB (ty,yy)) by A15, A17, A18

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

          hence thesis by A19;

        end;

        then

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

        

         A20: for i be Nat st i in ( Seg n) holds (tyn . i) = (ty . i)

        proof

          let i be Nat;

          assume

           A21: i in ( Seg n);

          then

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

          (tyn . i) = ( DigB (ty,i)) by A15, A16, A21

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

          hence thesis by A22, RADIX_1:def 3;

        end;

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

        consider tzn be FinSequence of INT such that

         A23: ( len tzn) = n and

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

        

         A25: ( dom tzn) = ( Seg n) by A23, FINSEQ_1:def 3;

        ( rng tzn) c= (k -SD )

        proof

          let z be object;

          assume z in ( rng tzn);

          then

          consider zz be object such that

           A26: zz in ( dom tzn) and

           A27: z = (tzn . zz) by FUNCT_1:def 3;

          reconsider zz as Element of NAT by A26;

          ( dom tzn) = ( Seg n) by A23, FINSEQ_1:def 3;

          then zz in ( Seg (n + 1)) by A26, FINSEQ_2: 8;

          then

           A28: ( DigA (tz,zz)) is Element of (k -SD ) by RADIX_1: 16;

          z = ( DigB (tz,zz)) by A24, A26, A27

          .= ( DigA (tz,zz)) by RADIX_1:def 4;

          hence thesis by A28;

        end;

        then

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

        

         A29: for i be Nat st i in ( Seg n) holds (tzn . i) = (tz . i)

        proof

          let i be Nat;

          assume

           A30: i in ( Seg n);

          then

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

          (tzn . i) = ( DigB (tz,i)) by A24, A25, A30

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

          hence thesis by A31, RADIX_1:def 3;

        end;

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

        consider twn be FinSequence of INT such that

         A32: ( len twn) = n and

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

        

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

        ( rng twn) c= (k -SD )

        proof

          let w be object;

          assume w in ( rng twn);

          then

          consider ww be object such that

           A35: ww in ( dom twn) and

           A36: w = (twn . ww) by FUNCT_1:def 3;

          reconsider ww as Element of NAT by A35;

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

          then ww in ( Seg (n + 1)) by A35, FINSEQ_2: 8;

          then

           A37: ( DigA (tw,ww)) is Element of (k -SD ) by RADIX_1: 16;

          w = ( DigB (tw,ww)) by A33, A35, A36

          .= ( DigA (tw,ww)) by RADIX_1:def 4;

          hence thesis by A37;

        end;

        then

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

        

         A38: for i be Nat st i in ( Seg n) holds (twn . i) = (tw . i)

        proof

          let i be Nat;

          assume

           A39: i in ( Seg n);

          then

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

          (twn . i) = ( DigB (tw,i)) by A33, A34, A39

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

          hence thesis by A40, RADIX_1:def 3;

        end;

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

        twn is Element of (n -tuples_on (k -SD )) by A32, FINSEQ_2: 92;

        then

        reconsider twn as Tuple of n, (k -SD );

        tzn is Element of (n -tuples_on (k -SD )) by A23, FINSEQ_2: 92;

        then

        reconsider tzn as Tuple of n, (k -SD );

        tyn is Element of (n -tuples_on (k -SD )) by A14, FINSEQ_2: 92;

        then

        reconsider tyn as Tuple of n, (k -SD );

        

         A41: (( SDDec tyn) + ((( Radix k) |^ n) * ( DigA (ty,(n + 1))))) = ( SDDec ty) by A20, RADIX_2: 10;

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

        then

         A42: ( DigA (tx,(n + 1))) = ( DigA (tz,(n + 1))) & ( DigA (ty,(n + 1))) = ( DigA (tw,(n + 1))) or ( DigA (ty,(n + 1))) = ( DigA (tz,(n + 1))) & ( DigA (tx,(n + 1))) = ( DigA (tw,(n + 1))) by A4;

        

         A43: (( SDDec twn) + ((( Radix k) |^ n) * ( DigA (tw,(n + 1))))) = ( SDDec tw) by A38, RADIX_2: 10;

        

         A44: (( SDDec tzn) + ((( Radix k) |^ n) * ( DigA (tz,(n + 1))))) = ( SDDec tz) by A29, RADIX_2: 10;

        txn is Element of (n -tuples_on (k -SD )) by A5, FINSEQ_2: 92;

        then

        reconsider txn as Tuple of n, (k -SD );

        for i be Nat st i in ( Seg n) holds ( DigA (txn,i)) = ( DigA (tzn,i)) & ( DigA (tyn,i)) = ( DigA (twn,i)) or ( DigA (tyn,i)) = ( DigA (tzn,i)) & ( DigA (txn,i)) = ( DigA (twn,i))

        proof

          let i be Nat;

          assume

           A45: i in ( Seg n);

          then i <= n by FINSEQ_1: 1;

          then

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

          1 <= i by A45, FINSEQ_1: 1;

          then

           A47: i in ( Seg (n + 1)) by A46, FINSEQ_1: 1;

          

          then

           A48: ( DigA (ty,i)) = (ty . i) by RADIX_1:def 3

          .= (tyn . i) by A20, A45

          .= ( DigA (tyn,i)) by A45, RADIX_1:def 3;

          

           A49: ( DigA (tw,i)) = (tw . i) by A47, RADIX_1:def 3

          .= (twn . i) by A38, A45

          .= ( DigA (twn,i)) by A45, RADIX_1:def 3;

          

           A50: ( DigA (tz,i)) = (tz . i) by A47, RADIX_1:def 3

          .= (tzn . i) by A29, A45

          .= ( DigA (tzn,i)) by A45, RADIX_1:def 3;

          ( DigA (tx,i)) = (tx . i) by A47, RADIX_1:def 3

          .= (txn . i) by A11, A45

          .= ( DigA (txn,i)) by A45, RADIX_1:def 3;

          hence thesis by A4, A47, A48, A50, A49;

        end;

        then

         A51: (( SDDec tzn) + ( SDDec twn)) = (( SDDec txn) + ( SDDec tyn)) by A2, A3;

        (( SDDec txn) + ((( Radix k) |^ n) * ( DigA (tx,(n + 1))))) = ( SDDec tx) by A11, RADIX_2: 10;

        hence thesis by A41, A44, A43, A51, A42;

      end;

      

       A52: P[1]

      proof

        let k be Nat;

        assume

         A53: k >= 2;

        let tx,ty,tz,tw be Tuple of 1, (k -SD );

        

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

        

         A55: ( SDDec (tx '+' ty)) = ( DigA ((tx '+' ty),1)) by Th4

        .= ( Add (tx,ty,1,k)) by A54, RADIX_1:def 14

        .= (( SD_Add_Data ((( DigA (tx,1)) + ( DigA (ty,1))),k)) + ( SD_Add_Carry (( DigA (tx,(1 -' 1))) + ( DigA (ty,(1 -' 1)))))) by A53, A54, RADIX_1:def 13

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

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

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

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

        .= (( SD_Add_Data ((( DigA (tx,1)) + ( DigA (ty,1))),k)) + 0 ) by RADIX_1:def 10;

        

         A56: ( SDDec (tz '+' tw)) = ( DigA ((tz '+' tw),1)) by Th4

        .= ( Add (tz,tw,1,k)) by A54, RADIX_1:def 14

        .= (( SD_Add_Data ((( DigA (tz,1)) + ( DigA (tw,1))),k)) + ( SD_Add_Carry (( DigA (tz,(1 -' 1))) + ( DigA (tw,(1 -' 1)))))) by A53, A54, RADIX_1:def 13

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

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

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

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

        .= (( SD_Add_Data ((( DigA (tz,1)) + ( DigA (tw,1))),k)) + 0 ) by RADIX_1:def 10;

        

         A57: ( DigA (tx,1)) = ( DigA (tz,1)) & ( DigA (ty,1)) = ( DigA (tw,1)) implies (( SDDec tz) + ( SDDec tw)) = (( SDDec tx) + ( SDDec ty))

        proof

          assume ( DigA (tx,1)) = ( DigA (tz,1)) & ( DigA (ty,1)) = ( DigA (tw,1));

          then (( SDDec tz) + ( SDDec tw)) = (( SDDec (tx '+' ty)) + (( SD_Add_Carry (( DigA (tx,1)) + ( DigA (ty,1)))) * (( Radix k) |^ 1))) by A53, A56, A55, RADIX_2: 11;

          hence thesis by A53, RADIX_2: 11;

        end;

        assume

         A58: for j be Nat st j in ( Seg 1) holds ( DigA (tx,j)) = ( DigA (tz,j)) & ( DigA (ty,j)) = ( DigA (tw,j)) or ( DigA (ty,j)) = ( DigA (tz,j)) & ( DigA (tx,j)) = ( DigA (tw,j));

        then

         A59: ( DigA (tx,1)) = ( DigA (tz,1)) & ( DigA (ty,1)) = ( DigA (tw,1)) or ( DigA (ty,1)) = ( DigA (tz,1)) & ( DigA (tx,1)) = ( DigA (tw,1)) by A54;

        ( DigA (ty,1)) = ( DigA (tz,1)) & ( DigA (tx,1)) = ( DigA (tw,1)) implies (( SDDec tz) + ( SDDec tw)) = (( SDDec tx) + ( SDDec ty))

        proof

          assume that ( DigA (ty,1)) = ( DigA (tz,1)) and ( DigA (tx,1)) = ( DigA (tw,1));

          (( SDDec tz) + ( SDDec tw)) = (( SDDec (tx '+' ty)) + (( SD_Add_Carry (( DigA (tx,1)) + ( DigA (ty,1)))) * (( Radix k) |^ 1))) by A53, A56, A55, A59, RADIX_2: 11;

          hence thesis by A53, RADIX_2: 11;

        end;

        hence thesis by A58, A54, A57;

      end;

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

      hence thesis;

    end;

    theorem :: RADIX_5:15

    for n,k be Nat st n >= 1 & k >= 2 holds for tx,ty,tz be Tuple of n, (k -SD ) st (for i be Nat st i in ( Seg n) holds (( DigA (tx,i)) = ( DigA (tz,i)) & ( DigA (ty,i)) = 0 ) or (( DigA (ty,i)) = ( DigA (tz,i)) & ( DigA (tx,i)) = 0 )) holds (( SDDec tz) + ( SDDec ( DecSD ( 0 ,n,k)))) = (( SDDec tx) + ( SDDec ty))

    proof

      let n,k be Nat;

      assume

       A1: n >= 1 & k >= 2;

      let tx,ty,tz be Tuple of n, (k -SD );

      assume

       A2: for i be Nat st i in ( Seg n) holds ( DigA (tx,i)) = ( DigA (tz,i)) & ( DigA (ty,i)) = 0 or ( DigA (ty,i)) = ( DigA (tz,i)) & ( DigA (tx,i)) = 0 ;

      for i be Nat st i in ( Seg n) holds ( DigA (tx,i)) = ( DigA (tz,i)) & ( DigA (ty,i)) = ( DigA (( DecSD ( 0 ,n,k)),i)) or ( DigA (ty,i)) = ( DigA (tz,i)) & ( DigA (tx,i)) = ( DigA (( DecSD ( 0 ,n,k)),i))

      proof

        let i be Nat;

        assume

         A3: i in ( Seg n);

        then ( DigA (( DecSD ( 0 ,n,k)),i)) = 0 by Th5;

        hence thesis by A2, A3;

      end;

      hence thesis by A1, Th14;

    end;

    begin

    definition

      let i,m,k be Nat;

      assume

       A1: k >= 2;

      :: RADIX_5:def1

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

      : Def1: (( - ( Radix k)) + 1) if 1 <= i & i < m

      otherwise 0 ;

      coherence

      proof

        ( Radix k) > 2 by A1, RADIX_4: 1;

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

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

        then

         A2: (( Radix k) - 1) > (1 - ( Radix k)) by XREAL_1: 21;

        (k -SD ) = { w where w be Element of INT : w <= (( Radix k) - 1) & w >= (( - ( Radix k)) + 1) } & (( - ( Radix k)) + 1) is Element of INT by INT_1:def 2, RADIX_1:def 2;

        then (( - ( Radix k)) + 1) in (k -SD ) by A2;

        hence thesis by RADIX_1: 14;

      end;

      consistency ;

    end

    definition

      let n,m,k be Nat;

      :: RADIX_5:def2

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

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

      existence

      proof

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

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

         A1: ( len z) = n and

         A2: for j be Nat st j in ( dom z) holds (z . j) = F(j) from FINSEQ_2:sch 1;

        

         A3: ( dom z) = ( Seg n) by A1, FINSEQ_1:def 3;

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

        then

        reconsider z as Tuple of n, (k -SD );

        take z;

        let i be Nat;

        assume

         A4: i in ( Seg n);

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

        hence thesis by A2, A3, A4;

      end;

      uniqueness

      proof

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

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

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

        

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

        then

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

         A9:

        now

          let j be Nat;

          assume

           A10: j in ( dom k1);

          

          then (k1 . j) = ( DigA (k1,j)) by A8, RADIX_1:def 3

          .= ( SDMinDigit (m,k,j)) by A5, A8, A10

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

          .= (k2 . j) by A8, A10, RADIX_1:def 3;

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

        end;

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

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    definition

      let i,m,k be Nat;

      assume

       A1: k >= 2;

      :: RADIX_5:def3

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

      : Def3: (( Radix k) - 1) if 1 <= i & i < m

      otherwise 0 ;

      coherence by A1, Th1, RADIX_1: 14;

      consistency ;

    end

    definition

      let n,m,k be Nat;

      :: RADIX_5:def4

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

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

      existence

      proof

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

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

         A1: ( len z) = n and

         A2: for j be Nat st j in ( dom z) holds (z . j) = F(j) from FINSEQ_2:sch 1;

        

         A3: ( dom z) = ( Seg n) by A1, FINSEQ_1:def 3;

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

        then

        reconsider z as Tuple of n, (k -SD );

        take z;

        let i be Nat;

        assume

         A4: i in ( Seg n);

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

        hence thesis by A2, A3, A4;

      end;

      uniqueness

      proof

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

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

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

        

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

        then

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

         A9:

        now

          let j be Nat;

          assume

           A10: j in ( dom k1);

          

          then (k1 . j) = ( DigA (k1,j)) by A8, RADIX_1:def 3

          .= ( SDMaxDigit (m,k,j)) by A5, A8, A10

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

          .= (k2 . j) by A8, A10, RADIX_1:def 3;

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

        end;

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

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    definition

      let i,m,k be Nat;

      assume

       A1: k >= 2;

      :: RADIX_5:def5

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

      : Def5: 1 if i = m

      otherwise 0 ;

      coherence

      proof

        

         A2: ( Radix k) > 2 by A1, RADIX_4: 1;

        then ( - ( Radix k)) < ( - 2) by XREAL_1: 24;

        then

         A3: (( - ( Radix k)) + 1) < (( - 2) + 1) by XREAL_1: 6;

        

         A4: (k -SD ) = { w where w be Element of INT : w <= (( Radix k) - 1) & w >= (( - ( Radix k)) + 1) } & 1 is Element of INT by INT_1:def 2, RADIX_1:def 2;

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

        then 1 in (k -SD ) by A3, A4;

        hence thesis by RADIX_1: 14;

      end;

      consistency ;

    end

    definition

      let n,m,k be Nat;

      :: RADIX_5:def6

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

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

      existence

      proof

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

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

         A1: ( len z) = n and

         A2: for j be Nat st j in ( dom z) holds (z . j) = F(j) from FINSEQ_2:sch 1;

        

         A3: ( dom z) = ( Seg n) by A1, FINSEQ_1:def 3;

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

        then

        reconsider z as Tuple of n, (k -SD );

        take z;

        let i be Nat;

        assume

         A4: i in ( Seg n);

        

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

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

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

        

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

        then

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

         A9:

        now

          let j be Nat;

          assume

           A10: j in ( dom k1);

          

          then (k1 . j) = ( DigA (k1,j)) by A8, RADIX_1:def 3

          .= ( FminDigit (m,k,j)) by A5, A8, A10

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

          .= (k2 . j) by A8, A10, RADIX_1:def 3;

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

        end;

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

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    definition

      let i,m,k be Nat;

      assume

       A1: k >= 2;

      :: RADIX_5:def7

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

      : Def7: (( Radix k) - 1) if i = m

      otherwise 0 ;

      coherence by A1, Th1, RADIX_1: 14;

      consistency ;

    end

    definition

      let n,m,k be Nat;

      :: RADIX_5:def8

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

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

      existence

      proof

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

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

         A1: ( len z) = n and

         A2: for j be Nat st j in ( dom z) holds (z . j) = F(j) from FINSEQ_2:sch 1;

        

         A3: ( dom z) = ( Seg n) by A1, FINSEQ_1:def 3;

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

        then

        reconsider z as Tuple of n, (k -SD );

        take z;

        let i be Nat;

        assume

         A4: i in ( Seg n);

        

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

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

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

        

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

        then

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

         A9:

        now

          let j be Nat;

          assume

           A10: j in ( dom k1);

          

          then (k1 . j) = ( DigA (k1,j)) by A8, RADIX_1:def 3

          .= ( FmaxDigit (m,k,j)) by A5, A8, A10

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

          .= (k2 . j) by A8, A10, RADIX_1:def 3;

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

        end;

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

        hence thesis by A7, A9, FINSEQ_2: 9;

      end;

    end

    begin

    theorem :: RADIX_5:16

    

     Th16: for n,m,k be Nat st k >= 2 holds for i be Nat st i in ( Seg n) holds (( DigA (( SDMax (n,m,k)),i)) + ( DigA (( SDMin (n,m,k)),i))) = 0

    proof

      let n,m,k be Nat;

      assume

       A1: k >= 2;

      let i be Nat;

      reconsider a = ( SDMinDigit (m,k,i)) as Element of INT ;

      reconsider b = ( SDMaxDigit (m,k,i)) as Element of INT ;

      assume

       A2: i in ( Seg n);

      then

       A3: i >= 1 by FINSEQ_1: 1;

      

       A4: ( DigA (( SDMin (n,m,k)),i)) = ( SDMinDigit (m,k,i)) by A2, Def2;

      now

        per cases ;

          suppose

           A5: i < m;

          

          then (a + b) = ((( - ( Radix k)) + 1) + b) by A1, A3, Def1

          .= ((( - ( Radix k)) + 1) + (( Radix k) - 1)) by A1, A3, A5, Def3

          .= 0 ;

          hence thesis by A2, A4, Def4;

        end;

          suppose

           A6: i >= m;

          

          then (a + b) = ( 0 + b) by A1, Def1

          .= ( 0 + 0 ) by A1, A6, Def3;

          hence thesis by A2, A4, Def4;

        end;

      end;

      hence thesis;

    end;

    theorem :: RADIX_5:17

    for n be Nat st n >= 1 holds for m,k be Nat st k >= 2 holds (( SDDec ( SDMax (n,m,k))) + ( SDDec ( SDMin (n,m,k)))) = ( SDDec ( DecSD ( 0 ,n,k)))

    proof

      let n be Nat;

      assume

       A1: n >= 1;

      then

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

      let m,k be Nat;

      assume

       A3: k >= 2;

      

       A4: for i be Nat st i in ( Seg n) holds ( DigA (( DecSD ( 0 ,n,k)),i)) = ( DigA ((( SDMax (n,m,k)) '+' ( SDMin (n,m,k))),i))

      proof

        let i be Nat;

        assume

         A5: i in ( Seg n);

        

        then

         A6: ( DigA ((( SDMax (n,m,k)) '+' ( SDMin (n,m,k))),i)) = ( Add (( SDMax (n,m,k)),( SDMin (n,m,k)),i,k)) by RADIX_1:def 14

        .= (( SD_Add_Data ((( DigA (( SDMax (n,m,k)),i)) + ( DigA (( SDMin (n,m,k)),i))),k)) + ( SD_Add_Carry (( DigA (( SDMax (n,m,k)),(i -' 1))) + ( DigA (( SDMin (n,m,k)),(i -' 1)))))) by A3, A5, RADIX_1:def 13

        .= (( SD_Add_Data ( 0 ,k)) + ( SD_Add_Carry (( DigA (( SDMax (n,m,k)),(i -' 1))) + ( DigA (( SDMin (n,m,k)),(i -' 1)))))) by A3, A5, Th16

        .= ( 0 + ( SD_Add_Carry (( DigA (( SDMax (n,m,k)),(i -' 1))) + ( DigA (( SDMin (n,m,k)),(i -' 1)))))) by RADIX_1: 19;

        

         A7: ( DigA (( DecSD ( 0 ,n,k)),i)) = 0 by A5, Th5;

        

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

        now

          per cases by A8, XXREAL_0: 1;

            suppose

             A9: i = 1;

            then ( DigA (( SDMin (n,m,k)),(i -' 1))) = 0 by NAT_2: 8, RADIX_1:def 3;

            then ( DigA ((( SDMax (n,m,k)) '+' ( SDMin (n,m,k))),i)) = ( SD_Add_Carry ( 0 + 0 )) by A6, A9, NAT_2: 8, RADIX_1:def 3;

            hence thesis by A7, RADIX_1:def 10;

          end;

            suppose i > 1;

            then (i -' 1) in ( Seg n) by A5, Th2;

            then ( DigA ((( SDMax (n,m,k)) '+' ( SDMin (n,m,k))),i)) = ( SD_Add_Carry 0 ) by A3, A6, Th16;

            hence thesis by A7, RADIX_1:def 10;

          end;

        end;

        hence thesis;

      end;

      (( SDDec ( SDMax (n,m,k))) + ( SDDec ( SDMin (n,m,k)))) = (( SDDec (( SDMax (n,m,k)) '+' ( SDMin (n,m,k)))) + (( SD_Add_Carry (( DigA (( SDMax (n,m,k)),n)) + ( DigA (( SDMin (n,m,k)),n)))) * (( Radix k) |^ n))) by A1, A3, RADIX_2: 11

      .= (( SDDec (( SDMax (n,m,k)) '+' ( SDMin (n,m,k)))) + (( SD_Add_Carry 0 ) * (( Radix k) |^ n))) by A3, A2, Th16

      .= (( SDDec (( SDMax (n,m,k)) '+' ( SDMin (n,m,k)))) + ( 0 * (( Radix k) |^ n))) by RADIX_1:def 10;

      hence thesis by A1, A4, Th12;

    end;

    theorem :: RADIX_5:18

    for n be Nat st n >= 1 holds for m,k be Nat st m in ( Seg n) & k >= 2 holds ( SDDec ( Fmin (n,m,k))) = (( SDDec ( SDMax (n,m,k))) + ( SDDec ( DecSD (1,n,k))))

    proof

      let n be Nat;

      

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

      assume

       A2: n >= 1;

      then

       A3: 1 in ( Seg n) by FINSEQ_1: 1;

      let m,k be Nat;

      assume that

       A4: m in ( Seg n) and

       A5: k >= 2;

      

       A6: n >= m by A4, FINSEQ_1: 1;

      

       A7: m >= 1 by A4, FINSEQ_1: 1;

      now

        per cases by A2, XXREAL_0: 1;

          suppose

           A8: n = 1;

          then

           A9: m = 1 by A6, A7, XXREAL_0: 1;

          

           A10: ( SDDec ( Fmin (1,m,k))) = ( DigA (( Fmin (1,m,k)),1)) by Th4

          .= ( FminDigit (m,k,1)) by A1, Def6

          .= 1 by A5, A9, Def5;

          

           A11: ( DigA (( SDMax (1,m,k)),1)) = ( SDMaxDigit (m,k,1)) by A1, Def4

          .= 0 by A5, A6, A8, Def3;

          ( SDDec (( SDMax (1,m,k)) '+' ( DecSD (1,1,k)))) = ( DigA ((( SDMax (1,m,k)) '+' ( DecSD (1,1,k))),1)) by Th4

          .= ( Add (( SDMax (1,m,k)),( DecSD (1,1,k)),1,k)) by A1, RADIX_1:def 14

          .= (( SD_Add_Data ((( DigA (( SDMax (1,m,k)),1)) + ( DigA (( DecSD (1,1,k)),1))),k)) + ( SD_Add_Carry (( DigA (( SDMax (1,m,k)),(1 -' 1))) + ( DigA (( DecSD (1,1,k)),(1 -' 1)))))) by A5, A1, RADIX_1:def 13

          .= (( SD_Add_Data ((( DigA (( SDMax (1,m,k)),1)) + ( DigA (( DecSD (1,1,k)),1))),k)) + ( SD_Add_Carry (( DigA (( SDMax (1,m,k)), 0 )) + ( DigA (( DecSD (1,1,k)),(1 -' 1)))))) by XREAL_1: 232

          .= (( SD_Add_Data ((( DigA (( SDMax (1,m,k)),1)) + ( DigA (( DecSD (1,1,k)),1))),k)) + ( SD_Add_Carry (( DigA (( SDMax (1,m,k)), 0 )) + ( DigA (( DecSD (1,1,k)), 0 ))))) by XREAL_1: 232

          .= (( SD_Add_Data ((( DigA (( SDMax (1,m,k)),1)) + ( DigA (( DecSD (1,1,k)),1))),k)) + ( SD_Add_Carry (( DigA (( SDMax (1,m,k)), 0 )) + 0 ))) by RADIX_1:def 3

          .= (( SD_Add_Data ((( DigA (( SDMax (1,m,k)),1)) + ( DigA (( DecSD (1,1,k)),1))),k)) + ( SD_Add_Carry ( 0 + 0 ))) by RADIX_1:def 3

          .= (( SD_Add_Data ((( DigA (( SDMax (1,m,k)),1)) + ( DigA (( DecSD (1,1,k)),1))),k)) + 0 ) by RADIX_1:def 10

          .= ( SD_Add_Data ((( DigA (( SDMax (1,m,k)),1)) + 1),k)) by A5, A1, Th7;

          

          then

           A12: ( SDDec (( SDMax (1,m,k)) '+' ( DecSD (1,1,k)))) = (1 - (( SD_Add_Carry 1) * ( Radix k))) by A11, RADIX_1:def 11

          .= (1 - ( 0 * ( Radix k))) by RADIX_1:def 10

          .= 1;

          (( SDDec ( SDMax (1,m,k))) + ( SDDec ( DecSD (1,1,k)))) = (( SDDec (( SDMax (1,m,k)) '+' ( DecSD (1,1,k)))) + (( SD_Add_Carry (( DigA (( SDMax (1,m,k)),1)) + ( DigA (( DecSD (1,1,k)),1)))) * (( Radix k) |^ 1))) by A5, RADIX_2: 11

          .= (1 + (( SD_Add_Carry ( 0 + 1)) * (( Radix k) |^ 1))) by A5, A1, A11, A12, Th7

          .= (1 + ( 0 * (( Radix k) |^ 1))) by RADIX_1:def 10;

          hence thesis by A8, A10;

        end;

          suppose

           A13: n > 1;

          

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

          

          then

           A15: ( DigA (( SDMax (n,m,k)),n)) = ( SDMaxDigit (m,k,n)) by Def4

          .= 0 by A5, A6, Def3;

          

           A16: for i be Nat st i in ( Seg n) holds ( DigA (( Fmin (n,m,k)),i)) = ( DigA ((( SDMax (n,m,k)) '+' ( DecSD (1,n,k))),i))

          proof

            let i be Nat;

            assume

             A17: i in ( Seg n);

            

            then

             A18: ( DigA ((( SDMax (n,m,k)) '+' ( DecSD (1,n,k))),i)) = ( Add (( SDMax (n,m,k)),( DecSD (1,n,k)),i,k)) by RADIX_1:def 14

            .= (( SD_Add_Data ((( DigA (( SDMax (n,m,k)),i)) + ( DigA (( DecSD (1,n,k)),i))),k)) + ( SD_Add_Carry (( DigA (( SDMax (n,m,k)),(i -' 1))) + ( DigA (( DecSD (1,n,k)),(i -' 1)))))) by A5, A17, RADIX_1:def 13;

            

             A19: ( DigA (( SDMax (n,m,k)),i)) = ( SDMaxDigit (m,k,i)) by A17, Def4;

            

             A20: ( DigA (( Fmin (n,m,k)),i)) = ( FminDigit (m,k,i)) by A17, Def6;

            

             A21: i >= 1 by A17, FINSEQ_1: 1;

            now

              per cases ;

                suppose

                 A22: i >= (m + 1);

                then

                 A23: i > m by NAT_1: 13;

                then

                 A24: ( DigA (( SDMax (n,m,k)),i)) = 0 by A5, A19, Def3;

                

                 A25: i > 1 by A7, A23, XXREAL_0: 2;

                then

                 A26: (i -' 1) in ( Seg n) & ( DigA (( DecSD (1,n,k)),i)) = 0 by A5, A17, Th2, Th8;

                now

                  per cases by A22, XXREAL_0: 1;

                    suppose i = (m + 1);

                    

                    then ( DigA (( SDMax (n,m,k)),(i -' 1))) = ( DigA (( SDMax (n,m,k)),m)) by NAT_D: 34

                    .= ( SDMaxDigit (m,k,m)) by A4, Def4

                    .= 0 by A5, Def3;

                    

                    then ( DigA ((( SDMax (n,m,k)) '+' ( DecSD (1,n,k))),i)) = (( SD_Add_Data (( 0 + 0 ),k)) + 0 ) by A5, A18, A24, A26, Lm2

                    .= 0 by RADIX_1: 19;

                    hence thesis by A5, A20, A23, Def5;

                  end;

                    suppose i > (m + 1);

                    then (i - 1) > ((m + 1) - 1) by XREAL_1: 14;

                    then

                     A27: (i -' 1) > m by XREAL_0:def 2;

                    (i -' 1) in ( Seg n) by A17, A25, Th2;

                    

                    then ( DigA (( SDMax (n,m,k)),(i -' 1))) = ( SDMaxDigit (m,k,(i -' 1))) by Def4

                    .= 0 by A5, A27, Def3;

                    

                    then ( DigA ((( SDMax (n,m,k)) '+' ( DecSD (1,n,k))),i)) = (( SD_Add_Data (( 0 + 0 ),k)) + 0 ) by A5, A18, A24, A26, Lm2

                    .= 0 by RADIX_1: 19;

                    hence thesis by A5, A20, A23, Def5;

                  end;

                end;

                hence thesis;

              end;

                suppose i < (m + 1);

                then

                 A28: i <= m by NAT_1: 13;

                

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

                now

                  per cases by A29, XXREAL_0: 1;

                    suppose

                     A30: i > 1;

                    then

                     A31: m > 1 by A28, XXREAL_0: 2;

                    then

                     A32: (m -' 1) < m by JORDAN5B: 1;

                    

                     A33: (m -' 1) in ( Seg n) by A4, A31, Th2;

                    then

                     A34: (m -' 1) >= 1 by FINSEQ_1: 1;

                    now

                      per cases by A28, XXREAL_0: 1;

                        suppose

                         A35: i = m;

                        then

                         A36: ( DigA (( SDMax (n,m,k)),i)) = 0 & ( DigA (( DecSD (1,n,k)),i)) = 0 by A4, A5, A19, A30, Def3, Th8;

                        

                         A37: ( DigA (( Fmin (n,m,k)),i)) = ( FminDigit (m,k,m)) by A4, A35, Def6

                        .= 1 by A5, Def5;

                        

                         A38: ( DigA (( SDMax (n,m,k)),(i -' 1))) = ( SDMaxDigit (m,k,(m -' 1))) by A33, A35, Def4

                        .= (( Radix k) - 1) by A5, A34, A32, Def3;

                        

                         A39: i >= (1 + 1) by A30, INT_1: 7;

                        now

                          per cases by A39, XXREAL_0: 1;

                            suppose i = 2;

                            then (i -' 1) = (2 - 1) by XREAL_1: 233;

                            

                            then ( DigA ((( SDMax (n,m,k)) '+' ( DecSD (1,n,k))),i)) = (( SD_Add_Data (( 0 + 0 ),k)) + ( SD_Add_Carry ((( Radix k) - 1) + 1))) by A5, A3, A18, A36, A38, Th7

                            .= ( 0 + ( SD_Add_Carry ((( Radix k) - 1) + 1))) by RADIX_1: 19

                            .= 1 by A5, Th10;

                            hence thesis by A37;

                          end;

                            suppose

                             A40: i > 2;

                            then (i - 1) > (2 - 1) by XREAL_1: 14;

                            then

                             A41: (i -' 1) > 1 by XREAL_0:def 2;

                            i > 1 by A40, XXREAL_0: 2;

                            then (i -' 1) in ( Seg n) by A17, Th2;

                            

                            then ( DigA ((( SDMax (n,m,k)) '+' ( DecSD (1,n,k))),i)) = (( SD_Add_Data (( 0 + 0 ),k)) + ( SD_Add_Carry ((( Radix k) - 1) + 0 ))) by A5, A18, A36, A38, A41, Th8

                            .= ( 0 + ( SD_Add_Carry (( Radix k) - 1))) by RADIX_1: 19

                            .= 1 by A5, Lm1;

                            hence thesis by A37;

                          end;

                        end;

                        hence thesis;

                      end;

                        suppose

                         A42: i < m;

                        (i -' 1) < i by A30, JORDAN5B: 1;

                        then

                         A43: (i -' 1) < m by A42, XXREAL_0: 2;

                        

                         A44: ( DigA (( DecSD (1,n,k)),i)) = 0 by A5, A17, A30, Th8;

                        

                         A45: (i -' 1) in ( Seg n) by A17, A30, Th2;

                        

                         A46: i >= (1 + 1) by A30, INT_1: 7;

                        now

                          per cases by A46, XXREAL_0: 1;

                            suppose i = 2;

                            then

                             A47: (i -' 1) = (2 - 1) by XREAL_1: 233;

                            then

                             A48: ( DigA (( DecSD (1,n,k)),(i -' 1))) = 1 by A5, A3, Th7;

                            ( DigA (( SDMax (n,m,k)),(i -' 1))) = ( SDMaxDigit (m,k,(i -' 1))) by A45, Def4

                            .= (( Radix k) - 1) by A5, A43, A47, Def3;

                            

                            then ( DigA ((( SDMax (n,m,k)) '+' ( DecSD (1,n,k))),i)) = (( SD_Add_Data ((( Radix k) - 1),k)) + ( SD_Add_Carry ((( Radix k) + 1) - 1))) by A5, A18, A19, A21, A42, A44, A48, Def3

                            .= (( SD_Add_Data ((( Radix k) - 1),k)) + 1) by A5, Th10

                            .= (((( Radix k) - 1) - (( SD_Add_Carry (( Radix k) - 1)) * ( Radix k))) + 1) by RADIX_1:def 11

                            .= (((( Radix k) - 1) - (1 * ( Radix k))) + 1) by A5, Lm1

                            .= 0 ;

                            hence thesis by A5, A20, A42, Def5;

                          end;

                            suppose

                             A49: i > 2;

                            then (i - 1) > (2 - 1) by XREAL_1: 14;

                            then

                             A50: (i -' 1) > 1 by XREAL_0:def 2;

                            i > 1 by A49, XXREAL_0: 2;

                            then (i -' 1) in ( Seg n) by A17, Th2;

                            then

                             A51: ( DigA (( DecSD (1,n,k)),(i -' 1))) = 0 by A5, A50, Th8;

                            ( DigA (( SDMax (n,m,k)),(i -' 1))) = ( SDMaxDigit (m,k,(i -' 1))) by A45, Def4

                            .= (( Radix k) - 1) by A5, A43, A50, Def3;

                            

                            then ( DigA ((( SDMax (n,m,k)) '+' ( DecSD (1,n,k))),i)) = (( SD_Add_Data (((( Radix k) - 1) + 0 ),k)) + ( SD_Add_Carry ((( Radix k) - 1) + 0 ))) by A5, A18, A19, A21, A42, A44, A51, Def3

                            .= (( SD_Add_Data ((( Radix k) - 1),k)) + 1) by A5, Lm1

                            .= (((( Radix k) - 1) - (( SD_Add_Carry (( Radix k) - 1)) * ( Radix k))) + 1) by RADIX_1:def 11

                            .= (((( Radix k) - 1) - (1 * ( Radix k))) + 1) by A5, Lm1

                            .= 0 ;

                            hence thesis by A5, A20, A42, Def5;

                          end;

                        end;

                        hence thesis;

                      end;

                    end;

                    hence thesis;

                  end;

                    suppose

                     A52: i = 1;

                    then

                     A53: ( DigA (( SDMax (n,m,k)),(i -' 1))) = 0 & ( DigA (( DecSD (1,n,k)),(i -' 1))) = 0 by NAT_2: 8, RADIX_1:def 3;

                    now

                      per cases by A28, XXREAL_0: 1;

                        suppose

                         A54: i < m;

                        then ( DigA (( SDMax (n,m,k)),i)) = (( Radix k) - 1) by A5, A19, A52, Def3;

                        

                        then ( DigA ((( SDMax (n,m,k)) '+' ( DecSD (1,n,k))),i)) = (( SD_Add_Data (((( Radix k) - 1) + 1),k)) + ( SD_Add_Carry ( 0 + 0 ))) by A5, A3, A18, A52, A53, Th7

                        .= (( Radix k) - (( SD_Add_Carry ( Radix k)) * ( Radix k))) by RADIX_1: 18, RADIX_1:def 11

                        .= (( Radix k) - (1 * ( Radix k))) by A5, Th10

                        .= 0 ;

                        hence thesis by A5, A20, A54, Def5;

                      end;

                        suppose

                         A55: i = m;

                        then ( DigA (( SDMax (n,m,k)),i)) = 0 by A5, A19, Def3;

                        

                        then ( DigA ((( SDMax (n,m,k)) '+' ( DecSD (1,n,k))),i)) = (( SD_Add_Data ((1 + 0 ),k)) + ( SD_Add_Carry ( 0 + 0 ))) by A5, A3, A18, A52, A53, Th7

                        .= (1 - (( SD_Add_Carry 1) * ( Radix k))) by RADIX_1: 18, RADIX_1:def 11

                        .= (1 - ( 0 * ( Radix k))) by RADIX_1:def 10

                        .= 1;

                        hence thesis by A5, A20, A55, Def5;

                      end;

                    end;

                    hence thesis;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

          (( SDDec ( SDMax (n,m,k))) + ( SDDec ( DecSD (1,n,k)))) = (( SDDec (( SDMax (n,m,k)) '+' ( DecSD (1,n,k)))) + (( SD_Add_Carry (( DigA (( SDMax (n,m,k)),n)) + ( DigA (( DecSD (1,n,k)),n)))) * (( Radix k) |^ n))) by A2, A5, RADIX_2: 11

          .= (( SDDec (( SDMax (n,m,k)) '+' ( DecSD (1,n,k)))) + ( 0 * (( Radix k) |^ n))) by A5, A13, A14, A15, Th8, RADIX_1: 18;

          hence thesis by A2, A16, Th12;

        end;

      end;

      hence thesis;

    end;

    theorem :: RADIX_5:19

    for n,m,k be Nat st m in ( Seg n) & k >= 2 holds ( SDDec ( Fmin ((n + 1),(m + 1),k))) = (( SDDec ( Fmin ((n + 1),m,k))) + ( SDDec ( Fmax ((n + 1),m,k))))

    proof

      let n,m,k be Nat;

      assume that

       A1: m in ( Seg n) and

       A2: k >= 2;

      n >= m by A1, FINSEQ_1: 1;

      then

       A3: (n + 1) > m by NAT_1: 13;

      

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

      

      then

       A5: ( DigA (( Fmin ((n + 1),m,k)),(n + 1))) = ( FminDigit (m,k,(n + 1))) by Def6

      .= 0 by A2, A3, Def5;

      

       A6: m in ( Seg (n + 1)) by A1, FINSEQ_2: 8;

      

       A7: m >= 1 by A1, FINSEQ_1: 1;

      

       A8: for i be Nat st i in ( Seg (n + 1)) holds ( DigA (( Fmin ((n + 1),(m + 1),k)),i)) = ( DigA ((( Fmin ((n + 1),m,k)) '+' ( Fmax ((n + 1),m,k))),i))

      proof

        let i be Nat;

        

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

        assume

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

        

        then

         A11: ( DigA ((( Fmin ((n + 1),m,k)) '+' ( Fmax ((n + 1),m,k))),i)) = ( Add (( Fmin ((n + 1),m,k)),( Fmax ((n + 1),m,k)),i,k)) by RADIX_1:def 14

        .= (( SD_Add_Data ((( DigA (( Fmin ((n + 1),m,k)),i)) + ( DigA (( Fmax ((n + 1),m,k)),i))),k)) + ( SD_Add_Carry (( DigA (( Fmin ((n + 1),m,k)),(i -' 1))) + ( DigA (( Fmax ((n + 1),m,k)),(i -' 1)))))) by A2, A10, RADIX_1:def 13;

        

         A12: ( DigA (( Fmin ((n + 1),(m + 1),k)),i)) = ( FminDigit ((m + 1),k,i)) by A10, Def6;

        

         A13: ( DigA (( Fmin ((n + 1),m,k)),i)) = ( FminDigit (m,k,i)) by A10, Def6;

        

         A14: ( DigA (( Fmax ((n + 1),m,k)),i)) = ( FmaxDigit (m,k,i)) by A10, Def8;

        

         A15: i >= 1 by A10, FINSEQ_1: 1;

        now

          per cases ;

            suppose

             A16: i >= (m + 1);

            now

              per cases ;

                suppose

                 A17: i = (m + 1);

                

                then

                 A18: ( DigA (( Fmin ((n + 1),(m + 1),k)),i)) = ( FminDigit ((m + 1),k,(m + 1))) by A10, Def6

                .= 1 by A2, Def5;

                

                 A19: ( DigA (( Fmax ((n + 1),m,k)),(i -' 1))) = ( DigA (( Fmax ((n + 1),m,k)),m)) by A17, NAT_D: 34

                .= ( FmaxDigit (m,k,m)) by A6, Def8

                .= (( Radix k) - 1) by A2, Def7;

                

                 A20: ( DigA (( Fmax ((n + 1),m,k)),i)) = ( FmaxDigit (m,k,(m + 1))) by A10, A17, Def8

                .= 0 by A2, A9, Def7;

                

                 A21: ( DigA (( Fmin ((n + 1),m,k)),(i -' 1))) = ( DigA (( Fmin ((n + 1),m,k)),m)) by A17, NAT_D: 34

                .= ( FminDigit (m,k,m)) by A6, Def6

                .= 1 by A2, Def5;

                ( DigA (( Fmin ((n + 1),m,k)),i)) = ( FminDigit (m,k,(m + 1))) by A10, A17, Def6

                .= 0 by A2, A9, Def5;

                

                then ( DigA ((( Fmin ((n + 1),m,k)) '+' ( Fmax ((n + 1),m,k))),i)) = ( 0 + ( SD_Add_Carry (1 + (( Radix k) - 1)))) by A11, A20, A21, A19, RADIX_1: 19

                .= 1 by A2, Th10;

                hence thesis by A18;

              end;

                suppose

                 A22: i <> (m + 1);

                then i > (m + 1) by A16, XXREAL_0: 1;

                then (i - 1) > ((m + 1) - 1) by XREAL_1: 14;

                then

                 A23: (i -' 1) > m by XREAL_0:def 2;

                i > m by A16, NAT_1: 13;

                then i > 1 by A7, XXREAL_0: 2;

                then

                 A24: (i -' 1) in ( Seg (n + 1)) by A10, Th2;

                

                then

                 A25: ( DigA (( Fmin ((n + 1),m,k)),(i -' 1))) = ( FminDigit (m,k,(i -' 1))) by Def6

                .= 0 by A2, A23, Def5;

                

                 A26: ( DigA (( Fmin ((n + 1),(m + 1),k)),i)) = 0 by A2, A12, A22, Def5;

                

                 A27: ( DigA (( Fmax ((n + 1),m,k)),(i -' 1))) = ( FmaxDigit (m,k,(i -' 1))) by A24, Def8

                .= 0 by A2, A23, Def7;

                ( DigA (( Fmin ((n + 1),m,k)),i)) = 0 & ( DigA (( Fmax ((n + 1),m,k)),i)) = 0 by A2, A9, A13, A14, A16, Def5, Def7;

                hence thesis by A11, A25, A27, A26, RADIX_1: 18, RADIX_1: 19;

              end;

            end;

            hence thesis;

          end;

            suppose i < (m + 1);

            then

             A28: i <= m by NAT_1: 13;

            now

              per cases by A15, XXREAL_0: 1;

                suppose

                 A29: i > 1;

                then

                 A30: m > 1 by A28, XXREAL_0: 2;

                then

                 A31: (m -' 1) < m by JORDAN5B: 1;

                

                 A32: (m -' 1) in ( Seg (n + 1)) by A6, A30, Th2;

                now

                  per cases by A28, XXREAL_0: 1;

                    suppose

                     A33: i = m;

                    

                    then

                     A34: ( DigA (( Fmax ((n + 1),m,k)),(i -' 1))) = ( FmaxDigit (m,k,(m -' 1))) by A32, Def8

                    .= 0 by A2, A31, Def7;

                    

                     A35: ( DigA (( Fmax ((n + 1),m,k)),i)) = (( Radix k) - 1) by A2, A14, A33, Def7;

                    

                     A36: ( DigA (( Fmin ((n + 1),(m + 1),k)),i)) = ( FminDigit ((m + 1),k,m)) by A10, A33, Def6

                    .= 0 by A2, A9, Def5;

                    ( DigA (( Fmin ((n + 1),m,k)),(i -' 1))) = ( FminDigit (m,k,(m -' 1))) by A32, A33, Def6

                    .= 0 by A2, A31, Def5;

                    

                    then ( DigA ((( Fmin ((n + 1),m,k)) '+' ( Fmax ((n + 1),m,k))),i)) = (( SD_Add_Data ((1 + (( Radix k) - 1)),k)) + 0 ) by A2, A11, A13, A33, A35, A34, Def5, RADIX_1: 18

                    .= 0 by A2, Th11;

                    hence thesis by A36;

                  end;

                    suppose

                     A37: i < m;

                    

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

                    

                     A39: (i -' 1) < i by A15, JORDAN5B: 1;

                    then (i -' 1) < m by A37, XXREAL_0: 2;

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

                    then

                     A40: (i -' 1) in ( Seg (n + 1)) by A38, FINSEQ_1: 1;

                    

                    then

                     A41: ( DigA (( Fmax ((n + 1),m,k)),(i -' 1))) = ( FmaxDigit (m,k,(i -' 1))) by Def8

                    .= 0 by A2, A37, A39, Def7;

                    

                     A42: ( DigA (( Fmax ((n + 1),m,k)),i)) = 0 by A2, A14, A37, Def7;

                    

                     A43: i < (m + 1) by A37, NAT_1: 13;

                    ( DigA (( Fmin ((n + 1),m,k)),(i -' 1))) = ( FminDigit (m,k,(i -' 1))) by A40, Def6

                    .= 0 by A2, A37, A39, Def5;

                    

                    then ( DigA ((( Fmin ((n + 1),m,k)) '+' ( Fmax ((n + 1),m,k))),i)) = (( SD_Add_Data (( 0 + 0 ),k)) + ( SD_Add_Carry ( 0 + 0 ))) by A2, A11, A13, A37, A42, A41, Def5

                    .= ( 0 + 0 ) by RADIX_1: 18, RADIX_1: 19;

                    hence thesis by A2, A12, A43, Def5;

                  end;

                end;

                hence thesis;

              end;

                suppose

                 A44: i = 1;

                then

                 A45: ( DigA (( Fmax ((n + 1),m,k)),(i -' 1))) = 0 by NAT_2: 8, RADIX_1:def 3;

                now

                  per cases by A28, XXREAL_0: 1;

                    suppose

                     A46: i < m;

                    then ( DigA (( Fmin ((n + 1),m,k)),i)) = 0 & ( DigA (( Fmax ((n + 1),m,k)),i)) = 0 by A2, A13, A14, Def5, Def7;

                    

                    then

                     A47: ( DigA ((( Fmin ((n + 1),m,k)) '+' ( Fmax ((n + 1),m,k))),i)) = (( SD_Add_Data (( 0 + 0 ),k)) + ( SD_Add_Carry ( 0 + 0 ))) by A11, A44, A45, NAT_2: 8, RADIX_1:def 3

                    .= ( 0 + 0 ) by RADIX_1: 18, RADIX_1: 19;

                    i < (m + 1) by A46, NAT_1: 13;

                    hence thesis by A2, A12, A47, Def5;

                  end;

                    suppose

                     A48: i = m;

                    then ( DigA (( Fmin ((n + 1),m,k)),i)) = 1 & ( DigA (( Fmax ((n + 1),m,k)),i)) = (( Radix k) - 1) by A2, A13, A14, Def5, Def7;

                    

                    then

                     A49: ( DigA ((( Fmin ((n + 1),m,k)) '+' ( Fmax ((n + 1),m,k))),i)) = (( SD_Add_Data ((1 + (( Radix k) - 1)),k)) + 0 ) by A11, A44, A45, NAT_2: 8, RADIX_1: 18, RADIX_1:def 3

                    .= 0 by A2, Th11;

                    i < (m + 1) by A48, NAT_1: 13;

                    hence thesis by A2, A12, A49, Def5;

                  end;

                end;

                hence thesis;

              end;

            end;

            hence thesis;

          end;

        end;

        hence thesis;

      end;

      

       A50: ( DigA (( Fmax ((n + 1),m,k)),(n + 1))) = ( FmaxDigit (m,k,(n + 1))) by A4, Def8

      .= 0 by A2, A3, Def7;

      (( SDDec ( Fmin ((n + 1),m,k))) + ( SDDec ( Fmax ((n + 1),m,k)))) = (( SDDec (( Fmin ((n + 1),m,k)) '+' ( Fmax ((n + 1),m,k)))) + (( SD_Add_Carry (( DigA (( Fmin ((n + 1),m,k)),(n + 1))) + ( DigA (( Fmax ((n + 1),m,k)),(n + 1))))) * (( Radix k) |^ (n + 1)))) by A2, NAT_1: 11, RADIX_2: 11

      .= (( SDDec (( Fmin ((n + 1),m,k)) '+' ( Fmax ((n + 1),m,k)))) + ( 0 * (( Radix k) |^ (n + 1)))) by A5, A50, RADIX_1: 18;

      hence thesis by A8, Th12, NAT_1: 11;

    end;