The Mizar article:

Magnitude Relation Properties of Radix-$2^k$ SD Number

by
Masaaki Niimura, and
Yasushi Fuwa

Received November 7, 2003

Copyright (c) 2003 Association of Mizar Users

MML identifier: RADIX_5
[ MML identifier index ]


environ

 vocabulary ARYTM_1, NAT_1, INT_1, RADIX_1, FINSEQ_1, POWER, MIDSP_3, FINSEQ_4,
      GROUP_1, RELAT_1, RLVECT_1, FUNCT_1, RADIX_5;
 notation TARSKI, SUBSET_1, XCMPLX_0, XREAL_0, NAT_1, BINARITH, RADIX_1, POWER,
      MIDSP_3, FINSEQ_4, FINSEQ_1, FUNCT_1, WSIERP_1;
 constructors RADIX_1, BINARITH, POWER, FINSEQ_4, EULER_2;
 clusters REAL_1, NUMBERS, XREAL_0, INT_1, RELSET_1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI;
 theorems RADIX_1, RADIX_4, AXIOMS, REAL_1, REAL_2, INT_1, NAT_1, XCMPLX_1,
      SCMFSA_7, FINSEQ_1, JORDAN3, POWER, GOBOARD9, FINSEQ_2, NEWTON, RADIX_2,
      NAT_2, PREPOWER, GR_CY_1, GROUP_4, BINARITH, PEPIN, JORDAN4, JORDAN5B,
      FUNCT_1, FINSEQ_4, RVSUM_1, XCMPLX_0;
 schemes BINOM, FINSEQ_2, INT_2;

begin :: Some Useful Theorems

theorem Lm1:
  for k be Nat st k >= 2 holds Radix(k) - 1 in k-SD
proof
  let k be Nat;
  assume
A1: k >= 2;
A2: k-SD = {w where w is Element of INT:w <= Radix(k)-1 & w >= -Radix(k)+1}
                                                           by RADIX_1:def 2;
    Radix(k) > 2 by A1,RADIX_4:1; then
    Radix(k) > 1 by AXIOMS:22; then
    Radix(k) + Radix(k) > 1 + 1 by REAL_1:67; then
    Radix(k) - 1 > 0 + 1 - Radix(k) by REAL_2:169; then
A4: Radix(k) - 1 > -Radix(k) + 1 + 0 by XCMPLX_1:155;
    Radix(k) - 1 is Element of INT by INT_1:def 2;
    hence thesis by A2,A4;
end;

Lm2:
  for k be Nat holds Radix(k) > 0 by RADIX_2:6;

theorem Th1:
  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
A1:   i > 1 & i in Seg n; then
    i - 1 > 1 - 1 by REAL_1:54; then
    i -' 1 > 0 by A1,SCMFSA_7:3; then
A2: i -' 1 >= 0 + 1 by NAT_1:38;
    i >= 1 & i <= n by A1,FINSEQ_1:3; then
    i -' 1 <= n by JORDAN3:7;
    hence thesis by A2,FINSEQ_1:3;
end;

reserve k for Nat;

theorem Th2:
  for k be Nat st 2 <= k holds 4 <= Radix(k)
proof
  defpred P[Nat] means 4 <= 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;
      then
A1:     P[2];
A2:  for kk be Nat st kk >= 2 & P[kk] holds P[kk + 1]
      proof
        let kk be Nat;
        assume
A6:       2 <= kk & 4 <= Radix(kk);
A7:     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) >= 0 by A6,AXIOMS:22; then
        Radix(kk + 1) >= Radix(kk) by A7,REAL_2:146;
        hence thesis by A6, AXIOMS:22;
      end;
      for i being Nat st 2 <= i holds P[i] from Ind2(A1,A2);
      hence thesis;
end;

theorem Th3:
  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;
A3: 1 in Seg 1 by FINSEQ_1:3; then
A4: (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 GOBOARD9:1
      .= 1 * DigA(tx,1) by NEWTON:9;
A5: len DigitSD(tx) = 1 by FINSEQ_2:109; then
    1 in dom DigitSD(tx) by A3,FINSEQ_1:def 3; then
A6: DigitSD(tx).1 = DigA(tx,1) by FINSEQ_4:def 4,A4;
    reconsider w = DigA(tx,1) as Element of INT by INT_1:def 2;
    SDDec(tx) = Sum DigitSD(tx) by RADIX_1:def 7
      .= Sum <*w*> by A5,A6,FINSEQ_1:57
      .= DigA(tx,1) by RVSUM_1:103;
    hence thesis;
end;

begin :: Properties of Primary Radix-$2^k$ SD Number

theorem Th4:
  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;
A2: Radix(k) > 0 by Lm2;
A3: i >= 1 by A1,FINSEQ_1:3;
    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,A3,RADIX_2:4
     .= 0 mod Radix(k) by NAT_2:4;
    hence thesis by GR_CY_1:6;
end;

theorem
  for n,k be Nat st n >= 1 holds
    SDDec(DecSD(0,n,k)) = 0
proof
  let n,k be Nat;
  assume
A1:   n >= 1;
    Radix(k) > 0 by Lm2; then
    Radix(k) >= 0 + 1 by INT_1:20; then
    Radix(k) |^ n >= 1 by PREPOWER:19; then
    Radix(k) |^ n > 0 by AXIOMS:22; then
    0 is_represented_by n,k by RADIX_1:def 12;
    hence thesis by A1,RADIX_1:25;
end;

theorem Th6:
  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
A1:   1 in Seg n & k >= 2; then
    Radix(k) > 2 by RADIX_4:1; then
A2: Radix(k) > 1 by AXIOMS:22; then
A3: Radix(k) > 0 by AXIOMS:22;
    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:10
     .= (1 div 1) mod Radix(k) by NEWTON:9
     .= 1 mod Radix(k) by NAT_2:6;
    hence thesis by A2,GROUP_4:102;
end;

theorem Th7:
  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
A1:   i in Seg n & i > 1 & k >= 2; then
    Radix(k) > 2 by RADIX_4:1; then
A2: Radix(k) > 1 by AXIOMS:22; then
A3: Radix(k) > 0 by AXIOMS:22;
A4: 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 A1,A3,RADIX_2:4;
    i-1 > 1 - 1 by A1,REAL_1:92; then
    i-'1 > 0 by BINARITH:def 3; then
   (Radix(k) |^ (i-'1)) > 1 by A2,PEPIN:26; then
    1 div (Radix(k) |^ (i-'1)) = 0 by JORDAN4:5;
   hence thesis by A4,GR_CY_1:6;
end;

theorem 
  for n,k be Nat st n >= 1 & k >= 2 holds
    SDDec(DecSD(1,n,k)) = 1
proof
  let n,k be Nat;
  assume
A1:   n >= 1 & k >= 2; then
A2:   Radix(k) > 2 by RADIX_4:1;
      Radix(k) > 0 by Lm2; then
      Radix(k) >= 0 + 1 by INT_1:20; then
      Radix(k) |^ n >= Radix(k) by A1,PREPOWER:20; then
      Radix(k) |^ n >= 2 by A2,AXIOMS:22; then
      Radix(k) |^ n > 1 by AXIOMS:22; then
      1 is_represented_by n,k by RADIX_1:def 12;
      hence thesis by A1,RADIX_1:25;
end;

theorem Th9:
  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 Th10:
  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 Th9;
    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 by XCMPLX_1:14;
end;

begin :: Primary Magnitude Relation of Radix-2^k SD Number

Lm5:
  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 Th2; then
      Radix(k) - 1 >= 4 - 1 by REAL_1:49; then
      Radix(k) - 1 > 2 by AXIOMS:22;
      hence thesis by RADIX_1:def 10;
end;

Lm6:
  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
A1: k >= 2 & i in Seg n; then
A2: i >= 1 by FINSEQ_1:3;
    now per cases by A2,REAL_1:def 5;
    suppose
      i = 1; then
      SD_Add_Carry(DigA(DecSD(1,n,k),i))
        = SD_Add_Carry(1) by A1,Th6;
      hence thesis by RADIX_1:def 10;
    suppose
      i > 1; then
      SD_Add_Carry(DigA(DecSD(1,n,k),i))
        = SD_Add_Carry(0) by A1,Th7;
      hence thesis by RADIX_1:def 10;
    end;
    hence thesis;
end;

theorem Th11:
  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: P[1]
    proof
      let k be Nat, tx,ty be Tuple of 1,k-SD;
      assume
A2:     for i be Nat st i in Seg 1 holds DigA(tx,i) = DigA(ty,i);
A3:   1 in Seg 1 by FINSEQ_1:3;
A4:   SDDec(tx) = DigA(tx,1) by Th3;
      SDDec(ty) = DigA(ty,1) by Th3;
      hence thesis by A2,A3,A4;
  end;
A10: for n be Nat st n >= 1 & P[n] holds P[n+1]
    proof
      let n be Nat;
      assume
A11:    n >= 1 & P[n];
      let k be Nat, tx,ty be Tuple of (n+1),k-SD;
      assume
A12:    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 being FinSequence of INT such that
A13:    len txn = n and
A14:    for i be Nat st i in Seg n holds txn.i = F(i) from SeqLambdaD;
      rng txn c= k-SD
        proof
          let z be set;
          assume z in rng txn; then
          consider xx be set such that
A16:        xx in dom txn and
A17:        z = txn.xx by FUNCT_1:def 5;
          reconsider xx as Nat by A16;
A18:      dom txn = Seg n by FINSEQ_1:def 3,A13; then
A19:      z = DigB(tx,xx) by A14,A16,A17
           .= DigA(tx,xx) by RADIX_1:def 4;
          xx in Seg (n+1) by A16,A18,FINSEQ_2:9; then
          DigA(tx,xx) is Element of k-SD by RADIX_1:19;
          hence thesis by A19;
        end;
      then reconsider txn as FinSequence of k-SD by FINSEQ_1:def 4;
A20:  for i be Nat st i in Seg n holds txn.i = tx.i
        proof
          let i be Nat;
          assume
A21:        i in Seg n; then
A22:        i in Seg (n+1) by FINSEQ_2:9;
            txn.i = DigB(tx,i) by A14,A21
                 .= DigA(tx,i) by RADIX_1:def 4;
          hence thesis by A22,RADIX_1:def 3;
        end;
        deffunc F(Nat) = DigB(ty,$1);
      consider tyn being FinSequence of INT such that
A23:    len tyn = n and
A24:    for i be Nat st i in Seg n holds tyn.i = F(i) from SeqLambdaD;
      rng tyn c= k-SD
        proof
          let z be set;
          assume z in rng tyn; then
          consider yy be set such that
A26:        yy in dom tyn and
A27:        z = tyn.yy by FUNCT_1:def 5;
          reconsider yy as Nat by A26;
A28:      dom tyn = Seg n by FINSEQ_1:def 3,A23; then
A29:      z = DigB(ty,yy) by A24,A26,A27
           .= DigA(ty,yy) by RADIX_1:def 4;
          yy in Seg (n+1) by A26,A28,FINSEQ_2:9; then
          DigA(ty,yy) is Element of k-SD by RADIX_1:19;
          hence thesis by A29;
        end;
      then reconsider tyn as FinSequence of k-SD by FINSEQ_1:def 4;
A30:  for i be Nat st i in Seg n holds tyn.i = ty.i
        proof
          let i be Nat;
          assume
A31:        i in Seg n; then
A32:        i in Seg (n+1) by FINSEQ_2:9;
            tyn.i = DigB(ty,i) by A24,A31
                 .= DigA(ty,i) by RADIX_1:def 4;
          hence thesis by A32,RADIX_1:def 3;
        end;
      reconsider txn as Tuple of n,k-SD by A13,FINSEQ_2:110;
      reconsider tyn as Tuple of n,k-SD by A23,FINSEQ_2:110;
A33:  SDDec(txn) + (Radix(k) |^ n)*DigA(tx,n+1) = SDDec(tx) by A20,RADIX_2:10;
A34:  SDDec(tyn) + (Radix(k) |^ n)*DigA(ty,n+1) = SDDec(ty) by A30,RADIX_2:10;
      for i be Nat st i in Seg n holds DigA(txn,i) = DigA(tyn,i)
        proof
          let i be Nat;
          assume
A35:        i in Seg n; then
A36:      DigA(txn,i) = txn.i by RADIX_1:def 3
            .= DigB(tx,i) by A14,A35
            .= DigA(tx,i) by RADIX_1:def 4;
A37:      DigA(tyn,i) = tyn.i by A35,RADIX_1:def 3
            .= DigB(ty,i) by A24,A35
            .= DigA(ty,i) by RADIX_1:def 4;
          i in Seg (n+1) by A35,FINSEQ_2:9;
          hence thesis by A12,A36,A37;
        end;
      then
A38:    SDDec(txn) = SDDec(tyn) by A11;
      (n+1) in Seg (n+1) by FINSEQ_1:6; then
      SDDec(tx) = SDDec(tyn) + (Radix(k) |^ n)*DigA(ty,n+1) by A12,A33,A38;
      hence thesis by A34;
    end;
  for n be Nat st n >= 1 holds P[n] from Ind1(A1,A10);
  hence thesis;
end;

theorem
  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: P[1]
    proof
      let k be Nat, tx,ty be Tuple of 1,k-SD;
      assume
A2:     for i be Nat st i in Seg 1 holds DigA(tx,i) >= DigA(ty,i);
A3:     1 in Seg 1 by FINSEQ_1:3;
A4:   SDDec(tx) = DigA(tx,1) by Th3;
      SDDec(ty) = DigA(ty,1) by Th3;
      hence thesis by A2,A3,A4;
  end;
A10: for n be Nat st n >= 1 & P[n] holds P[n+1]
    proof
      let n be Nat;
      assume
A11:    n >= 1 & P[n];
      let k be Nat, tx,ty be Tuple of (n+1),k-SD;
      assume
A12:    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 being FinSequence of INT such that
A13:    len txn = n and
A14:    for i be Nat st i in Seg n holds txn.i = F(i) from SeqLambdaD;
      rng txn c= k-SD
        proof
          let z be set;
          assume z in rng txn; then
          consider xx be set such that
A16:        xx in dom txn and
A17:        z = txn.xx by FUNCT_1:def 5;
          reconsider xx as Nat by A16;
A18:      dom txn = Seg n by FINSEQ_1:def 3,A13; then
A19:      z = DigB(tx,xx) by A14,A16,A17
           .= DigA(tx,xx) by RADIX_1:def 4;
          xx in Seg (n+1) by A16,A18,FINSEQ_2:9; then
          DigA(tx,xx) is Element of k-SD by RADIX_1:19;
          hence thesis by A19;
        end;
      then reconsider txn as FinSequence of k-SD by FINSEQ_1:def 4;
A20:  for i be Nat st i in Seg n holds txn.i = tx.i
        proof
          let i be Nat;
          assume
A21:        i in Seg n; then
A22:        i in Seg (n+1) by FINSEQ_2:9;
            txn.i = DigB(tx,i) by A14,A21
                 .= DigA(tx,i) by RADIX_1:def 4;
          hence thesis by A22,RADIX_1:def 3;
        end;
      deffunc F(Nat) = DigB(ty,$1);
      consider tyn being FinSequence of INT such that
A23:    len tyn = n and
A24:    for i be Nat st i in Seg n holds tyn.i = F(i) from SeqLambdaD;
      rng tyn c= k-SD
        proof
          let z be set;
          assume z in rng tyn; then
          consider yy be set such that
A26:        yy in dom tyn and
A27:        z = tyn.yy by FUNCT_1:def 5;
          reconsider yy as Nat by A26;
A28:      dom tyn = Seg n by FINSEQ_1:def 3,A23; then
A29:      z = DigB(ty,yy) by A24,A26,A27
           .= DigA(ty,yy) by RADIX_1:def 4;
          yy in Seg (n+1) by A26,A28,FINSEQ_2:9; then
          DigA(ty,yy) is Element of k-SD by RADIX_1:19;
          hence thesis by A29;
        end;
      then reconsider tyn as FinSequence of k-SD by FINSEQ_1:def 4;
A30:  for i be Nat st i in Seg n holds tyn.i = ty.i
        proof
          let i be Nat;
          assume
A31:        i in Seg n; then
A32:        i in Seg (n+1) by FINSEQ_2:9;
            tyn.i = DigB(ty,i) by A24,A31
                 .= DigA(ty,i) by RADIX_1:def 4;
          hence thesis by A32,RADIX_1:def 3;
        end;
      reconsider txn as Tuple of n,k-SD by A13,FINSEQ_2:110;
      reconsider tyn as Tuple of n,k-SD by A23,FINSEQ_2:110;
A33:  SDDec(txn) + (Radix(k) |^ n)*DigA(tx,n+1) = SDDec(tx) by A20,RADIX_2:10;
A34:  SDDec(tyn) + (Radix(k) |^ n)*DigA(ty,n+1) = SDDec(ty) by A30,RADIX_2:10;
      for i be Nat st i in Seg n holds DigA(txn,i) >= DigA(tyn,i)
        proof
          let i be Nat;
          assume
A35:        i in Seg n; then
A36:      DigA(txn,i) = txn.i by RADIX_1:def 3
            .= DigB(tx,i) by A14,A35
            .= DigA(tx,i) by RADIX_1:def 4;
A37:      DigA(tyn,i) = tyn.i by A35,RADIX_1:def 3
            .= DigB(ty,i) by A24,A35
            .= DigA(ty,i) by RADIX_1:def 4;
          i in Seg (n+1) by A35,FINSEQ_2:9;
          hence thesis by A12,A36,A37;
        end;
      then
A38:    SDDec(txn) >= SDDec(tyn) by A11;
      (n+1) in Seg (n+1) by FINSEQ_1:6; then
A39:  DigA(tx,n+1) >= DigA(ty,n+1) by A12;
      Radix(k) > 0 by Lm2; then
      (Radix(k) |^ n) > 0 by PREPOWER:13; then
      (Radix(k) |^ n)*DigA(tx,n+1) >= (Radix(k) |^ n)*DigA(ty,n+1)
                                                     by A39,AXIOMS:25;
      hence thesis by A33,A34,A38,REAL_1:55;
    end;
  for n be Nat st n >= 1 holds P[n] from Ind1(A1,A10);
  hence thesis;
end;

theorem Th13:
  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: P[1]
    proof
      let k be Nat;
      assume
A2:     k >= 2;
      let tx,ty,tz,tw be Tuple of 1,k-SD;
      assume
A3:     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));
A4:   1 in Seg 1 by FINSEQ_1:3;
A5:   SDDec(tz '+' tw) = DigA(tz '+' tw,1) by Th3
       .= Add(tz,tw,1,k) by A4,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 A2,A4,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 GOBOARD9:1
       .= SD_Add_Data(DigA(tz,1)+DigA(tw,1),k)
           + SD_Add_Carry(DigA(tz,0)+DigA(tw,0)) by GOBOARD9:1
       .= 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;
A6:   SDDec(tx '+' ty) = DigA(tx '+' ty,1) by Th3
       .= Add(tx,ty,1,k) by A4,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 A2,A4,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 GOBOARD9:1
       .= SD_Add_Data(DigA(tx,1)+DigA(ty,1),k)
           + SD_Add_Carry(DigA(tx,0)+DigA(ty,0)) by GOBOARD9:1
       .= 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;
A7:   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 A3,A4;
A8:   DigA(tx,1) = DigA(tz,1) & DigA(ty,1) = DigA(tw,1) implies
          SDDec(tz) + SDDec(tw) = SDDec(tx) + SDDec(ty)
      proof
        assume
A9:       DigA(tx,1) = DigA(tz,1) & DigA(ty,1) = DigA(tw,1);
        SDDec(tz) + SDDec(tw)
         = (SDDec(tx '+' ty))
             + (SD_Add_Carry(DigA(tx,1)+DigA(ty,1))*(Radix(k) |^ 1))
                                                  by A2,A5,A6,A9,RADIX_2:11;
        hence thesis by A2,RADIX_2:11;
      end;
     DigA(ty,1) = DigA(tz,1) & DigA(tx,1) = DigA(tw,1) implies
          SDDec(tz) + SDDec(tw) = SDDec(tx) + SDDec(ty)
      proof
        assume
          DigA(ty,1) = DigA(tz,1) & 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 A2,A5,A6,A7,RADIX_2:11;
        hence thesis by A2,RADIX_2:11;
      end;
      hence thesis by A7,A8;
  end;
A20: for n be Nat st n >= 1 & P[n] holds P[n+1]
    proof
      let n be Nat;
      assume
A21:    n >= 1 & P[n];
      let k be Nat;
      assume
A22:    k >= 2;
      let tx,ty,tz,tw be Tuple of (n+1),k-SD;
      assume
A23:   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 being FinSequence of INT such that
A24:   len txn = n and
A25:   for i be Nat st i in Seg n holds txn.i = F(i) from SeqLambdaD;
      rng txn c= k-SD
        proof
          let z be set;
          assume z in rng txn; then
          consider xx be set such that
A26:       xx in dom txn and
A27:       z = txn.xx by FUNCT_1:def 5;
          reconsider xx as Nat by A26;
A28:     dom txn = Seg n by FINSEQ_1:def 3,A24; then
A29:     z = DigB(tx,xx) by A25,A26,A27
           .= DigA(tx,xx) by RADIX_1:def 4;
          xx in Seg (n+1) by A26,A28,FINSEQ_2:9; then
          DigA(tx,xx) is Element of k-SD by RADIX_1:19;
          hence thesis by A29;
        end;
      then reconsider txn as FinSequence of k-SD by FINSEQ_1:def 4;
A30: for i be Nat st i in Seg n holds txn.i = tx.i
        proof
          let i be Nat;
          assume
A31:       i in Seg n; then
A32:       i in Seg (n+1) by FINSEQ_2:9;
            txn.i = DigB(tx,i) by A25,A31
                 .= DigA(tx,i) by RADIX_1:def 4;
          hence thesis by A32,RADIX_1:def 3;
        end;
      deffunc F(Nat) = DigB(ty,$1);
      consider tyn being FinSequence of INT such that
A33:   len tyn = n and
A34:   for i be Nat st i in Seg n holds tyn.i = F(i) from SeqLambdaD;
      rng tyn c= k-SD
        proof
          let z be set;
          assume z in rng tyn; then
          consider yy be set such that
A36:       yy in dom tyn and
A37:       z = tyn.yy by FUNCT_1:def 5;
          reconsider yy as Nat by A36;
A38:     dom tyn = Seg n by FINSEQ_1:def 3,A33; then
A39:     z = DigB(ty,yy) by A34,A36,A37
           .= DigA(ty,yy) by RADIX_1:def 4;
          yy in Seg (n+1) by A36,A38,FINSEQ_2:9; then
          DigA(ty,yy) is Element of k-SD by RADIX_1:19;
          hence thesis by A39;
        end;
      then reconsider tyn as FinSequence of k-SD by FINSEQ_1:def 4;
A40: for i be Nat st i in Seg n holds tyn.i = ty.i
        proof
          let i be Nat;
          assume
A41:       i in Seg n; then
A42:       i in Seg (n+1) by FINSEQ_2:9;
            tyn.i = DigB(ty,i) by A34,A41
                 .= DigA(ty,i) by RADIX_1:def 4;
          hence thesis by A42,RADIX_1:def 3;
        end;
      deffunc F(Nat) = DigB(tz,$1);
      consider tzn being FinSequence of INT such that
A43:   len tzn = n and
A44:   for i be Nat st i in Seg n holds tzn.i = F(i) from SeqLambdaD;
      rng tzn c= k-SD
        proof
          let z be set;
          assume z in rng tzn; then
          consider zz be set such that
A46:       zz in dom tzn and
A47:       z = tzn.zz by FUNCT_1:def 5;
          reconsider zz as Nat by A46;
A48:     dom tzn = Seg n by FINSEQ_1:def 3,A43; then
A49:     z = DigB(tz,zz) by A44,A46,A47
           .= DigA(tz,zz) by RADIX_1:def 4;
          zz in Seg (n+1) by A46,A48,FINSEQ_2:9; then
          DigA(tz,zz) is Element of k-SD by RADIX_1:19;
          hence thesis by A49;
        end;
      then reconsider tzn as FinSequence of k-SD by FINSEQ_1:def 4;
A50: for i be Nat st i in Seg n holds tzn.i = tz.i
        proof
          let i be Nat;
          assume
A51:       i in Seg n; then
A52:       i in Seg (n+1) by FINSEQ_2:9;
            tzn.i = DigB(tz,i) by A44,A51
                 .= DigA(tz,i) by RADIX_1:def 4;
          hence thesis by A52,RADIX_1:def 3;
        end;
      deffunc F(Nat) = DigB(tw,$1);
      consider twn being FinSequence of INT such that
A53:   len twn = n and
A54:   for i be Nat st i in Seg n holds twn.i = F(i) from SeqLambdaD;
      rng twn c= k-SD
        proof
          let w be set;
          assume w in rng twn; then
          consider ww be set such that
A56:       ww in dom twn and
A57:       w = twn.ww by FUNCT_1:def 5;
          reconsider ww as Nat by A56;
A58:     dom twn = Seg n by FINSEQ_1:def 3,A53; then
A59:     w = DigB(tw,ww) by A54,A56,A57
           .= DigA(tw,ww) by RADIX_1:def 4;
          ww in Seg (n+1) by A56,A58,FINSEQ_2:9; then
          DigA(tw,ww) is Element of k-SD by RADIX_1:19;
          hence thesis by A59;
        end;
      then reconsider twn as FinSequence of k-SD by FINSEQ_1:def 4;
A60:  for i be Nat st i in Seg n holds twn.i = tw.i
        proof
          let i be Nat;
          assume
A61:       i in Seg n; then
A62:       i in Seg (n+1) by FINSEQ_2:9;
            twn.i = DigB(tw,i) by A54,A61
                 .= DigA(tw,i) by RADIX_1:def 4;
          hence thesis by A62,RADIX_1:def 3;
        end;
      reconsider txn as Tuple of n,k-SD by A24,FINSEQ_2:110;
      reconsider tyn as Tuple of n,k-SD by A33,FINSEQ_2:110;
      reconsider tzn as Tuple of n,k-SD by A43,FINSEQ_2:110;
      reconsider twn as Tuple of n,k-SD by A53,FINSEQ_2:110;
A65:  SDDec(txn) + (Radix(k) |^ n)*DigA(tx,n+1) = SDDec(tx) by A30,RADIX_2:10;
A66:  SDDec(tyn) + (Radix(k) |^ n)*DigA(ty,n+1) = SDDec(ty) by A40,RADIX_2:10;
A67:  SDDec(tzn) + (Radix(k) |^ n)*DigA(tz,n+1) = SDDec(tz) by A50,RADIX_2:10;
A68:  SDDec(twn) + (Radix(k) |^ n)*DigA(tw,n+1) = SDDec(tw) by A60,RADIX_2:10;
     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
A70:      i in Seg n; then
A71:    1 <= i & i <= n by FINSEQ_1:3; then
        i <= n + 1 by NAT_1:37; then
A72:    i in Seg (n+1) by A71,FINSEQ_1:3; then
A73:    (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)) by A23;
A74:    DigA(tx,i) = tx.i by A72,RADIX_1:def 3
         .= txn.i by A70,A30
         .= DigA(txn,i) by A70,RADIX_1:def 3;
A75:    DigA(ty,i) = ty.i by A72,RADIX_1:def 3
         .= tyn.i by A70,A40
         .= DigA(tyn,i) by A70,RADIX_1:def 3;
A76:    DigA(tz,i) = tz.i by A72,RADIX_1:def 3
         .= tzn.i by A70,A50
         .= DigA(tzn,i) by A70,RADIX_1:def 3;
A77:    DigA(tw,i) = tw.i by A72,RADIX_1:def 3
         .= twn.i by A70,A60
         .= DigA(twn,i) by A70,RADIX_1:def 3;
        thus thesis by A73,A74,A75,A76,A77;
      end; then
A83:  SDDec(tzn) + SDDec(twn) = SDDec(txn) + SDDec(tyn) by A21,A22;
A84:  n+1 >= 1 by NAT_1:29;
A85:  SDDec(tz) + SDDec(tw)
        = SDDec(tzn) + (Radix(k) |^ n)*DigA(tz,n+1)
          + SDDec(twn) + (Radix(k) |^ n)*DigA(tw,n+1) by A67,A68,XCMPLX_1:1
       .= SDDec(tzn) + SDDec(twn) + (Radix(k) |^ n)*DigA(tz,n+1)
             + (Radix(k) |^ n)*DigA(tw,n+1) by XCMPLX_1:1
       .= SDDec(tzn) + SDDec(twn) + ((Radix(k) |^ n)*DigA(tz,n+1)
             + (Radix(k) |^ n)*DigA(tw,n+1)) by XCMPLX_1:1;
A86:  SDDec(tx) + SDDec(ty)
       = SDDec(txn) + (Radix(k) |^ n)*DigA(tx,n+1)
          + SDDec(tyn) + (Radix(k) |^ n)*DigA(ty,n+1) by A65,A66,XCMPLX_1:1
       .= SDDec(txn) + SDDec(tyn) + (Radix(k) |^ n)*DigA(tx,n+1)
             + (Radix(k) |^ n)*DigA(ty,n+1) by XCMPLX_1:1
       .= SDDec(tzn) + SDDec(twn) + ((Radix(k) |^ n)*DigA(tx,n+1)
             + (Radix(k) |^ n)*DigA(ty,n+1)) by A83,XCMPLX_1:1;
      n+1 > 0 by A84,AXIOMS:22; then
      n+1 in Seg (n+1) by FINSEQ_1:5; then
A87:  (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 A23;
      thus thesis by A87,A85,A86;
    end;
  for n be Nat st n >= 1 holds P[n] from Ind1(A1,A20);
  hence thesis;
end;

theorem
  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 Th4;
        hence thesis by A2,A3;
      end;
      hence thesis by A1,Th13;
end;

begin :: Definiton of Max/Min Radix-2^k SD Number in Some Digits

definition let i,m,k be Nat;
  assume
A1:  k >= 2;
  func SDMinDigit(m,k,i) -> Element of k-SD equals
    :Def1:
    -Radix(k)+1 if 1 <= i & i < m
    otherwise 0;
coherence
  proof
A3: k-SD = {w where w is Element of INT:w <= Radix(k)-1 & w >= -Radix(k)+1}
                                                           by RADIX_1:def 2;
    Radix(k) > 2 by A1,RADIX_4:1; then
    Radix(k) > 1 by AXIOMS:22; then
    Radix(k) + Radix(k) > 1 + 1 by REAL_1:67; then
    Radix(k) - 1 > 1 - Radix(k) by REAL_2:169; then
A4: Radix(k) - 1 > -Radix(k) + 1 by XCMPLX_0:def 8;
    -Radix(k) + 1 is Element of INT by INT_1:def 2; then
    -Radix(k) + 1 in k-SD by A3,A4;
    hence thesis by RADIX_1:16;
  end;
consistency;
end;

definition let n,m,k be Nat;
  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 being FinSequence of k-SD such that
A2:   len z = n and
A3:   for j be Nat st j in Seg n holds
        z.j = F(j) from SeqLambdaD;
    reconsider z as Tuple of n,(k-SD) by A2,FINSEQ_2:110;
    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 A3,A4;
  end;
uniqueness
  proof
      let k1,k2 be Tuple of n,k-SD such that
A10:  for i be Nat st i in Seg n holds DigA(k1,i) = SDMinDigit(m,k,i) and
A11:  for i be Nat st i in Seg n holds DigA(k2,i) = SDMinDigit(m,k,i);
A12:  len k1 = n & len k2 = n by FINSEQ_2:109;
      now let j be Nat;
        assume
A13:      j in Seg n; then
        k1.j = DigA(k1,j) by RADIX_1:def 3
            .= SDMinDigit(m,k,j) by A10,A13
            .= DigA(k2,j) by A11,A13
            .= k2.j by A13,RADIX_1:def 3;
        hence k1.j = k2.j;
        end;
      hence k1 = k2 by A12,FINSEQ_2:10;
  end;
end;

definition let i,m,k be Nat;
  assume
A1:  k >= 2;
  func SDMaxDigit(m,k,i) -> Element of k-SD equals
    :Def3:
    Radix(k)-1 if 1 <= i & i < m
    otherwise 0;
coherence by RADIX_1:16,A1,Lm1;
consistency;
end;

definition let n,m,k be Nat;
  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 being FinSequence of k-SD such that
A2:   len z = n and
A3:   for j be Nat st j in Seg n holds
        z.j = F(j) from SeqLambdaD;
    reconsider z as Tuple of n,(k-SD) by A2,FINSEQ_2:110;
    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 A3,A4;
  end;
uniqueness
  proof
      let k1,k2 be Tuple of n,k-SD such that
A10:  for i be Nat st i in Seg n holds DigA(k1,i) = SDMaxDigit(m,k,i) and
A11:  for i be Nat st i in Seg n holds DigA(k2,i) = SDMaxDigit(m,k,i);
A12:  len k1 = n & len k2 = n by FINSEQ_2:109;
      now let j be Nat;
        assume
A13:      j in Seg n; then
        k1.j = DigA(k1,j) by RADIX_1:def 3
            .= SDMaxDigit(m,k,j) by A10,A13
            .= DigA(k2,j) by A11,A13
            .= k2.j by A13,RADIX_1:def 3;
        hence k1.j = k2.j;
        end;
      hence k1 = k2 by A12,FINSEQ_2:10;
  end;
end;

definition let i,m,k be Nat;
  assume
A1:  k >= 2;
  func FminDigit(m,k,i) -> Element of k-SD equals
    :Def5:
    1 if i = m
    otherwise 0;
coherence
  proof
    1 in k-SD
    proof
A3:   k-SD = {w where w is Element of INT:w <= Radix(k)-1 & w >= -Radix(k)+1}
                                                      by RADIX_1:def 2;
A4:   Radix(k) > 2 by A1, RADIX_4:1; then
      Radix(k)+  -1 > 2 + -1 by REAL_1:53; then
A5:   Radix(k) - 1 >= 1 by XCMPLX_0:def 8;
      -Radix(k) < -2 by A4,REAL_1:50; then
      -Radix(k) + 1 < -2 + 1 by REAL_1:53; then
A6:   -Radix(k) + 1 <= 1 by AXIOMS:22;
      1 is Element of INT by INT_1:def 2;
      hence thesis by A3,A5,A6;
    end;
    hence thesis by RADIX_1:16;
  end;
consistency;
end;

definition let n,m,k be Nat;
  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 being FinSequence of k-SD such that
A2:   len z = n and
A3:   for j be Nat st j in Seg n holds
        z.j = F(j) from SeqLambdaD;
    reconsider z as Tuple of n,(k-SD) by A2,FINSEQ_2:110;
    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 A3,A4;
  end;
uniqueness
  proof
      let k1,k2 be Tuple of n,k-SD such that
A10:  for i be Nat st i in Seg n holds DigA(k1,i) = FminDigit(m,k,i) and
A11:  for i be Nat st i in Seg n holds DigA(k2,i) = FminDigit(m,k,i);
A12:  len k1 = n & len k2 = n by FINSEQ_2:109;
      now let j be Nat;
        assume
A13:      j in Seg n; then
        k1.j = DigA(k1,j) by RADIX_1:def 3
            .= FminDigit(m,k,j) by A10,A13
            .= DigA(k2,j) by A11,A13
            .= k2.j by A13,RADIX_1:def 3;
        hence k1.j = k2.j;
        end;
      hence k1 = k2 by A12,FINSEQ_2:10;
  end;
end;

definition let i,m,k be Nat;
  assume
A1:  k >= 2;
  func FmaxDigit(m,k,i) -> Element of k-SD equals
    :Def7:
    Radix(k) - 1 if i = m
    otherwise 0;
coherence by A1,Lm1,RADIX_1:16;
consistency;
end;

definition let n,m,k be Nat;
  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 being FinSequence of k-SD such that
A2:   len z = n and
A3:   for j be Nat st j in Seg n holds
        z.j = F(j) from SeqLambdaD;
    reconsider z as Tuple of n,(k-SD) by A2,FINSEQ_2:110;
    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 A3,A4;
  end;
uniqueness
  proof
      let k1,k2 be Tuple of n,k-SD such that
A10:  for i be Nat st i in Seg n holds DigA(k1,i) = FmaxDigit(m,k,i) and
A11:  for i be Nat st i in Seg n holds DigA(k2,i) = FmaxDigit(m,k,i);
A12:  len k1 = n & len k2 = n by FINSEQ_2:109;
      now let j be Nat;
        assume
A13:      j in Seg n; then
        k1.j = DigA(k1,j) by RADIX_1:def 3
            .= FmaxDigit(m,k,j) by A10,A13
            .= DigA(k2,j) by A11,A13
            .= k2.j by A13,RADIX_1:def 3;
        hence k1.j = k2.j;
        end;
      hence k1 = k2 by A12,FINSEQ_2:10;
  end;
end;

begin :: Properties of Max/Min Radix-$2^k$ SD Numbers

theorem Th15:
  for n,m,k be Nat st n >= 1 & k >= 2 & m in Seg n 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:     n >= 1 & k >= 2 & m in Seg n;
      let i be Nat;
      assume
A2:     i in Seg n; then
A3:   i >= 1 & i <= n by FINSEQ_1:3;
      reconsider a = SDMinDigit(m,k,i) as Element of INT;
      reconsider b = SDMaxDigit(m,k,i) as Element of INT;
      DigA(SDMin(n,m,k),i) = SDMinDigit(m,k,i) by A2,Def2; then
A9:   DigA(SDMax(n,m,k),i) + DigA(SDMin(n,m,k),i)
        = b + a by A2,Def4;
      now per cases;
      suppose
A10:    i < m; then
        a + b
          = -Radix(k) + 1 + b by A1,A3,Def1
         .= -Radix(k) + 1 + (Radix(k) - 1) by A1,A3,A10,Def3
         .= -Radix(k) + ( 1 + (Radix(k) - 1)) by XCMPLX_1:1
         .= -Radix(k) + ( Radix(k) ) by XCMPLX_1:27
         .= 0 by XCMPLX_0:def 6;
        hence thesis by A9;
      suppose
A11:    i >= m; then
        a + b
          = 0 + b by A1,Def1
         .= 0 + 0 by A1,A11,Def3;
        hence thesis by A9;
      end;
      hence thesis;
end;

theorem
  for n be Nat st n >= 1 holds
    for m,k be Nat st m in Seg n & 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;
      let m,k be Nat;
      assume
A2:     m in Seg n & k >= 2;
A4:   n in Seg n by A1,FINSEQ_1:3;
      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
A10:      i in Seg n; then
A11:    i >= 1 & i <= n by FINSEQ_1:3;
A12:    DigA(SDMax(n,m,k) '+' SDMin(n,m,k),i)
          = Add(SDMax(n,m,k),SDMin(n,m,k),i,k) by A10,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 A2,A10,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 A1,A2,A10,Th15
         .= 0+SD_Add_Carry(DigA(SDMax(n,m,k),i-'1)+DigA(SDMin(n,m,k),i-'1))
                                                    by RADIX_1:22;
A13:  DigA(DecSD(0,n,k),i) = 0 by A10,Th4;
        now per cases by A11,REAL_1:def 5;
        suppose
          i = 1; then
A15:      i -' 1 = 0 by NAT_2:10; then
          DigA(SDMin(n,m,k),i-'1) = 0 by RADIX_1:def 3; then
          DigA(SDMax(n,m,k) '+' SDMin(n,m,k),i)
            = SD_Add_Carry(0+0) by A12,A15,RADIX_1:def 3;
          hence thesis by RADIX_1:def 10,A13;
        suppose
          i > 1; then
          i -' 1 in Seg n by A10,Th1; then
          DigA(SDMax(n,m,k) '+' SDMin(n,m,k),i)
            = SD_Add_Carry(0) by A12,A1,A2,Th15;
          hence thesis by RADIX_1:def 10,A13;
        end;
        hence thesis;
      end; then
A90:  SDDec(DecSD(0,n,k)) = SDDec(SDMax(n,m,k) '+' SDMin(n,m,k)) by A1,Th11;
      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,A2,RADIX_2:11
       .= SDDec(SDMax(n,m,k) '+' SDMin(n,m,k))
            + SD_Add_Carry(0) * (Radix(k) |^ n) by A1,A2,A4,Th15
       .= SDDec(SDMax(n,m,k) '+' SDMin(n,m,k)) + 0 * (Radix(k) |^ n)
                                                by RADIX_1:def 10;
      hence thesis by A90;
end;

theorem
  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;
      assume
A1:     n >= 1;
      let m,k be Nat;
      assume
A2:     m in Seg n & k >= 2; then
A3:   n >= m & m >= 1 by FINSEQ_1:3;
A4:   1 in Seg 1 by FINSEQ_1:3;
A5:   1 in Seg n by A1,FINSEQ_1:3;
      now per cases by A1,REAL_1:def 5;
      suppose
A10:    n = 1;
A12:    SDDec(SDMax(1,m,k) '+' DecSD(1,1,k))
          = DigA(SDMax(1,m,k) '+' DecSD(1,1,k),1) by Th3
         .= Add(SDMax(1,m,k),DecSD(1,1,k),1,k) by A4,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 A2,A4,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 GOBOARD9:1
         .= 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 GOBOARD9:1
         .= 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 A2,A4,Th6;
A13:    m = 1 by A3,A10,AXIOMS:21;
A14:    DigA(SDMax(1,m,k),1) = SDMaxDigit(m,k,1) by A4,Def4
         .= 0 by A13,A2,Def3; then
A15:    SDDec(SDMax(1,m,k) '+' DecSD(1,1,k)) = SD_Add_Data(0+1,k) by A12
         .= 1 - SD_Add_Carry(1) * Radix(k) by RADIX_1:def 11
         .= 1 - 0 * Radix(k) by RADIX_1:def 10
         .= 1;
A16:    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 A2,RADIX_2:11
         .= 1 + SD_Add_Carry(DigA(SDMax(1,m,k),1)+DigA(DecSD(1,1,k),1))
                    *(Radix(k) |^ 1) by A15
         .= 1 + SD_Add_Carry(0+1) *(Radix(k) |^ 1) by A2,A4,Th6,A14 
         .= 1 + 0 * (Radix(k) |^ 1) by RADIX_1:def 10;
        SDDec(Fmin(1,m,k))
          = DigA(Fmin(1,m,k),1) by Th3
         .= FminDigit(m,k,1) by A4,Def6
         .= 1 by A2,A13,Def5;
        hence thesis by A10,A16;
      suppose
A30:    n > 1;
A31:    n in Seg n by A1,FINSEQ_1:3; then
A32:    DigA(SDMax(n,m,k),n) = SDMaxDigit(m,k,n) by Def4
          .= 0 by A2,A3,Def3;
A33:    DigA(DecSD(1,n,k),n) = 0 by A31,A30,A2,Th7;
A35:    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 A1,A2,RADIX_2:11
         .= SDDec(SDMax(n,m,k) '+' DecSD(1,n,k))
            + 0 * (Radix(k) |^ n) by RADIX_1:21,A32,A33;
        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
A40:        i in Seg n; then
A41:      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 A2,A40,RADIX_1:def 13;
A42:      DigA(Fmin(n,m,k),i) = FminDigit(m,k,i) by A40,Def6;
A43:      DigA(SDMax(n,m,k),i) = SDMaxDigit(m,k,i) by A40,Def4;
A44:      i >= 1 & i <= n by A40,FINSEQ_1:3;
          now per cases;
          suppose
A50:        i >= m+1; then
A52:        i > m by NAT_1:38; then
A53:        i > 1 by A3,AXIOMS:22; then
A54:        i -' 1 in Seg n by A40,Th1;
A55:        DigA(Fmin(n,m,k),i) = 0 by A42,A2,A52,Def5;
A56:        DigA(SDMax(n,m,k),i) = 0 by A43,A2,A52,Def3;
A57:        DigA(DecSD(1,n,k),i) = 0 by A2,A40,A53,Th7;
            now per cases by A50,REAL_1:def 5;
            suppose
A60:          i = m+1;
              DigA(SDMax(n,m,k),i-'1) = DigA(SDMax(n,m,k),m) by A60,BINARITH:39
                .= SDMaxDigit(m,k,m) by A2,Def4
                .= 0 by A2,Def3; then
              DigA(SDMax(n,m,k) '+' DecSD(1,n,k),i)
                = SD_Add_Data(0+0,k) + SD_Add_Carry(0+DigA(DecSD(1,n,k),i-'1))
                                                     by A41,A56,A57
               .= SD_Add_Data(0+0,k) + 0 by A2,A54,Lm6
               .= 0 by RADIX_1:22;
              hence thesis by A55;
            suppose i > m+1; then
              i - 1 > m + 1 - 1 by REAL_1:92; then
A63:          i - 1 > m by XCMPLX_1:26; then
              i - 1 > 0 by A3,AXIOMS:22; then
A64:          i -' 1 > m by A63,BINARITH:def 3;
              i -' 1 in Seg n by A53,A40,Th1; then
              DigA(SDMax(n,m,k),i-'1) = SDMaxDigit(m,k,i-'1) by Def4
               .= 0 by A2,A64,Def3; then
              DigA(SDMax(n,m,k) '+' DecSD(1,n,k),i)
                = SD_Add_Data(0+0,k) + SD_Add_Carry(0+DigA(DecSD(1,n,k),i-'1))
                                                     by A41,A56,A57
               .= SD_Add_Data(0+0,k) + 0 by A2,A54,Lm6
               .= 0 by RADIX_1:22;
              hence thesis by A55;
            end;
            hence thesis;
          suppose i < m+1; then
A67:        i <= m by NAT_1:38;
A68:        i >= 1 by A40,FINSEQ_1:3;
            now per cases by A68,REAL_1:def 5;
            suppose
A69:          i > 1; then
A70:          m > 1 by A67,AXIOMS:22; then
A71:          m -' 1 in Seg n by A2,Th1; then
A72:          m -' 1 >= 1 by FINSEQ_1:3;
A73:          m -' 1 < m by A70,JORDAN5B:1;
              now per cases by A67,REAL_1:def 5;
              suppose
A74:            i = m; then
A75:            DigA(Fmin(n,m,k),i) = FminDigit(m,k,m) by A2,Def6
                 .= 1 by A2,Def5;
A76:            DigA(SDMax(n,m,k),i) = 0 by A43,A2,A74,Def3;
A77:            DigA(DecSD(1,n,k),i) = 0 by A2,A70,A74,Th7;
A78:            DigA(SDMax(n,m,k),i-'1) = DigA(SDMax(n,m,k),m-'1) by A74
                 .= SDMaxDigit(m,k,m-'1) by A71,Def4
                 .= Radix(k) - 1 by A2,A72,A73,Def3;
A79:            i >= 1 + 1 by A69,INT_1:20;
                now per cases by A79,REAL_1:def 5;
                suppose
                  i = 2; then
                  i -' 1 = 2 - 1 by SCMFSA_7:3; then
                  DigA(DecSD(1,n,k),i-'1) = 1 by A5,A2,Th6; 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 A41,A76,A77,A78
                   .= 0 + SD_Add_Carry(Radix(k) - 1 + 1) by RADIX_1:22
                   .= SD_Add_Carry(Radix(k) + 1 - 1)  by XCMPLX_1:29
                   .= SD_Add_Carry(Radix(k)) by XCMPLX_1:26
                   .= 1  by A2,Th9;
                  hence thesis by A75;
                suppose
A83:              i > 2; then
A84:              i - 1 > 2 - 1 by REAL_1:92; then
                  i - 1 > 0 by AXIOMS:22; then
A85:              i -' 1 > 1 by A84,BINARITH:def 3;
                  i > 1 by A83,AXIOMS:22; then
                  i -' 1 in Seg n by A40,Th1; then
                  DigA(DecSD(1,n,k),i-'1) = 0 by A2,A85,Th7; 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 A41,A76,A77,A78
                   .= 0 + SD_Add_Carry(Radix(k) - 1) by RADIX_1:22 
                   .= 1 by A2,Lm5;
                  hence thesis by A75;
                end;
                hence thesis;
              suppose
A87:            i < m;
A89:            DigA(Fmin(n,m,k),i) = 0 by A42,A2,A87,Def5;
A90:            DigA(SDMax(n,m,k),i) = Radix(k)-1 by A43,A2,A44,A87,Def3;
A91:            DigA(DecSD(1,n,k),i) = 0 by A2,A40,A69,Th7;
A92:            i >= 1 + 1 by A69,INT_1:20;
                i -' 1 < i by A69,JORDAN5B:1; then
A94:            i -' 1 < m by A87,AXIOMS:22;
A95:            i -' 1 in Seg n by A40,A69,Th1;
                now per cases by A92,REAL_1:def 5;
                suppose i = 2; then
A97:              i -' 1 = 2 - 1 by SCMFSA_7:3; then
A98:              i -' 1 >= 1;
A99:              DigA(DecSD(1,n,k),i-'1) = 1 by A97,A5,A2,Th6;
                  DigA(SDMax(n,m,k),i-'1)
                    = SDMaxDigit(m,k,i-'1) by A95,Def4
                   .= Radix(k) - 1 by A98,A94,A2,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 + 1)  by A41,A90,A91,A99
                   .= SD_Add_Data(Radix(k)-1,k)
                      +SD_Add_Carry(Radix(k) + 1 - 1)  by XCMPLX_1:29 
                   .= SD_Add_Data(Radix(k)-1,k)
                      +SD_Add_Carry(Radix(k))  by XCMPLX_1:26 
                   .= SD_Add_Data(Radix(k)-1,k) + 1  by A2,Th9
                   .= (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 A2,Lm5
                   .= (Radix(k) - 1 ) + 1 - Radix(k) by XCMPLX_1:29 
                   .= (Radix(k) + 1 - 1) - Radix(k) by XCMPLX_1:29
                   .= Radix(k) - Radix(k) by XCMPLX_1:26
                   .= 0 by XCMPLX_1:14;
                  hence thesis by A89;
                suppose
A100:             i > 2; then
A101:             i - 1 > 2 - 1 by REAL_1:92; then
                  i - 1 > 0 by AXIOMS:22; then
A102:             i -' 1 > 1 by A101,BINARITH:def 3;
                  i > 1 by A100,AXIOMS:22; then
                  i -' 1 in Seg n by A40,Th1; then
A104:             DigA(DecSD(1,n,k),i-'1) = 0 by A2,A102,Th7;
                  DigA(SDMax(n,m,k),i-'1)
                    = SDMaxDigit(m,k,i-'1) by A95,Def4
                   .= Radix(k) - 1 by A102,A94,A2,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 A41,A90,A91,A104
                   .= SD_Add_Data(Radix(k)-1,k) + 1 by A2,Lm5
                   .= (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 A2,Lm5
                   .= (Radix(k) - 1 ) + 1 - Radix(k) by XCMPLX_1:29 
                   .= (Radix(k) + 1 - 1) - Radix(k) by XCMPLX_1:29
                   .= Radix(k) - Radix(k) by XCMPLX_1:26
                   .= 0 by XCMPLX_1:14;
                  hence thesis by A89;
                end;
                hence thesis;
              end;
              hence thesis;
            suppose
A106:         i = 1;
A107:         i -' 1 = 0 by A106,NAT_2:10; then
A108:         DigA(SDMax(n,m,k),i-'1) = 0 by RADIX_1:def 3;
A109:         DigA(DecSD(1,n,k),i-'1) = 0 by A107,RADIX_1:def 3;
              now per cases by A67,REAL_1:def 5;
              suppose
A110:           i < m;
A111:           i >= 1 by A106;
A112:           DigA(Fmin(n,m,k),i) = 0 by A110,A42,A2,Def5;
A113:           DigA(SDMax(n,m,k),i)=Radix(k)-1 by A43,A2,A110,A111,Def3;
                DigA(DecSD(1,n,k),i) = 1 by A2,A5,A106,Th6; 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 A41,A108,A109,A113
                 .= SD_Add_Data(Radix(k)-1+1,k) + 0 by RADIX_1:21
                 .= SD_Add_Data(Radix(k)+1-1,k) + 0 by XCMPLX_1:29
                 .= SD_Add_Data(Radix(k),k) + 0 by XCMPLX_1:26
                 .= Radix(k) - SD_Add_Carry(Radix(k)) * Radix(k)
                                                          by RADIX_1:def 11
                 .= Radix(k) - 1 * Radix(k) by A2,Th9
                 .= 0 by XCMPLX_1:14;
                hence thesis by A112;
              suppose
A115:           i = m;
A116:           DigA(Fmin(n,m,k),i) = 1 by A115,A42,A2,Def5;
A117:           DigA(SDMax(n,m,k),i) = 0 by A43,A2,A115,Def3;
                DigA(DecSD(1,n,k),i) = 1 by A2,A5,A106,Th6; then
                DigA(SDMax(n,m,k) '+' DecSD(1,n,k),i)
                  = SD_Add_Data(1+0,k)+SD_Add_Carry(0+0) by A41,A108,A109,A117
                 .= SD_Add_Data(1,k) + 0 by RADIX_1:21
                 .= 1 - SD_Add_Carry(1) * Radix(k)  by RADIX_1:def 11
                 .= 1 - 0 * Radix(k) by RADIX_1:def 10
                 .= 1;
                hence thesis by A116;
              end;
              hence thesis;
            end;
            hence thesis;
          end;
          hence thesis;
        end;
        hence thesis by A1,A35,Th11;
      end;
      hence thesis;
end;

theorem
    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
A2:     m in Seg n & k >= 2; then
A3:   n >= m & m >= 1 by FINSEQ_1:3; then
A4:   n + 1 > m by NAT_1:38;
A5:   n+1 >= 1 by NAT_1:29; then
      n+1 > 0 by AXIOMS:22; then
A6:   n+1 in Seg(n+1) by FINSEQ_1:5; then
A7:   DigA(Fmin(n+1,m,k),n+1) = FminDigit(m,k,n+1) by Def6
       .= 0 by A2,A4,Def5;
A8:   DigA(Fmax(n+1,m,k),n+1) = FmaxDigit(m,k,n+1) by A6,Def8
       .= 0 by A2,A4,Def7;
A9:   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,A5,RADIX_2:11
       .= SDDec(Fmin(n+1,m,k) '+' Fmax(n+1,m,k))
          + 0 * (Radix(k) |^ (n+1)) by RADIX_1:21,A7,A8;
A10:  m in Seg (n+1) by A2,FINSEQ_2:9;
      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;
        assume
A12:      i in Seg (n+1); then
A13:    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,A12,RADIX_1:def 13;
A14:    m + 1 > m by NAT_1:38;
A16:    DigA(Fmin(n+1,m,k),i) = FminDigit(m,k,i) by A12,Def6;
A17:    DigA(Fmax(n+1,m,k),i) = FmaxDigit(m,k,i) by A12,Def8;
A18:    DigA(Fmin(n+1,m+1,k),i) = FminDigit(m+1,k,i) by A12,Def6;
A19:    i >= 1 by A12,FINSEQ_1:3;
        now per cases;
        suppose
A21:      i >= m+1;
          now per cases;
          suppose
A22:        i = m+1;
A24:        DigA(Fmin(n+1,m,k),i) = FminDigit(m,k,m+1) by A12,A22,Def6
             .= 0 by A2,A14,Def5;
A25:        DigA(Fmax(n+1,m,k),i) = FmaxDigit(m,k,m+1) by A12,A22,Def8
             .= 0 by A2,A14,Def7;
A26:        DigA(Fmin(n+1,m,k),i-'1) = DigA(Fmin(n+1,m,k),m) by A22,BINARITH:39
             .= FminDigit(m,k,m) by A10,Def6
             .= 1 by A2,Def5;
A27:        DigA(Fmax(n+1,m,k),i-'1) = DigA(Fmax(n+1,m,k),m) by A22,BINARITH:39
             .= FmaxDigit(m,k,m) by A10,Def8
             .= Radix(k) - 1 by A2,Def7;
A29:        DigA(Fmin(n+1,m+1,k),i) = FminDigit(m+1,k,m+1) by A18,A22
             .= 1 by A2,Def5;
            DigA(Fmin(n+1,m,k) '+' Fmax(n+1,m,k),i)
              = SD_Add_Data(0+0,k) + SD_Add_Carry(1+(Radix(k)-1))
                                                        by A13,A24,A25,A26,A27
             .= 0 + SD_Add_Carry(1+(Radix(k)-1)) by RADIX_1:22
             .= SD_Add_Carry(Radix(k)) by XCMPLX_1:27
             .= 1 by A2,Th9;
            hence thesis by A29;
          suppose i <> m + 1; then
A31:        i > m + 1 by A21,REAL_1:def 5; then
A32:        i > m by A14,AXIOMS:22; then
            i > 1 by A3,AXIOMS:22; then
A34:        i -' 1 in Seg (n+1) by A12,Th1;
            i - 1 > m + 1 - 1 by A31,REAL_1:92; then
A35:        i - 1 > m by XCMPLX_1:26; then
            i - 1 > 0 by A3,AXIOMS:22; then
A36:        i -' 1 > m by A35,BINARITH:def 3;
A37:        DigA(Fmin(n+1,m,k),i) = 0 by A16,A2,A32,Def5;
A38:        DigA(Fmax(n+1,m,k),i) = 0 by A17,A2,A32,Def7;
A39:        DigA(Fmin(n+1,m,k),i-'1) = FminDigit(m,k,i-'1) by A34,Def6
             .= 0 by A2,A36,Def5;
A40:        DigA(Fmax(n+1,m,k),i-'1) = FmaxDigit(m,k,i-'1) by A34,Def8
             .= 0 by A2,A36,Def7;
A41:        DigA(Fmin(n+1,m+1,k),i) = 0 by A18,A2,A31,Def5;
            DigA(Fmin(n+1,m,k) '+' Fmax(n+1,m,k),i)
              = SD_Add_Data(0+0,k) + SD_Add_Carry(0+0) by A13,A37,A38,A39,A40;
            hence thesis by RADIX_1:22,RADIX_1:21,A41;
          end;
          hence thesis;
        suppose i < m+1; then
A50:      i <= m by NAT_1:38;
          now per cases by A19,REAL_1:def 5;
          suppose
A51:        i > 1; then
A60:        m > 1 by A50,AXIOMS:22; then
A61:        m -' 1 in Seg (n+1) by A10,Th1;
A62:        m -' 1 < m by A60,JORDAN5B:1;
            now per cases by A50,REAL_1:def 5;
            suppose
A63:          i = m; then
A64:          DigA(Fmin(n+1,m,k),i) = 1 by A16,A2,Def5;
A65:          DigA(Fmax(n+1,m,k),i) = Radix(k) - 1 by A17,A2,A63,Def7;
A66:          DigA(Fmin(n+1,m,k),i-'1) = DigA(Fmin(n+1,m,k),m-'1) by A63
               .= FminDigit(m,k,m-'1) by A61,Def6
               .= 0 by A2,A62,Def5;
A67:          DigA(Fmax(n+1,m,k),i-'1) = DigA(Fmax(n+1,m,k),m-'1) by A63
               .= FmaxDigit(m,k,m-'1) by A61,Def8
               .= 0 by A2,A62,Def7;
A68:          DigA(Fmin(n+1,m+1,k),i) = FminDigit(m+1,k,m) by A18,A63
               .= 0 by A2,A14,Def5;
              DigA(Fmin(n+1,m,k) '+' Fmax(n+1,m,k),i)
                = SD_Add_Data(1 + (Radix(k) - 1),k)
                  + SD_Add_Carry(0+0) by A13,A64,A65,A66,A67
               .= SD_Add_Data(1 + (Radix(k) - 1),k) + 0 by RADIX_1:21
               .= SD_Add_Data(Radix(k),k) by XCMPLX_1:27
               .= 0 by A2,Th10;
              hence thesis by A68;
            suppose
A70:          i < m;
              i -' 1 < i by A19,JORDAN5B:1; then
A71:          i -' 1 < m by A70,AXIOMS:22; then
A72:          i -' 1 <= n+1 by A4,AXIOMS:22;
              i -' 1 >= 1 by A51,JORDAN3:12; then
A73:          i -' 1 in Seg (n+1) by A72,FINSEQ_1:3;
A74:          DigA(Fmin(n+1,m,k),i) = 0 by A16,A2,A70,Def5;
A75:          DigA(Fmax(n+1,m,k),i) = 0 by A17,A2,A70,Def7;
A76:          DigA(Fmin(n+1,m,k),i-'1)
                = FminDigit(m,k,i-'1) by A73,Def6
               .= 0 by A2,A71,Def5;
A77:          DigA(Fmax(n+1,m,k),i-'1)
                = FmaxDigit(m,k,i-'1) by A73,Def8
               .= 0 by A2,A71,Def7;
              i < m + 1 by A70,NAT_1:38; then
A78:          DigA(Fmin(n+1,m+1,k),i) = 0 by A18,A2,Def5;
              DigA(Fmin(n+1,m,k) '+' Fmax(n+1,m,k),i)
                = SD_Add_Data(0+0,k) + SD_Add_Carry(0+0) by A13,A74,A75,A76,A77
               .= 0 + 0 by RADIX_1:22,RADIX_1:21;
              hence thesis by A78;
            end;
            hence thesis;
          suppose
A80:        i = 1;
A81:        i -' 1 = 0 by A80,NAT_2:10;
A82:        DigA(Fmin(n+1,m,k),i-'1) = 0 by A81,RADIX_1:def 3;
A83:        DigA(Fmax(n+1,m,k),i-'1) = 0 by A81,RADIX_1:def 3;
            now per cases by A50,REAL_1:def 5;
            suppose
A86:          i < m; then
A87:          DigA(Fmin(n+1,m,k),i) = 0 by A16,A2,Def5;
A88:          DigA(Fmax(n+1,m,k),i) = 0 by A17,A2,A86,Def7;
              i < m + 1 by A86,NAT_1:38; then
A89:          DigA(Fmin(n+1,m+1,k),i) = 0 by A18,A2,Def5;
              DigA(Fmin(n+1,m,k) '+' Fmax(n+1,m,k),i)
                = SD_Add_Data(0+0,k) + SD_Add_Carry(0+0) by A13,A82,A83,A87,A88
               .= 0 + 0 by RADIX_1:22,RADIX_1:21;
              hence thesis by A89;
            suppose
A90:          i = m; then
A91:          DigA(Fmin(n+1,m,k),i) = 1 by A16,A2,Def5;
A92:          DigA(Fmax(n+1,m,k),i) = Radix(k) - 1 by A17,A2,A90,Def7;
              i < m + 1 by A90,NAT_1:38; then
A93:          DigA(Fmin(n+1,m+1,k),i) = 0 by A18,A2,Def5;
              DigA(Fmin(n+1,m,k) '+' Fmax(n+1,m,k),i)
                = SD_Add_Data(1+(Radix(k)-1),k)
                   + SD_Add_Carry(0+0) by A13,A82,A83,A91,A92
               .= SD_Add_Data(1 + (Radix(k) - 1),k) + 0 by RADIX_1:21
               .= SD_Add_Data(Radix(k),k) by XCMPLX_1:27
               .= 0 by A2,Th10;
              hence thesis by A93;
            end;
            hence thesis;
          end;
          hence thesis;
        end;
        hence thesis;
      end;
      hence thesis by A9,A5,Th11;
end;


Back to top