:: High-speed algorithms for RSA cryptograms
:: by Yasushi Fuwa and Yoshinori Fujisawa
::
:: Received February 1, 2000
:: Copyright (c) 2000-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, INT_1, CARD_1, RELAT_1, ARYTM_3, XXREAL_0,
ARYTM_1, NEWTON, FINSEQ_1, RADIX_1, POWER, FINSEQ_2, PARTFUN1, FUNCT_1,
CARD_3, ORDINAL4, SUBSET_1, TARSKI, REAL_1, RADIX_2, FUNCT_7;
notations TARSKI, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, INT_1,
NAT_1, NAT_D, FUNCT_1, POWER, PARTFUN1, FINSEQ_1, FINSEQ_2, NEWTON,
RVSUM_1, GR_CY_1, WSIERP_1, RADIX_1, SUBSET_1, RECDEF_1;
constructors REAL_1, NAT_D, NEWTON, POWER, BINARITH, WSIERP_1, GR_CY_1,
RADIX_1, RECDEF_1, NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, INT_1,
MEMBERED, NEWTON, VALUED_0, FINSEQ_2, FINSEQ_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
theorems NAT_1, NAT_2, INT_1, FINSEQ_1, PREPOWER, POWER, RVSUM_1, FINSEQ_2,
TARSKI, FUNCT_1, PEPIN, RADIX_1, EULER_2, NEWTON, INT_2, XCMPLX_1,
XREAL_1, XXREAL_0, XREAL_0, NAT_D, ORDINAL1, PARTFUN1, CARD_1;
schemes NAT_1, FINSEQ_2, RECDEF_1;
begin :: Some Useful Theorems
reserve k for Nat;
theorem
for a be Nat holds a mod 1 = 0
proof
let a be Nat;
a = 1 * a + 0;
thus thesis;
end;
theorem Th2:
for a,b be Integer, n be Nat holds
((a mod n)+(b mod n)) mod n = (a + (b mod n)) mod n
proof
let a,b be Integer;
let n be Nat;
per cases;
suppose
0 < n;
then a mod n + (a div n)*n = (a-(a div n)*n) + (a div n)*n by INT_1:def 10
.= a+0;
then n divides (a + (b mod n))-((a mod n)+(b mod n)) by INT_1:def 3;
then (a + (b mod n)),((a mod n)+(b mod n)) are_congruent_mod n by INT_2:15;
hence thesis by NAT_D:64;
end;
suppose
A1: n = 0;
hence ((a mod n)+(b mod n)) mod n = 0
.= (a + (b mod n)) mod n by A1;
end;
end;
theorem Th3:
for a,b be Integer, n be Nat holds (a*b) mod n = (a*(b mod n)) mod n
proof
let a,b be Integer;
let n be Nat;
per cases;
suppose n > 0;
then b mod n + (b div n)*n = (b-(b div n)*n) + (b div n)*n by INT_1:def 10
.= b+0;
then (a*b)-(a*(b mod n)) = (a*(b div n))*n;
then n divides ((a*b)-(a*(b mod n))) by INT_1:def 3;
then (a*b),(a*(b mod n)) are_congruent_mod n by INT_2:15;
hence thesis by NAT_D:64;
end;
suppose
A1: n = 0;
hence (a*b) mod n = 0
.= (a*(b mod n)) mod n by A1;
end;
end;
theorem Th4:
for a,b,i be Nat st 1 <= i & 0 < b holds
(a mod (b |^ i)) div (b |^ (i -'1)) = (a div (b |^ (i -'1))) mod b
proof
let a,b,i be Nat;
assume that
A1: 1 <= i and
A2: 0 < b;
set j = i -' 1;
set B0 = b |^ j;
A3: B0 > 0 by A2,PREPOWER:6;
set B1 = b |^ (j+1);
A4: a mod B1 = a - (B1)*(a div B1) by A2,NEWTON:63,PREPOWER:6;
reconsider Z = (b*(-(a div B1))) as Integer;
j + 1 = i - 1 + 1 by A1,XREAL_1:233
.= i;
then
(a mod (b |^ i)) div (b |^ (i-'1)) = (a + (B1)*(-(a div B1))) div B0 by A4
.= (a + (B0)*b*(-(a div B1))) div B0 by NEWTON:6
.= [\ (a + (B0)*Z)/B0 /] by INT_1:def 9
.= [\ a/B0 + Z /] by A3,XCMPLX_1:113
.= [\ a/B0 /] + Z by INT_1:28
.= (a div B0) + -b*(a div B1) by INT_1:def 9
.= (a div B0) - b*(a div B1)
.= (a div B0) - b*(a div B0*b) by NEWTON:6
.= (a div B0) - b*((a div B0) div b) by NAT_2:27;
hence thesis by A2,NEWTON:63;
end;
theorem Th5:
for i,n be Nat st i in Seg n holds i+1 in Seg (n+1)
proof
let i,n be Nat;
assume
A1: i in Seg n;
then 1 <= i by FINSEQ_1:1;
then 1+1 <= i+1 by XREAL_1:6;
then
A2: 1 <= i+1 by XXREAL_0:2;
i <= n by A1,FINSEQ_1:1;
then i+1 <= n+1 by XREAL_1:6;
hence thesis by A2,FINSEQ_1:1;
end;
begin :: Properties of Addition operation using radix-2^k SD numbers
theorem Th6:
for k be Nat holds Radix(k) > 0
proof
let k be Nat;
Radix(k) = 2 to_power k by RADIX_1:def 1;
hence thesis by POWER:34;
end;
theorem Th7:
for x be Tuple of 1,k-SD holds SDDec(x) = DigA(x,1)
proof
1 - 1 = 0;
then
A1: 1 -' 1 = 0 by XREAL_0:def 2;
let x be Tuple of 1,k-SD;
A2: 1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A3: (DigitSD(x))/.1 = SubDigit(x,1,k) by RADIX_1:def 6;
A4: len (DigitSD(x)) = 1 by CARD_1:def 7;
then 1 in dom DigitSD(x) by A2,FINSEQ_1:def 3;
then
A5: DigitSD(x).1 = SubDigit(x,1,k) by A3,PARTFUN1:def 6;
thus SDDec(x) = Sum DigitSD(x) by RADIX_1:def 7
.= Sum <*SubDigit(x,1,k)*> by A4,A5,FINSEQ_1:40
.= SubDigit(x,1,k) by RVSUM_1:73
.= (Radix(k) |^ 0)*DigB(x,1) by A1,RADIX_1:def 5
.= 1*DigB(x,1) by NEWTON:4
.= DigA(x,1) by RADIX_1:def 4;
end;
theorem Th8:
for x be Integer holds SD_Add_Data(x,k) + SD_Add_Carry(x)*Radix(k ) = x
proof
let x be Integer;
SD_Add_Data(x,k) + SD_Add_Carry(x)*Radix(k) = x - SD_Add_Carry(x)*Radix(
k) + SD_Add_Carry(x)*Radix(k) by RADIX_1:def 11;
hence thesis;
end;
theorem Th9:
for n be Nat for x be Tuple of (n+1),k-SD, xn be Tuple of n,k-SD
st (for i be Nat st i in Seg n holds x.i = xn.i) holds Sum DigitSD(x) = Sum(
DigitSD(xn)^<*SubDigit(x,n+1,k)*>)
proof
let n be Nat;
let x be Tuple of (n+1),k-SD, xn be Tuple of n,k-SD;
A1: len DigitSD(x) = n+1 by CARD_1:def 7;
assume
A2: for i be Nat st i in Seg n holds x.i = xn.i;
A3: for i be Element of NAT st i in Seg n holds DigA(x,i) = DigA(xn,i)
proof
let i be Element of NAT;
assume
A4: i in Seg n;
then i in Seg (n+1) by FINSEQ_2:8;
then DigA(x,i) = x.i by RADIX_1:def 3
.= xn.i by A2,A4;
hence thesis by A4,RADIX_1:def 3;
end;
A5: len DigitSD(xn) = n by CARD_1:def 7;
A6: for i be Nat st 1 <= i & i <= len DigitSD(x) holds (DigitSD(x)).i = ((
DigitSD(xn))^<*SubDigit(x,n+1,k)*>).i
proof
let i be Nat;
assume that
A7: 1 <= i and
A8: i <= len DigitSD(x);
A9: n+1 in Seg(n+1) by FINSEQ_1:3;
i <= n+1 by A8,CARD_1:def 7;
then
A10: i in Seg (n+1) by A7,FINSEQ_1:1;
now
per cases by A10,FINSEQ_2:7;
suppose
A11: i in Seg n;
then
A12: i in Seg (n+1) by FINSEQ_2:8;
then
A13: i in dom DigitSD(x) by A1,FINSEQ_1:def 3;
A14: i in dom DigitSD(xn) by A5,A11,FINSEQ_1:def 3;
then ((DigitSD(xn))^<*SubDigit(x,n+1,k)*>).i = DigitSD(xn).i by
FINSEQ_1:def 7
.= (DigitSD(xn))/.i by A14,PARTFUN1:def 6
.= SubDigit(xn,i,k) by A11,RADIX_1:def 6
.= (Radix(k) |^ (i -'1))*DigB(xn,i) by RADIX_1:def 5
.= (Radix(k) |^ (i -'1))*DigA(xn,i) by RADIX_1:def 4
.= (Radix(k) |^ (i -'1))*DigA(x,i) by A3,A11
.= (Radix(k) |^ (i -'1))*DigB(x,i) by RADIX_1:def 4
.= SubDigit(x,i,k) by RADIX_1:def 5
.= (DigitSD(x))/.i by A12,RADIX_1:def 6;
hence thesis by A13,PARTFUN1:def 6;
end;
suppose
A15: i = n+1;
then
A16: i in dom DigitSD(x) by A1,A9,FINSEQ_1:def 3;
((DigitSD(xn))^<*SubDigit(x,n+1,k)*>).i = ((DigitSD(xn))^<*
SubDigit(x,n+1,k)*>).((len (DigitSD(xn)))+1) by A15,CARD_1:def 7
.= SubDigit(x,n+1,k) by FINSEQ_1:42
.= (DigitSD(x))/.(n+1) by A9,RADIX_1:def 6
.= DigitSD(x).(n+1) by A15,A16,PARTFUN1:def 6;
hence thesis by A15;
end;
end;
hence thesis;
end;
A17: len <*SubDigit(x,n+1,k)*> = 1 by FINSEQ_1:39;
len (DigitSD(xn)^<*SubDigit(x,n+1,k)*>) = len DigitSD(xn) + len <*
SubDigit(x,n+1,k)*> by FINSEQ_1:22
.= n+1 by A17,CARD_1:def 7;
then len DigitSD(x) = len (DigitSD(xn)^<*SubDigit(x,n+1,k)*>) by CARD_1:def 7
;
hence thesis by A6,FINSEQ_1:14;
end;
theorem Th10:
for n be Nat for x be Tuple of (n+1),k-SD, xn be Tuple of n,k-SD
st (for i be Nat st i in Seg n holds x.i = xn.i) holds SDDec(xn) + (Radix(k) |^
n)*DigA(x,n+1) = SDDec(x)
proof
let n be Nat;
let x be Tuple of (n+1),k-SD, xn be Tuple of n,k-SD;
assume
A1: for i be Nat st i in Seg n holds x.i = xn.i;
SDDec(x) = Sum DigitSD(x) by RADIX_1:def 7
.= Sum(DigitSD(xn)^<*SubDigit(x,n+1,k)*>) by A1,Th9
.= Sum DigitSD(xn) + SubDigit(x,n+1,k) by RVSUM_1:74
.= Sum DigitSD(xn) + (Radix(k) |^ (n+1-'1))*DigB(x,n+1) by RADIX_1:def 5
.= Sum DigitSD(xn) + (Radix(k) |^ n)*DigB(x,n+1) by NAT_D:34
.= Sum DigitSD(xn) + (Radix(k) |^ n)*DigA(x,n+1) by RADIX_1:def 4;
hence thesis by RADIX_1:def 7;
end;
theorem
for n be Nat st n >= 1 holds for x,y be Tuple of n,k-SD st k >= 2
holds SDDec(x '+' y) + SD_Add_Carry(DigA(x,n) + DigA(y,n)) *(Radix(k) |^ n) =
SDDec(x) + SDDec(y)
proof
defpred PP[Nat] means for x,y be Tuple of $1,k-SD st k >= 2 holds SDDec(x
'+' y) + SD_Add_Carry(DigA(x,$1)+DigA(y,$1))*(Radix(k) |^ $1) = SDDec(x) +
SDDec(y);
A1: for n be Nat st n >= 1 & PP[n] holds PP[n+1]
proof
let n be Nat;
assume that
A2: n >= 1 and
A3: PP[n];
A4: n in Seg n by A2,FINSEQ_1:3;
let x,y be Tuple of (n+1),k-SD;
assume
A5: k >= 2;
deffunc F(Nat) = DigB(x,$1);
consider xn being FinSequence of INT such that
A6: len xn = n and
A7: for i be Nat st i in dom xn holds xn.i = F(i) from FINSEQ_2:sch 1;
A8: dom xn = Seg n by A6,FINSEQ_1:def 3;
rng xn c= k-SD
proof
let z be object;
assume z in rng xn;
then consider xx be object such that
A9: xx in dom xn and
A10: z = xn.xx by FUNCT_1:def 3;
reconsider xx as Element of NAT by A9;
dom xn = Seg n by A6,FINSEQ_1:def 3;
then xx in Seg (n+1) by A9,FINSEQ_2:8;
then
A11: DigA(x,xx) is Element of k-SD by RADIX_1:16;
z = DigB(x,xx) by A7,A9,A10
.= DigA(x,xx) by RADIX_1:def 4;
hence thesis by A11;
end;
then reconsider xn as FinSequence of k-SD by FINSEQ_1:def 4;
A12: for i be Nat st i in Seg n holds xn.i = x.i
proof
let i be Nat;
assume
A13: i in Seg n;
then
A14: i in Seg (n+1) by FINSEQ_2:8;
xn.i = DigB(x,i) by A7,A8,A13
.= DigA(x,i) by RADIX_1:def 4;
hence thesis by A14,RADIX_1:def 3;
end;
reconsider xn as Tuple of n,(k-SD) by A6,CARD_1:def 7;
deffunc F(Nat)=DigB(y,$1);
consider yn being FinSequence of INT such that
A15: len yn = n and
A16: for i be Nat st i in dom yn holds yn.i = F(i) from FINSEQ_2:sch 1;
A17: dom yn = Seg n by A15,FINSEQ_1:def 3;
rng yn c= k-SD
proof
let z be object;
assume z in rng yn;
then consider yy be object such that
A18: yy in dom yn and
A19: z = yn.yy by FUNCT_1:def 3;
reconsider yy as Element of NAT by A18;
dom yn = Seg n by A15,FINSEQ_1:def 3;
then yy in Seg (n+1) by A18,FINSEQ_2:8;
then
A20: DigA(y,yy) is Element of k-SD by RADIX_1:16;
z = DigB(y,yy) by A16,A18,A19
.= DigA(y,yy) by RADIX_1:def 4;
hence thesis by A20;
end;
then reconsider yn as FinSequence of k-SD by FINSEQ_1:def 4;
A21: for i be Nat st i in Seg n holds yn.i = y.i
proof
let i be Nat;
assume
A22: i in Seg n;
then
A23: i in Seg (n+1) by FINSEQ_2:8;
yn.i = DigB(y,i) by A16,A17,A22
.= DigA(y,i) by RADIX_1:def 4;
hence thesis by A23,RADIX_1:def 3;
end;
reconsider yn as Tuple of n,(k-SD) by A15,CARD_1:def 7;
A24: for i be Nat st i in Seg n holds DigA(y,i) = DigA(yn,i)
proof
let i be Nat;
assume
A25: i in Seg n;
then i in Seg (n+1) by FINSEQ_2:8;
then DigA(y,i) = y.i by RADIX_1:def 3
.= yn.i by A21,A25;
hence thesis by A25,RADIX_1:def 3;
end;
A26: n+1 in Seg (n+1) by FINSEQ_1:3;
A27: for i be Element of NAT st i in Seg n holds DigA(x,i) = DigA(xn,i)
proof
let i be Element of NAT;
assume
A28: i in Seg n;
then i in Seg (n+1) by FINSEQ_2:8;
then DigA(x,i) = x.i by RADIX_1:def 3
.= xn.i by A12,A28;
hence thesis by A28,RADIX_1:def 3;
end;
for i be Nat st i in Seg n holds (x '+' y).i = (xn '+' yn).i
proof
let i be Nat;
assume
A29: i in Seg n;
then
A30: i in Seg (n+1) by FINSEQ_2:8;
(x '+' y).i = (xn '+' yn).i
proof
A31: i <= n+1 by A30,FINSEQ_1:1;
A32: i >= 1 by A29,FINSEQ_1:1;
now
per cases by A32,XXREAL_0:1;
suppose
A33: i > 1;
then i - 1 > 1 - 1 by XREAL_1:9;
then
A34: i -'1 = i - 1 by XREAL_0:def 2;
i -'1 > 1 -'1 by A33,NAT_D:57;
then
A35: i -'1 >= 1 by NAT_1:14;
i - 1 <= n + 1 - 1 by A31,XREAL_1:9;
then
A36: i -'1 in Seg n by A35,A34,FINSEQ_1:1;
(x '+' y).i = DigA(x '+' y,i) by A30,RADIX_1:def 3
.= Add(x,y,i,k) by A30,RADIX_1:def 14
.= SD_Add_Data(DigA(x,i)+DigA(y,i),k) + SD_Add_Carry(DigA(x,i
-'1)+DigA(y,i -'1)) by A5,A30,RADIX_1:def 13
.= SD_Add_Data(DigA(xn,i)+DigA(y,i),k) + SD_Add_Carry(DigA(x,i
-'1)+DigA(y,i -'1)) by A27,A29
.= SD_Add_Data(DigA(xn,i)+DigA(y,i),k) + SD_Add_Carry(DigA(xn,
i -'1)+DigA(y,i -'1)) by A27,A36
.= SD_Add_Data(DigA(xn,i)+DigA(yn,i),k) + SD_Add_Carry(DigA(xn
,i -'1)+DigA(y,i -'1)) by A24,A29
.= SD_Add_Data(DigA(xn,i)+DigA(yn,i),k) + SD_Add_Carry(DigA(xn
,i -'1)+DigA(yn,i -'1)) by A24,A36
.= Add(xn,yn,i,k) by A5,A29,RADIX_1:def 13
.= DigA(xn '+' yn,i) by A29,RADIX_1:def 14;
hence thesis by A29,RADIX_1:def 3;
end;
suppose
A37: i = 1;
(x '+' y).i = DigA(x '+' y,i) by A30,RADIX_1:def 3
.= Add(x,y,i,k) by A30,RADIX_1:def 14
.= SD_Add_Data(DigA(x,i)+DigA(y,i),k) + SD_Add_Carry(DigA(x,1
-'1)+DigA(y,1 -'1)) by A5,A30,A37,RADIX_1:def 13
.= SD_Add_Data(DigA(x,i)+DigA(y,i),k) + SD_Add_Carry(DigA(x,0)
+DigA(y,1 -'1)) by XREAL_1:232
.= SD_Add_Data(DigA(x,i)+DigA(y,i),k) + SD_Add_Carry(DigA(x,0)
+DigA(y,0)) by XREAL_1:232
.= SD_Add_Data(DigA(x,i)+DigA(y,i),k) + SD_Add_Carry(0+DigA(y,
0)) by RADIX_1:def 3
.= SD_Add_Data(DigA(x,i)+DigA(y,i),k) + SD_Add_Carry(0+0) by
RADIX_1:def 3
.= SD_Add_Data(DigA(x,i)+DigA(y,i),k) + SD_Add_Carry(DigA(xn,0
)+0) by RADIX_1:def 3
.= SD_Add_Data(DigA(x,i)+DigA(y,i),k) + SD_Add_Carry(DigA(xn,0
)+DigA(yn,0)) by RADIX_1:def 3
.= SD_Add_Data(DigA(xn,i)+DigA(y,i),k) + SD_Add_Carry(DigA(xn,
0)+DigA(yn,0)) by A27,A29
.= SD_Add_Data(DigA(xn,i)+DigA(yn,i),k) + SD_Add_Carry(DigA(xn
,0)+DigA(yn,0)) by A24,A29
.= SD_Add_Data(DigA(xn,i)+DigA(yn,i),k) + SD_Add_Carry(DigA(xn
,1-'1)+DigA(yn,0)) by XREAL_1:232
.= SD_Add_Data(DigA(xn,i)+DigA(yn,i),k) + SD_Add_Carry(DigA(xn
,i-'1)+DigA(yn,i-'1)) by A37,XREAL_1:232
.= Add(xn,yn,i,k) by A5,A29,RADIX_1:def 13
.= DigA(xn '+' yn,i) by A29,RADIX_1:def 14;
hence thesis by A29,RADIX_1:def 3;
end;
end;
hence thesis;
end;
hence thesis;
end;
then
Sum DigitSD(x '+' y) = Sum(DigitSD(xn '+' yn) ^ <*SubDigit(x '+' y,n+
1,k) *>) by Th9;
then SDDec(x '+' y) = Sum(DigitSD(xn '+' yn)^<*SubDigit(x '+' y,n+1,k)*>)
by RADIX_1:def 7
.= Sum DigitSD(xn '+' yn) + SubDigit(x '+' y,n+1,k) by RVSUM_1:74
.= Sum DigitSD(xn '+' yn) + (Radix(k) |^ (n+1-'1)*DigB(x '+' y,n+1))
by RADIX_1:def 5
.= Sum DigitSD(xn '+' yn) + (Radix(k) |^ n)*DigB(x '+' y,n+1) by NAT_D:34
.= Sum DigitSD(xn '+' yn) + (Radix(k) |^ n)*DigA(x '+' y,n+1) by
RADIX_1:def 4
.= Sum DigitSD(xn '+' yn) + (Radix(k) |^ n)*Add(x,y,n+1,k) by A26,
RADIX_1:def 14
.= Sum DigitSD(xn '+' yn) + (Radix(k) |^ n)* (SD_Add_Data(DigA(x,n+1)+
DigA(y,n+1),k) + SD_Add_Carry(DigA(x,n+1-'1)+DigA(y,n+1-'1))) by A5,A26,
RADIX_1:def 13
.= Sum DigitSD(xn '+' yn) + (Radix(k) |^ n)* (SD_Add_Data(DigA(x,n+1)+
DigA(y,n+1),k) + SD_Add_Carry(DigA(x,n)+DigA(y,n+1-'1))) by NAT_D:34
.= Sum DigitSD(xn '+' yn) + (Radix(k) |^ n)* (SD_Add_Data(DigA(x,n+1)+
DigA(y,n+1),k) + SD_Add_Carry(DigA(x,n)+DigA(y,n))) by NAT_D:34
.= Sum DigitSD(xn '+' yn) + (Radix(k) |^ n)*SD_Add_Carry(DigA(x,n)+
DigA(y,n)) + (Radix(k) |^ n)*SD_Add_Data(DigA(x,n+1)+DigA(y,n+1),k)
.= SDDec(xn '+' yn) + (Radix(k) |^ n)*SD_Add_Carry(DigA(x,n)+DigA(y,n)
) + (Radix(k) |^ n)*SD_Add_Data(DigA(x,n+1)+DigA(y,n+1),k) by RADIX_1:def 7
.= SDDec(xn '+' yn) + (Radix(k) |^ n)*SD_Add_Carry(DigA(xn,n)+DigA(y,n
)) + (Radix(k) |^ n)*SD_Add_Data(DigA(x,n+1)+DigA(y,n+1),k) by A27,A4
.= SDDec(xn '+' yn) + (Radix(k) |^ n)*SD_Add_Carry(DigA(xn,n)+DigA(yn,
n)) + (Radix(k) |^ n)*SD_Add_Data(DigA(x,n+1)+DigA(y,n+1),k) by A2,A24,
FINSEQ_1:3
.= SDDec(xn) + SDDec(yn) + (Radix(k) |^ n)*SD_Add_Data(DigA(x,n+1)+
DigA(y,n+1),k) by A3,A5;
then
SDDec(x '+' y) + SD_Add_Carry(DigA(x,n+1)+DigA(y,n+1))*(Radix(k) |^ (
n+1)) = SDDec(xn) + SDDec(yn) + ((Radix(k) |^ n)*SD_Add_Data(DigA(x,n+1)+DigA(y
,n+1),k) + SD_Add_Carry(DigA(x,n+1)+DigA(y,n+1))*(Radix(k) |^ (n+1)))
.= SDDec(xn) + SDDec(yn) + ((Radix(k) |^ n)*SD_Add_Data(DigA(x,n+1)+
DigA(y,n+1),k) + SD_Add_Carry(DigA(x,n+1)+DigA(y,n+1))*((Radix(k) |^ n)*Radix(k
))) by NEWTON:6
.= SDDec(xn) + SDDec(yn) + ((Radix(k) |^ n) *(SD_Add_Data(DigA(x,n+1)+
DigA(y,n+1),k) + (SD_Add_Carry(DigA(x,n+1)+DigA(y,n+1))*Radix(k))))
.= SDDec(xn) + SDDec(yn) + ((Radix(k) |^ n)*(DigA(x,n+1) + DigA(y,n+1)
)) by Th8
.= (SDDec(xn) + (Radix(k) |^ n)*DigA(x,n+1)) + (SDDec(yn) + (Radix(k)
|^ n)*DigA(y,n+1))
.= SDDec(x) + (SDDec(yn) + (Radix(k) |^ n)*DigA(y,n+1)) by A12,Th10;
hence thesis by A21,Th10;
end;
A38: PP[1]
proof
1 - 1 = 0;
then
A39: 1 -' 1 = 0 by XREAL_0:def 2;
let x,y be Tuple of 1,k-SD;
assume
A40: k >= 2;
A41: SDDec(y) = DigA(y,1) & SD_Add_Data(DigA(x,1) + DigA(y,1),k) = DigA(x,1
) + DigA(y,1) - SD_Add_Carry(DigA(x,1)+DigA(y,1))*Radix(k) by Th7,
RADIX_1:def 11;
A42: 1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then DigA(x '+' y,1) = Add(x,y,1,k) by RADIX_1:def 14
.= SD_Add_Data(DigA(x,1)+DigA(y,1),k) + SD_Add_Carry(DigA(x,0)+DigA(y,
0)) by A40,A42,A39,RADIX_1:def 13
.= SD_Add_Data(DigA(x,1)+DigA(y,1),k) + SD_Add_Carry(0+DigA(y,0)) by
RADIX_1:def 3
.= SD_Add_Data(DigA(x,1)+DigA(y,1),k) + 0 by RADIX_1:18,def 3;
then SDDec(x '+' y) = SD_Add_Data(DigA(x,1)+DigA(y,1),k) by Th7;
hence SDDec(x '+' y) + SD_Add_Carry(DigA(x,1)+DigA(y,1))*(Radix(k) |^ 1) =
SD_Add_Data(DigA(x,1)+DigA(y,1),k) + SD_Add_Carry(DigA(x,1)+DigA(y,1))*Radix(k)
.= SDDec(x) + SDDec(y) by A41,Th7;
end;
for n be Nat st n >= 1 holds PP[n] from NAT_1:sch 8(A38,A1);
hence thesis;
end;
begin :: Definitions on the relation between a FinSequence of k-SD and
:: a FinSequence of NAT and some properties about them
definition
let i,k,n be Nat, x be Tuple of n,NAT;
func SubDigit2(x,i,k) -> Element of NAT equals
(Radix(k) |^ (i -'1))*(x.i);
coherence;
end;
definition
let n,k be Nat, x be Tuple of n,NAT;
func DigitSD2(x,k) -> Tuple of n,NAT means
:Def2:
for i be Nat st i in Seg n holds it/.i = SubDigit2(x,i,k);
existence
proof
deffunc F(Nat)= SubDigit2(x,$1,k);
consider z being FinSequence of NAT 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;
reconsider z as Tuple of n,NAT by A1,CARD_1:def 7;
take z;
let i be Nat;
assume
A4: i in Seg n;
then i in dom z by A1,FINSEQ_1:def 3;
hence z/.i = z.i by PARTFUN1:def 6
.= SubDigit2(x,i,k) by A2,A3,A4;
end;
uniqueness
proof
let k1,k2 be Tuple of n,NAT such that
A5: for i be Nat st i in Seg n holds k1/.i = SubDigit2(x,i,k) and
A6: for i be Nat st i in Seg n holds k2/.i = SubDigit2(x,i,k);
A7: len k1 = n by CARD_1:def 7;
then
A8: dom k1 = Seg n by FINSEQ_1:def 3;
A9: len k2 = n by CARD_1:def 7;
now
let j be Nat;
assume
A10: j in dom k1;
then
A11: j in dom k2 by A9,A8,FINSEQ_1:def 3;
k1.j = k1/.j by A10,PARTFUN1:def 6
.= SubDigit2(x,j,k) by A5,A8,A10
.= k2/.j by A6,A8,A10;
hence k1.j = k2.j by A11,PARTFUN1:def 6;
end;
hence thesis by A7,A9,FINSEQ_2:9;
end;
end;
definition
let n,k be Nat, x be Tuple of n,NAT;
func SDDec2(x,k) -> Element of NAT equals
Sum DigitSD2(x,k);
coherence;
end;
definition
let i,k,x be Nat;
func DigitDC2(x,i,k) -> Element of NAT equals
(x mod (Radix(k) |^ i)) div (
Radix(k) |^ (i -'1));
coherence;
end;
definition
let k,n,x be Nat;
func DecSD2(x,n,k) -> Tuple of n,NAT means
:Def5:
for i be Nat st i in Seg n holds it.i = DigitDC2(x,i,k);
existence
proof
deffunc F(Nat)=DigitDC2(x,$1,k);
consider z being FinSequence of NAT 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;
reconsider z as Tuple of n,NAT by A1,CARD_1:def 7;
take z;
let i be Nat;
assume i in Seg n;
hence thesis by A2,A3;
end;
uniqueness
proof
let k1,k2 be Tuple of n,NAT such that
A4: for i be Nat st i in Seg n holds k1.i = DigitDC2(x,i,k) and
A5: for i be Nat st i in Seg n holds k2.i = DigitDC2(x,i,k);
A6: len k1 = n by CARD_1:def 7;
then
A7: dom k1 = Seg n by FINSEQ_1:def 3;
A8: now
let j be Nat;
assume
A9: j in dom k1;
then k1.j = DigitDC2(x,j,k) by A4,A7;
hence k1.j = k2.j by A5,A7,A9;
end;
len k2 = n by CARD_1:def 7;
hence thesis by A6,A8,FINSEQ_2:9;
end;
end;
theorem Th12:
for n,k be Nat, x be Tuple of n,NAT, y be Tuple of n,k-SD st x = y
holds DigitSD2(x,k) = DigitSD(y)
proof
let n,k be Nat;
let x be Tuple of n,NAT;
let y be Tuple of n,k-SD;
A1: len DigitSD(y) = n by CARD_1:def 7;
A2: len DigitSD2(x,k) = n by CARD_1:def 7;
then
A3: dom DigitSD2(x,k) = Seg n by FINSEQ_1:def 3;
assume
A4: x=y;
A5: now
let i be Element of NAT;
assume i in Seg n;
then x.i = DigA(y,i) by A4,RADIX_1:def 3
.= DigB(y,i) by RADIX_1:def 4;
hence x.i = DigB(y,i);
end;
now
let j be Nat;
assume
A6: j in dom DigitSD2(x,k);
then
A7: j in dom DigitSD(y) by A1,A3,FINSEQ_1:def 3;
DigitSD2(x,k).j = (DigitSD2(x,k))/.j by A6,PARTFUN1:def 6
.= SubDigit2(x,j,k) by A3,A6,Def2
.= (Radix(k) |^ (j -'1))*DigB(y,j) by A5,A3,A6
.= SubDigit(y,j,k) by RADIX_1:def 5
.= (DigitSD(y))/.j by A3,A6,RADIX_1:def 6
.= DigitSD(y).j by A7,PARTFUN1:def 6;
hence DigitSD2(x,k).j = DigitSD(y).j;
end;
hence thesis by A2,A1,FINSEQ_2:9;
end;
theorem Th13:
for n,k be Nat, x be Tuple of n,NAT, y be Tuple of n,k-SD st x = y
holds SDDec2(x,k) = SDDec(y)
proof
let n,k be Nat;
let x be Tuple of n,NAT;
let y be Tuple of n,k-SD;
assume x = y;
then SDDec2(x,k) = Sum DigitSD(y) by Th12;
hence thesis by RADIX_1:def 7;
end;
theorem Th14:
for x,n,k be Nat holds DecSD2(x,n,k) = DecSD(x,n,k)
proof
let x,n,k be Nat;
A1: len DecSD2(x,n,k) = n by CARD_1:def 7;
then
A2: dom DecSD2(x,n,k) = Seg n by FINSEQ_1:def 3;
A3: now
let j be Nat;
assume
A4: j in dom DecSD2(x,n,k);
then DecSD2(x,n,k).j = DigitDC2(x,j,k) by A2,Def5
.= DigitDC(x,j,k) by RADIX_1:def 8
.= DigA(DecSD(x,n,k),j) by A2,A4,RADIX_1:def 9
.= DecSD(x,n,k).j by A2,A4,RADIX_1:def 3;
hence DecSD2(x,n,k).j = DecSD(x,n,k).j;
end;
len DecSD(x,n,k) = n by CARD_1:def 7;
hence thesis by A1,A3,FINSEQ_2:9;
end;
theorem Th15:
for n be Nat st n >= 1 holds for m,k be Nat st m
is_represented_by n,k holds m = SDDec2(DecSD2(m,n,k),k)
proof
let n be Nat;
assume
A1: n >= 1;
let m,k be Nat;
assume
A2: m is_represented_by n,k;
SDDec2(DecSD2(m,n,k),k) = SDDec(DecSD(m,n,k)) by Th13,Th14;
hence thesis by A1,A2,RADIX_1:22;
end;
begin :: Algorithm of calculation of (a*b) mod c based on
:: radix-2^k SD numbers and its correctness
definition
let q be Integer, f,j,k,n be Nat, c be Tuple of n,k-SD;
func Table1(q,c,f,j) -> Integer equals
(q*DigA(c,j)) mod f;
correctness;
end;
definition
let q be Integer, k,f,n be Nat, c be Tuple of n,k-SD;
assume
A1: n >= 1;
func Mul_mod(q,c,f,k) -> Tuple of n,INT means
:Def7:
it.1 = Table1(q,c,f,n)
& for i be Nat st 1 <= i & i <= n - 1 holds ex I1,I2 be Integer st I1 = it.i &
I2 = it.(i+1) & I2 = (Radix(k)*I1+Table1(q,c,f,n -'i)) mod f;
existence
proof
defpred PP[Nat,set,set] means ex i1,i2 be Integer st i1 = $2 &
i2 = $3 & i2 = (Radix(k)*i1+Table1(q,c,f,n -'$1)) mod f;
reconsider n1=n as Element of NAT by ORDINAL1:def 12;
reconsider T = Table1(q,c,f,n) as Element of INT by INT_1:def 2;
A2: for i be Nat st 1 <= i & i < n1 for x be Element of INT ex
y be Element of INT st PP[i,x,y]
proof
let i be Nat;
assume that
1 <= i and
i < n1;
let x be Element of INT;
reconsider x as Integer;
consider y be Integer such that
A3: y = (Radix(k)*x+Table1(q,c,f,n -'i)) mod f;
reconsider z = y as Element of INT by INT_1:def 2;
take z;
thus thesis by A3;
end;
consider r be FinSequence of INT such that
A4: len r = n1 & (r.1 = T or n1 = 0) and
A5: for i be Nat st 1 <= i & i < n1 holds PP[i,r.i,r.(i+1)]
from RECDEF_1:sch 4(A2);
reconsider r as Tuple of n,INT by A4,CARD_1:def 7;
take r;
thus r.1 = Table1(q,c,f,n) by A1,A4;
let i be Nat;
assume
A6: 1 <= i & i <= n - 1;
thus thesis by A5,A6,XREAL_1:147;
end;
uniqueness
proof
let s1,s2 be Tuple of n,INT such that
A7: s1.1 = Table1(q,c,f,n) and
A8: for i be Nat st 1 <= i & i <= n - 1 holds ex I1,I2 be Integer st
I1 = s1.i & I2 = s1.(i+1) & I2 = (Radix(k)*I1+Table1(q,c,f,n -'i)) mod f
and
A9: s2.1 = Table1(q,c,f,n) and
A10: for i be Nat st 1 <= i & i <= n - 1 holds ex I1,I2 be Integer st
I1 = s2.i & I2 = s2.(i+1) & I2 = (Radix(k)*I1+Table1(q,c,f,n -'i)) mod f;
defpred P[Nat] means 1 <= $1 & $1 <= n - 1 implies s1.$1 = s2.$1;
A11: for k be Nat st P[k] holds P[k+1]
proof
let kk be Nat;
assume
A12: 1 <= kk & kk <= n - 1 implies s1.kk = s2.kk;
A13: 0 = kk or 0 < kk & 0 + 1 = 1;
assume that
1 <= kk + 1 and
A14: kk + 1 <= n - 1;
per cases by A13,NAT_1:13;
suppose
0 = kk;
hence thesis by A7,A9;
end;
suppose
A15: 1 <= kk;
A16: kk <= kk + 1 by NAT_1:11;
then kk <= n - 1 by A14,XXREAL_0:2;
then ( ex I1,I2 be Integer st I1 = s1.kk & I2 = s1.(kk+1) & I2 = (
Radix(k)*I1+Table1 (q,c,f,n -'kk)) mod f)& ex i1,i2 be Integer st i1 = s2.kk &
i2 = s2.(kk+1) & i2 = (Radix(k)*i1+Table1(q,c,f,n -'kk)) mod f by A8,A10,A15;
hence thesis by A12,A14,A15,A16,XXREAL_0:2;
end;
end;
A17: len s1 = n by CARD_1:def 7;
A18: P[0];
A19: for kk be Nat holds P[kk] from NAT_1:sch 2(A18,A11);
A20: s1.n = s2.n
proof
n - 1 >= 1 - 1 by A1,XREAL_1:9;
then reconsider U1 = n - 1 as Element of NAT by INT_1:3;
now
per cases;
suppose
U1 = 0;
hence thesis by A7,A9;
end;
suppose
0 < U1;
then
A21: 1 <= U1 by NAT_1:14;
then (ex i1,i2 be Integer st i1 = s1.U1 & i2 = s1.(U1+1) & i2 = (
Radix(k)*i1+ Table1(q,c,f,n -'U1)) mod f )& ex j1,j2 be Integer st j1 = s2.U1 &
j2 = s2.( U1+1) & j2 = (Radix(k)*j1+Table1(q,c,f,n -'U1)) mod f by A8,A10;
hence thesis by A19,A21;
end;
end;
hence thesis;
end;
A22: for kk be Nat st 1 <= kk & kk <= len s1 holds s1.kk = s2.kk
proof
let kk be Nat;
assume that
A23: 1 <= kk and
A24: kk <= len s1;
now
per cases by A24,XXREAL_0:1;
suppose
A25: kk < len s1;
n - 1 >= 1 - 1 by A1,XREAL_1:9;
then reconsider U1 = len s1 - 1 as Element of NAT by A17,INT_1:3;
U1 + 1 = len s1;
then kk <= U1 by A25,NAT_1:13;
hence thesis by A17,A19,A23;
end;
suppose
kk = len s1;
hence thesis by A17,A20;
end;
end;
hence thesis;
end;
len s1 = len s2 by A17,CARD_1:def 7;
hence thesis by A22,FINSEQ_1:14;
end;
end;
theorem
for n be Nat st n >= 1 holds for q be Integer, ic,f,k be Nat st ic
is_represented_by n,k & f > 0 holds for c be Tuple of n,k-SD st c = DecSD(ic,n,
k) holds Mul_mod(q,c,f,k).n = (q * ic) mod f
proof
defpred PP[Nat] means for q be Integer, ic,f,k be Nat st ic
is_represented_by $1,k & f > 0 holds for c be Tuple of $1,k-SD st c = DecSD(ic,
$1,k) holds Mul_mod(q,c,f,k).$1 = (q * ic) mod f;
A1: for n be Nat st n >= 1 & PP[n] holds PP[n+1]
proof
let n be Nat;
assume that
A2: n >= 1 and
A3: PP[n];
let q be Integer;
let ic,f,k be Nat;
assume that
A4: ic is_represented_by (n+1),k and
A5: f > 0;
let c be Tuple of (n+1),k-SD;
deffunc F(Nat) =DigB(c,($1+1));
consider cn being FinSequence of INT such that
A6: len cn = n and
A7: for i be Nat st i in dom cn holds cn.i = F(i) from FINSEQ_2:sch 1;
A8: dom cn = Seg n by A6,FINSEQ_1:def 3;
rng cn c= k-SD
proof
let z be object;
assume z in rng cn;
then consider xx be object such that
A9: xx in dom cn and
A10: z = cn.xx by FUNCT_1:def 3;
reconsider xx as Element of NAT by A9;
dom cn = Seg n by A6,FINSEQ_1:def 3;
then xx+1 in Seg (n+1) by A9,Th5;
then
A11: DigA(c,(xx+1)) is Element of k-SD by RADIX_1:16;
z = DigB(c,(xx+1)) by A7,A9,A10
.= DigA(c,(xx+1)) by RADIX_1:def 4;
hence thesis by A11;
end;
then reconsider cn as FinSequence of k-SD by FINSEQ_1:def 4;
reconsider cn as Tuple of n,(k-SD) by A6,CARD_1:def 7;
A12: n+1 >= 1 by NAT_1:12;
set c2 = DecSD2(ic,(n+1),k);
A13: Radix(k) > 0 by Th6;
deffunc F(Nat) = c2.($1+1);
consider cn2 being FinSequence of NAT such that
A14: len cn2 = n and
A15: for i be Nat st i in dom cn2 holds cn2.i = F(i) from FINSEQ_2:sch
1;
A16: dom cn2 = Seg n by A14,FINSEQ_1:def 3;
reconsider cn2 as Tuple of n,NAT by A14,CARD_1:def 7;
set icn2 = SDDec2(cn2,k);
A17: ic < (Radix(k) |^ (n+1)) by A4,RADIX_1:def 12;
set icn = SDDec(cn);
assume
A18: c = DecSD(ic,(n+1),k);
then
A19: c2 = c by Th14;
A20: for i be Nat st 1 <= i & i <= len cn holds cn.i = cn2.i
proof
let i be Nat;
assume 1 <= i & i <= len cn;
then
A21: i in Seg n by A6,FINSEQ_1:1;
then
A22: i+1 in Seg (n+1) by Th5;
cn.i = DigB(c,(i+1)) by A7,A8,A21
.= DigA(c,(i+1)) by RADIX_1:def 4
.= c.(i+1) by A22,RADIX_1:def 3
.= c2.(i+1) by A18,Th14;
hence thesis by A15,A16,A21;
end;
then
A23: icn = icn2 by A6,A14,Th13,FINSEQ_1:14;
1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A24: 1 in Seg (1+n) by FINSEQ_2:8;
A25: ic = Radix(k)*icn2 + c2.1
proof
A26: len <*SubDigit2(c2,1,k)*> = 1 by FINSEQ_1:39;
A27: 1 - 1 = 0;
deffunc F(Nat)=In(DigitSD2(cn2,k).$1,REAL);
reconsider r2 = Radix(k) as Element of REAL by XREAL_0:def 1;
consider rD being FinSequence of REAL such that
A28: len rD = n and
A29: for i be Nat st i in dom rD holds rD.i = F(i) from FINSEQ_2:sch 1;
A30: for i be Nat st i in dom rD holds rD.i = DigitSD2(cn2,k).i
proof let i be Nat;
assume i in dom rD;
then rD.i = F(i) by A29;
hence thesis;
end;
reconsider rD as Tuple of n,REAL by A28,CARD_1:def 7;
A31: dom DigitSD2(cn2,k) = Seg (len DigitSD2(cn2,k)) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
reconsider rD1=rD as Element of n-tuples_on REAL by FINSEQ_2:131;
A32: dom rD = Seg n by A28,FINSEQ_1:def 3;
then
A33: len (Radix(k) * DigitSD2(cn2,k)) = len (r2 * rD1) by A30,A31,FINSEQ_1:13
.= n by CARD_1:def 7;
A34: len (<*SubDigit2(c2,1,k)*> ^ (Radix(k) * DigitSD2(cn2,k))) = len <*
SubDigit2(c2,1,k)*> + len (Radix(k) * DigitSD2(cn2,k)) by FINSEQ_1:22
.= n+1 by A33,CARD_1:def 7;
A35: len DigitSD2(c2,k) = n+1 by CARD_1:def 7;
A36: for i be Nat st 1 <= i & i <= len DigitSD2(c2,k) holds DigitSD2(c2,
k).i=(<*SubDigit2(c2,1,k)*>^(Radix(k)*DigitSD2(cn2,k))).i
proof
let i be Nat;
assume that
A37: 1 <= i and
A38: i <= len DigitSD2(c2,k);
A39: i <= n+1 by A38,CARD_1:def 7;
then
A40: i in Seg (n+1) by A37,FINSEQ_1:1;
then
A41: i in dom DigitSD2(c2,k) by A35,FINSEQ_1:def 3;
per cases;
suppose
A42: i = 1;
then (<*SubDigit2(c2,1,k)*> ^ (Radix(k)*DigitSD2(cn2,k))).i =
SubDigit2(c2,1,k) by FINSEQ_1:41
.= (DigitSD2(c2,k))/.1 by A24,Def2
.= DigitSD2(c2,k).1 by A41,A42,PARTFUN1:def 6;
hence thesis by A42;
end;
suppose
A43: i <> 1;
reconsider rs2 = DigitSD2(cn2,k).(i-1) as Element of NAT;
reconsider rs = rD.(i-1) as Real;
1 - 1 <= i - 1 by A37,XREAL_1:9;
then reconsider i1 = i - 1 as Element of NAT by INT_1:3;
1 < i by A37,A43,XXREAL_0:1;
then 1 + 1 <= i by INT_1:7;
then
A44: 1 + 1 - 1 <= i - 1 by XREAL_1:9;
i - 1 <= n + 1 - 1 by A39,XREAL_1:9;
then
A45: i1 in Seg n by A44,FINSEQ_1:1;
1 < i by A37,A43,XXREAL_0:1;
then
(<*SubDigit2(c2,1,k)*> ^ (Radix(k)*DigitSD2(cn2,k))).i =(Radix(
k)*DigitSD2(cn2,k)).(i - 1) by A26,A34,A39,FINSEQ_1:24
.=(r2*rD).(i-1) by A30,A31,A32,FINSEQ_1:13
.=r2*rs by RVSUM_1:45
.=Radix(k)*rs2 by A30,A31,A32,FINSEQ_1:13
.=Radix(k)*((DigitSD2(cn2,k))/.i1) by A31,A45,PARTFUN1:def 6
.=Radix(k)*SubDigit2(cn2,i1,k) by A45,Def2
.=Radix(k)*(Radix(k) |^ (i1-'1))*(cn2.i1)
.=(Radix(k) |^ (i1-'1+1))*(cn2.i1) by NEWTON:6
.=(Radix(k) |^ i1)*(cn2.i1) by A44,XREAL_1:235
.=(Radix(k) |^ i1)*(c2.(i1+1)) by A15,A16,A45
.=SubDigit2(c2,i,k) by A37,XREAL_1:233
.=(DigitSD2(c2,k))/.i by A40,Def2;
hence thesis by A41,PARTFUN1:def 6;
end;
end;
len DigitSD2(c2,k) = len (<*SubDigit2(c2,1,k)*> ^ (Radix(k) *
DigitSD2(cn2,k))) by A34,CARD_1:def 7;
then
A46: DigitSD2(c2,k) = <*SubDigit2(c2,1,k)*>^(Radix(k)*DigitSD2(cn2,k))
by A36,FINSEQ_1:14;
ic = SDDec2(DecSD2(ic,(n+1),k),k) by A4,Th15,NAT_1:12
.= SubDigit2(c2,1,k)+ Sum(Radix(k)*DigitSD2(cn2,k)) by A46,RVSUM_1:76
.= SubDigit2(c2,1,k) + Sum(r2 * rD) by A30,A31,A32,FINSEQ_1:13
.= SubDigit2(c2,1,k) + r2 * Sum(rD) by RVSUM_1:87
.= SubDigit2(c2,1,k) + Radix(k) * icn2 by A30,A31,A32,FINSEQ_1:13
.= (Radix(k) |^ 0)*(c2.1) + Radix(k) * icn2 by A27,XREAL_0:def 2
.= 1*(c2.1) + Radix(k) * icn2 by NEWTON:4;
hence thesis;
end;
then
A47: (q * ic) mod f = (q * Radix(k)*icn2 + q * c2.1) mod f
.= (((Radix(k) *(q * icn2)) mod f) + ((q * c2.1) mod f)) mod f by
NAT_D:66
.= (((Radix(k) *((q * icn2) mod f)) mod f) + ((q * c2.1) mod f)) mod f
by Th3
.= ((Radix(k) *((q * icn2) mod f)) + ((q * c2.1) mod f)) mod f by Th2;
A48: cn = cn2 by A6,A14,A20,FINSEQ_1:14;
A49: for i be Nat st 1 <= i & i <= len cn holds cn.i=DecSD2(icn2,n,k).i
proof
A50: c2.1 = DigitDC2(ic,1,k) by A24,Def5
.= (ic mod (Radix(k) |^ 1)) div (Radix(k) |^ 0) by XREAL_1:232
.= (ic mod (Radix(k) |^ 1)) div 1 by NEWTON:4
.= ic mod (Radix(k) |^ 1)
.= ic mod Radix(k);
A51: 0 < Radix(k) by Th6;
A52: (c2.1 + icn2*Radix(k)) div Radix(k) = [\(c2.1 + icn2*Radix(k))/
Radix(k)/] by INT_1:def 9
.= [\c2.1/Radix(k) + icn2/] by A51,XCMPLX_1:113
.= [\c2.1/Radix(k)/] + icn2 by INT_1:28
.= (c2.1) div Radix(k) + icn2 by INT_1:def 9
.= 0 + icn2 by A13,A50,NAT_D:1,27;
A53: Radix(k) <> 0 by Th6;
let i be Nat;
assume that
A54: 1 <= i and
A55: i <= len cn;
A56: i in Seg n by A6,A54,A55,FINSEQ_1:1;
reconsider i as Element of NAT by ORDINAL1:def 12;
A57: 1 <= i+1 by A54,XREAL_1:29;
1 <= (i+1) & (i+1) <= (n+1) by A6,A54,A55,XREAL_1:6,29;
then
A58: (i+1) in Seg (n+1) by FINSEQ_1:1;
cn.i = c2.(i+1) by A15,A16,A48,A56
.= DigitDC2(ic,(i+1),k) by A58,Def5
.= ((icn2*Radix(k) + c2.1) div (Radix(k) |^ ((i+1)-'1))) mod Radix(k
) by A25,A57,Th4,Th6
.= ((icn2*Radix(k) + c2.1) div (Radix(k) |^ i)) mod Radix(k) by
NAT_D:34
.= ((icn2*Radix(k) + c2.1) div (Radix(k)*(Radix(k) |^ (i -'1)))) mod
Radix(k) by A54,A53,PEPIN:26
.= (icn2 div (Radix(k) |^ (i -'1))) mod Radix(k) by A52,NAT_2:27
.= DigitDC2(icn2,i,k) by A54,Th4,Th6;
hence thesis by A56,Def5;
end;
reconsider icn as Element of NAT by A23;
len cn = len DecSD2(icn2,n,k) by A6,CARD_1:def 7;
then cn = DecSD2(icn2,n,k) by A49,FINSEQ_1:14;
then
A59: cn = DecSD(icn,n,k) by A23,Th14;
ic >= Radix(k)*icn2 by A25,INT_1:6;
then icn2 * Radix(k) < (Radix(k) |^ (n+1)) by A17,XXREAL_0:2;
then icn2 * Radix(k) < (Radix(k) |^ n)* Radix(k) by NEWTON:6;
then icn < (Radix(k) |^ n) by A23,XREAL_1:64;
then
A60: icn is_represented_by n,k by RADIX_1:def 12;
A61: for i be Element of NAT st i in Seg n holds DigA(cn,i) = DigA(c,i+1)
proof
let i be Element of NAT;
assume
A62: i in Seg n;
DigA(c,i+1) = DigB(c,i+1) by RADIX_1:def 4
.= cn.i by A7,A8,A62;
hence thesis by A62,RADIX_1:def 3;
end;
A63: for i be Element of NAT st i in Seg n holds Mul_mod(q,cn,f,k).i =
Mul_mod(q,c,f,k).i
proof
defpred P[Nat] means $1 in Seg n implies Mul_mod(q,cn,f,k).$1
= Mul_mod(q,c,f,k).$1;
A64: for i be Nat st P[i] holds P[i+1]
proof
let i be Nat;
assume
A65: i in Seg n implies Mul_mod(q,cn,f,k).i = Mul_mod(q,c,f,k).i;
A66: i=0 or i+1>1+0 by XREAL_1:6;
assume (i+1) in Seg n;
then
A67: (i+1) <= n by FINSEQ_1:1;
then
A68: (i+1)-1 <= n - 1 by XREAL_1:9;
A69: n in Seg n by A2,FINSEQ_1:1;
now
per cases by A66,NAT_1:13;
case
A70: i=0;
then Mul_mod(q,cn,f,k).(i+1) = Table1(q,cn,f,n) by A2,Def7
.= Table1(q,c,f,n+1) by A61,A69
.= Mul_mod(q,c,f,k).1 by A12,Def7;
hence thesis by A70;
end;
case
A71: i>=1;
reconsider nn = n - 1 as Element of NAT by A2,INT_1:5;
A72: i <= nn + 1 by A68,NAT_1:12;
then i <= (n+1)-1;
then
A73: ex I1,I2 be Integer st I1=Mul_mod(q,c,f,k).i & I2=Mul_mod(q,c
,f,k).(i+1) & I2 = (Radix(k)*I1+Table1(q,c,f,(n+1) -' i)) mod f by A12,A71,Def7
;
A74: n -' i <= n by NAT_D:35;
1 + i - i <= n - i by A67,XREAL_1:9;
then 1 <= n -' i by A72,XREAL_1:233;
then
A75: (n -' i) in Seg n by A74,FINSEQ_1:1;
ex I1,I2 be Integer st I1=Mul_mod(q,cn,f,k).i & I2=Mul_mod(q,
cn,f,k).(i+1) & I2 = (Radix(k)*I1+Table1(q,cn,f,n -' i)) mod f by A2,A68,A71
,Def7;
then Mul_mod(q,cn,f,k).(i+1) = (Radix(k)*Mul_mod(q,c,f,k).i + (q*
DigA(c,(n -' i)+1) mod f)) mod f by A61,A65,A71,A72,A75,FINSEQ_1:1
.= Mul_mod(q,c,f,k).(i+1) by A72,A73,NAT_D:38;
hence thesis;
end;
end;
hence thesis;
end;
A76: P[0] by FINSEQ_1:1;
for i be Nat holds P[i] from NAT_1:sch 2(A76,A64);
hence thesis;
end;
n <= (n+1) - 1 & n+1 >= 1 by NAT_1:11;
then
A77: ex I1,I2 be Integer st I1=Mul_mod(q,c,f,k).n & I2=Mul_mod(q,c,f,k).(
n+1) & I2 = (Radix(k)*I1+Table1(q,c,f,(n+1) -'n)) mod f by A2,Def7;
n in Seg n by A2,FINSEQ_1:3;
then Mul_mod(q,c,f,k).(n+1) = (Radix(k)*Mul_mod(q,cn,f,k).n + Table1(q,c,
f,(n+1) -'n)) mod f by A63,A77
.= (Radix(k)*((q * icn) mod f) + Table1(q,c,f,(n+1) -'n)) mod f by A3,A5
,A60,A59
.= (Radix(k)*((q * icn2) mod f) + Table1(q,c,f,(n+1) -'n)) mod f by A6
,A14,A20,Th13,FINSEQ_1:14
.= ((Radix(k)*((q * icn2) mod f)) + ((q*DigA(c,1)) mod f)) mod f by
NAT_D:34
.= ((Radix(k)*((q * icn2) mod f)) + ((q*c2.1) mod f)) mod f by A19,A24,
RADIX_1:def 3;
hence thesis by A47;
end;
A78: PP[1]
proof
let q be Integer;
let ic,f,k be Nat;
assume that
A79: ic is_represented_by 1,k and
f > 0;
let c be Tuple of 1,k-SD;
assume
A80: c = DecSD(ic,1,k);
Mul_mod(q,c,f,k).1 = Table1(q,c,f,1) by Def7
.= (q*SDDec(DecSD(ic,1,k))) mod f by A80,Th7;
hence thesis by A79,RADIX_1:22;
end;
for n be Nat st n >= 1 holds PP[n] from NAT_1:sch 8(A78,A1);
hence thesis;
end;
begin :: Algorithm of calculation of (a^b) mod c based on
:: radix-2^k SD numbers and its correctness
definition
let n,f,j,m be Nat, e be Tuple of n,NAT;
func Table2(m,e,f,j) -> Element of NAT equals
(m |^ (e/.j)) mod f;
correctness;
end;
definition
let k,f,m,n be Nat, e be Tuple of n,NAT;
assume
A1: n >= 1;
func Pow_mod(m,e,f,k) -> Tuple of n,NAT means
:Def9:
it.1 = Table2(m,e,f,n)
& for i be Nat st 1 <= i & i <= n - 1 holds ex i1,i2 be Nat st i1 = it.i & i2 =
it.(i+1) & i2 = (((i1 |^ Radix(k)) mod f) * Table2(m,e,f,n-'i)) mod f;
existence
proof
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
reconsider T = Table2(m,e,f,n) as Element of NAT;
defpred PP[Nat,set,set] means ex i1,i2 be Nat st i1 = $2 & i2 = $3 & i2 =
(((i1 |^ Radix(k)) mod f)*Table2(m,e,f,n1-'$1)) mod f;
A2: for i be Nat st 1 <= i & i < n1 for x be Element of NAT ex
y be Element of NAT st PP[i,x,y]
proof
let i be Nat;
assume that
1 <= i and
i < n1;
let x be Element of NAT;
reconsider x as Element of NAT;
consider y be Element of NAT such that
A3: y = (((x |^ Radix(k)) mod f)*Table2(m,e,f,n-'i)) mod f;
reconsider z = y as Element of NAT;
take z;
thus thesis by A3;
end;
consider r be FinSequence of NAT such that
A4: len r = n1 & (r.1 = T or n1 = 0) and
A5: for i be Nat st 1 <= i & i < n1 holds PP[i,r.i,r.(i+1)]
from RECDEF_1:sch 4(A2);
reconsider r as Tuple of n,NAT by A4,CARD_1:def 7;
take r;
thus r.1 = Table2(m,e,f,n) by A1,A4;
let i be Nat;
assume
A6: 1 <= i & i <= n - 1;
thus thesis by A5,A6,XREAL_1:147;
end;
uniqueness
proof
let s1,s2 be Tuple of n,NAT such that
A7: s1.1 = Table2(m,e,f,n) and
A8: for i be Nat st 1 <= i & i <= n - 1 holds ex I1,I2 be Nat st I1 =
s1.i & I2 = s1.(i+1) & I2 = (((I1 |^ Radix(k)) mod f)*Table2(m,e,f,n-'i)) mod f
and
A9: s2.1 = Table2(m,e,f,n) and
A10: for i be Nat st 1 <= i & i <= n - 1 holds ex I1,I2 be Nat st I1 =
s2.i & I2 = s2.(i+1) & I2 = (((I1 |^ Radix(k)) mod f)*Table2(m,e,f,n-'i)) mod f
;
defpred P[Nat] means 1 <= $1 & $1 <= n - 1 implies s1.$1 = s2.$1;
A11: for i be Nat st P[i] holds P[i+1]
proof
let kk be Nat;
assume
A12: 1 <= kk & kk <= n - 1 implies s1.kk = s2.kk;
A13: 0 = kk or 0 < kk & 0 + 1 = 1;
assume that
1 <= kk + 1 and
A14: kk + 1 <= n - 1;
per cases by A13,NAT_1:13;
suppose
0 = kk;
hence thesis by A7,A9;
end;
suppose
A15: 1 <= kk;
A16: kk <= kk + 1 by NAT_1:11;
then kk <= n - 1 by A14,XXREAL_0:2;
then (ex i1,i2 be Nat st i1 = s1.kk & i2 = s1.(kk+1) & i2 = ( ((i1 |^
Radix(k)) mod f)*Table2(m,e,f,n-'kk)) mod f )& ex i1,i2 be Nat st i1 = s2.kk &
i2 = s2 .(kk+1) & i2 = ( ((i1 |^ Radix(k)) mod f)*Table2(m,e,f,n-'kk)) mod f
by A8,A10,A15;
hence thesis by A12,A14,A15,A16,XXREAL_0:2;
end;
end;
A17: len s1 = n by CARD_1:def 7;
A18: P[0];
A19: for kk be Nat holds P[kk] from NAT_1:sch 2(A18,A11);
A20: s1.n = s2.n
proof
n - 1 >= 1 - 1 by A1,XREAL_1:9;
then reconsider U1 = n - 1 as Element of NAT by INT_1:3;
now
per cases;
suppose
U1 = 0;
hence thesis by A7,A9;
end;
suppose
0 < U1;
then
A21: 1 <= U1 by NAT_1:14;
then (ex i1,i2 be Nat st i1 = s1.U1 & i2 = s1.(U1+1) & i2 = ( ((i1
|^ Radix(k)) mod f)*Table2(m,e,f,n-'U1)) mod f )& ex j1,j2 be Nat st j1 = s2.U1
& j2 = s2 .(U1+1) & j2 = ( ((j1 |^ Radix(k)) mod f)*Table2(m,e,f,n-'U1)) mod f
by A8,A10;
hence thesis by A19,A21;
end;
end;
hence thesis;
end;
A22: for kk be Nat st 1 <= kk & kk <= len s1 holds s1.kk = s2.kk
proof
let kk be Nat;
assume that
A23: 1 <= kk and
A24: kk <= len s1;
now
per cases by A24,XXREAL_0:1;
suppose
A25: kk < len s1;
n - 1 >= 1 - 1 by A1,XREAL_1:9;
then reconsider U1 = len s1 - 1 as Element of NAT by A17,INT_1:3;
U1 + 1 = len s1;
then kk <= U1 by A25,NAT_1:13;
hence thesis by A17,A19,A23;
end;
suppose
kk = len s1;
hence thesis by A17,A20;
end;
end;
hence thesis;
end;
len s1 = len s2 by A17,CARD_1:def 7;
hence thesis by A22,FINSEQ_1:14;
end;
end;
theorem
for n be Nat st n >= 1 holds for m,k,f,ie be Nat st ie
is_represented_by n,k & f>0 holds for e be Tuple of n,NAT st e = DecSD2(ie,n,k)
holds Pow_mod(m,e,f,k).n = (m |^ ie) mod f
proof
defpred PP[Nat] means for m,k,f,ie be Nat st ie is_represented_by $1,k & f>0
holds for e be Tuple of $1,NAT st e = DecSD2(ie,$1,k) holds Pow_mod(m,e,f,k).$1
= (m |^ ie) mod f;
A1: for n be Nat st n >= 1 & PP[n] holds PP[n+1]
proof
let n be Nat;
assume that
A2: n >= 1 and
A3: PP[n];
let m,k,f,ie be Nat;
A4: n+1 >= 1 by NAT_1:12;
assume that
A5: ie is_represented_by (n+1),k and
A6: f>0;
let e be Tuple of (n+1),NAT;
assume
A7: e = DecSD2(ie,(n+1),k);
reconsider n as Element of NAT by ORDINAL1:def 12;
deffunc F(Nat)=e.($1+1);
consider en being FinSequence of NAT such that
A8: len en = n and
A9: for i be Nat st i in dom en holds en.i = F(i) from FINSEQ_2:sch 1;
A10: dom en = Seg n by A8,FINSEQ_1:def 3;
reconsider en as Tuple of n,NAT by A8,CARD_1:def 7;
A11: n in Seg n by A2,FINSEQ_1:1;
A12: ie < (Radix(k) |^ (n+1)) by A5,RADIX_1:def 12;
set ien = SDDec2(en,k);
A13: 1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
then
A14: 1 in Seg (1+n) by FINSEQ_2:8;
A15: ie = ien*Radix(k) + (e/.1)
proof
A16: len <*SubDigit2(e,1,k)*> = 1 by FINSEQ_1:39;
deffunc F(Nat)=In(DigitSD2(en,k).$1,REAL);
reconsider r2 = Radix(k) as Element of REAL by XREAL_0:def 1;
consider rD being FinSequence of REAL such that
A17: len rD = n and
A18: for i be Nat st i in dom rD holds rD.i = F(i) from FINSEQ_2:sch 1;
A19: for i be Nat st i in dom rD holds rD.i = DigitSD2(en,k).i
proof let i be Nat;
assume i in dom rD;
then rD.i = F(i) by A18;
hence thesis;
end;
reconsider rD as Tuple of n,REAL by A17,CARD_1:def 7;
A20: dom rD = Seg n by A17,FINSEQ_1:def 3;
reconsider rD1=rD as Element of n-tuples_on REAL by FINSEQ_2:131;
A21: dom DigitSD2(en,k) = Seg (len DigitSD2(en,k)) by FINSEQ_1:def 3
.= Seg n by CARD_1:def 7;
then
A22: len (Radix(k) * DigitSD2(en,k)) = len (r2 * rD1) by A19,A20,FINSEQ_1:13
.= n by CARD_1:def 7;
A23: len (<*SubDigit2(e,1,k)*> ^ (Radix(k) * DigitSD2(en,k))) = len <*
SubDigit2(e,1,k)*> + len (Radix(k) * DigitSD2(en,k)) by FINSEQ_1:22
.= n+1 by A22,CARD_1:def 7;
A24: len DigitSD2(e,k) = n+1 by CARD_1:def 7;
A25: for i be Nat st 1 <= i & i <= len DigitSD2(e,k) holds DigitSD2(e,k)
.i=(<*SubDigit2(e,1,k)*> ^ (Radix(k)*DigitSD2(en,k))).i
proof
let i be Nat;
assume that
A26: 1 <= i and
A27: i <= len DigitSD2(e,k);
A28: i <= n+1 by A27,CARD_1:def 7;
then
A29: i in Seg (n+1) by A26,FINSEQ_1:1;
then
A30: i in dom DigitSD2(e,k) by A24,FINSEQ_1:def 3;
per cases;
suppose
A31: i = 1;
then (<*SubDigit2(e,1,k)*> ^ (Radix(k)*DigitSD2(en,k))).i =
SubDigit2(e,1,k) by FINSEQ_1:41
.= (DigitSD2(e,k))/.1 by A14,Def2
.= DigitSD2(e,k).1 by A30,A31,PARTFUN1:def 6;
hence thesis by A31;
end;
suppose
A32: i<>1;
reconsider rs2 = DigitSD2(en,k).(i-1) as Element of NAT;
reconsider rs = rD.(i-1) as Real;
1-1 <= i-1 by A26,XREAL_1:9;
then reconsider i1 = i-1 as Element of NAT by INT_1:3;
1<i by A26,A32,XXREAL_0:1;
then 1+1<=i by INT_1:7;
then
A33: 1+1-1<=i-1 by XREAL_1:9;
A34: i-1<=n+1-1 by A28,XREAL_1:9;
then
A35: i1 in Seg n by A33,FINSEQ_1:1;
A36: i1 in dom rD by A20,A33,A34,FINSEQ_1:1;
1 < i by A26,A32,XXREAL_0:1;
then
(<*SubDigit2(e,1,k)*> ^ (Radix(k)*DigitSD2(en,k))).i =(Radix(k)
*DigitSD2(en,k)).(i - 1) by A16,A23,A28,FINSEQ_1:24
.=(r2*rD).(i-1) by A19,A21,A20,FINSEQ_1:13
.=r2*rs by RVSUM_1:45
.=Radix(k)*rs2 by A19,A21,A20,FINSEQ_1:13
.=Radix(k)*((DigitSD2(en,k))/.i1) by A21,A20,A36,PARTFUN1:def 6
.=Radix(k)*SubDigit2(en,i1,k) by A35,Def2
.=Radix(k)*(Radix(k) |^ (i1-'1))*(en.i1)
.=(Radix(k) |^ (i1-'1+1))*(en.i1) by NEWTON:6
.=(Radix(k) |^ i1)*(en.i1) by A33,XREAL_1:235
.=(Radix(k) |^ i1)*(e.(i1+1)) by A9,A10,A35
.=SubDigit2(e,i,k) by A26,XREAL_1:233
.=(DigitSD2(e,k))/.i by A29,Def2;
hence thesis by A30,PARTFUN1:def 6;
end;
end;
len DigitSD2(e,k) = len (<*SubDigit2(e,1,k)*> ^ (Radix(k) *
DigitSD2(en,k))) by A23,CARD_1:def 7;
then
A37: DigitSD2(e,k) = <*SubDigit2(e,1,k)*>^(Radix(k)*DigitSD2(en,k)) by A25,
FINSEQ_1:14;
dom e = Seg (len e) by FINSEQ_1:def 3;
then
A38: 1 in dom e by A14,CARD_1:def 7;
A39: 1 - 1 = 0;
ie = SDDec2(e,k) by A5,A7,Th15,NAT_1:12
.= SubDigit2(e,1,k) + Sum(Radix(k) * DigitSD2(en,k)) by A37,RVSUM_1:76
.= SubDigit2(e,1,k) + Sum(r2 * rD) by A19,A21,A20,FINSEQ_1:13
.= SubDigit2(e,1,k) + r2 * Sum(rD) by RVSUM_1:87
.= SubDigit2(e,1,k) + Radix(k) * SDDec2(en,k) by A19,A21,A20,
FINSEQ_1:13
.= (Radix(k) |^ 0)*(e.1) + Radix(k) * ien by A39,XREAL_0:def 2
.= 1*(e.1) + Radix(k) * ien by NEWTON:4;
hence thesis by A38,PARTFUN1:def 6;
end;
then ie >= ien * Radix(k) by INT_1:6;
then ien * Radix(k) < (Radix(k) |^ (n+1)) by A12,XXREAL_0:2;
then ien * Radix(k) < (Radix(k) |^ n)* Radix(k) by NEWTON:6;
then ien < (Radix(k) |^ n) by XREAL_1:64;
then
A40: ien is_represented_by n,k by RADIX_1:def 12;
A41: (n+1) in Seg (n+1) by A4,FINSEQ_1:1;
A42: for i be Element of NAT st i in Seg n holds Pow_mod(m,en,f,k).i =
Pow_mod(m,e,f,k).i
proof
defpred Z[Nat] means
$1 in Seg n implies Pow_mod(m,en,f,k).$1
= Pow_mod(m,e,f,k).$1;
A43: for i be Nat st Z[i] holds Z[i+1]
proof
let i be Nat;
assume
A44: i in Seg n implies Pow_mod(m,en,f,k).i = Pow_mod(m,e,f,k).i;
A45: i=0 or i+1>1+0 by XREAL_1:6;
A46: dom en = Seg n by A8,FINSEQ_1:def 3;
assume
A47: (i+1) in Seg n;
then
A48: (i+1) <= n by FINSEQ_1:1;
then
A49: (i+1)-1 <= n - 1 by XREAL_1:9;
A50: dom e = Seg (len e) by FINSEQ_1:def 3;
then
A51: dom e = Seg (n+1) by CARD_1:def 7;
now
per cases by A45,NAT_1:13;
case
A52: i=0;
then Pow_mod(m,en,f,k).(i+1) = Table2(m,en,f,n) by A2,Def9
.= (m |^ (en.n)) mod f by A11,A46,PARTFUN1:def 6
.= (m |^ (e.(n+1))) mod f by A9,A10,A11
.= Table2(m,e,f,n+1) by A41,A51,PARTFUN1:def 6
.= Pow_mod(m,e,f,k).1 by A4,Def9;
hence thesis by A52;
end;
case
A53: i>=1;
reconsider nn = n - 1 as Element of NAT by A2,INT_1:5;
A54: i <= nn + 1 by A49,NAT_1:12;
then i <= (n+1)-1;
then
A55: ex I1,I2 be Nat st I1=Pow_mod(m,e,f,k).i & I2=Pow_mod(m,e,f,k
).(i+1) & I2 = (((I1 |^ Radix(k)) mod f) * Table2(m,e,f,(n+1)-'i)) mod f by A4
,A53,Def9;
A56: ex I1,I2 be Nat st I1=Pow_mod(m,en,f,k).i & I2=Pow_mod(m,en,f
,k).(i+1) & I2 = (((I1 |^ Radix(k)) mod f) * Table2(m,en,f,n-'i)) mod f by A2
,A49,A53,Def9;
A57: n -' i <= n by NAT_D:35;
i+1 <= n by A47,FINSEQ_1:1;
then i+1-1 <= n-1 by XREAL_1:9;
then (n+1)-'i >= (n+1)-'nn by NAT_D:41;
then (n+1)-'i >= (n+1)-(n-1) by XREAL_0:def 2;
then (n+1) -' i <= n+1 & 1 <= (n+1)-'i by NAT_D:35,XXREAL_0:2;
then ((n+1)-'i) in Seg (n+1) by FINSEQ_1:1;
then
A58: ((n+1) -' i) in dom e by A50,CARD_1:def 7;
1 + i - i <= n - i by A48,XREAL_1:9;
then 1 <= n -' i by A54,XREAL_1:233;
then
A59: (n -' i) in Seg n by A57,FINSEQ_1:1;
then (n -' i) in dom en by A8,FINSEQ_1:def 3;
then
Pow_mod(m,en,f,k).(i+1) = ((((Pow_mod(m,e,f,k).i) |^ Radix(k)
) mod f) * ((m |^ (en.(n-'i))) mod f)) mod f by A44,A53,A54,A56,FINSEQ_1:1
,PARTFUN1:def 6
.= ((((Pow_mod(m,e,f,k).i) |^ Radix(k)) mod f) * ((m |^ (e.(n
-'i+1))) mod f)) mod f by A9,A10,A59
.= ((((Pow_mod(m,e,f,k).i) |^ Radix(k)) mod f) * ((m |^ (e.((n
+1) -'i))) mod f)) mod f by A54,NAT_D:38
.= ((((Pow_mod(m,e,f,k).i) |^ Radix(k)) mod f) * Table2(m,e,f,
(n+1)-'i)) mod f by A58,PARTFUN1:def 6;
hence thesis by A55;
end;
end;
hence thesis;
end;
A60: Z[0] by FINSEQ_1:1;
for i be Nat holds Z[i] from NAT_1:sch 2(A60,A43);
hence thesis;
end;
A61: Radix(k) > 0 by Th6;
A62: for i be Nat st 1 <= i & i <= len en holds en.i=DecSD2(ien,n,k).i
proof
dom e = Seg (len e) by FINSEQ_1:def 3;
then
A63: dom e = Seg (n+1) by CARD_1:def 7;
A64: e.1 = DigitDC2(ie,1,k) by A7,A14,Def5
.= (ie mod (Radix(k) |^ 1)) div (Radix(k) |^ 0) by XREAL_1:232
.= (ie mod (Radix(k) |^ 1)) div 1 by NEWTON:4
.= ie mod (Radix(k) |^ 1)
.= ie mod Radix(k);
A65: 0 < Radix(k) by Th6;
A66: (e.1 + ien*Radix(k)) div Radix(k) = [\(e.1 + ien*Radix(k))/Radix(k
)/] by INT_1:def 9
.= [\e.1/Radix(k) + ien/] by A65,XCMPLX_1:113
.= [\e.1/Radix(k)/] + ien by INT_1:28
.= (e.1) div Radix(k) + ien by INT_1:def 9
.= 0 + ien by A61,A64,NAT_D:1,27;
A67: Radix(k) <> 0 by Th6;
let i be Nat;
assume that
A68: 1 <= i and
A69: i <= len en;
A70: 1 <= i+1 by A68,XREAL_1:29;
1 <= (i+1) & (i+1) <= (n+1) by A8,A68,A69,XREAL_1:6,29;
then
A71: (i+1) in Seg (n+1) by FINSEQ_1:1;
A72: i in Seg n by A8,A68,A69,FINSEQ_1:1;
then en.i = e.(i+1) by A9,A10
.= DigitDC2(ie,(i+1),k) by A7,A71,Def5
.= ((ien*Radix(k) + (e/.1)) div (Radix(k) |^ ((i+1)-'1))) mod Radix(
k) by A15,A70,Th4,Th6
.= ((ien*Radix(k) + e.1) div (Radix(k) |^ ((i+1)-'1))) mod Radix(k)
by A13,A63,FINSEQ_2:8,PARTFUN1:def 6
.= ((ien*Radix(k) + e.1) div (Radix(k) |^ i)) mod Radix(k) by NAT_D:34
.= ((ien*Radix(k) + e.1) div (Radix(k)*(Radix(k) |^ (i -'1)))) mod
Radix(k) by A68,A67,PEPIN:26
.= (((e.1 + ien*Radix(k)) div Radix(k)) div (Radix(k) |^ (i -'1)))
mod Radix(k) by NAT_2:27
.= DigitDC2(ien,i,k) by A68,A66,Th4,Th6;
hence thesis by A72,Def5;
end;
len en = len DecSD2(ien,n,k) by A8,CARD_1:def 7;
then
A73: en = DecSD2(ien,n,k) by A62,FINSEQ_1:14;
n <= (n+1) - 1 & n+1 >= 1 by NAT_1:11;
then ex I1,I2 be Nat st I1=Pow_mod(m,e,f,k).n & I2=Pow_mod(m,e,f,k).(n+1)
& I2 = (((I1 |^ Radix(k)) mod f)* Table2(m,e,f,(n+1)-'n)) mod f by A2,Def9;
then Pow_mod(m,e,f,k).(n+1) = ((((Pow_mod(m,en,f,k).n) |^ Radix(k)) mod f
) *Table2(m,e,f,(n+1)-'n)) mod f by A2,A42,FINSEQ_1:3
.= (((((m |^ ien) mod f) |^ Radix(k)) mod f) *Table2(m,e,f,(n+1)-'n))
mod f by A3,A6,A40,A73
.= ((((m |^ ien) |^ Radix(k)) mod f) *Table2(m,e,f,(n+1)-'n)) mod f by
PEPIN:12
.= (((m |^ ien) |^ Radix(k))*Table2(m,e,f,(n+1)-'n)) mod f by EULER_2:8
.= (m |^ (ien*Radix(k))*Table2(m,e,f,(n+1)-'n)) mod f by NEWTON:9
.= (m |^ (ien*Radix(k))*((m |^ (e/.1)) mod f)) mod f by NAT_D:34
.= (m |^ (ien*Radix(k))*(m |^ (e/.1))) mod f by EULER_2:7
.= (m |^ (ien*Radix(k) + (e/.1))) mod f by NEWTON:8;
hence thesis by A15;
end;
A74: PP[1]
proof
let m,k,f,ie be Nat;
assume that
A75: ie is_represented_by 1,k and
f>0;
ie < (Radix(k) |^ 1) by A75,RADIX_1:def 12;
then
A76: ie < Radix(k);
let e be Tuple of 1,NAT;
A77: 1 - 1 = 0;
A78: 1 in Seg 1 by FINSEQ_1:2,TARSKI:def 1;
len DecSD2(ie,1,k) = 1 by CARD_1:def 7;
then
A79: 1 in dom DecSD2(ie,1,k) by A78,FINSEQ_1:def 3;
assume e = DecSD2(ie,1,k);
then e/.1 = DecSD2(ie,1,k).1 by A79,PARTFUN1:def 6
.= DigitDC2(ie,1,k) by A78,Def5
.= (ie mod (Radix(k) |^ 1)) div (Radix(k) |^ 0) by A77,XREAL_0:def 2
.= (ie mod (Radix(k) |^ 1)) div 1 by NEWTON:4
.= ie mod (Radix(k) |^ 1)
.= ie mod Radix(k)
.= ie by A76,NAT_D:24;
then (m |^ ie) mod f = Table2(m,e,f,1);
hence thesis by Def9;
end;
for n be Nat st n >= 1 holds PP[n] from NAT_1:sch 8(A74,A1);
hence thesis;
end;