The Mizar article:

High Speed Adder Algorithm with Radix-$2^k$ Sub Signed-Digit Number

by
Masaaki Niimura, and
Yasushi Fuwa

Received January 3, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: RADIX_4
[ MML identifier index ]


environ

 vocabulary INT_1, NAT_1, ARYTM_1, POWER, MIDSP_3, FINSEQ_1, FUNCT_1, RELAT_1,
      RLVECT_1, RADIX_1, FINSEQ_4, RADIX_3, RADIX_4, GROUP_1;
 notation TARSKI, SUBSET_1, XCMPLX_0, XREAL_0, INT_1, NAT_1, FUNCT_1, POWER,
      FINSEQ_1, FINSEQ_4, BINARITH, TREES_4, WSIERP_1, MIDSP_3, RADIX_1,
      RADIX_3;
 constructors REAL_1, POWER, BINARITH, FINSEQ_4, EULER_2, RADIX_3, MEMBERED;
 clusters INT_1, RELSET_1, NAT_1, MEMBERED;
 requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;
 theorems AXIOMS, REAL_1, REAL_2, RADIX_1, POWER, NAT_1, INT_1, BINARITH,
      FINSEQ_1, FINSEQ_2, FINSEQ_4, JORDAN3, GOBOARD9, NEWTON, RVSUM_1,
      PREPOWER, JORDAN12, EULER_2, RADIX_3, XCMPLX_0, XCMPLX_1;
 schemes FINSEQ_2, INT_2, BINOM;

begin :: Some Useful Theorems

reserve i,n,m,k,x,y for Nat,
        i1 for Integer;

theorem Th1:
  for k be Nat st 2 <= k holds 2 < Radix(k)
proof
  defpred P[Nat] means 2 < Radix($1);
        Radix(2) = 2 to_power (1+1) by RADIX_1:def 1
              .= 2 to_power 1 * 2 to_power 1 by POWER:32
              .= 2 * (2 to_power 1) by POWER:30
              .= 2 * 2 by POWER:30
              .= 4;
then A1:     P[2];
A2: for kk be Nat st
      kk >= 2 & P[kk] holds P[(kk + 1)]
      proof
        let kk be Nat;
        assume
A3:       2 <= kk & 2 < Radix(kk);
A4:     Radix(kk + 1) = 2 to_power (kk + 1) by RADIX_1:def 1
                 .= 2 to_power (1) * 2 to_power (kk) by POWER:32
                 .= 2 * 2 to_power (kk) by POWER:30
                 .= 2 * Radix(kk) by RADIX_1:def 1;
          Radix(kk) > 1 by A3,AXIOMS:22;
        hence thesis by A4,REAL_2:144;
        end;
        2 <= k implies P[k] from Ind2(A1,A2);
      hence thesis;
end;

Lm1:
  i1 in k-SD_Sub_S implies i1 >= -Radix(k-'1) & i1 <= Radix(k-'1) - 1
proof
  assume
A1:  i1 in k-SD_Sub_S;
      k-SD_Sub_S =
     {e where e is Element of INT:
       -Radix(k-'1) <= e & e <= Radix(k-'1) - 1 } by RADIX_3:def 1;
  then consider i be Element of INT such that
A2:  i = i1 and
A3:  -Radix(k-'1) <= i & i <= Radix(k-'1) - 1 by A1;
  thus thesis by A2,A3;
end;

Lm2:
  for i st i in Seg n holds
    DigA(DecSD(m,n+1,k),i)=DigA(DecSD(m,n,k),i)
proof
  let i;
  assume
A1:   i in Seg n;
then A2:   1 <= i & i <= n by FINSEQ_1:3;
    then i <= n+1 by NAT_1:37;
then A3:   i in Seg (n+1) by A2,FINSEQ_1:3;
      DigA(DecSD(m,n,k),i)
       = DigitDC(m,i,k) by A1,RADIX_1:def 9
      .= DigA(DecSD(m,n+1,k),i) by A3,RADIX_1:def 9;
  hence thesis;
end;

Lm3:
  for k,x,n be Nat st
    n >= 1 & x is_represented_by (n+1),k holds
      DigA(DecSD(x mod (Radix(k) |^ n),n,k),n) = DigA(DecSD(x,n,k),n)
proof
  let k,x,n be Nat;
  assume n >= 1 & x is_represented_by (n+1),k;
      then n <> 0;
then A1:   n in Seg n by FINSEQ_1:5;
      set xn = x mod (Radix(k) |^ n);
      set Rn = (Radix(k) |^ n);
        DigA(DecSD(xn,n,k),n)
        = DigitDC(xn,n,k) by A1,RADIX_1:def 9
       .= ((x mod Rn) mod Rn) div (Radix(k) |^ (n-'1)) by RADIX_1:def 8
       .= (x mod Rn) div (Radix(k) |^ (n-'1)) by EULER_2:7
       .= DigitDC(x,n,k) by RADIX_1:def 8
       .= DigA(DecSD(x,n,k),n) by A1,RADIX_1:def 9;
      hence thesis;
end;

begin :: Carry operation at n+1 digits Radix-2^k SD_Sub number

theorem Th2:
  for x,y be Integer, k be Nat st 3 <= k holds
    SDSub_Add_Carry( SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k), k ) = 0
proof
  let x,y be Integer, k be Nat;
  assume
A1:   k >= 3;
    then A2:   k - 1 >= 3 - 1 by REAL_1:92;
    then k - 1 > 0 by AXIOMS:22;
    then k - 1 = k -' 1 by BINARITH:def 3;
    then A3:   Radix(k-'1) > 2 by A2,Th1;
    then A4:   -Radix(k-'1) <= -2 by REAL_1:50;
    set CC = SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k);
A5:  k >= 2 by A1,AXIOMS:22;
then A6:   -1 <= SDSub_Add_Carry(x,k) & SDSub_Add_Carry(x,k) <= 1 by RADIX_3:13
;
A7:   -1 <= SDSub_Add_Carry(y,k) & SDSub_Add_Carry(y,k) <= 1 by A5,RADIX_3:13;
      then -1 + -1 <= CC by A6,REAL_1:55;
      then A8:     -Radix(k-'1) <= CC by A4,AXIOMS:22;
      CC <= 1 + 1 by A6,A7,REAL_1:55;
    then CC < Radix(k-'1) by A3,AXIOMS:22;
    hence SDSub_Add_Carry(CC,k) = 0 by A8,RADIX_3:def 3;
end;

theorem Th3:
  2 <= k implies
    DigA_SDSub(SD2SDSub(DecSD(m,n,k)),n+1)
         = SDSub_Add_Carry( DigA(DecSD(m,n,k),n), k)
proof
  assume
A1:   2 <= k;
        0 <= n by NAT_1:18;
      then 0 + 1 <= n + 1 by REAL_1:55;
then A2:   (n+1) in Seg (n+1) by FINSEQ_1:3;
      hence DigA_SDSub(SD2SDSub(DecSD(m,n,k)),n+1)
          = SD2SDSubDigitS(DecSD(m,n,k), n+1, k) by RADIX_3:def 8
         .= SD2SDSubDigit(DecSD(m,n,k), n+1, k) by A1,A2,RADIX_3:def 7
         .= SDSub_Add_Carry( DigA(DecSD(m,n,k),n+1-'1), k)
                                                 by RADIX_3:def 6
         .= SDSub_Add_Carry( DigA(DecSD(m,n,k),n), k) by BINARITH:39;
end;

theorem Th4:
  2 <= k & m is_represented_by 1,k implies
    DigA_SDSub(SD2SDSub(DecSD(m,1,k)),1+1) = SDSub_Add_Carry(m, k)
proof
  assume
A1: 2 <= k & m is_represented_by 1,k;
  hence DigA_SDSub(SD2SDSub(DecSD(m,1,k)),1+1)
      = SDSub_Add_Carry( DigA(DecSD(m,1,k),1), k) by Th3
     .= SDSub_Add_Carry(m, k) by A1,RADIX_1:24;
end;

theorem Th5:
  for k,x,n be Nat st
    n >= 1 & k >= 3 & x is_represented_by (n+1),k holds
      DigA_SDSub(SD2SDSub(DecSD(x mod (Radix(k) |^ n),n,k)),n+1)
        = SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k)
proof
  let k,x,n be Nat;
  assume
A1:   n >= 1 & k >= 3 & x is_represented_by (n+1),k;
A2:   n+1 in Seg (n+1) by FINSEQ_1:5;
A3:   k >= 2 by A1,AXIOMS:22;
      set xn = x mod (Radix(k) |^ n);
        DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1)
        = SD2SDSubDigitS(DecSD(xn,n,k),n+1,k) by A2,RADIX_3:def 8
        .= SD2SDSubDigit(DecSD(xn,n,k),n+1,k) by A2,A3,RADIX_3:def 7
        .= SDSub_Add_Carry(DigA(DecSD(xn,n,k),n+1-'1),k) by RADIX_3:def 6
        .= SDSub_Add_Carry(DigA(DecSD(xn,n,k),n+0),k) by BINARITH:39
        .= SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k) by A1,Lm3;
      hence thesis;
end;

theorem Th6:
  2 <= k & m is_represented_by 1,k implies
    DigA_SDSub(SD2SDSub(DecSD(m,1,k)),1) = m - SDSub_Add_Carry(m,k)*Radix(k)
proof
  assume
A1:   2 <= k & m is_represented_by 1,k;
A2:   1 in Seg (1+1) by FINSEQ_1:3;
then A3:   DigA_SDSub(SD2SDSub(DecSD(m,1,k)),1)
          = SD2SDSubDigitS(DecSD(m,1,k), 1, k) by RADIX_3:def 8
         .= SD2SDSubDigit(DecSD(m,1,k), 1, k) by A1,A2,RADIX_3:def 7;
    1 in Seg 1 by FINSEQ_1:5;
  hence
      DigA_SDSub(SD2SDSub(DecSD(m,1,k)),1)
         = SDSub_Add_Data( DigA(DecSD(m,1,k),1), k )
            + SDSub_Add_Carry( DigA(DecSD(m,1,k),1-'1), k)
              by A3,RADIX_3:def 6
        .= SDSub_Add_Data( DigA(DecSD(m,1,k),1), k )
            + SDSub_Add_Carry( DigA(DecSD(m,1,k),0), k) by GOBOARD9:1
        .= SDSub_Add_Data( DigA(DecSD(m,1,k),1), k )
            + SDSub_Add_Carry( 0, k) by RADIX_1:def 3
        .= SDSub_Add_Data( m, k ) + SDSub_Add_Carry( 0, k) by A1,RADIX_1:24
        .= SDSub_Add_Data( m, k ) + 0 by A1,RADIX_3:17
        .= m - SDSub_Add_Carry(m,k) * Radix(k) by RADIX_3:def 4;
end;

theorem Th7:
  for k,x,n be Nat st
    n >= 1 & k >= 2 & x is_represented_by (n+1),k holds
      (Radix(k) |^ n) * DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1)
      = (Radix(k) |^ n) * DigA(DecSD(x,n+1,k),n+1)
        - (Radix(k) |^ (n+1)) * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k)
        + (Radix(k) |^ n) * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k)
proof
  let k,x,n be Nat;
  assume
A1:   n >= 1 & k >= 2 & x is_represented_by (n+1),k;
A2:   n+1 in Seg (n+1) by FINSEQ_1:5;
then A3:   (n+1) in Seg (n+1+1) by FINSEQ_2:9;
    then (Radix(k) |^ n) * DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1)
       = (Radix(k) |^ n) *
           (SD2SDSubDigitS(DecSD(x,n+1,k),n+1,k)) by RADIX_3:def 8
      .= (Radix(k) |^ n) *
           (SD2SDSubDigit(DecSD(x,n+1,k),n+1,k)) by A1,A3,RADIX_3:def 7
      .= (Radix(k) |^ n) * (
          SDSub_Add_Data(DigA(DecSD(x,n+1,k),n+1),k)
        + SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1-'1),k))
                                                  by A2,RADIX_3:def 6
      .= (Radix(k) |^ n) * (
          SDSub_Add_Data(DigA(DecSD(x,n+1,k),n+1),k)
        + SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k) ) by BINARITH:39
      .= (Radix(k) |^ n) * (
          DigA(DecSD(x,n+1,k),n+1)
        - Radix(k) * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k)
        + SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k) ) by RADIX_3:def 4
      .= (Radix(k) |^ n) * (
         ( DigA(DecSD(x,n+1,k),n+1)
        - Radix(k) * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k) ))
        + (Radix(k) |^ n) * (
           SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k) ) by XCMPLX_1:8
      .= (Radix(k) |^ n) * DigA(DecSD(x,n+1,k),n+1)
        - (Radix(k) |^ n) * (Radix(k) *
              SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k))
        + (Radix(k) |^ n) * (
           SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k) ) by XCMPLX_1:40
      .= (Radix(k) |^ n) * DigA(DecSD(x,n+1,k),n+1)
        - ((Radix(k) |^ n) * Radix(k)) *
              SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k)
        + (Radix(k) |^ n) * (
           SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k) ) by XCMPLX_1:4
      .= (Radix(k) |^ n) * DigA(DecSD(x,n+1,k),n+1)
        - (Radix(k) |^ (n+1)) * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k)
        + (Radix(k) |^ n) * ( SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k) )
                                                            by RADIX_3:1;
      hence thesis;
end;

begin :: Definition for adder operation on Radix-2^k SD-Sub number

definition
  let i,n,k be Nat,
      x be Tuple of n,(k-SD_Sub), y be Tuple of n,(k-SD_Sub);
  assume A1:i in Seg n & k >= 2;
  func SDSubAddDigit(x,y,i,k) -> Element of k-SD_Sub equals
    :Def1:
    SDSub_Add_Data( DigA_SDSub(x,i) + DigA_SDSub(y,i), k )
      + SDSub_Add_Carry( DigA_SDSub(x,i -'1) + DigA_SDSub(y,i -'1), k);
coherence
  proof
    set SDAD = SDSub_Add_Data(DigA_SDSub(x,i) + DigA_SDSub(y,i), k );
    set SDAC = SDSub_Add_Carry(DigA_SDSub(x,i -'1)+DigA_SDSub(y,i -'1), k);
      DigA_SDSub(x,i) is Element of k-SD_Sub by A1,RADIX_3:19;
then A2:   DigA_SDSub(x,i) in k-SD_Sub;
    A3: k-SD_Sub c= k-SD by A1,RADIX_3:5;
      DigA_SDSub(y,i) is Element of k-SD_Sub by A1,RADIX_3:19;
    then SDAD in k-SD_Sub_S by A1,A2,A3,RADIX_3:20;
    then A4:   SDAD >= -Radix(k-'1) & SDAD <= Radix(k-'1) - 1 by Lm1;
A5:   -1 <= SDAC & SDAC <= 1 by A1,RADIX_3:13;
    then -Radix(k-'1) + -1 <= SDAD + SDAC by A4,REAL_1:55;
then A6:   SDAD + SDAC >= -Radix(k-'1) - 1 by XCMPLX_0:def 8;
      SDAD + SDAC <= Radix(k-'1) -1 + 1 by A4,A5,REAL_1:55;
    then SDAD + SDAC <= Radix(k-'1) + 1 - 1 by XCMPLX_1:29;
then A7:   SDAD + SDAC <= Radix(k-'1) by XCMPLX_1:26;
A8:   SDAD + SDAC is Element of INT by INT_1:def 2;
      k-SD_Sub = {w where w is Element of INT:
        w >= -Radix(k -' 1) - 1 & w <= Radix(k -' 1) } by RADIX_3:def 2;
    then SDAD + SDAC in k-SD_Sub by A6,A7,A8;
    hence thesis;
  end;
end;

definition let n,k be Nat,x,y be Tuple of n,(k-SD_Sub);
  func x '+' y -> Tuple of n,(k-SD_Sub) means
    :Def2:
    for i st i in Seg n holds DigA_SDSub(it,i) = SDSubAddDigit(x,y,i,k);
existence
  proof
    deffunc F(Nat)=SDSubAddDigit(x,y,$1,k);
    consider z being FinSequence of (k-SD_Sub) such that
A1:   len z = n and
A2:   for j be Nat st j in Seg n holds
        z.j = F(j) from SeqLambdaD;
    reconsider z as Tuple of n,(k-SD_Sub) by A1,FINSEQ_2:110;
    take z;
    let i;
    assume
A3:   i in Seg n;
    hence DigA_SDSub(z,i) = z.i by RADIX_3:def 5
                 .= SDSubAddDigit(x,y,i,k) by A2,A3;
  end;
uniqueness
  proof
    let k1,k2 be Tuple of n,(k-SD_Sub) such that
A4: for i be Nat st i in Seg n holds
           DigA_SDSub(k1,i) = SDSubAddDigit(x,y,i,k) and
A5: for i be Nat st i in Seg n holds
           DigA_SDSub(k2,i) = SDSubAddDigit(x,y,i,k);
    A6:len k1 = n & len k2 = n by FINSEQ_2:109;
      now let j be Nat;
      assume
A7:     j in Seg n;
      then k1.j = DigA_SDSub(k1,j) by RADIX_3:def 5
          .= SDSubAddDigit(x,y,j,k) by A4,A7
          .= DigA_SDSub(k2,j) by A5,A7
          .= k2.j by A7,RADIX_3:def 5;
      hence k1.j = k2.j;
    end;
    hence k1 = k2 by A6,FINSEQ_2:10;
  end;
end;

theorem Th8:
  for i st i in Seg n holds
    2 <= k implies
      SDSubAddDigit(SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),i,k)=
        SDSubAddDigit(
           SD2SDSub(DecSD((x mod (Radix(k) |^ n)),n,k)),
           SD2SDSub(DecSD((y mod (Radix(k) |^ n)),n,k)),i,k)
proof
  let i;
  assume
A1:   i in Seg n;
then A2:   1 <= i & i <= n by FINSEQ_1:3;
then A3:   i <= n + 1 by NAT_1:37;
then A4:   i in Seg (n+1) by A2,FINSEQ_1:3;
          i <= (n+1)+1 by A3,NAT_1:37;
then A5:   i in Seg ((n+1)+1) by A2,FINSEQ_1:3;
  assume
A6:   2 <= k;
      set X = x mod (Radix(k) |^ n);
      set Y = y mod (Radix(k) |^ n);
A7: SDSubAddDigit(SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),i,k)
       = SDSub_Add_Data(
            DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i)
          + DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i), k)
        + SDSub_Add_Carry(
            DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i-'1)
          + DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1), k) by A5,A6,Def1;
        now per cases;
        suppose
A8:      i = 1;
then A9:      DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i-'1)
            = DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),0) by GOBOARD9:1
            .= 0 by RADIX_3:def 5;
A10:      DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1)
            = DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),0) by A8,GOBOARD9:1
            .= 0 by RADIX_3:def 5;
A11:      DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i)
            = DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i) by A1,A6,RADIX_3:21;
          A12: DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i)
            = DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i) by A1,A6,RADIX_3:21;
A13:      DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i-'1)
            = DigA_SDSub(SD2SDSub(DecSD(X,n,k)),0) by A8,GOBOARD9:1
            .= 0 by RADIX_3:def 5;
       DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i-'1)
            = DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),0) by A8,GOBOARD9:1
            .= 0 by RADIX_3:def 5;
          hence thesis by A4,A6,A7,A9,A10,A11,A12,A13,Def1;
        suppose
A14:      i <> 1;
            i >= 1 by A1,FINSEQ_1:3;
          then 1 < i by A14,REAL_1:def 5;
          then 0 < i-'1 by JORDAN12:1;
then A15:      0 + 1 <= i-'1 by INT_1:20;
            i <= n by A1,FINSEQ_1:3;
          then i -' 1 <= n by JORDAN3:7;
then A16:      i -' 1 in Seg n by A15,FINSEQ_1:3;
            SDSubAddDigit(SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),i,k
)
            = SDSub_Add_Data(
               DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i)
             + DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i), k)
            + SDSub_Add_Carry(
               DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i-'1)
             + DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1), k)
                                                  by A1,A6,A7,RADIX_3:21
           .= SDSub_Add_Data(
               DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i)
             + DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i), k)
            + SDSub_Add_Carry(
               DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),i-'1)
             + DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1), k)
                                                  by A1,A6,RADIX_3:21
           .= SDSub_Add_Data(
               DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i)
             + DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i), k)
            + SDSub_Add_Carry(
               DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i-'1)
             + DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),i-'1), k)
                                                  by A6,A16,RADIX_3:21
           .= SDSub_Add_Data(
               DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i)
             + DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i), k)
            + SDSub_Add_Carry(
               DigA_SDSub(SD2SDSub(DecSD(X,n,k)),i-'1)
             + DigA_SDSub(SD2SDSub(DecSD(Y,n,k)),i-'1), k)
                                                  by A6,A16,RADIX_3:21
           .= SDSubAddDigit(SD2SDSub(DecSD(X,n,k)),SD2SDSub(DecSD(Y,n,k)),i,k)
                                                  by A4,A6,Def1;
         hence thesis;
      end;
    hence thesis;
end;

theorem
    for n st n >= 1 holds
    for k,x,y st
      k >= 3 & x is_represented_by n,k & y is_represented_by n,k holds
        x + y =
          SDSub2IntOut( SD2SDSub(DecSD(x,n,k)) '+' SD2SDSub(DecSD(y,n,k)) )
proof
  defpred P[Nat] means
    for k,x,y be Nat st
      k >= 3 & x is_represented_by $1,k & y is_represented_by $1,k holds
        x + y =
          SDSub2IntOut( SD2SDSub(DecSD(x,$1,k)) '+' SD2SDSub(DecSD(y,$1,k)) );

A1: P[1]
  proof
    let k,x,y be Nat;
    assume
A2:   k >= 3 & x is_represented_by 1,k & y is_represented_by 1,k;
then A3: k >= 2 by AXIOMS:22;
      set X = SD2SDSub(DecSD(x,1,k));
      set Y = SD2SDSub(DecSD(y,1,k));
      reconsider
        CRY1 = SDSub_Add_Carry(DigA_SDSub(X,1)+DigA_SDSub(Y,1),k) as Integer;
A4:   1 in Seg (1+1) by FINSEQ_1:3;
then A5:   DigA_SDSub(X '+' Y, 1)
        = SDSubAddDigit(X,Y,1,k) by Def2
       .= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k )
         + SDSub_Add_Carry( DigA_SDSub(X,1-'1)+DigA_SDSub(Y,1 -'1), k)
                                                         by A3,A4,Def1
       .= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k )
         + SDSub_Add_Carry( DigA_SDSub(X,0)+DigA_SDSub(Y,1 -'1), k)
                                                         by GOBOARD9:1
       .= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k )
         + SDSub_Add_Carry( DigA_SDSub(X,0) + DigA_SDSub(Y,0), k)
                                                      by GOBOARD9:1
       .= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k )
         + SDSub_Add_Carry( 0 + DigA_SDSub(Y,0), k) by RADIX_3:def 5
       .= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k )
         + SDSub_Add_Carry(0 + 0, k) by RADIX_3:def 5
       .= SDSub_Add_Data( DigA_SDSub(X,1) + DigA_SDSub(Y,1), k ) + 0
                                                      by A3,RADIX_3:17
      .= DigA_SDSub(X,1) + DigA_SDSub(Y,1) - Radix(k) * CRY1 by RADIX_3:def 4;
        2 - 1 = 1;
then A6:   2 -' 1 = 1 by BINARITH:def 3;
A7:   2 in Seg (1+1) by FINSEQ_1:3;
then A8:   DigA_SDSub(X '+' Y, 2)
        = SDSubAddDigit(X,Y,2,k) by Def2
       .= SDSub_Add_Data( DigA_SDSub(X,2) + DigA_SDSub(Y,2), k )
         + SDSub_Add_Carry( DigA_SDSub(X,2-'1)+DigA_SDSub(Y,2 -'1), k)
                                                         by A3,A7,Def1
       .= SDSub_Add_Data( SDSub_Add_Carry(x,k) + DigA_SDSub(Y,2), k )
                                                + CRY1 by A2,A3,A6,Th4
       .= SDSub_Add_Data( SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k), k )
                                                      + CRY1 by A2,A3,Th4
       .= SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k)
          - Radix(k)
            * SDSub_Add_Carry( SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k), k )
          + CRY1 by RADIX_3:def 4
       .= SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k)
          -Radix(k) * 0 + CRY1 by A2,Th2
       .= SDSub_Add_Carry(x,k) + SDSub_Add_Carry(y,k) - 0 + CRY1;
A9:  (SDSub2INT(X '+' Y))/.1
         = SDSub2INTDigit((X '+' Y),1,k) by A4,RADIX_3:def 11
        .= (Radix(k) |^ (1-'1)) * DigB_SDSub((X '+' Y),1) by RADIX_3:def 10
        .= (Radix(k) |^ (0)) * DigB_SDSub((X '+' Y),1) by GOBOARD9:1
        .= 1 * DigB_SDSub((X '+' Y),1) by NEWTON:9
        .= DigA_SDSub((X '+' Y),1) by RADIX_3:def 9;
      reconsider DIG1 = DigA_SDSub((X '+' Y),1) as Element of INT
                                                            by INT_1:def 2;
A10:  (SDSub2INT(X '+' Y))/.2
         = SDSub2INTDigit((X '+' Y),2,k) by A7,RADIX_3:def 11
        .= (Radix(k) |^ (2-'1)) * DigB_SDSub((X '+' Y),2) by RADIX_3:def 10
        .= Radix(k) * DigB_SDSub((X '+' Y),2) by A6,NEWTON:10
        .= Radix(k) * DigA_SDSub((X '+' Y),2) by RADIX_3:def 9;
      reconsider DIG2 = Radix(k) * DigA_SDSub((X '+' Y),2) as Element of INT
                                                            by INT_1:def 2;
A11:  len (SDSub2INT(X '+' Y)) = 1 + 1 by FINSEQ_2:109;
      then 1 in dom SDSub2INT(X '+' Y) by A4,FINSEQ_1:def 3;
      then A12:    SDSub2INT(X '+' Y).1 = DIG1 by A9,FINSEQ_4:def 4;
        2 in dom SDSub2INT(X '+' Y) by A7,A11,FINSEQ_1:def 3;
      then SDSub2INT(X '+' Y).2 = DIG2 by A10,FINSEQ_4:def 4;
      then SDSub2INT(X '+' Y) = <* DIG1 , DIG2 *> by A11,A12,FINSEQ_1:61;
      then A13:    Sum SDSub2INT(X '+' Y)
          = DIG1 + DIG2 by RVSUM_1:107;
      reconsider RSDCX = Radix(k)*SDSub_Add_Carry(x,k),
                 RSDCY = Radix(k)*SDSub_Add_Carry(y,k) as Integer;
      reconsider RCRY1 = Radix(k)*
              (SDSub_Add_Carry(DigA_SDSub(X,1)+DigA_SDSub(Y,1),k)) as Integer;
A14:  DIG1 = x - RSDCX + DigA_SDSub(Y,1) - RCRY1 by A2,A3,A5,Th6
       .= x - RSDCX + (y - RSDCY) - RCRY1 by A2,A3,Th6
       .= x - RSDCX + (y - RSDCY)+ -RCRY1 by XCMPLX_0:def 8
       .= x - RSDCX + (y + -RSDCY) + -RCRY1 by XCMPLX_0:def 8
       .= x - RSDCX + y + -RSDCY + -RCRY1 by XCMPLX_1:1
       .= x - RSDCX + y - RSDCY + -RCRY1 by XCMPLX_0:def 8
       .= x - RSDCX + y - RSDCY - RCRY1 by XCMPLX_0:def 8
       .= x + y - RSDCX - RSDCY - RCRY1 by XCMPLX_1:29;
   DIG2 = RSDCX + RSDCY + RCRY1 by A8,XCMPLX_1:9;
      then DIG1 + DIG2
       = x + y - RSDCX - RSDCY - RCRY1 + (RSDCX + (RSDCY + RCRY1)) by A14,
XCMPLX_1:1
      .= x + y - RSDCX - RSDCY - RCRY1 + RSDCX + (RSDCY + RCRY1) by XCMPLX_1:1
      .= x + y - RSDCX - RSDCY - RCRY1 + RSDCX + RSDCY + RCRY1 by XCMPLX_1:1
      .= x + y - RSDCX - RSDCY + RSDCX - RCRY1 + RSDCY + RCRY1 by XCMPLX_1:29
      .= x + y - RSDCX - RSDCY + RSDCX + -RCRY1 + RSDCY + RCRY1 by XCMPLX_0:def
8
      .= x + y - RSDCX - RSDCY + RSDCX + (-RCRY1 + RSDCY)+RCRY1 by XCMPLX_1:1
      .= x + y - RSDCX - RSDCY + RSDCX + ((-RCRY1 + RSDCY)+RCRY1) by XCMPLX_1:1
      .= x + y - RSDCX - RSDCY + RSDCX + RSDCY by XCMPLX_1:139
      .= x + y - RSDCX + -RSDCY + RSDCX + RSDCY by XCMPLX_0:def 8
      .= x + y - RSDCX + (-RSDCY + RSDCX) + RSDCY by XCMPLX_1:1
      .= x + y - RSDCX + ((-RSDCY + RSDCX) + RSDCY) by XCMPLX_1:1
      .= x + y - RSDCX + RSDCX by XCMPLX_1:139
      .= x + y + -RSDCX + RSDCX by XCMPLX_0:def 8
      .= x + y + (-RSDCX + RSDCX) by XCMPLX_1:1
      .= x + y + 0 by XCMPLX_0:def 6;
    hence thesis by A13,RADIX_3:def 12;
  end;
A15:  for n be Nat st n >= 1 & P[n] holds P[n+1]
proof
  let n be Nat;
  assume
A16:  n >= 1 & P[n];
      then n <> 0;
then A17:  n in Seg n by FINSEQ_1:5;
A18:  n+1 in Seg (n+1) by FINSEQ_1:5;
  let k,x,y be Nat;
  assume
A19:  k >= 3 & x is_represented_by (n+1),k & y is_represented_by (n+1),k;
then A20:  k >= 2 by AXIOMS:22;
    set xn = x mod (Radix(k) |^ n);
    set yn = y mod (Radix(k) |^ n);
    set z = SD2SDSub(DecSD(x,n+1,k)) '+' SD2SDSub(DecSD(y,n+1,k));
    set zn = SD2SDSub(DecSD(xn,n,k)) '+' SD2SDSub(DecSD(yn,n,k));
      Radix(k) <> 0 by RADIX_1:9;
    then Radix(k) > 0 by NAT_1:19;
then A21:  (Radix(k) |^ n) > 0 by PREPOWER:13;
then A22:  x = (x div (Radix(k) |^ n))*(Radix(k) |^ n)
                          + (x mod (Radix(k) |^ n)) by NAT_1:47;
      xn < Radix(k) |^ n & yn < Radix(k) |^ n by A21,NAT_1:46;
      then xn is_represented_by n,k & yn is_represented_by n,k by RADIX_1:def
12;
    then A23:  xn + yn
        = SDSub2IntOut(zn) by A16,A19
       .= Sum SDSub2INT(zn) by RADIX_3:def 12;
A24:  (n+1) in Seg (n+1+1) by A18,FINSEQ_2:9;
A25:  (n+1+1) in Seg (n+1+1) by FINSEQ_1:5;
      deffunc G(Nat)=SDSub2INTDigit(z,$1,k);
      consider zp being FinSequence of INT such that
A26:  len zp = n+1 and
A27:  for i be Nat st i in Seg (n+1) holds zp.i = G(i) from SeqLambdaD;
      consider zpp being FinSequence of INT such that
A28:  len zpp = n and
A29:  for i be Nat st i in Seg n holds zpp.i = G(i) from SeqLambdaD;
      deffunc GF(Nat)= SDSub2INTDigit(zn,$1,k);
      consider znpp being FinSequence of INT such that
A30:  len znpp = n and
A31:  for i be Nat st i in Seg n holds znpp.i = GF(i) from SeqLambdaD;
A32:  SDSub2INT(z) = zp^<* SDSub2INTDigit(z,(n+1)+1,k) *>
        proof
A33:     len (zp^<*SDSub2INTDigit(z,n+1+1,k)*>)
            = n+1+1 by A26,FINSEQ_2:19;
A34:     len SDSub2INT(z) = n+1+1 by FINSEQ_2:109;
          for j be Nat st 1 <= j & j <= len SDSub2INT(z) holds
            SDSub2INT(z).j = (zp^<* SDSub2INTDigit(z,n+1+1,k) *>).j
            proof
              let j be Nat;
              assume 1 <= j & j <= len SDSub2INT(z);
then A35:           j in Seg (n+1+1) by A34,FINSEQ_1:3;
then A36:           j in dom SDSub2INT(z) by A34,FINSEQ_1:def 3;
                  now per cases by A35,FINSEQ_2:8;
                  suppose
A37:               j in Seg (n+1);
                    then j in dom zp by A26,FINSEQ_1:def 3;
                    then (zp^<*SDSub2INTDigit(z,n+1+1,k)*>).j
                       = zp.j by FINSEQ_1:def 7
                      .= SDSub2INTDigit(z,j,k) by A27,A37
                      .= (SDSub2INT(z))/.j by A35,RADIX_3:def 11
                      .= SDSub2INT(z).j by A36,FINSEQ_4:def 4;
                    hence thesis;
                  suppose
A38:                j = (n+1)+1;
A39:                j in dom SDSub2INT(z) by A34,A35,FINSEQ_1:def 3;
                      (zp^<*SDSub2INTDigit(z,n+1+1,k)*>).j
                        = SDSub2INTDigit(z,n+1+1,k) by A26,A38,FINSEQ_1:59
                       .= (SDSub2INT(z))/.(n+1+1) by A35,A38,RADIX_3:def 11
                       .= SDSub2INT(z).j by A38,A39,FINSEQ_4:def 4;
                    hence thesis;
                end;
              hence thesis;
            end;
          hence thesis by A33,A34,FINSEQ_1:18;
        end;
A40:  zp = zpp^<* SDSub2INTDigit(z,(n+1),k) *>
        proof
A41:     len (zpp^<*SDSub2INTDigit(z,n+1,k)*>) = n+1 by A28,FINSEQ_2:19;
          for j be Nat st 1 <= j & j <= len zp holds
            zp.j = (zpp^<* SDSub2INTDigit(z,n+1,k) *>).j
            proof
              let j be Nat;
                assume 1 <= j & j <= len zp;
then A42:           j in Seg (n+1) by A26,FINSEQ_1:3;
                  now per cases by A42,FINSEQ_2:8;
                  suppose
A43:               j in Seg n;
                    then j in dom zpp by A28,FINSEQ_1:def 3;
                    then (zpp^<*SDSub2INTDigit(z,n+1,k)*>).j
                       = zpp.j by FINSEQ_1:def 7
                      .= SDSub2INTDigit(z,j,k) by A29,A43
                      .= zp.j by A27,A42;
                    hence thesis;
                  suppose
A44:                j = n+1;
                    then (zpp^<*SDSub2INTDigit(z,n+1,k)*>).j
                        = SDSub2INTDigit(z,n+1,k) by A28,FINSEQ_1:59
                       .= zp.j by A27,A42,A44;
                    hence thesis;
                end;
              hence thesis;
            end;
          hence thesis by A26,A41,FINSEQ_1:18;
        end;
A45:  SDSub2INT(zn) = znpp^<* SDSub2INTDigit(zn,n+1,k) *>
        proof
A46:     len (znpp^<*SDSub2INTDigit(zn,n+1,k)*>)
            = n+1 by A30,FINSEQ_2:19;
A47:     len SDSub2INT(zn) = n+1 by FINSEQ_2:109;
          for j be Nat st 1 <= j & j <= len SDSub2INT(zn) holds
            SDSub2INT(zn).j = (znpp^<* SDSub2INTDigit(zn,n+1,k) *>).j
            proof
              let j be Nat;
              assume 1 <= j & j <= len SDSub2INT(zn);
then A48:           j in Seg (n+1) by A47,FINSEQ_1:3;
then A49:           j in dom SDSub2INT(zn) by A47,FINSEQ_1:def 3;
                  now per cases by A48,FINSEQ_2:8;
                  suppose
A50:               j in Seg n;
                    then j in dom znpp by A30,FINSEQ_1:def 3;
                    then (znpp^<*SDSub2INTDigit(zn,n+1,k)*>).j
                       = znpp.j by FINSEQ_1:def 7
                      .= SDSub2INTDigit(zn,j,k) by A31,A50
                      .= (SDSub2INT(zn))/.j by A48,RADIX_3:def 11
                      .= SDSub2INT(zn).j by A49,FINSEQ_4:def 4;
                    hence thesis;
                  suppose
A51:                j = n+1;
A52:                j in dom SDSub2INT(zn) by A47,A48,FINSEQ_1:def 3;
                      (znpp^<*SDSub2INTDigit(zn,n+1,k)*>).j
                        = SDSub2INTDigit(zn,n+1,k) by A30,A51,FINSEQ_1:59
                       .= (SDSub2INT(zn))/.(n+1) by A48,A51,RADIX_3:def 11
                       .= SDSub2INT(zn).j by A51,A52,FINSEQ_4:def 4;
                    hence thesis;
                end;
              hence thesis;
            end;
          hence thesis by A46,A47,FINSEQ_1:18;
        end;
A53:  zpp = znpp
        proof
          for j be Nat st 1 <= j & j <= len znpp holds znpp.j = zpp.j
          proof
            let j be Nat;
            assume A54: 1 <= j & j <= len znpp;
then A55:       j in Seg n by A30,FINSEQ_1:3;
A56:       j <= n + 1 by A30,A54,NAT_1:37;
then A57:       j in Seg (n+1) by A54,FINSEQ_1:3;
              j <= (n+1)+1 by A56,NAT_1:37;
then A58:       j in Seg ((n+1)+1) by A54,FINSEQ_1:3;
              zpp.j
              = SDSub2INTDigit(z,j,k) by A29,A55
             .= (Radix(k) |^ (j -' 1))* DigB_SDSub(z,j) by RADIX_3:def 10
             .= (Radix(k) |^ (j -' 1))* DigA_SDSub(z,j) by RADIX_3:def 9
             .= (Radix(k) |^ (j -' 1))*
        SDSubAddDigit(SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),j,k)
                                      by A58,Def2
             .= (Radix(k) |^ (j -' 1))*
           SDSubAddDigit(SD2SDSub(DecSD(xn,n,k)),SD2SDSub(DecSD(yn,n,k)),j,k)
                                      by A20,A55,Th8
             .= (Radix(k) |^ (j -' 1)) * DigA_SDSub(zn,j) by A57,Def2
             .= (Radix(k) |^ (j -' 1)) * DigB_SDSub(zn,j) by RADIX_3:def 9
             .= SDSub2INTDigit(zn,j,k) by RADIX_3:def 10
             .= znpp.j by A31,A55;
            hence thesis;
          end;
          hence thesis by A28,A30,FINSEQ_1:18;
        end;

A59: Sum SDSub2INT(z)
        = Sum (zp) + SDSub2INTDigit(z,(n+1)+1,k) by A32,RVSUM_1:104
       .= Sum (znpp) + SDSub2INTDigit(z,(n+1),k)
            + SDSub2INTDigit(z,(n+1)+1,k) by A40,A53,RVSUM_1:104;
        (xn + yn) + 0 = Sum (znpp) + SDSub2INTDigit(zn,n+1,k) by A23,A45,
RVSUM_1:104;
      then A60: Sum (znpp) - 0 = (xn + yn) - SDSub2INTDigit(zn,n+1,k) by
XCMPLX_1:33;
       set SDN11 = DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1)
                    +DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1);
       set SDN1 = DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1)
                    +DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1);
       set SDN = DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n)
                    +DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n);
       set RN1 = (Radix(k) |^ (n+1));
       set RN = (Radix(k) |^ n);
A61: SDSub2INTDigit(z,n+1+1,k)
        = (Radix(k) |^ (n+1+1-'1)) * DigB_SDSub(z,n+1+1) by RADIX_3:def 10
       .= (Radix(k) |^ (n+1+1-'1)) * DigA_SDSub(z,n+1+1) by RADIX_3:def 9
       .= (Radix(k) |^ (n+1))* DigA_SDSub(z,n+1+1) by BINARITH:39
       .= RN1* SDSubAddDigit(
            SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),n+1+1,k)
                                                      by A25,Def2
       .= RN1* (SDSub_Add_Data(SDN11, k)
         + SDSub_Add_Carry(
              DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1-'1)
             +DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1-'1), k))
                                                       by A20,A25,Def1
       .= RN1* (SDSub_Add_Data(SDN11, k) + SDSub_Add_Carry(
              DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1)
             +DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1-'1), k))
                                                       by BINARITH:39
       .= RN1 * ( SDSub_Add_Data(SDN11,k) + SDSub_Add_Carry(SDN1,k) + 0 )
                                                       by BINARITH:39
       .= RN1 * ( SDSub_Add_Data(SDN11,k)) + RN1 * ( SDSub_Add_Carry(SDN1,k) )
                                                       by XCMPLX_1:8;
A62: SDSub2INTDigit(z,n+1,k)
        = (Radix(k) |^ (n+1-'1)) * DigB_SDSub(z,n+1) by RADIX_3:def 10
       .= (Radix(k) |^ (n+1-'1)) * DigA_SDSub(z,n+1) by RADIX_3:def 9
       .= RN* DigA_SDSub(z,n+1) by BINARITH:39
       .= RN* SDSubAddDigit(
            SD2SDSub(DecSD(x,n+1,k)),SD2SDSub(DecSD(y,n+1,k)),n+1,k)
                                                               by A24,Def2
       .= RN* (SDSub_Add_Data(SDN1, k)
         + SDSub_Add_Carry(
              DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1-'1)
             +DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1-'1), k)) by A20,A24,Def1
       .= RN* (SDSub_Add_Data(SDN1, k)
         + SDSub_Add_Carry(
              DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n)
             +DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1-'1), k)) by BINARITH:39
       .= RN*(SDSub_Add_Data(SDN1, k)+SDSub_Add_Carry(SDN,k)+0)
                                                              by BINARITH:39
       .= RN * (SDSub_Add_Data(SDN1, k)) + RN * (SDSub_Add_Carry(SDN,k))
                                                              by XCMPLX_1:8
       .= RN * (SDN1 - Radix(k) * SDSub_Add_Carry(SDN1, k))
         + RN * (SDSub_Add_Carry(SDN,k)) by RADIX_3:def 4
       .= RN * SDN1 - RN * (Radix(k) * SDSub_Add_Carry(SDN1, k))
         + RN * (SDSub_Add_Carry(SDN,k)) by XCMPLX_1:40
       .= RN * SDN1 - (RN * (Radix(k))) * SDSub_Add_Carry(SDN1, k)
         + RN * (SDSub_Add_Carry(SDN,k)) by XCMPLX_1:4
       .= RN * SDN1 - (Radix(k) |^ (n+1) * SDSub_Add_Carry(SDN1, k))
         + RN * (SDSub_Add_Carry(SDN,k)) by RADIX_3:1
       .= RN * SDN1 + - (Radix(k) |^ (n+1) * SDSub_Add_Carry(SDN1, k))
         + RN * (SDSub_Add_Carry(SDN,k)) by XCMPLX_0:def 8;
A63: SDSub2INTDigit(zn,n+1,k)
        = (Radix(k) |^ (n+1-'1)) * DigB_SDSub(zn,n+1) by RADIX_3:def 10
       .= (Radix(k) |^ (n+1-'1)) * DigA_SDSub(zn,n+1) by RADIX_3:def 9
       .= RN* DigA_SDSub(zn,n+1) by BINARITH:39
       .= RN* SDSubAddDigit(
            SD2SDSub(DecSD(xn,n,k)),SD2SDSub(DecSD(yn,n,k)),n+1,k) by A18,Def2
       .= RN * (SDSub_Add_Data(
              DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1)
             +DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1), k)
         + SDSub_Add_Carry(
              DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1-'1)
             +DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1-'1), k)) by A18,A20,Def1
       .= RN * (SDSub_Add_Data(
              DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1)
             +DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1), k)
         + SDSub_Add_Carry(
              DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n)
             +DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1-'1), k)) by BINARITH:39
       .= RN * (SDSub_Add_Data(
              DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n+1)
             +DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1), k)
         + SDSub_Add_Carry(
              DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n)
             +DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n), k)) by BINARITH:39
       .= RN * (SDSub_Add_Data(
              SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k)
             +DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n+1), k)
         + SDSub_Add_Carry(
              DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n)
             +DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n), k)) by A16,A19,Th5
       .= RN * (SDSub_Add_Data(
              SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k)
             +SDSub_Add_Carry(DigA(DecSD(y,n,k),n),k), k)
         + SDSub_Add_Carry(
              DigA_SDSub(SD2SDSub(DecSD(xn,n,k)),n)
             +DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n), k)) by A16,A19,Th5
       .= RN * (SDSub_Add_Data(
              SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k)
             +SDSub_Add_Carry(DigA(DecSD(y,n,k),n),k), k)
         + SDSub_Add_Carry(
              DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n)
             +DigA_SDSub(SD2SDSub(DecSD(yn,n,k)),n), k)) by A17,A20,RADIX_3:21
       .= RN * (SDSub_Add_Data(
              SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k)
             +SDSub_Add_Carry(DigA(DecSD(y,n,k),n),k), k)
         + SDSub_Add_Carry(SDN,k)) by A17,A20,RADIX_3:21
       .= RN * (SDSub_Add_Data(
              SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k)
             +SDSub_Add_Carry(DigA(DecSD(y,n,k),n),k), k))
         + RN * (SDSub_Add_Carry(SDN,k)) by XCMPLX_1:8;
      set SDACx = SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k);
      set SDACy = SDSub_Add_Carry(DigA(DecSD(y,n,k),n),k);
      set RNSDACxy = RN*(SDACx + SDACy);
      A64: SDSub_Add_Data(SDACx + SDACy, k)
        =(SDACx + SDACy) - Radix(k) * SDSub_Add_Carry(SDACx+SDACy,k)
                                           by RADIX_3:def 4
       .=(SDACx + SDACy) - Radix(k) * 0 by A19,Th2;
      set RN1SD11 = RN1 * (SDSub_Add_Data(SDN11,k));
      set RN1SC1 = RN1 * (SDSub_Add_Carry(SDN1,k));
      set RNSC = RN * (SDSub_Add_Carry(SDN,k));
A65: Sum SDSub2INT(z)
        = (xn + yn) - SDSub2INTDigit(zn,n+1,k) + ((RN*SDN1 + -RN1SC1) + RNSC)
           + RN1SD11 + RN1SC1 by A59,A60,A61,A62,XCMPLX_1:1
        .= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + (RN*SDN1 + -RN1SC1) + RNSC
           + RN1SD11 + RN1SC1 by XCMPLX_1:1
        .= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + RN*SDN1 + -RN1SC1 + RNSC
           + RN1SD11 + RN1SC1 by XCMPLX_1:1
        .= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + RN*SDN1 - RN1SC1 + RNSC
           + RN1SD11 + RN1SC1 by XCMPLX_0:def 8
        .= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + RN*SDN1 + RNSC - RN1SC1
           + RN1SD11 + RN1SC1 by XCMPLX_1:29
        .= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + RN*SDN1 + RNSC
           + RN1SD11 - RN1SC1 + RN1SC1 by XCMPLX_1:29
        .= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + RN*SDN1 + RNSC
           + RN1SD11 + RN1SC1 - RN1SC1 by XCMPLX_1:29
        .= (xn + yn) - SDSub2INTDigit(zn,n+1,k) + RN*SDN1 + RNSC
           + RN1SD11 by XCMPLX_1:26
        .= (xn + yn) + RN*SDN1 - SDSub2INTDigit(zn,n+1,k) + RNSC
           + RN1SD11 by XCMPLX_1:29
        .= (xn + yn) + RN*SDN1 + - SDSub2INTDigit(zn,n+1,k) + RNSC
          + RN1SD11 by XCMPLX_0:def 8
        .= (xn + yn) + RN*SDN1 + ( - SDSub2INTDigit(zn,n+1,k) + RNSC )
          + RN1SD11 by XCMPLX_1:1;
A66: - SDSub2INTDigit(zn,n+1,k) + RNSC
         = - RNSDACxy - RNSC + RNSC by A63,A64,XCMPLX_1:161
        .= - RNSDACxy + RNSC - RNSC by XCMPLX_1:29
        .= - RNSDACxy by XCMPLX_1:26;
A67: RN1SD11 = RN1 * ( DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1)
            +DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1)
           - Radix(k) * SDSub_Add_Carry(
            DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1)
            +DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1), k)) by RADIX_3:def 4;
A68: DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1)
        = SD2SDSubDigitS(DecSD(x,n+1,k),n+1+1,k) by A25,RADIX_3:def 8
       .= SD2SDSubDigit(DecSD(x,n+1,k),n+1+1,k) by A20,A25,RADIX_3:def 7
       .= SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1+1-'1),k)
                                                 by RADIX_3:def 6
       .= SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k) by BINARITH:39;
A69: DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1)
        = SD2SDSubDigitS(DecSD(y,n+1,k),n+1+1,k) by A25,RADIX_3:def 8
       .= SD2SDSubDigit(DecSD(y,n+1,k),n+1+1,k) by A20,A25,RADIX_3:def 7
       .= SDSub_Add_Carry(DigA(DecSD(y,n+1,k),n+1+1-'1),k)
                                                 by RADIX_3:def 6
       .= SDSub_Add_Carry(DigA(DecSD(y,n+1,k),n+1),k) by BINARITH:39;
then A70: RN1SD11 = RN1 * (DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1+1)
                    +DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1+1)
           - Radix(k) * 0) by A19,A67,A68,Th2
        .= RN1 * (SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k)
            + SDSub_Add_Carry(DigA(DecSD(y,n+1,k),n+1),k) ) by A68,A69;
      reconsider RNDx11 = RN * DigA_SDSub(SD2SDSub(DecSD(x,n+1,k)),n+1),
                 RNDy11 = RN * DigA_SDSub(SD2SDSub(DecSD(y,n+1,k)),n+1),
                 RN1Cx11 = RN1*SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n+1),k),
                 RN1Cy11 = RN1*SDSub_Add_Carry(DigA(DecSD(y,n+1,k),n+1),k),
                 RNCx1 = RN * SDSub_Add_Carry(DigA(DecSD(x,n+1,k),n),k),
                 RNCy1 = RN * SDSub_Add_Carry(DigA(DecSD(y,n+1,k),n),k),
                 RNCx = RN*SDSub_Add_Carry(DigA(DecSD(x,n,k),n),k),
                 RNCy = RN*SDSub_Add_Carry(DigA(DecSD(y,n,k),n),k)
                                                            as Integer;
A71: Sum SDSub2INT(z)
        = (xn + yn) + (RNDx11 + RNDy11)
         + (- RNSDACxy) + RN1SD11 by A65,A66,XCMPLX_1:8
       .= (xn + yn) + (RNDx11 + RNDy11)
         + - (RNCx + RNCy) + RN1SD11 by XCMPLX_1:8
       .= (xn + yn) + (RNDx11 + RNDy11)
         + - (RNCx + RNCy) + (RN1Cx11 + RN1Cy11) by A70,XCMPLX_1:8
       .= (xn + yn) + RNDx11 + RNDy11
         + - (RNCx + RNCy) + (RN1Cx11 + RN1Cy11) by XCMPLX_1:1
       .= (xn + yn)
         + (RN * DigA(DecSD(x,n+1,k),n+1) - RN1Cx11 + RNCx1)
         + RNDy11
         + - (RNCx + RNCy) + (RN1Cx11 + RN1Cy11) by A16,A19,A20,Th7
       .= (xn + yn)
         + (RN * DigA(DecSD(x,n+1,k),n+1) - RN1Cx11 + RNCx1)
         + RNDy11
         - (RNCx + RNCy) + (RN1Cx11 + RN1Cy11) by XCMPLX_0:def 8
       .= (xn + yn)
         + (RN * DigA(DecSD(x,n+1,k),n+1) - RN1Cx11 + RNCx1) + RNDy11
         + (RN1Cx11 + RN1Cy11) - (RNCx + RNCy) by XCMPLX_1:29
       .= (xn + yn)
         + (RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 - RN1Cx11) + RNDy11
         + (RN1Cx11 + RN1Cy11) - (RNCx + RNCy) by XCMPLX_1:29
       .= (xn + yn)
         + ((RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1) + -RN1Cx11) + RNDy11
         + (RN1Cx11 + RN1Cy11) - (RNCx + RNCy) by XCMPLX_0:def 8
       .= (xn + yn)
         + (RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1) + -RN1Cx11 + RNDy11
         + (RN1Cx11 + RN1Cy11) - (RNCx + RNCy) by XCMPLX_1:1
       .= (xn + yn)
         + (RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1) + -RN1Cx11 + RNDy11
         + RN1Cx11 + RN1Cy11 - (RNCx + RNCy) by XCMPLX_1:1
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 + -RN1Cx11 + RNDy11
         + RN1Cx11 + RN1Cy11 - (RNCx + RNCy) by XCMPLX_1:1
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 + (-RN1Cx11 + RNDy11)
         + RN1Cx11 + RN1Cy11 - (RNCx + RNCy) by XCMPLX_1:1
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 + ((-RN1Cx11 + RNDy11)
         + RN1Cx11) + RN1Cy11 - (RNCx + RNCy) by XCMPLX_1:1
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 + (RNDy11)
         + RN1Cy11 - (RNCx + RNCy) by XCMPLX_1:139
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + (RN * DigA(DecSD(y,n+1,k),n+1) - RN1Cy11 + RNCy1)
         + RN1Cy11 - (RNCx + RNCy) by A16,A19,A20,Th7
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + (RN * DigA(DecSD(y,n+1,k),n+1) - RN1Cy11 + RNCy1)
         + RN1Cy11 + - (RNCx + RNCy) by XCMPLX_0:def 8
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + ((RN * DigA(DecSD(y,n+1,k),n+1) + -RN1Cy11) + RNCy1)
         + RN1Cy11 + - (RNCx + RNCy) by XCMPLX_0:def 8
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + (RN * DigA(DecSD(y,n+1,k),n+1) + -RN1Cy11) + RNCy1
         + RN1Cy11 + - (RNCx + RNCy) by XCMPLX_1:1
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + RN * DigA(DecSD(y,n+1,k),n+1) + - RN1Cy11 + RNCy1
         + RN1Cy11 + - (RNCx + RNCy) by XCMPLX_1:1
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + RN * DigA(DecSD(y,n+1,k),n+1) + (- RN1Cy11 + RNCy1)
         + RN1Cy11 + - (RNCx + RNCy) by XCMPLX_1:1
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + RN * DigA(DecSD(y,n+1,k),n+1) + ((- RN1Cy11 + RNCy1)
         + RN1Cy11) + - (RNCx + RNCy) by XCMPLX_1:1
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + RN * DigA(DecSD(y,n+1,k),n+1) + (RNCy1) + - (RNCx + RNCy)
                                      by XCMPLX_1:139
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + RN * DigA(DecSD(y,n+1,k),n+1) + (RNCy1) + - (RNCx1 + RNCy)
                                       by A17,Lm2
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + RN * DigA(DecSD(y,n+1,k),n+1) + (RNCy1) + - (RNCx1 + RNCy1)
                                       by A17,Lm2
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + RN * DigA(DecSD(y,n+1,k),n+1) + RNCy1 - (RNCx1 + RNCy1)
                                       by XCMPLX_0:def 8
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + RN * DigA(DecSD(y,n+1,k),n+1) + RNCy1 - RNCx1 - RNCy1
                                       by XCMPLX_1:36
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + RN * DigA(DecSD(y,n+1,k),n+1) + RNCy1 - RNCx1 + - RNCy1
                                       by XCMPLX_0:def 8
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + RN * DigA(DecSD(y,n+1,k),n+1) - RNCx1 + RNCy1 + - RNCy1
                                       by XCMPLX_1:29
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + RN * DigA(DecSD(y,n+1,k),n+1) - RNCx1 + (RNCy1 + - RNCy1)
                                       by XCMPLX_1:1
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1
         + RN * DigA(DecSD(y,n+1,k),n+1) - RNCx1 + 0 by XCMPLX_0:def 6
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 - RNCx1
         + RN * DigA(DecSD(y,n+1,k),n+1) by XCMPLX_1:29
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + RNCx1 + - RNCx1
         + RN * DigA(DecSD(y,n+1,k),n+1) by XCMPLX_0:def 8
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + (RNCx1 + - RNCx1)
         + RN * DigA(DecSD(y,n+1,k),n+1) by XCMPLX_1:1
       .= (xn + yn)
         + RN * DigA(DecSD(x,n+1,k),n+1) + (0)
         + RN * DigA(DecSD(y,n+1,k),n+1) by XCMPLX_0:def 6;
A72: RN * DigA(DecSD(x,n+1,k),n+1)
        = RN * (x div (Radix(k) |^ n)) by A19,RADIX_1:27;
        RN * DigA(DecSD(y,n+1,k),n+1)
        = RN * (y div (Radix(k) |^ n)) by A19,RADIX_1:27;
then A73: Sum SDSub2INT(z)
       = yn + x + RN * (y div (Radix(k) |^ n)) by A22,A71,A72,XCMPLX_1:1;
   y = (y div (Radix(k) |^ n))*(Radix(k) |^ n)
                          + (y mod (Radix(k) |^ n)) by A21,NAT_1:47;
     then Sum SDSub2INT(z) = x + y by A73,XCMPLX_1:1;
     hence thesis by RADIX_3:def 12;
  end;
    for n be Nat st n >= 1 holds P[n] from Ind1(A1,A15);
  hence thesis;
end;

Back to top