:: High Speed Modulo Calculation Algorithm with Radix-$2^k$ SD Number
:: by Masaaki Niimura and Yasushi Fuwa
::
:: Received November 7, 2003
:: Copyright (c) 2003-2026 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, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, INT_1, 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, RELSET_1;
registrations RELSET_1, XREAL_0, NAT_1, INT_1, ORDINAL1, NEWTON, 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
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;
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;
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;
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;
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;
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;
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
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;
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;