:: High Speed Modulo Calculation Algorithm with Radix-$2^k$ SD Number
::  by Masaaki Niimura and Yasushi Fuwa
::
:: Received November 7, 2003
:: Copyright (c) 2003-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, NAT_1, XXREAL_0, ARYTM_3, RADIX_1, RADIX_5, FINSEQ_1,
      CARD_1, FUNCT_1, NEWTON, RELAT_1, PARTFUN1, ARYTM_1, CARD_3, FINSEQ_2,
      SUBSET_1, INT_1, RADIX_6;
 notations SUBSET_1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, ORDINAL1, NAT_D,
      NEWTON, RADIX_1, FINSEQ_1, FINSEQ_2, FUNCT_1, RELSET_1, PARTFUN1,
      GR_CY_1, RADIX_5;
 constructors REAL_1, NAT_D, NEWTON, GR_CY_1, RADIX_5, SEQ_1, RELSET_1;
 registrations RELSET_1, XXREAL_0, XREAL_0, NAT_1, INT_1, ORDINAL1, NEWTON,
      XBOOLE_0, FINSEQ_2;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 theorems RADIX_1, RADIX_2, RADIX_4, RADIX_5, INT_1, NAT_1, NAT_2, FINSEQ_1,
      FINSEQ_2, RVSUM_1, NEWTON, PREPOWER, FUNCT_1, FINSEQ_3, XREAL_1,
      XXREAL_0, NAT_D, CARD_1;
 schemes FINSEQ_2, NAT_1;

begin

Lm1: for m be Nat st m >= 1 holds m+2 > 1
proof
  let m be Nat;
  m+2 > m by XREAL_1:29;
  hence thesis by XXREAL_0:2;
end;

theorem Th1:
  for n be Nat st n >= 1 holds for m,k be Nat st m >= 1 & k >= 2
  holds SDDec(Fmin(m+n,m,k)) = SDDec(Fmin(m,m,k))
proof
  defpred P[Nat] means for m,k be Nat st m >= 1 & k >= 2 holds SDDec(Fmin(m+$1
  ,m,k)) = SDDec(Fmin(m,m,k));
A1: for n be Nat st n >= 1 & P[n] holds P[n+1]
  proof
    let n be Nat;
    assume that
    n >= 1 and
A2: P[n];
    let m,k be Nat;
    assume that
A3: m >= 1 and
A4: k >= 2;
    m + n >= m by NAT_1:11;
    then
A5: m + n + 1 > m by NAT_1:13;
    m+n+1 in Seg (m+n+1) by FINSEQ_1:4;
    then
A6: DigA(Fmin(m+n+1,m,k),m+n+1) = FminDigit(m,k,m+n+1) by RADIX_5:def 6
      .= 0 by A4,A5,RADIX_5:def 5;
    for i be Nat st i in Seg (m+n) holds Fmin((m+n)+1,m,k).i = Fmin(m+n,m ,k).i
    proof
      let i be Nat;
      assume
A7:   i in Seg (m+n);
      then
A8:   i in Seg (m+n+1) by FINSEQ_2:8;
      then Fmin(m+n+1,m,k).i = DigA(Fmin(m+n+1,m,k),i) by RADIX_1:def 3
        .= FminDigit(m,k,i) by A8,RADIX_5:def 6
        .= DigA(Fmin(m+n,m,k),i) by A7,RADIX_5:def 6;
      hence thesis by A7,RADIX_1:def 3;
    end;
    then
    SDDec(Fmin(m+(n+1),m,k)) = SDDec(Fmin(m+n,m,k)) + (Radix(k) |^ (m+n))
    *DigA(Fmin((m+n)+1,m,k),(m+n)+1) by RADIX_2:10
      .= SDDec(Fmin(m,m,k)) by A2,A3,A4,A6;
    hence thesis;
  end;
A9: P[1]
  proof
    let m,k be Nat;
    assume that
    m >= 1 and
A10: k >= 2;
A11: m + 1 > m by NAT_1:13;
    for i be Nat st i in Seg m holds Fmin(m+1,m,k).i = Fmin(m,m,k).i
    proof
      let i be Nat;
      assume
A12:  i in Seg m;
      then
A13:  i in Seg (m+1) by FINSEQ_2:8;
      then Fmin(m+1,m,k).i = DigA(Fmin(m+1,m,k),i) by RADIX_1:def 3
        .= FminDigit(m,k,i) by A13,RADIX_5:def 6
        .= DigA(Fmin(m,m,k),i) by A12,RADIX_5:def 6;
      hence thesis by A12,RADIX_1:def 3;
    end;
    then
A14: SDDec(Fmin(m+1,m,k)) = SDDec(Fmin(m,m,k)) + (Radix(k) |^ m)*DigA(Fmin
    (m+1,m,k),m+1) by RADIX_2:10;
    m+1 in Seg (m+1) by FINSEQ_1:4;
    then DigA(Fmin(m+1,m,k),m+1) = FminDigit(m,k,m+1) by RADIX_5:def 6
      .= 0 by A10,A11,RADIX_5:def 5;
    hence thesis by A14;
  end;
  for n be Nat st n >= 1 holds P[n] from NAT_1:sch 8(A9,A1);
  hence thesis;
end;

theorem
  for m,k be Nat st m >= 1 & k >= 2 holds SDDec(Fmin(m,m,k)) > 0
proof
  defpred P[Nat] means for k be Nat st k >= 2 holds SDDec(Fmin($1,$1,k)) > 0;
A1: for m be Nat st m >= 1 & P[m] holds P[m+1]
  proof
    let m be Nat;
    assume that
A2: m >= 1 and
    P[m];
    let k be Nat;
    assume
A3: k >= 2;
    then Radix(k) > 2 by RADIX_4:1;
    then
A4: Radix(k) > 1 by XXREAL_0:2;
    m+1 in Seg (m+1) by FINSEQ_1:4;
    then
A5: DigA(Fmin(m+1,m+1,k),m+1) = FminDigit(m+1,k,m+1) by RADIX_5:def 6
      .= 1 by A3,RADIX_5:def 5;
    for i be Nat st i in Seg m holds Fmin(m+1,m+1,k).i = DecSD(0,m,k).i
    proof
      let i be Nat;
      assume
A6:   i in Seg m;
      then i <= m by FINSEQ_1:1;
      then
A7:   i < m + 1 by NAT_1:13;
A8:   i in Seg (m+1) by A6,FINSEQ_2:8;
      then Fmin(m+1,m+1,k).i = DigA(Fmin(m+1,m+1,k),i) by RADIX_1:def 3
        .= FminDigit(m+1,k,i) by A8,RADIX_5:def 6
        .= 0 by A3,A7,RADIX_5:def 5
        .= DigA(DecSD(0,m,k),i) by A6,RADIX_5:5;
      hence thesis by A6,RADIX_1:def 3;
    end;
    then SDDec(Fmin(m+1,m+1,k)) = SDDec(DecSD(0,m,k)) + (Radix(k) |^ m)*DigA(
    Fmin(m+1,m+1,k),m+1) by RADIX_2:10
      .= 0 + (Radix(k) |^ m) by A2,A5,RADIX_5:6;
    hence thesis by A4,PREPOWER:11;
  end;
A9: P[1]
  proof
    let k be Nat;
    assume
A10: k >= 2;
A11: 1 in Seg 1 by FINSEQ_1:1;
    then DigitSD(Fmin(1,1,k))/.1 = SubDigit(Fmin(1,1,k),1,k) by RADIX_1:def 6
      .= (Radix(k) |^ (1-'1)) * DigB(Fmin(1,1,k),1) by RADIX_1:def 5
      .= (Radix(k) |^ (1-'1)) * DigA(Fmin(1,1,k),1) by RADIX_1:def 4
      .= (Radix(k) |^ 0) * DigA(Fmin(1,1,k),1) by XREAL_1:232
      .= 1 * DigA(Fmin(1,1,k),1) by NEWTON:4
      .= FminDigit(1,k,1) by A11,RADIX_5:def 6
      .= 1 by A10,RADIX_5:def 5;
    then
A12: DigitSD(Fmin(1,1,k)) = <* 1 *> by RADIX_1:17;
    SDDec(Fmin(1,1,k)) = Sum DigitSD(Fmin(1,1,k)) by RADIX_1:def 7
      .= 1 by A12,RVSUM_1:73;
    hence thesis;
  end;
  for m be Nat st m >= 1 holds P[m] from NAT_1:sch 8(A9,A1);
  hence thesis;
end;

begin :: Definitions of Upper 3 Digits of Radix-$2^k$ SD number and its property

definition
  let i,m,k be Nat, r be Tuple of (m+2),(k-SD);
  assume
A1: i in Seg (m+2);
  func M0Digit(r,i) -> Element of k-SD equals
  :Def1:
  r.i if i >= m otherwise 0;
  coherence
  proof
    len r = m+2 by CARD_1:def 7;
    then i in dom r by A1,FINSEQ_1:def 3;
    then r.i in rng r by FUNCT_1:def 3;
    hence thesis by RADIX_1:14;
  end;
  consistency;
end;

definition
  let m,k be Nat, r be Tuple of (m+2),(k-SD);
  func M0(r) -> Tuple of (m+2),k-SD means
  :Def2:
  for i be Nat st i in Seg (m+2) holds DigA(it,i) = M0Digit(r,i);
  existence
  proof
    deffunc F1(Nat) = M0Digit(r,$1);
    consider z being FinSequence of k-SD such that
A1: len z = m+2 and
A2: for j be Nat st j in dom z holds z.j = F1(j) from FINSEQ_2:sch 1;
A3: dom z = Seg(m+2) by A1,FINSEQ_1:def 3;
    z is Element of (m+2)-tuples_on (k-SD) by A1,FINSEQ_2:92;
    then reconsider z as Tuple of (m+2),(k-SD);
    take z;
    let i be Nat;
    assume
A4: i in Seg (m+2);
    hence DigA(z,i) = z.i by RADIX_1:def 3
      .= M0Digit(r,i) by A2,A3,A4;
  end;
  uniqueness
  proof
    let k1,k2 be Tuple of (m+2),k-SD such that
A5: for i be Nat st i in Seg (m+2) holds DigA(k1,i) = M0Digit(r,i) and
A6: for i be Nat st i in Seg (m+2) holds DigA(k2,i) = M0Digit(r,i);
A7: len k1 = m+2 by CARD_1:def 7;
    then
A8: dom k1 = Seg (m+2) by FINSEQ_1:def 3;
A9: now
      let j be Nat;
      assume
A10:  j in dom k1;
      then k1.j = DigA(k1,j) by A8,RADIX_1:def 3
        .= M0Digit(r,j) by A5,A8,A10
        .= DigA(k2,j) by A6,A8,A10
        .= k2.j by A8,A10,RADIX_1:def 3;
      hence k1.j = k2.j;
    end;
    len k2 = m+2 by CARD_1:def 7;
    hence k1 = k2 by A7,A9,FINSEQ_2:9;
  end;
end;

definition
  let i,m,k be Nat, r be Tuple of (m+2),(k-SD);
  assume that
A1: k >= 2 and
A2: i in Seg (m+2);
  func MmaxDigit(r,i) -> Element of k-SD equals
  :Def3:
  r.i if i >= m otherwise Radix(k)-1;
  coherence
  proof
    len r = m+2 by CARD_1:def 7;
    then i in dom r by A2,FINSEQ_1:def 3;
    then r.i in rng r by FUNCT_1:def 3;
    hence thesis by A1,RADIX_5:1;
  end;
  consistency;
end;

definition
  let m,k be Nat, r be Tuple of (m+2),(k-SD);
  func Mmax(r) -> Tuple of (m+2),k-SD means
  :Def4:
  for i be Nat st i in Seg (m+2) holds DigA(it,i) = MmaxDigit(r,i);
  existence
  proof
    deffunc F(Nat) = MmaxDigit(r,$1);
    consider z being FinSequence of k-SD such that
A1: len z = m+2 and
A2: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
A3: dom z = Seg(m+2) by A1,FINSEQ_1:def 3;
        z is Element of (m+2)-tuples_on (k-SD) by A1,FINSEQ_2:92;
    then reconsider z as Tuple of (m+2),(k-SD);
    take z;
    let i be Nat;
    assume
A4: i in Seg (m+2);
    hence DigA(z,i) = z.i by RADIX_1:def 3
      .= MmaxDigit(r,i) by A2,A3,A4;
  end;
  uniqueness
  proof
    let k1,k2 be Tuple of (m+2),k-SD such that
A5: for i be Nat st i in Seg (m+2) holds DigA(k1,i) = MmaxDigit(r,i) and
A6: for i be Nat st i in Seg (m+2) holds DigA(k2,i) = MmaxDigit(r,i);
A7: len k1 = m+2 by CARD_1:def 7;
    then
A8: dom k1 = Seg(m+2) by FINSEQ_1:def 3;
A9: now
      let j be Nat;
      assume
A10:  j in dom k1;
      then k1.j = DigA(k1,j) by A8,RADIX_1:def 3
        .= MmaxDigit(r,j) by A5,A8,A10
        .= DigA(k2,j) by A6,A8,A10
        .= k2.j by A8,A10,RADIX_1:def 3;
      hence k1.j = k2.j;
    end;
    len k2 = m+2 by CARD_1:def 7;
    hence k1 = k2 by A7,A9,FINSEQ_2:9;
  end;
end;

definition
  let i,m,k be Nat, r be Tuple of (m+2),(k-SD);
  assume that
A1: k >= 2 and
A2: i in Seg (m+2);
  func MminDigit(r,i) -> Element of k-SD equals
  :Def5:
  r.i if i >= m otherwise -Radix(k)+1;
  coherence
  proof
    len r = m+2 by CARD_1:def 7;
    then i in dom r by A2,FINSEQ_1:def 3;
    then
A3: r.i in rng r by FUNCT_1:def 3;
    Radix(k) > 2 by A1,RADIX_4:1;
    then Radix(k) > 1 by XXREAL_0:2;
    then Radix(k) + Radix(k) > 1 + 1 by XREAL_1:8;
    then
A4: Radix(k) - 1 > 1 - Radix(k) by XREAL_1:21;
A5: -Radix(k) + 1 is Element of INT by INT_1:def 2;
    k-SD = {w where w is Element of INT:w <= Radix(k)-1 & w >= -Radix(k)+1
    } by RADIX_1:def 2;
    then -Radix(k) + 1 in k-SD by A4,A5;
    hence thesis by A3;
  end;
  consistency;
end;

definition
  let m,k be Nat, r be Tuple of (m+2),(k-SD);
  func Mmin(r) -> Tuple of (m+2),k-SD means
  :Def6:
  for i be Nat st i in Seg (m+2) holds DigA(it,i) = MminDigit(r,i);
  existence
  proof
    deffunc F(Nat) = MminDigit(r,$1);
    consider z being FinSequence of k-SD such that
A1: len z = m+2 and
A2: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
A3: dom z = Seg(m+2) by A1,FINSEQ_1:def 3;
        z is Element of (m+2)-tuples_on (k-SD) by A1,FINSEQ_2:92;
    then reconsider z as Tuple of (m+2),(k-SD);
    take z;
    let i be Nat;
    assume
A4: i in Seg (m+2);
    hence DigA(z,i) = z.i by RADIX_1:def 3
      .= F(i) by A2,A3,A4;
  end;
  uniqueness
  proof
    let k1,k2 be Tuple of (m+2),k-SD such that
A5: for i be Nat st i in Seg (m+2) holds DigA(k1,i) = MminDigit(r,i) and
A6: for i be Nat st i in Seg (m+2) holds DigA(k2,i) = MminDigit(r,i);
A7: len k1 = m+2 by CARD_1:def 7;
    then
A8: dom k1 = Seg(m+2) by FINSEQ_1:def 3;
A9: now
      let j be Nat;
      assume
A10:  j in dom k1;
      then k1.j = DigA(k1,j) by A8,RADIX_1:def 3
        .= MminDigit(r,j) by A5,A8,A10
        .= DigA(k2,j) by A6,A8,A10
        .= k2.j by A8,A10,RADIX_1:def 3;
      hence k1.j = k2.j;
    end;
    len k2 = m+2 by CARD_1:def 7;
    hence k1 = k2 by A7,A9,FINSEQ_2:9;
  end;
end;

theorem Th3:
  for m,k be Nat st k >= 2 holds for r be Tuple of (m+2),k-SD holds
  SDDec(Mmax(r)) >= SDDec(r)
proof
  let m,k be Nat;
  assume that
A1: k >= 2;
  let r be Tuple of (m+2),k-SD;
  for i be Nat st i in Seg (m+2) holds DigA(Mmax(r),i) >= DigA(r,i)
  proof
    let i be Nat;
    assume
A2: i in Seg (m+2);
    then
A3: DigA(Mmax(r),i) = MmaxDigit(r,i) by Def4;
    now
      per cases;
      suppose
        i >= m;
        then DigA(Mmax(r),i) = r.i by A1,A2,A3,Def3
          .= DigA(r,i) by A2,RADIX_1:def 3;
        hence thesis;
      end;
      suppose
A4:     i < m;
A5:     DigA(r,i) = r.i by A2,RADIX_1:def 3;
A6:     r.i is Element of k-SD by A2,RADIX_1:15;
        DigA(Mmax(r),i) = Radix(k) - 1 by A1,A2,A3,A4,Def3;
        hence thesis by A5,A6,RADIX_1:13;
      end;
    end;
    hence thesis;
  end;
  hence thesis by NAT_1:12,RADIX_5:13;
end;

theorem Th4:
  for m,k be Nat st k >= 2 holds for r be Tuple of (m+2),k-SD holds
  SDDec(r) >= SDDec(Mmin(r))
proof
  let m,k be Nat;
  assume that
A1: k >= 2;
  let r be Tuple of (m+2),k-SD;
  for i be Nat st i in Seg (m+2) holds DigA(r,i) >= DigA(Mmin(r),i)
  proof
    let i be Nat;
    assume
A2: i in Seg (m+2);
    then
A3: DigA(Mmin(r),i) = MminDigit(r,i) by Def6;
    now
      per cases;
      suppose
        i >= m;
        then DigA(Mmin(r),i) = r.i by A1,A2,A3,Def5
          .= DigA(r,i) by A2,RADIX_1:def 3;
        hence thesis;
      end;
      suppose
A4:     i < m;
A5:     DigA(r,i) = r.i by A2,RADIX_1:def 3;
A6:     r.i is Element of k-SD by A2,RADIX_1:15;
        DigA(Mmin(r),i) = - Radix(k) + 1 by A1,A2,A3,A4,Def5;
        hence thesis by A5,A6,RADIX_1:13;
      end;
    end;
    hence thesis;
  end;
  hence thesis by NAT_1:12,RADIX_5:13;
end;

begin :: Properties of minimum digits of Radix-$2^k$ SD number

definition
  let n,k be Nat, x be Integer;
  pred x needs_digits_of n,k means
  :Def7:
  x < Radix(k) |^ n & x >= Radix(k) |^ (n-'1);
end;

theorem Th5:
  for x,n,k,i be Nat st i in Seg n holds DigA(DecSD(x,n,k),i) >= 0
proof
  let x,n,k,i be Nat;
  assume
A1: i in Seg n;
  then
A2: i >= 1 by FINSEQ_1:1;
  DigA(DecSD(x,n,k),i) = DigitDC(x,i,k) by A1,RADIX_1:def 9
    .= (x mod (Radix(k) |^ i)) div (Radix(k) |^ (i -'1)) by RADIX_1:def 8
    .= (x div (Radix(k) |^ (i -'1))) mod Radix(k) by A2,RADIX_2:4,6;
  hence thesis;
end;

theorem Th6:
  for n,k,x be Nat st n >= 1 & x needs_digits_of n,k holds DigA(
  DecSD(x,n,k),n) > 0
proof
  let n,k,x be Nat;
  assume that
A1: n >= 1 and
A2: x needs_digits_of n,k;
  x < (Radix(k) |^ n) by A2,Def7;
  then
A3: x mod (Radix(k) |^ n) = x by NAT_D:24;
  n in Seg n by A1,FINSEQ_1:3;
  then
A4: DigA(DecSD(x,n,k),n) = DigitDC(x,n,k) by RADIX_1:def 9
    .= x div (Radix(k) |^ (n -'1)) by A3,RADIX_1:def 8;
A5: (Radix(k) |^ (n-'1)) > 0 by PREPOWER:6,RADIX_2:6;
  x >= (Radix(k) |^ (n-'1)) by A2,Def7;
  hence thesis by A4,A5,NAT_2:13;
end;

theorem Th7:
  for f,m,k be Nat st m >= 1 & k >= 2 & f needs_digits_of m,k holds
  f >= SDDec(Fmin(m+2,m,k))
proof
  let f,m,k be Nat;
  assume that
A1: m >= 1 and
A2: k >= 2 and
A3: f needs_digits_of m,k;
  for i be Nat st i in Seg m holds DigA(DecSD(f,m,k),i) >= DigA(Fmin(m,m,k ),i)
  proof
    let i be Nat;
    assume
A4: i in Seg m;
    then
A5: i <= m by FINSEQ_1:1;
    now
      per cases by A5,XXREAL_0:1;
      suppose
A6:     i = m;
        then DigA(DecSD(f,m,k),i) > 0 by A1,A3,Th6;
        then
A7:     DigA(DecSD(f,m,k),i) >= 0 + 1 by INT_1:7;
        DigA(Fmin(m,m,k),i) = FminDigit(m,k,i) by A4,RADIX_5:def 6
          .= 1 by A2,A6,RADIX_5:def 5;
        hence thesis by A7;
      end;
      suppose
A8:     i < m;
        DigA(Fmin(m,m,k),i) = FminDigit(m,k,i) by A4,RADIX_5:def 6
          .= 0 by A2,A8,RADIX_5:def 5;
        hence thesis by A4,Th5;
      end;
    end;
    hence thesis;
  end;
  then SDDec(DecSD(f,m,k)) >= SDDec(Fmin(m,m,k)) by A1,RADIX_5:13;
  then
A9: SDDec(DecSD(f,m,k)) >= SDDec(Fmin(m+2,m,k)) by A1,A2,Th1;
  f < (Radix(k) |^ m) by A3,Def7;
  then f is_represented_by m,k by RADIX_1:def 12;
  hence thesis by A1,A9,RADIX_1:22;
end;

begin :: Modulo calculation algorithm using Upper 3 Digits of Radix-$2^k$ SD number

theorem Th8:
  for mlow,mhigh,f be Integer st mhigh < mlow + f & f > 0 holds ex
  s be Integer st -f < mlow - s * f & mhigh - s * f < f
proof
  let mlow,mhigh,f be Integer;
  assume that
A1: mhigh < mlow + f and
A2: f > 0;
  reconsider f as Element of NAT by A2,INT_1:3;
A3: mhigh + - ((mhigh div f) * f) < mlow + f + - ((mhigh div f) * f) by A1,
XREAL_1:6;
A4: mhigh mod f = mhigh - (mhigh div f) * f by A2,INT_1:def 10;
  then 0 <= mhigh - (mhigh div f) * f by A2,NAT_D:62;
  then 0 + -f < (mlow + - ((mhigh div f) * f)) + f + -f by A3,XREAL_1:6;
  then - f < mlow - (mhigh div f) * f;
  hence thesis by A2,A4,NAT_D:62;
end;

theorem Th9:
  for m,k be Nat st k >= 2 holds for r be Tuple of (m+2),k-SD holds
  SDDec(Mmax(r)) + SDDec(DecSD(0,m+2,k)) = SDDec(M0(r)) + SDDec(SDMax(m+2,m,k))
proof
  let m,k be Nat;
  assume that
A1: k >= 2;
  let r be Tuple of (m+2),k-SD;
A2: for i be Nat st i in Seg (m+2) holds DigA(M0(r),i) = DigA(Mmax(r),i) &
DigA(SDMax(m+2,m,k),i) = 0 or DigA(SDMax(m+2,m,k),i) = DigA(Mmax(r),i) & DigA(
  M0(r),i) = 0
  proof
    let i be Nat;
    assume
A3: i in Seg (m+2);
    then
A4: DigA(Mmax(r),i) = MmaxDigit(r,i) by Def4;
A5: i >= 1 by A3,FINSEQ_1:1;
    now
      per cases;
      suppose
A6:     i < m;
A7:     DigA(M0(r),i) = M0Digit(r,i) by A3,Def2
          .= 0 by A3,A6,Def1;
        DigA(Mmax(r),i) = Radix(k) - 1 by A1,A3,A4,A6,Def3
          .= SDMaxDigit(m,k,i) by A1,A5,A6,RADIX_5:def 3
          .= DigA(SDMax(m+2,m,k),i) by A3,RADIX_5:def 4;
        hence thesis by A7;
      end;
      suppose
A8:     i >= m;
A9:     DigA(SDMax(m+2,m,k),i) = SDMaxDigit(m,k,i) by A3,RADIX_5:def 4
          .= 0 by A1,A8,RADIX_5:def 3;
        DigA(Mmax(r),i) = r.i by A1,A3,A4,A8,Def3
          .= M0Digit(r,i) by A3,A8,Def1
          .= DigA(M0(r),i) by A3,Def2;
        hence thesis by A9;
      end;
    end;
    hence thesis;
  end;
  m + 2 >= 1 by NAT_1:12;
  hence thesis by A1,A2,RADIX_5:15;
end;

theorem Th10:
  for m,k be Nat st m >= 1 & k >= 2 holds for r be Tuple of (m+2),
  k-SD holds SDDec(Mmax(r)) < SDDec(M0(r)) + SDDec(Fmin(m+2,m,k))
proof
  let m,k be Nat;
  assume that
A1: m >= 1 and
A2: k >= 2;
A3: m+2 > 1 by A1,Lm1;
  let r be Tuple of (m+2),k-SD;
A4: SDDec(Mmax(r)) + 1 > SDDec(Mmax(r)) + 0 by XREAL_1:8;
A5: SDDec(M0(r)) + SDDec(SDMax(m+2,m,k)) = SDDec(Mmax(r)) + SDDec(DecSD(0,m+
  2,k)) by A2,Th9
    .= SDDec(Mmax(r)) + 0 by A3,RADIX_5:6;
  m in Seg (m+2) by A1,FINSEQ_3:9;
  then
  SDDec(Fmin(m+2,m,k)) = SDDec(SDMax(m+2,m,k)) + SDDec(DecSD(1,m+2,k)) by A2,A3
,RADIX_5:18
    .= SDDec(SDMax(m+2,m,k)) + 1 by A2,A3,RADIX_5:9;
  hence thesis by A5,A4;
end;

theorem Th11:
  for m,k be Nat st k >= 2 holds for r be Tuple of (m+2),k-SD
holds SDDec(Mmin(r)) + SDDec(DecSD(0,m+2,k)) = SDDec(M0(r)) + SDDec(SDMin(m+2,m
  ,k))
proof
  let m,k be Nat;
  assume that
A1: k >= 2;
  let r be Tuple of (m+2),k-SD;
A2: for i be Nat st i in Seg (m+2) holds DigA(M0(r),i) = DigA(Mmin(r),i) &
DigA(SDMin(m+2,m,k),i) = 0 or DigA(SDMin(m+2,m,k),i) = DigA(Mmin(r),i) & DigA(
  M0(r),i) = 0
  proof
    let i be Nat;
    assume
A3: i in Seg (m+2);
    then
A4: DigA(Mmin(r),i) = MminDigit(r,i) by Def6;
A5: i >= 1 by A3,FINSEQ_1:1;
    now
      per cases;
      suppose
A6:     i < m;
A7:     DigA(M0(r),i) = M0Digit(r,i) by A3,Def2
          .= 0 by A3,A6,Def1;
        DigA(Mmin(r),i) = -Radix(k) + 1 by A1,A3,A4,A6,Def5
          .= SDMinDigit(m,k,i) by A1,A5,A6,RADIX_5:def 1
          .= DigA(SDMin(m+2,m,k),i) by A3,RADIX_5:def 2;
        hence thesis by A7;
      end;
      suppose
A8:     i >= m;
A9:     DigA(SDMin(m+2,m,k),i) = SDMinDigit(m,k,i) by A3,RADIX_5:def 2
          .= 0 by A1,A8,RADIX_5:def 1;
        DigA(Mmin(r),i) = r.i by A1,A3,A4,A8,Def5
          .= M0Digit(r,i) by A3,A8,Def1
          .= DigA(M0(r),i) by A3,Def2;
        hence thesis by A9;
      end;
    end;
    hence thesis;
  end;
  m + 2 >= 1 by NAT_1:12;
  hence thesis by A1,A2,RADIX_5:15;
end;

theorem Th12:
  for m,k be Nat, r be Tuple of (m+2),k-SD st m >= 1 & k >= 2
holds SDDec(M0(r)) + SDDec(DecSD(0,m+2,k)) = SDDec(Mmin(r)) + SDDec(SDMax(m+2,m
  ,k))
proof
  let m,k be Nat, r be Tuple of (m+2),k-SD;
  assume that
A1: m >= 1 and
A2: k >= 2;
A3: m+2 > 1 by A1,Lm1;
  SDDec(M0(r)) + SDDec(SDMin(m+2,m,k)) = SDDec(Mmin(r)) + SDDec(DecSD(0,m+
  2,k)) by A2,Th11
    .= SDDec(Mmin(r)) + 0 by A3,RADIX_5:6;
  then
  SDDec(Mmin(r)) + SDDec(SDMax(m+2,m,k)) = SDDec(M0(r)) + (SDDec(SDMax(m+2
  ,m,k)) + SDDec(SDMin(m+2,m,k)))
    .= SDDec(M0(r)) + SDDec(DecSD(0,m+2,k)) by A2,A3,RADIX_5:17;
  hence thesis;
end;

theorem Th13:
  for m,k be Nat st m >= 1 & k >= 2 holds for r be Tuple of (m+2),
  k-SD holds SDDec(M0(r)) < SDDec(Mmin(r)) + SDDec(Fmin(m+2,m,k))
proof
  let m,k be Nat;
  assume that
A1: m >= 1 and
A2: k >= 2;
  let r be Tuple of (m+2),k-SD;
A3: m+2 > 1 by A1,Lm1;
A4: SDDec(Mmin(r)) + SDDec(SDMax(m+2,m,k)) = SDDec(M0(r)) + SDDec(DecSD(0,m+
  2,k)) by A1,A2,Th12
    .= SDDec(M0(r)) + 0 by A3,RADIX_5:6;
A5: SDDec(M0(r)) + 1 > SDDec(M0(r)) + 0 by XREAL_1:8;
  m in Seg (m+2) by A1,FINSEQ_3:9;
  then
  SDDec(Fmin(m+2,m,k)) = SDDec(SDMax(m+2,m,k)) + SDDec(DecSD(1,m+2,k)) by A2,A3
,RADIX_5:18
    .= SDDec(SDMax(m+2,m,k)) + 1 by A2,A3,RADIX_5:9;
  hence thesis by A4,A5;
end;

theorem
  for m,k,f be Nat, r be Tuple of (m+2),k-SD st m >= 1 & k >= 2 & f
needs_digits_of m,k holds ex s be Integer st - f < (SDDec(M0(r)) - s*f) & SDDec
  (Mmax(r)) - s*f < f
proof
  let m,k,f be Nat, r be Tuple of (m+2),k-SD;
  assume that
A1: m >= 1 and
A2: k >= 2 and
A3: f needs_digits_of m,k;
  SDDec(Fmin(m+2,m,k)) <= f by A1,A2,A3,Th7;
  then
A4: SDDec(M0(r)) + SDDec(Fmin(m+2,m,k)) <= SDDec(M0(r)) + f by XREAL_1:7;
  SDDec(Mmax(r)) < SDDec(M0(r)) + SDDec(Fmin(m+2,m,k)) by A1,A2,Th10;
  then
A5: SDDec(Mmax(r)) < SDDec(M0(r)) + f by A4,XXREAL_0:2;
  Radix(k) |^ (m-'1) > 0 by NEWTON:83,RADIX_2:6;
  then f > 0 by A3,Def7;
  hence thesis by A5,Th8;
end;

theorem
  for m,k,f be Nat, r be Tuple of (m+2),k-SD st m >= 1 & k >= 2 & f
  needs_digits_of m,k holds ex s be Integer st - f < (SDDec(Mmin(r)) - s*f) &
  SDDec(M0(r)) - s*f < f
proof
  let m,k,f be Nat, r be Tuple of (m+2),k-SD;
  assume that
A1: m >= 1 and
A2: k >= 2 and
A3: f needs_digits_of m,k;
  SDDec(Fmin(m+2,m,k)) <= f by A1,A2,A3,Th7;
  then
A4: SDDec(Mmin(r)) + SDDec(Fmin(m+2,m,k)) <= SDDec(Mmin(r)) + f by XREAL_1:7;
  SDDec(M0(r)) < SDDec(Mmin(r)) + SDDec(Fmin(m+2,m,k)) by A1,A2,Th13;
  then
A5: SDDec(M0(r)) < SDDec(Mmin(r)) + f by A4,XXREAL_0:2;
  Radix(k) |^ (m-'1) > 0 by NEWTON:83,RADIX_2:6;
  then f > 0 by A3,Def7;
  hence thesis by A5,Th8;
end;

theorem
  for m,k be Nat, r be Tuple of (m+2),k-SD st k >= 2 holds SDDec(M0(r))
<= SDDec(r) & SDDec(r) <= SDDec(Mmax(r)) or SDDec(Mmin(r)) <= SDDec(r) & SDDec(
  r) < SDDec(M0(r))
proof
  let m,k be Nat;
  let r be Tuple of (m+2),k-SD;
  set MZero = SDDec(M0(r));
  set R = SDDec(r);
  assume that
A1: k >= 2;
  now
    per cases;
    suppose
      R < MZero;
      hence thesis by A1,Th4;
    end;
    suppose
      R >= MZero;
      hence thesis by A1,Th3;
    end;
  end;
  hence thesis;
end;

begin :: How to identify the range of modulo arithmetic result

definition
  let i,m,k be Nat, r be Tuple of (m+2),(k-SD);
  assume
A1: i in Seg (m+2);
  func MmaskDigit(r,i) -> Element of k-SD equals
  :Def8:
  r.i if i < m otherwise 0;
  coherence
  proof
    len r = m+2 by CARD_1:def 7;
    then i in dom r by A1,FINSEQ_1:def 3;
    then r.i in rng r by FUNCT_1:def 3;
    hence thesis by RADIX_1:14;
  end;
  consistency;
end;

definition
  let m,k be Nat, r be Tuple of (m+2),(k-SD);
  func Mmask(r) -> Tuple of (m+2),k-SD means
  :Def9:
  for i be Nat st i in Seg (m+2) holds DigA(it,i) = MmaskDigit(r,i);
  existence
  proof
    deffunc F(Nat) = MmaskDigit(r,$1);
    consider z being FinSequence of k-SD such that
A1: len z = m+2 and
A2: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
A3: dom z = Seg(m+2) by A1,FINSEQ_1:def 3;
        z is Element of (m+2)-tuples_on (k-SD) by A1,FINSEQ_2:92;
    then reconsider z as Tuple of (m+2),(k-SD);
    take z;
    let i be Nat;
    assume
A4: i in Seg (m+2);
    hence DigA(z,i) = z.i by RADIX_1:def 3
      .= MmaskDigit(r,i) by A2,A3,A4;
  end;
  uniqueness
  proof
    let k1,k2 be Tuple of (m+2),k-SD such that
A5: for i be Nat st i in Seg (m+2) holds DigA(k1,i) = MmaskDigit(r,i) and
A6: for i be Nat st i in Seg (m+2) holds DigA(k2,i) = MmaskDigit(r,i);
A7: len k1 = m+2 by CARD_1:def 7;
    then
A8: dom k1 = Seg(m+2) by FINSEQ_1:def 3;
A9: now
      let j be Nat;
      assume
A10:  j in dom k1;
      then k1.j = DigA(k1,j) by A8,RADIX_1:def 3
        .= MmaskDigit(r,j) by A5,A8,A10
        .= DigA(k2,j) by A6,A8,A10
        .= k2.j by A8,A10,RADIX_1:def 3;
      hence k1.j = k2.j;
    end;
    len k2 = m+2 by CARD_1:def 7;
    hence k1 = k2 by A7,A9,FINSEQ_2:9;
  end;
end;

theorem Th17:
  for m,k be Nat, r be Tuple of (m+2),k-SD st k >= 2 holds SDDec(
  M0(r)) + SDDec(Mmask(r)) = SDDec(r) + SDDec(DecSD(0,m+2,k))
proof
  let m,k be Nat, r be Tuple of (m+2),k-SD;
A1: m + 2 >= 1 by NAT_1:12;
A2: for i be Nat st i in Seg (m+2) holds DigA(M0(r),i) = DigA(r,i) & DigA(
  Mmask(r),i) = 0 or DigA(Mmask(r),i) = DigA(r,i) & DigA(M0(r),i) = 0
  proof
    let i be Nat;
    assume
A3: i in Seg (m+2);
    now
      per cases;
      suppose
A4:     i < m;
A5:     DigA(M0(r),i) = M0Digit(r,i) by A3,Def2
          .= 0 by A3,A4,Def1;
        DigA(Mmask(r),i) = MmaskDigit(r,i) by A3,Def9
          .= r.i by A3,A4,Def8
          .= DigA(r,i) by A3,RADIX_1:def 3;
        hence thesis by A5;
      end;
      suppose
A6:     i >= m;
A7:     DigA(Mmask(r),i) = MmaskDigit(r,i) by A3,Def9
          .= 0 by A3,A6,Def8;
        DigA(M0(r),i) = M0Digit(r,i) by A3,Def2
          .= r.i by A3,A6,Def1
          .= DigA(r,i) by A3,RADIX_1:def 3;
        hence thesis by A7;
      end;
    end;
    hence thesis;
  end;
  assume k >= 2;
  hence thesis by A1,A2,RADIX_5:15;
end;

theorem
  for m,k be Nat, r be Tuple of (m+2),k-SD st m >= 1 & k >= 2 holds
  SDDec(Mmask(r)) > 0 implies SDDec(r) > SDDec(M0(r))
proof
  let m,k be Nat, r be Tuple of (m+2),k-SD;
  assume that
A1: m >= 1 and
A2: k >= 2;
A3: m+2 > 1 by A1,Lm1;
  SDDec(M0(r)) + SDDec(Mmask(r)) = SDDec(r) + SDDec(DecSD(0,m+2,k)) by A2,Th17
    .= SDDec(r) + 0 by A3,RADIX_5:6;
  then
A4: SDDec(r) - SDDec(M0(r)) = SDDec(Mmask(r)) - 0;
  assume SDDec(Mmask(r)) > 0;
  hence thesis by A4,XREAL_1:47;
end;

definition
  let i,m,k be Nat;
  assume
A1: k >= 2;
  func FSDMinDigit(m,k,i) -> Element of k-SD equals
  :Def10:
  0 if i > m, 1 if i = m otherwise -Radix(k)+1;
  coherence
  proof
    Radix(k) > 2 by A1,RADIX_4:1;
    then Radix(k) > 1 by XXREAL_0:2;
    then Radix(k) + Radix(k) > 1 + 1 by XREAL_1:8;
    then
A2: Radix(k) - 1 > 1 - Radix(k) by XREAL_1:21;
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) < -2 by XREAL_1:24;
    then
A5: -Radix(k) + 1 < -2 + 1 by XREAL_1:6;
    -Radix(k) + 1 is Element of INT by INT_1:def 2;
    then
A6: -Radix(k) + 1 in k-SD by A3,A2;
A7: 1 is Element of INT by INT_1:def 2;
    Radix(k)+ -1 > 2 + -1 by A4,XREAL_1:6;
    then 1 in k-SD by A3,A5,A7;
    hence thesis by A6,RADIX_1:14;
  end;
  consistency;
end;

definition
  let n,m,k be Nat;
  func FSDMin(n,m,k) -> Tuple of n,k-SD means
  :Def11:
  for i be Nat st i in Seg n holds DigA(it,i) = FSDMinDigit(m,k,i);
  existence
  proof
    deffunc F(Nat) = FSDMinDigit(m,k,$1);
    consider z being FinSequence of k-SD such that
A1: len z = n and
A2: for j be Nat st j in dom z holds z.j = F(j) from FINSEQ_2:sch 1;
A3: dom z = Seg n by A1,FINSEQ_1:def 3;
        z is Element of n-tuples_on (k-SD) by A1,FINSEQ_2:92;
    then reconsider z as Tuple of n,(k-SD);
    take z;
    let i be Nat;
    assume
A4: i in Seg n;
    then DigA(z,i) = z.i by RADIX_1:def 3;
    hence thesis by A2,A3,A4;
  end;
  uniqueness
  proof
    let k1,k2 be Tuple of n,k-SD such that
A5: for i be Nat st i in Seg n holds DigA(k1,i) = FSDMinDigit(m,k,i) and
A6: for i be Nat st i in Seg n holds DigA(k2,i) = FSDMinDigit(m,k,i);
A7: len k1 = n by CARD_1:def 7;
    then
A8: dom k1 = Seg n by FINSEQ_1:def 3;
A9: now
      let j be Nat;
      assume
A10:  j in dom k1;
      then k1.j = DigA(k1,j) by A8,RADIX_1:def 3
        .= FSDMinDigit(m,k,j) by A5,A8,A10
        .= DigA(k2,j) by A6,A8,A10
        .= k2.j by A8,A10,RADIX_1:def 3;
      hence k1.j = k2.j;
    end;
    len k2 = n by CARD_1:def 7;
    hence k1 = k2 by A7,A9,FINSEQ_2:9;
  end;
end;

theorem Th19:
  for n be Nat st n >= 1 holds for m,k be Nat st m in Seg n & k >=
  2 holds SDDec(FSDMin(n,m,k)) = 1
proof
  let n be Nat;
  assume
A1: n >= 1;
  let m,k be Nat;
  assume that
A2: m in Seg n and
A3: k >= 2;
  for i be Nat st i in Seg n holds DigA(FSDMin(n,m,k),i) = DigA(Fmin(n,m,k
),i) & DigA(SDMin(n,m,k),i) = 0 or DigA(FSDMin(n,m,k),i) = DigA(SDMin(n,m,k),i)
  & DigA(Fmin(n,m,k),i) = 0
  proof
    let i be Nat;
    assume
A4: i in Seg n;
    then
A5: i >= 1 by FINSEQ_1:1;
    now
      per cases;
      suppose
A6:     i > m;
A7:     DigA(Fmin(n,m,k),i) = FminDigit(m,k,i) by A4,RADIX_5:def 6
          .= 0 by A3,A6,RADIX_5:def 5;
A8:     DigA(SDMin(n,m,k),i) = SDMinDigit(m,k,i) by A4,RADIX_5:def 2
          .= 0 by A3,A6,RADIX_5:def 1;
        DigA(FSDMin(n,m,k),i) = FSDMinDigit(m,k,i) by A4,Def11
          .= 0 by A3,A6,Def10;
        hence thesis by A8,A7;
      end;
      suppose
A9:     i <= m;
        now
          per cases by A9,XXREAL_0:1;
          suppose
A10:        i = m;
A11:        DigA(Fmin(n,m,k),i) = FminDigit(m,k,i) by A4,RADIX_5:def 6
              .= 1 by A3,A10,RADIX_5:def 5;
A12:        DigA(SDMin(n,m,k),i) = SDMinDigit(m,k,i) by A4,RADIX_5:def 2
              .= 0 by A3,A10,RADIX_5:def 1;
            DigA(FSDMin(n,m,k),i) = FSDMinDigit(m,k,i) by A4,Def11
              .= 1 by A3,A10,Def10;
            hence thesis by A12,A11;
          end;
          suppose
A13:        i < m;
A14:        DigA(Fmin(n,m,k),i) = FminDigit(m,k,i) by A4,RADIX_5:def 6
              .= 0 by A3,A13,RADIX_5:def 5;
A15:        DigA(SDMin(n,m,k),i) = SDMinDigit(m,k,i) by A4,RADIX_5:def 2
              .= -Radix(k) + 1 by A3,A5,A13,RADIX_5:def 1;
            DigA(FSDMin(n,m,k),i) = FSDMinDigit(m,k,i) by A4,Def11
              .= -Radix(k) + 1 by A3,A13,Def10;
            hence thesis by A15,A14;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  then
  SDDec(FSDMin(n,m,k)) + SDDec(DecSD(0,n,k)) = SDDec(Fmin(n,m,k)) + SDDec
  ( SDMin(n,m,k)) by A1,A3,RADIX_5:15;
  then SDDec(FSDMin(n,m,k)) + 0 = SDDec(Fmin(n,m,k)) + SDDec(SDMin(n,m,k)) by
A1,RADIX_5:6
    .= SDDec(SDMax(n,m,k)) + SDDec(DecSD(1,n,k)) + SDDec(SDMin(n,m,k)) by A1,A2
,A3,RADIX_5:18
    .= (SDDec(SDMax(n,m,k)) + SDDec(SDMin(n,m,k))) + SDDec(DecSD(1,n,k))
    .= SDDec(DecSD(0,n,k)) + SDDec(DecSD(1,n,k)) by A1,A3,RADIX_5:17
    .= 0 + SDDec(DecSD(1,n,k)) by A1,RADIX_5:6;
  hence thesis by A1,A3,RADIX_5:9;
end;

definition
  let n,m,k be Nat, r be Tuple of m+2,k-SD;
  pred r is_Zero_over n means
  :Def12:
  for i be Nat st i > n holds DigA(r,i) = 0;
end;

theorem
  for m be Nat st m >= 1 holds for n,k be Nat, r be Tuple of m+2,k-SD st
k >= 2 & n in Seg (m+2) & Mmask(r) is_Zero_over n & DigA(Mmask(r),n) > 0 holds
  SDDec(Mmask(r)) > 0
proof
  let m be Nat;
  assume m >= 1;
  then
A1: m+2 >= 1 by Lm1;
  let n,k be Nat, r be Tuple of m+2,k-SD;
  assume that
A2: k >= 2 and
A3: n in Seg (m+2) and
A4: Mmask(r) is_Zero_over n and
A5: DigA(Mmask(r),n)> 0;
  for i be Nat st i in Seg (m+2) holds DigA(Mmask(r),i) >= DigA(FSDMin(m+2
  ,n,k),i)
  proof
    let i be Nat;
    assume
A6: i in Seg (m+2);
    now
      per cases;
      suppose
A7:     i > n;
        DigA(FSDMin(m+2,n,k),i) = FSDMinDigit(n,k,i) by A6,Def11
          .= 0 by A2,A7,Def10;
        hence thesis by A4,A7,Def12;
      end;
      suppose
A8:     i <= n;
        now
          per cases by A8,XXREAL_0:1;
          suppose
A9:         i = n;
            then
A10:        DigA(Mmask(r),i) >= 0 + 1 by A5,INT_1:7;
            DigA(FSDMin(m+2,n,k),i) = FSDMinDigit(n,k,i) by A6,Def11
              .= 1 by A2,A9,Def10;
            hence thesis by A10;
          end;
          suppose
A11:        i < n;
A12:        DigA(Mmask(r),i) = Mmask(r).i by A6,RADIX_1:def 3;
A13:        Mmask(r).i is Element of k-SD by A6,RADIX_1:15;
            DigA(FSDMin(m+2,n,k),i) = FSDMinDigit(n,k,i) by A6,Def11
              .= -Radix(k) + 1 by A2,A11,Def10;
            hence thesis by A12,A13,RADIX_1:13;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  then SDDec(Mmask(r)) >= SDDec(FSDMin(m+2,n,k)) by A1,RADIX_5:13;
  hence thesis by A2,A3,A1,Th19;
end;