Copyright (c) 2000 Association of Mizar Users
environ
vocabulary ARYTM_1, NAT_1, INT_1, ARYTM_3, FINSEQ_1, RADIX_1, POWER, MIDSP_3,
RELAT_1, FUNCT_1, RLVECT_1, RADIX_2, FINSEQ_4, GROUP_1;
notation TARSKI, SUBSET_1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, INT_1, NAT_1,
FUNCT_1, POWER, FINSEQ_1, FINSEQ_4, BINARITH, EULER_2, RVSUM_1, TREES_4,
WSIERP_1, RADIX_1, MIDSP_3;
constructors REAL_1, POWER, BINARITH, FINSEQ_4, EULER_2, RADIX_1, SEQ_1,
MEMBERED, RAT_1;
clusters INT_1, RELSET_1, XREAL_0, WSIERP_1, NAT_1, MEMBERED, ORDINAL2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI;
theorems REAL_1, NAT_1, NAT_2, INT_1, FINSEQ_1, AXIOMS, GOBOARD9, RLVECT_1,
GR_CY_1, BINARITH, PREPOWER, POWER, JORDAN3, JORDAN4, RVSUM_1, FINSEQ_2,
FINSEQ_4, TARSKI, FUNCT_1, GR_CY_2, PEPIN, SCMFSA_7, SPRECT_3, RADIX_1,
EULER_2, INT_3, NEWTON, INT_2, SCMFSA9A, SPPOL_1, AMI_5, XCMPLX_0,
XCMPLX_1;
schemes NAT_1, FINSEQ_2, INT_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;
hence thesis by NAT_1:def 2;
end;
theorem Th2:
for a,b be Integer, n be Nat st n>0 holds
((a mod n)+(b mod n)) mod n = (a + (b mod n)) mod n &
((a mod n)+(b mod n)) mod n = ((a mod n) + b) mod n
proof
let a,b be Integer;
let n be Nat;
assume A1: n>0;
then a mod n + (a div n)*n
= (a-(a div n)*n) + (a div n)*n by INT_1:def 8
.= (a+ -(a div n)*n) + (a div n)*n by XCMPLX_0:def 8
.= a+(-(a div n)*n + (a div n)*n) by XCMPLX_1:1
.= a+0 by XCMPLX_0:def 6;
then (a + (b mod n))-((a mod n)+(b mod n))
= ((a div n)*n+((a mod n)+(b mod n)))-((a mod n)+(b mod n)) by XCMPLX_1:1
.= (a div n)*n+(((a mod n)+(b mod n))-((a mod n)+(b mod n))) by XCMPLX_1:29
.= (a div n)*n+0 by XCMPLX_1:14;
then n divides (a + (b mod n))-((a mod n)+(b mod n)) by INT_1:def 9;
then (a + (b mod n)),((a mod n)+(b mod n)) are_congruent_mod n by INT_2:19;
hence ((a mod n)+(b mod n)) mod n = (a + (b mod n)) mod n by A1,INT_3:12;
b mod n + (b div n)*n
= (b-(b div n)*n) + (b div n)*n by A1,INT_1:def 8
.= (b+ -(b div n)*n) + (b div n)*n by XCMPLX_0:def 8
.= b+(-(b div n)*n + (b div n)*n) by XCMPLX_1:1
.= b+0 by XCMPLX_0:def 6;
then ((a mod n) + b)-((a mod n)+(b mod n))
= ((a mod n)+(b mod n)+(b div n)*n)-((a mod n)+(b mod n)) by XCMPLX_1:1
.= ((a mod n)+(b mod n))+((b div n)*n-((a mod n)+(b mod n))) by XCMPLX_1:29
.= (b div n)*n-(((a mod n)+(b mod n))-((a mod n)+(b mod n))) by XCMPLX_1:37
.= (b div n)*n-0 by XCMPLX_1:14
.= (b div n)*n;
then n divides ((a mod n) + b)-((a mod n)+(b mod n)) by INT_1:def 9;
then ((a mod n) + b),((a mod n)+(b mod n)) are_congruent_mod n by INT_2:19;
hence thesis by A1,INT_3:12;
end;
theorem Th3:
for a,b be Integer, n be Nat st n>0 holds
(a*b) mod n = (a*(b mod n)) mod n &
(a*b) mod n = ((a mod n)*b) mod n
proof
let a,b be Integer;
let n be Nat;
assume A1: n > 0;
then b mod n + (b div n)*n
= (b-(b div n)*n) + (b div n)*n by INT_1:def 8
.= (b+ -(b div n)*n) + (b div n)*n by XCMPLX_0:def 8
.= b+(-(b div n)*n + (b div n)*n) by XCMPLX_1:1
.= b+0 by XCMPLX_0:def 6;
then (a*b)-(a*(b mod n))
= a*(b mod n)+a*((b div n)*n)-a*(b mod n) by XCMPLX_1:8
.= a*((b div n)*n)+(a*(b mod n)-a*(b mod n)) by XCMPLX_1:29
.= a*((b div n)*n)+0 by XCMPLX_1:14
.= (a*(b div n))*n by XCMPLX_1:4;
then n divides ((a*b)-(a*(b mod n))) by INT_1:def 9;
then (a*b),(a*(b mod n)) are_congruent_mod n by INT_2:19;
hence (a*b) mod n = (a*(b mod n)) mod n by A1,INT_3:12;
a mod n + (a div n)*n
= (a-(a div n)*n) + (a div n)*n by A1,INT_1:def 8
.= (a+ -(a div n)*n) + (a div n)*n by XCMPLX_0:def 8
.= a+(-(a div n)*n + (a div n)*n) by XCMPLX_1:1
.= a+0 by XCMPLX_0:def 6;
then (a*b)-((a mod n)*b)
= (a mod n)*b+((a div n)*n)*b-(a mod n)*b by XCMPLX_1:8
.= ((a div n)*n)*b+((a mod n)*b-(a mod n)*b) by XCMPLX_1:29
.= ((a div n)*n)*b+0 by XCMPLX_1:14
.= ((a div n)*b)*n by XCMPLX_1:4;
then n divides ((a*b)-((a mod n)*b)) by INT_1:def 9;
then (a*b),((a mod n)*b) are_congruent_mod n by INT_2:19;
hence thesis by A1,INT_3:12;
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 A1: 1 <= i & 0 < b;
set j = i -' 1;
set B0 = b |^ j;
set B1 = b |^ (j+1);
A2: j + 1 = i - 1 + 1 by A1,SCMFSA_7:3
.= i - (1 - 1) by XCMPLX_1:37
.= i;
A3: B1 > 0 by A1,PREPOWER:13;
A4: B0 > 0 by A1,PREPOWER:13;
A5: a mod B1 = a - (B1)*(a div B1) by A3,GR_CY_2:1;
reconsider R = a - (B1)*(a div B1) as Integer;
reconsider Z = (b*(-(a div B1))) as Integer;
reconsider a' = a as Integer;
(a mod (b |^ i)) div (b |^ (i-'1))
= R div B0 by A2,A5,SCMFSA9A:5
.= (a + (-(B1)*(a div B1))) div B0 by XCMPLX_0:def 8
.= (a + (B1)*(-(a div B1))) div B0 by XCMPLX_1:175
.= (a + (B0)*b*(-(a div B1))) div B0 by NEWTON:11
.= (a + (B0)*(b*(-(a div B1)))) div B0 by XCMPLX_1:4
.= [\ (a + (B0)*Z)/B0 /] by INT_1:def 7
.= [\ a/B0 + Z /] by A4,XCMPLX_1:114
.= [\ a/B0 /] + Z by INT_1:51
.= (a' div B0) + Z by INT_1:def 7
.= (a div B0) + Z by SCMFSA9A:5
.= (a div B0) + -b*(a div B1) by XCMPLX_1:175
.= (a div B0) - b*(a div B1) by XCMPLX_0:def 8
.= (a div B0) - b*(a div B0*b) by NEWTON:11
.= (a div B0) - b*((a div B0) div b) by NAT_2:29;
hence thesis by A1,GR_CY_2:1;
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 i in Seg n;
then 1 <= i & i <= n by FINSEQ_1:3;
then 1+1 <= i+1 & i+1 <= n+1 by AXIOMS:24;
then 1 <= i+1 & i+1 <= n+1 by AXIOMS:22;
hence i+1 in Seg (n+1) by FINSEQ_1:3;
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:39;
end;
theorem Th7:
for x be Tuple of 1,k-SD holds SDDec(x) = DigA(x,1)
proof
let x be Tuple of 1,k-SD;
A1: 1 in Seg 1 by FINSEQ_1:4,TARSKI:def 1;
1 - 1 = 0;
then A2: 1 -' 1 = 0 by BINARITH:def 3;
A3: (DigitSD(x))/.1 = SubDigit(x,1,k) by A1,RADIX_1:def 6;
A4: len (DigitSD(x)) = 1 by FINSEQ_2:109;
then 1 in dom DigitSD(x) by A1,FINSEQ_1:def 3;
then A5:DigitSD(x).1 = SubDigit(x,1,k) by A3,FINSEQ_4:def 4;
thus SDDec(x) = Sum DigitSD(x) by RADIX_1:def 7
.= Sum <*SubDigit(x,1,k)*> by A4,A5,FINSEQ_1:57
.= SubDigit(x,1,k) by RVSUM_1:103
.= (Radix(k) |^ 0)*DigB(x,1) by A2,RADIX_1:def 5
.= 1*DigB(x,1) by NEWTON:9
.= 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 by XCMPLX_1:27;
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;
assume A1:for i be Nat st i in Seg n holds x.i = xn.i;
A2:len DigitSD(x) = n+1 by FINSEQ_2:109;
A3:len DigitSD(xn) = n by FINSEQ_2:109;
A4:len <*SubDigit(x,n+1,k)*> = 1 by FINSEQ_1:56;
len (DigitSD(xn)^<*SubDigit(x,n+1,k)*>)
= len DigitSD(xn) + len <*SubDigit(x,n+1,k)*> by FINSEQ_1:35
.= n+1 by A4,FINSEQ_2:109;
then A5:len DigitSD(x) = len (DigitSD(xn)^<*SubDigit(x,n+1,k)*>)
by FINSEQ_2:109;
A6: for i be Nat st i in Seg n holds DigA(x,i) = DigA(xn,i)
proof
let i be Nat;
assume A7: i in Seg n;
then i in Seg (n+1) by FINSEQ_2:9;
then DigA(x,i) = x.i by RADIX_1:def 3
.= xn.i by A1,A7;
hence thesis by A7,RADIX_1:def 3;
end;
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 1 <= i & i <= len DigitSD(x);
then 1 <= i & i <= n+1 by FINSEQ_2:109;
then A8:i in Seg (n+1) by FINSEQ_1:3;
A9: n+1 in Seg(n+1) by FINSEQ_1:5;
now per cases by A8,FINSEQ_2:8;
suppose A10:i in Seg n;
then A11:i in Seg (n+1) by FINSEQ_2:9;
A12:i in dom DigitSD(xn) by A3,A10,FINSEQ_1:def 3;
A13:i in dom DigitSD(x) by A2,A11,FINSEQ_1:def 3;
((DigitSD(xn))^<*SubDigit(x,n+1,k)*>).i
= DigitSD(xn).i by A12,FINSEQ_1:def 7
.= (DigitSD(xn))/.i by A12,FINSEQ_4:def 4
.= SubDigit(xn,i,k) by A10,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 A6,A10
.= (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 A11,RADIX_1:def 6;
hence thesis by A13,FINSEQ_4:def 4;
suppose A14:i = n+1;
then A15:i in dom DigitSD(x) by A2,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 A14,FINSEQ_2:109
.= SubDigit(x,n+1,k) by FINSEQ_1:59
.= (DigitSD(x))/.(n+1) by A9,RADIX_1:def 6
.= DigitSD(x).(n+1) by A14,A15,FINSEQ_4:def 4;
hence thesis by A14;
end;
hence thesis;
end;
hence thesis by A5,FINSEQ_1:18;
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;
A2:DigitSD(xn) is FinSequence of INT;
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 A2,RVSUM_1:104
.= 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 BINARITH:39
.= 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:PP[1]
proof
let x,y be Tuple of 1,k-SD;
assume A2: k >= 2;
A3: 1 in Seg 1 by FINSEQ_1:4,TARSKI:def 1;
1 - 1 = 0;
then A4: 1 -' 1 = 0 by BINARITH:def 3;
A5: DigA(x '+' y,1) = Add(x,y,1,k) by A3,RADIX_1:def 14
.= SD_Add_Data(DigA(x,1)+DigA(y,1),k) + SD_Add_Carry(DigA(x,0)+DigA(y,0))
by A2,A3,A4,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:21,def 3;
A6: SDDec(y) = DigA(y,1) by Th7;
A7: SDDec(x '+' y) = SD_Add_Data(DigA(x,1)+DigA(y,1),k) by A5,Th7;
A8: 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 RADIX_1:def 11;
thus 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) by A7,NEWTON:10
.= DigA(x,1) + DigA(y,1) - (SD_Add_Carry(DigA(x,1)+DigA(y,1))*Radix(k)
- SD_Add_Carry(DigA(x,1)+DigA(y,1))*Radix(k)) by A8,XCMPLX_1:37
.= DigA(x,1) + DigA(y,1) - 0 by XCMPLX_1:14
.= SDDec(x) + SDDec(y) by A6,Th7;
end;
A9:for n be Nat st n >= 1 & PP[n] holds PP[n+1]
proof
let n be Nat;
assume that A10:n >= 1 and A11: PP[n];
let x,y be Tuple of (n+1),k-SD;
assume A12: k >= 2;
deffunc F(Nat) = DigB(x,$1);
consider xn being FinSequence of INT such that
A13: len xn = n and
A14: for i be Nat st i in Seg n holds xn.i = F(i) from SeqLambdaD;
rng xn c= k-SD
proof
let z be set;
assume z in rng xn;
then consider xx be set such that
A15: xx in dom xn and
A16: z = xn.xx by FUNCT_1:def 5;
reconsider xx as Nat by A15;
A17:dom xn = Seg n by A13,FINSEQ_1:def 3;
then A18: z = DigB(x,xx) by A14,A15,A16
.= DigA(x,xx) by RADIX_1:def 4;
xx in Seg (n+1) by A15,A17,FINSEQ_2:9;
then DigA(x,xx) is Element of k-SD by RADIX_1:19;
hence thesis by A18;
end;
then reconsider xn as FinSequence of k-SD by FINSEQ_1:def 4;
A19: for i be Nat st i in Seg n holds xn.i = x.i
proof
let i be Nat;
assume A20: i in Seg n;
then A21: i in Seg (n+1) by FINSEQ_2:9;
xn.i = DigB(x,i) by A14,A20
.= DigA(x,i) by RADIX_1:def 4;
hence thesis by A21,RADIX_1:def 3;
end;
deffunc F(Nat)=DigB(y,$1);
consider yn being FinSequence of INT such that
A22: len yn = n and
A23: for i be Nat st i in Seg n holds yn.i = F(i) from SeqLambdaD;
rng yn c= k-SD
proof
let z be set;
assume z in rng yn;
then consider yy be set such that
A24: yy in dom yn and
A25: z = yn.yy by FUNCT_1:def 5;
reconsider yy as Nat by A24;
A26:dom yn = Seg n by A22,FINSEQ_1:def 3;
then A27: z = DigB(y,yy) by A23,A24,A25
.= DigA(y,yy) by RADIX_1:def 4;
yy in Seg (n+1) by A24,A26,FINSEQ_2:9;
then DigA(y,yy) is Element of k-SD by RADIX_1:19;
hence thesis by A27;
end;
then reconsider yn as FinSequence of k-SD by FINSEQ_1:def 4;
A28: for i be Nat st i in Seg n holds yn.i = y.i
proof
let i be Nat;
assume A29: i in Seg n;
then A30: i in Seg (n+1) by FINSEQ_2:9;
yn.i = DigB(y,i) by A23,A29
.= DigA(y,i) by RADIX_1:def 4;
hence thesis by A30,RADIX_1:def 3;
end;
reconsider xn as Tuple of n,(k-SD) by A13,FINSEQ_2:110;
reconsider yn as Tuple of n,(k-SD) by A22,FINSEQ_2:110;
A31: for i be Nat st i in Seg n holds DigA(x,i) = DigA(xn,i)
proof
let i be Nat;
assume A32: i in Seg n;
then i in Seg (n+1) by FINSEQ_2:9;
then DigA(x,i) = x.i by RADIX_1:def 3
.= xn.i by A19,A32;
hence thesis by A32,RADIX_1:def 3;
end;
A33: for i be Nat st i in Seg n holds DigA(y,i) = DigA(yn,i)
proof
let i be Nat;
assume A34: i in Seg n;
then i in Seg (n+1) by FINSEQ_2:9;
then DigA(y,i) = y.i by RADIX_1:def 3
.= yn.i by A28,A34;
hence thesis by A34,RADIX_1:def 3;
end;
A35: Sum DigitSD(x '+' y)
= Sum(DigitSD(xn '+' yn) ^ <*SubDigit(x '+' y,n+1,k)*>)
proof
for i be Nat st i in Seg n holds (x '+' y).i = (xn '+' yn).i
proof
let i be Nat;
assume A36: i in Seg n;
then A37: i in Seg (n+1) by FINSEQ_2:9;
(x '+' y).i = (xn '+' yn).i
proof
A38: i >= 1 & i <= n+1 by A37,FINSEQ_1:3;
now per cases by A38,AXIOMS:21;
suppose A39:i > 1;
then i -'1 > 1 -'1 by SPRECT_3:10;
then i -'1 > 0 by GOBOARD9:1;
then A40:i -'1 >= 1 by RLVECT_1:99;
i - 1 > 1 - 1 by A39,REAL_1:54;
then A41:i -'1 = i - 1 by BINARITH:def 3;
i - 1 <= n + 1 - 1 by A38,REAL_1:49;
then i - 1 <= n by XCMPLX_1:26;
then A42:i -'1 in Seg n by A40,A41,FINSEQ_1:3;
(x '+' y).i
= DigA(x '+' y,i) by A37,RADIX_1:def 3
.= Add(x,y,i,k) by A37,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 A12,A37,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 A31,A36
.= SD_Add_Data(DigA(xn,i)+DigA(y,i),k)
+ SD_Add_Carry(DigA(xn,i -'1)+DigA(y,i -'1)) by A31,A42
.= SD_Add_Data(DigA(xn,i)+DigA(yn,i),k)
+ SD_Add_Carry(DigA(xn,i -'1)+DigA(y,i -'1)) by A33,A36
.= SD_Add_Data(DigA(xn,i)+DigA(yn,i),k)
+ SD_Add_Carry(DigA(xn,i -'1)+DigA(yn,i -'1)) by A33,A42
.= Add(xn,yn,i,k) by A12,A36,RADIX_1:def 13
.= DigA(xn '+' yn,i) by A36,RADIX_1:def 14;
hence thesis by A36,RADIX_1:def 3;
suppose A43:i = 1;
(x '+' y).i
= DigA(x '+' y,i) by A37,RADIX_1:def 3
.= Add(x,y,i,k) by A37,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 A12,A37,A43,
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 GOBOARD9:1
.= SD_Add_Data(DigA(x,i)+DigA(y,i),k)
+ SD_Add_Carry(DigA(x,0)+DigA(y,0)) by GOBOARD9:1
.= 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 A31,A36
.= SD_Add_Data(DigA(xn,i)+DigA(yn,i),k)
+ SD_Add_Carry(DigA(xn,0)+DigA(yn,0)) by A33,A36
.= SD_Add_Data(DigA(xn,i)+DigA(yn,i),k)
+ SD_Add_Carry(DigA(xn,1-'1)+DigA(yn,0)) by GOBOARD9:1
.= SD_Add_Data(DigA(xn,i)+DigA(yn,i),k)
+ SD_Add_Carry(DigA(xn,i-'1)+DigA(yn,i-'1)) by A43,
GOBOARD9:1
.= Add(xn,yn,i,k) by A12,A36,RADIX_1:def 13
.= DigA(xn '+' yn,i) by A36,RADIX_1:def 14;
hence thesis by A36,RADIX_1:def 3;
end;
hence thesis;
end;
hence thesis;
end;
hence thesis by Th9;
end;
A44:DigitSD(xn '+' yn) is FinSequence of INT;
A45:n+1 in Seg (n+1) by FINSEQ_1:5;
n <> 0 by A10;
then A46:n in Seg n by FINSEQ_1:5;
SDDec(x '+' y)
= Sum(DigitSD(xn '+' yn)^<*SubDigit(x '+' y,n+1,k)*>) by A35,RADIX_1:def 7
.= Sum DigitSD(xn '+' yn) + SubDigit(x '+' y,n+1,k) by A44,RVSUM_1:104
.= 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 BINARITH:39
.= 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 A45,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 A12,A45,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 BINARITH:39
.= 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 BINARITH:39
.= 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)) by XCMPLX_1:8
.= 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) by XCMPLX_1:1
.= 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 A31,A46
.= 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 A33,A46
.= SDDec(xn) + SDDec(yn)
+ (Radix(k) |^ n)*SD_Add_Data(DigA(x,n+1)+DigA(y,n+1),k) by A11,A12;
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))) by XCMPLX_1:
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:11
.= 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))*(Radix(k) |^ n))
by XCMPLX_1:4
.= 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)))) by XCMPLX_1:8
.= SDDec(xn) + SDDec(yn)
+ ((Radix(k) |^ n)*(DigA(x,n+1) + DigA(y,n+1))) by Th8
.= SDDec(xn) + SDDec(yn)
+ ((Radix(k) |^ n)*DigA(x,n+1) + (Radix(k) |^ n)*DigA(y,n+1))
by XCMPLX_1:8
.= SDDec(xn) + SDDec(yn)
+ (Radix(k) |^ n)*DigA(x,n+1) + (Radix(k) |^ n)*DigA(y,n+1) by XCMPLX_1:1
.= SDDec(xn) + (Radix(k) |^ n)*DigA(x,n+1)
+ SDDec(yn) + (Radix(k) |^ n)*DigA(y,n+1) by XCMPLX_1:1
.= (SDDec(xn) + (Radix(k) |^ n)*DigA(x,n+1))
+ (SDDec(yn) + (Radix(k) |^ n)*DigA(y,n+1)) by XCMPLX_1:1
.= SDDec(x) + (SDDec(yn) + (Radix(k) |^ n)*DigA(y,n+1)) by A19,Th10;
hence thesis by A28,Th10;
end;
for n be Nat st n >= 1 holds PP[n] from Ind1(A1,A9);
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
:Def1:
(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 Seg n holds z.j = F(j)
from SeqLambdaD;
reconsider z as Tuple of n,NAT by A1,FINSEQ_2:110;
take z;
let i be Nat;
assume A3:i in Seg n;
then i in dom z by A1,FINSEQ_1:def 3;
hence z/.i = z.i by FINSEQ_4:def 4
.= SubDigit2(x,i,k) 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 = SubDigit2(x,i,k) and
A5:for i be Nat st i in Seg n holds k2/.i = SubDigit2(x,i,k);
A6:len k1 = n & len k2 = n by FINSEQ_2:109;
now let j be Nat;
assume A7:j in Seg n;
then A8:j in dom k1 & j in dom k2 by A6,FINSEQ_1:def 3;
then k1.j = k1/.j by FINSEQ_4:def 4
.= SubDigit2(x,j,k) by A4,A7
.= k2/.j by A5,A7;
hence k1.j = k2.j by A8,FINSEQ_4:def 4;
end;
hence k1 = k2 by A6,FINSEQ_2:10;
end;
end;
definition let n,k be Nat, x be Tuple of n,NAT;
func SDDec2(x,k) -> Nat equals
:Def3:
Sum DigitSD2(x,k);
coherence;
end;
definition let i,k,x be Nat;
func DigitDC2(x,i,k) -> Nat equals
:Def4:
(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 Seg n holds z.j = F(j)
from SeqLambdaD;
reconsider z as Tuple of n,NAT by A1,FINSEQ_2:110;
take z;
let i be Nat;
assume i in Seg n;
hence z.i = DigitDC2(x,i,k) by A2;
end;
uniqueness
proof
let k1,k2 be Tuple of n,NAT such that
A3:for i be Nat st i in Seg n holds k1.i = DigitDC2(x,i,k) and
A4:for i be Nat st i in Seg n holds k2.i = DigitDC2(x,i,k);
A5:len k1 = n & len k2 = n by FINSEQ_2:109;
now let j be Nat;
assume A6:j in Seg n;
then k1.j = DigitDC2(x,j,k) by A3;
hence k1.j = k2.j by A4,A6;
end;
hence k1 = k2 by A5,FINSEQ_2:10;
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;
assume A1: x=y;
A2: now let i be Nat;
assume i in Seg n;
then x.i = DigA(y,i) by A1,RADIX_1:def 3
.= DigB(y,i) by RADIX_1:def 4;
hence x.i = DigB(y,i);
end;
A3:len DigitSD2(x,k) = n & len DigitSD(y) = n by FINSEQ_2:109;
now let j be Nat;
assume A4:j in Seg n;
then A5:j in dom DigitSD2(x,k) & j in
dom DigitSD(y) by A3,FINSEQ_1:def 3;
then DigitSD2(x,k).j = (DigitSD2(x,k))/.j by FINSEQ_4:def 4
.= SubDigit2(x,j,k) by A4,Def2
.= (Radix(k) |^ (j -'1))*(x.j) by Def1
.= (Radix(k) |^ (j -'1))*DigB(y,j) by A2,A4
.= SubDigit(y,j,k) by RADIX_1:def 5
.= (DigitSD(y))/.j by A4,RADIX_1:def 6
.= DigitSD(y).j by A5,FINSEQ_4:def 4;
hence DigitSD2(x,k).j = DigitSD(y).j;
end;
hence thesis by A3,FINSEQ_2:10;
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 A1: x = y;
SDDec2(x,k) = Sum DigitSD2(x,k) by Def3
.= Sum DigitSD(y) by A1,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 & len DecSD(x,n,k) = n by FINSEQ_2:109;
now let j be Nat;
assume A2: j in Seg n;
then DecSD2(x,n,k).j = DigitDC2(x,j,k) by Def5
.= (x mod (Radix(k) |^ j)) div (Radix(k) |^ (j -'1)) by Def4
.= DigitDC(x,j,k) by RADIX_1:def 8
.= DigA(DecSD(x,n,k),j) by A2,RADIX_1:def 9
.= DecSD(x,n,k).j by A2,RADIX_1:def 3;
hence DecSD2(x,n,k).j = DecSD(x,n,k).j;
end;
hence DecSD2(x,n,k) = DecSD(x,n,k) by A1,FINSEQ_2:10;
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;
DecSD2(m,n,k) = DecSD(m,n,k) by Th14;
then SDDec2(DecSD2(m,n,k),k) = SDDec(DecSD(m,n,k)) by Th13;
hence thesis by A1,A2,RADIX_1:25;
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
:Def6:
(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
reconsider T = Table1(q,c,f,n) as Element of INT by INT_1:def 2;
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;
A2: for i be Nat st 1 <= i & i < n holds for x be Element of INT
ex y be Element of INT st PP[i,x,y]
proof
let i be Nat;
assume 1 <= i & i < n;
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 = n & (r.1 = T or n = 0) and
A5:for i be Nat st 1 <= i & i < n holds PP[i,r.i,r.(i+1)]
from FinRecExD(A2);
reconsider r as Tuple of n,INT by A4,FINSEQ_2:110;
take r;
thus r.1 = Table1(q,c,f,n) by A1,A4;
let i be Nat;
assume 1 <= i & i <= n - 1;
then 1 <= i & i < n by SPPOL_1:5;
hence thesis by A5;
end;
uniqueness
proof
let s1,s2 be Tuple of n,INT such that
A6: s1.1 = Table1(q,c,f,n) &
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
A7: s2.1 = Table1(q,c,f,n) &
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;
A8: len s1 = n by FINSEQ_2:109;
then A9:len s1 = len s2 by FINSEQ_2:109;
defpred P[Nat] means 1 <= $1 & $1 <= n - 1 implies s1.$1 = s2.$1;
A10: P[0];
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;
assume A13: 1 <= kk + 1 & kk + 1 <= n - 1;
A14:0 = kk or 0 < kk & 0 + 1 = 1 by NAT_1:19;
per cases by A14,NAT_1:38;
suppose 0 = kk;
hence s1.(kk+1) = s2.(kk+1) by A6,A7;
suppose
A15: 1 <= kk;
A16:kk <= kk + 1 by NAT_1:29;
then A17:1 <= kk & kk <= n - 1 by A13,A15,AXIOMS:22;
then A18: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 by A6;
consider i1,i2 be Integer such that
A19: i1 = s2.kk & i2 = s2.(kk+1) &
i2 = (Radix(k)*i1+Table1(q,c,f,n -'kk)) mod f by A7,A17;
thus s1.(kk+1) = s2.(kk+1) by A12,A13,A15,A16,A18,A19,AXIOMS:22;
end;
A20:for kk be Nat holds P[kk] from Ind (A10,A11);
A21:s1.n = s2.n
proof
A22: n - 1 >= 1 - 1 by A1,REAL_1:49;
then reconsider U1 = n - 1 as Nat by INT_1:16;
n = n + - 1 + 1 by XCMPLX_1:139;
then A23:n = n - 1 + 1 by XCMPLX_0:def 8;
now per cases by A22;
suppose U1 = 0;
then 0 + 1 = n by XCMPLX_1:27;
hence thesis by A6,A7;
suppose 0 < U1;
then A24:1 <= U1 & U1 <= U1 by RLVECT_1:99;
then consider i1,i2 be Integer such that
A25:i1 = s1.U1 & i2 = s1.(U1+1) and
A26:i2 = (Radix(k)*i1+Table1(q,c,f,n -'U1)) mod f by A6;
consider j1,j2 be Integer such that
A27:j1 = s2.U1 & j2 = s2.(U1+1) and
A28:j2 = (Radix(k)*j1+Table1(q,c,f,n -'U1)) mod f by A7,A24;
thus thesis by A20,A23,A24,A25,A26,A27,A28;
end;
hence thesis;
end;
for kk be Nat st 1 <= kk & kk <= len s1 holds s1.kk = s2.kk
proof
let kk be Nat;
assume A29:1 <= kk & kk <= len s1;
now per cases by A29,AXIOMS:21;
suppose A30:kk < len s1;
n - 1 >= 1 - 1 by A1,REAL_1:49;
then reconsider U1 = len s1 - 1 as Nat by A8,INT_1:16;
U1 + 1 = len s1 by XCMPLX_1:27;
then kk <= U1 by A30,NAT_1:38;
hence s1.kk = s2.kk by A8,A20,A29;
suppose kk = len s1;
hence s1.kk = s2.kk by A8,A21;
end;
hence thesis;
end;
hence s1 = s2 by A9,FINSEQ_1:18;
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:PP[1]
proof
let q be Integer;
let ic,f,k be Nat;
assume A2: ic is_represented_by 1,k & f > 0;
let c be Tuple of 1,k-SD;
assume A3: c = DecSD(ic,1,k);
Mul_mod(q,c,f,k).1 = Table1(q,c,f,1) by Def7
.= (q*DigA(c,1)) mod f by Def6
.= (q*SDDec(DecSD(ic,1,k))) mod f by A3,Th7;
hence thesis by A2,RADIX_1:25;
end;
A4:for n be Nat st n >= 1 & PP[n] holds PP[n+1]
proof
let n be Nat;
assume A5: n >= 1 & PP[n];
A6: n+1 >= 1 by NAT_1:37;
let q be Integer;
let ic,f,k be Nat;
assume A7: ic is_represented_by (n+1),k & f > 0;
let c be Tuple of (n+1),k-SD;
assume A8: c = DecSD(ic,(n+1),k);
set c2 = DecSD2(ic,(n+1),k);
A9: c2 = c by A8,Th14;
deffunc F(Nat) =DigB(c,($1+1));
consider cn being FinSequence of INT such that
A10: len cn = n and
A11: for i be Nat st i in Seg n holds cn.i = F(i) from SeqLambdaD;
rng cn c= k-SD
proof
let z be set;
assume z in rng cn;
then consider xx be set such that
A12: xx in dom cn and
A13: z = cn.xx by FUNCT_1:def 5;
reconsider xx as Nat by A12;
A14:dom cn = Seg n by A10,FINSEQ_1:def 3;
then A15: z = DigB(c,(xx+1)) by A11,A12,A13
.= DigA(c,(xx+1)) by RADIX_1:def 4;
xx+1 in Seg (n+1) by A12,A14,Th5;
then DigA(c,(xx+1)) is Element of k-SD by RADIX_1:19;
hence thesis by A15;
end;
then reconsider cn as FinSequence of k-SD by FINSEQ_1:def 4;
reconsider cn as Tuple of n,(k-SD) by A10,FINSEQ_2:110;
deffunc F(Nat) = c2.($1+1);
consider cn2 being FinSequence of NAT such that
A16: len cn2 = n and
A17: for i be Nat st i in Seg n holds cn2.i = F(i) from SeqLambdaD;
reconsider cn2 as Tuple of n,NAT by A16,FINSEQ_2:110;
A18: for i be Nat st i in Seg n holds DigA(cn,i) = DigA(c,i+1)
proof
let i be Nat;
assume A19: i in Seg n;
DigA(c,i+1) = DigB(c,i+1) by RADIX_1:def 4
.= cn.i by A11,A19;
hence thesis by A19,RADIX_1:def 3;
end;
A20:cn = cn2
proof
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 A10,FINSEQ_1:3;
then A22: i+1 in Seg (n+1) by Th5;
cn.i = DigB(c,(i+1)) by A11,A21
.= DigA(c,(i+1)) by RADIX_1:def 4
.= c.(i+1) by A22,RADIX_1:def 3
.= c2.(i+1) by A8,Th14;
hence thesis by A17,A21;
end;
hence thesis by A10,A16,FINSEQ_1:18;
end;
1 in Seg 1 by FINSEQ_1:4,TARSKI:def 1;
then A23:1 in Seg (1+n) by FINSEQ_2:9;
A24: for i be 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;
A25: P[0] by FINSEQ_1:3;
A26: for i be Nat st P[i] holds P[i+1]
proof let i be Nat;
assume A27: i in Seg n implies
Mul_mod(q,cn,f,k).i = Mul_mod(q,c,f,k).i;
assume A28: (i+1) in Seg n;
A29: n in Seg n by A5,FINSEQ_1:3;
1 <= (i+1) & (i+1) <= n by A28,FINSEQ_1:3;
then A30:(i+1)-1 <= n - 1 by REAL_1:49;
(i=0 or i>0) by NAT_1:19;
then A31:(i=0 or i+1>1+0) by REAL_1:53;
now per cases by A31,NAT_1:38;
case A32: i=0;
then Mul_mod(q,cn,f,k).(i+1)
= Table1(q,cn,f,n) by A5,Def7
.= (q*DigA(cn,n)) mod f by Def6
.= (q*DigA(c,n+1)) mod f by A18,A29
.= Table1(q,c,f,n+1) by Def6
.= Mul_mod(q,c,f,k).1 by A6,Def7;
hence Mul_mod(q,cn,f,k).(i+1) = Mul_mod(q,c,f,k).(i+1) by A32;
case A33: i>=1;
reconsider nn = n - 1 as Nat by A5,INT_1:18;
A34: 1 <= i & i <= n - 1 by A30,A33,XCMPLX_1:26;
then A35:1 <= i & i <= nn + 1 by NAT_1:37;
then A36:1 <= i & i <= n by XCMPLX_1:27;
A37: 1 <= i & i <= (n+1)-1 by A35,XCMPLX_1:29;
A38: 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 A5,A34,Def7;
A39: 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 A6,A37,Def7;
i + 1 <= n - 1 + 1 by A34,AXIOMS:24;
then 1 + i <= n by XCMPLX_1:27;
then 1 + i - i <= n - i by REAL_1:49;
then 1 + (i - i) <= n - i by XCMPLX_1:29;
then 1 + 0 <= n - i by XCMPLX_1:14;
then A40: 1 <= n -' i by A36,SCMFSA_7:3;
n -' i <= n by GOBOARD9:2;
then A41: (n -' i) in Seg n by A40,FINSEQ_1:3;
Mul_mod(q,cn,f,k).(i+1)
= (Radix(k)*Mul_mod(q,c,f,k).i
+ (q*DigA(cn,(n -' i)) mod f)) mod f by A27,A36,
A38,Def6,FINSEQ_1:3
.= (Radix(k)*Mul_mod(q,c,f,k).i
+ (q*DigA(c,(n -' i)+1) mod f)) mod f
by A18,A41
.= (Radix(k)*Mul_mod(q,c,f,k).i
+ (q*DigA(c,((n+1) -' i)) mod f)) mod f by A36,JORDAN4:3
.= Mul_mod(q,c,f,k).(i+1) by A39,Def6;
hence Mul_mod(q,cn,f,k).(i+1)=Mul_mod(q,c,f,k).(i+1);
end;
hence Mul_mod(q,cn,f,k).(i+1) = Mul_mod(q,c,f,k).(i+1);
end;
for i be Nat holds P[i] from Ind(A25,A26);
hence thesis;
end;
n <> 0 by A5;
then A42: n in Seg n by FINSEQ_1:5;
set icn = SDDec(cn);
set icn2 = SDDec2(cn2,k);
A43: icn = icn2 by A20,Th13;
A44: ic = Radix(k)*icn2 + c2.1
proof
reconsider r2 = Radix(k) as Element of REAL;
deffunc F(Nat)=DigitSD2(cn2,k).$1;
consider rD being FinSequence of REAL such that
A45: len rD = n and
A46: for i be Nat st i in Seg n holds rD.i = F(i)
from SeqLambdaD;
reconsider rD as Tuple of n,REAL by A45,FINSEQ_2:110;
A47: dom DigitSD2(cn2,k) = Seg (len DigitSD2(cn2,k)) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:109;
A48: dom rD = Seg n by A45,FINSEQ_1:def 3;
A49:1 - 1 = 0;
A50: DigitSD2(c2,k) = <*SubDigit2(c2,1,k)*>^(Radix(k)*DigitSD2(cn2,k))
proof
A51:len DigitSD2(c2,k) = n+1 by FINSEQ_2:109;
A52:len (Radix(k) * DigitSD2(cn2,k))
= len (r2 * rD) by A46,A47,A48,FINSEQ_1:17
.= n by FINSEQ_2:109;
A53:len <*SubDigit2(c2,1,k)*> = 1 by FINSEQ_1:56;
A54:len (<*SubDigit2(c2,1,k)*> ^ (Radix(k) * DigitSD2(cn2,k)))
= len <*SubDigit2(c2,1,k)*> + len (Radix(k) * DigitSD2(cn2,k))
by FINSEQ_1:35
.= n+1 by A52,FINSEQ_2:109;
then A55:len DigitSD2(c2,k)
= len (<*SubDigit2(c2,1,k)*> ^ (Radix(k) * DigitSD2(cn2,k)))
by FINSEQ_2:109;
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 A56:1 <= i & i <= len DigitSD2(c2,k);
then A57:i <= n+1 by FINSEQ_2:109;
then A58:i in Seg (n+1) by A56,FINSEQ_1:3;
then A59: i in dom DigitSD2(c2,k) by A51,FINSEQ_1:def 3;
per cases;
suppose A60:i = 1;
then (<*SubDigit2(c2,1,k)*> ^ (Radix(k)*DigitSD2(cn2,k))).i
= SubDigit2(c2,1,k) by FINSEQ_1:58
.= (DigitSD2(c2,k))/.1 by A23,Def2
.= DigitSD2(c2,k).1 by A59,A60,FINSEQ_4:def 4;
hence thesis by A60;
suppose A61:i <> 1;
1 - 1 <= i - 1 by A56,REAL_1:49;
then reconsider i1 = i - 1 as Nat by INT_1:16;
1 < i by A56,A61,REAL_1:def 5;
then 1 + 1 <= i by INT_1:20;
then A62: 1 + 1 - 1 <= i - 1 by REAL_1:49;
i - 1 <= n + 1 - 1 by A57,REAL_1:49;
then i - 1 <= n by XCMPLX_1:26;
then A63: i1 in Seg n by A62,FINSEQ_1:3;
then reconsider rs = rD.(i-1) as Real by A48,FINSEQ_2:13;
reconsider rs2 = DigitSD2(cn2,k).(i-1) as Nat
by A47,A63,FINSEQ_2:13;
1 < i by A56,A61,REAL_1:def 5;
then (<*SubDigit2(c2,1,k)*> ^ (Radix(k)*DigitSD2(cn2,k))).i
=(Radix(k)*DigitSD2(cn2,k)).(i - 1) by A53,A54,A57,FINSEQ_1:
37
.=(r2*rD).(i-1) by A46,A47,A48,FINSEQ_1:17
.=r2*rs by A63,RVSUM_1:67
.=Radix(k)*rs2 by A46,A47,A48,FINSEQ_1:17
.=Radix(k)*((DigitSD2(cn2,k))/.i1)
by A47,A63,FINSEQ_4:def 4
.=Radix(k)*SubDigit2(cn2,i1,k) by A63,Def2
.=Radix(k)*((Radix(k) |^ (i1-'1))*(cn2.i1)) by Def1
.=Radix(k)*(Radix(k) |^ (i1-'1))*(cn2.i1) by XCMPLX_1:4
.=(Radix(k) |^ (i1-'1+1))*(cn2.i1) by NEWTON:11
.=(Radix(k) |^ i1)*(cn2.i1) by A62,AMI_5:4
.=(Radix(k) |^ i1)*(c2.(i1+1)) by A17,A63
.=(Radix(k) |^ (i-'1))*(c2.(i1+1)) by A56,SCMFSA_7:3
.=(Radix(k) |^ (i-'1))*(c2.i) by XCMPLX_1:27
.=SubDigit2(c2,i,k) by Def1
.=(DigitSD2(c2,k))/.i by A58,Def2;
hence thesis by A59,FINSEQ_4:def 4;
end;
hence thesis by A55,FINSEQ_1:18;
end;
ic = SDDec2(DecSD2(ic,(n+1),k),k) by A6,A7,Th15
.= Sum DigitSD2(c2,k) by Def3
.= SubDigit2(c2,1,k)+ Sum(Radix(k)*DigitSD2(cn2,k)) by A50,RVSUM_1:106
.= SubDigit2(c2,1,k) + Sum(r2 * rD) by A46,A47,A48,FINSEQ_1:17
.= SubDigit2(c2,1,k) + r2 * Sum(rD) by RVSUM_1:117
.= SubDigit2(c2,1,k) + Radix(k) * Sum(DigitSD2(cn2,k))
by A46,A47,A48,FINSEQ_1:17
.= SubDigit2(c2,1,k) + Radix(k) * icn2 by Def3
.= (Radix(k) |^ (1 -' 1))*(c2.1) + Radix(k) * icn2 by Def1
.= (Radix(k) |^ 0)*(c2.1) + Radix(k) * icn2 by A49,BINARITH:def 3
.= 1*(c2.1) + Radix(k) * icn2 by NEWTON:9;
hence thesis;
end;
reconsider icn as Nat by A43;
A64: ic >= Radix(k)*icn2 by A44,INT_1:19;
A65: Radix(k) > 0 by Th6;
ic < (Radix(k) |^ (n+1)) by A7,RADIX_1:def 12;
then icn2 * Radix(k) < (Radix(k) |^ (n+1)) by A64,AXIOMS:22;
then icn2 * Radix(k) < (Radix(k) |^ n)* Radix(k) by NEWTON:11;
then icn < (Radix(k) |^ n) by A43,A65,AXIOMS:25;
then A66: icn is_represented_by n,k by RADIX_1:def 12;
cn = DecSD2(icn2,n,k)
proof
A67:len cn = len DecSD2(icn2,n,k) by A10,FINSEQ_2:109;
for i be Nat st 1 <= i & i <= len cn holds cn.i=DecSD2(icn2,n,k).i
proof
let i be Nat;
assume A68: 1 <= i & i <= len cn;
then A69: i in Seg n by A10,FINSEQ_1:3;
A70: i <= i+1 by REAL_1:69;
then 1 <= (i+1) & (i+1) <= (n+1) by A10,A68,AXIOMS:22,24;
then A71: (i+1) in Seg (n+1) by FINSEQ_1:3;
c2.1 = DigitDC2(ic,1,k) by A23,Def5
.= (ic mod (Radix(k) |^ 1)) div (Radix(k) |^ (1 -' 1)) by Def4
.= (ic mod (Radix(k) |^ 1)) div (Radix(k) |^ 0) by GOBOARD9:1
.= (ic mod (Radix(k) |^ 1)) div 1 by NEWTON:9
.= ic mod (Radix(k) |^ 1) by NAT_2:6
.= ic mod Radix(k) by NEWTON:10;
then A72: c2.1 < Radix(k) by A65,NAT_1:46;
A73:1 <= i+1 & 0 < Radix(k) by A68,A70,Th6,AXIOMS:22;
A74:Radix(k) <> 0 & i <> 0 by A68,Th6;
reconsider a = c2.1 as Integer;
reconsider b = icn2 as Integer;
reconsider G = a + b*Radix(k) as Integer;
A75:(c2.1 + icn2*Radix(k)) div Radix(k)
= G div Radix(k) by SCMFSA9A:5
.= [\(c2.1 + icn2*Radix(k))/Radix(k)/] by INT_1:def 7
.= [\c2.1/Radix(k) + icn2/] by A73,XCMPLX_1:114
.= [\c2.1/Radix(k)/] + icn2 by INT_1:51
.= a div Radix(k) + icn2 by INT_1:def 7
.= (c2.1) div Radix(k) + icn2 by SCMFSA9A:5
.= 0 + icn2 by A72,JORDAN4:5;
cn.i
= c2.(i+1) by A17,A20,A69
.= DigitDC2(ic,(i+1),k) by A71,Def5
.= (ic mod (Radix(k) |^ (i+1))) div (Radix(k) |^ ((i+1) -'1)) by Def4
.= ((icn2*Radix(k) + c2.1) div (Radix(k) |^ ((i+1)-'1)))
mod Radix(k) by A44,A73,Th4
.= ((icn2*Radix(k) + c2.1) div (Radix(k) |^ i))
mod Radix(k) by BINARITH:39
.= ((icn2*Radix(k) + c2.1) div (Radix(k)*(Radix(k) |^ (i -'1))))
mod Radix(k) by A74,PEPIN:27
.= (icn2 div (Radix(k) |^ (i -'1))) mod Radix(k) by A75,NAT_2:29
.= (icn2 mod (Radix(k) |^ i)) div (Radix(k) |^ (i -'1)) by A68,A73,Th4
.= DigitDC2(icn2,i,k) by Def4;
hence thesis by A69,Def5;
end;
hence thesis by A67,FINSEQ_1:18;
end;
then A76: cn = DecSD(icn,n,k) by A43,Th14;
A77: (q * ic) mod f
= (q * (Radix(k)*icn2) + q * c2.1) mod f by A44,XCMPLX_1:8
.= (q * Radix(k)*icn2 + q * c2.1) mod f by XCMPLX_1:4
.= (((Radix(k) * q * icn2) mod f) + ((q * c2.1) mod f)) mod f
by A7,INT_3:14
.= (((Radix(k) *(q * icn2)) mod f) + ((q * c2.1) mod f)) mod f
by XCMPLX_1:4
.= (((Radix(k) *((q * icn2) mod f)) mod f)
+ ((q * c2.1) mod f)) mod f by A7,Th3
.= ((Radix(k) *((q * icn2) mod f))
+ ((q * c2.1) mod f)) mod f by A7,Th2;
n <= n + (1 - 1);
then A78: n <= (n+1) - 1 by XCMPLX_1:29;
n+1 >= 1 by NAT_1:29;
then 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 A5,A78,Def7;
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 A24,
A42
.= (Radix(k)*((q * icn) mod f) + Table1(q,c,f,(n+1) -'n)) mod f
by A5,A7,A66,A76
.= (Radix(k)*((q * icn2) mod f) + Table1(q,c,f,(n+1) -'n)) mod f
by A20,Th13
.= (Radix(k)*((q * icn2) mod f) + Table1(q,c,f,1)) mod f by BINARITH:39
.= ((Radix(k)*((q * icn2) mod f)) + ((q*DigA(c,1)) mod f)) mod f by Def6
.= ((Radix(k)*((q * icn2) mod f)) + ((q*c2.1) mod f)) mod f
by A9,A23,RADIX_1:def 3;
hence thesis by A77;
end;
for n be Nat st n >= 1 holds PP[n] from Ind1(A1,A4);
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) -> Nat equals
:Def8:
(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 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,n-'$1)) mod f;
A2: for i be Nat st 1 <= i & i < n holds for x be Element of NAT
ex y be Element of NAT st PP[i,x,y]
proof
let i be Nat;
assume 1 <= i & i < n;
let x be Element of NAT;
reconsider x as Nat;
consider y be 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 = n & (r.1 = T or n = 0) and
A5:for i be Nat st 1 <= i & i < n holds PP[i,r.i,r.(i+1)]
from FinRecExD(A2);
reconsider r as Tuple of n,NAT by A4,FINSEQ_2:110;
take r;
thus r.1 = Table2(m,e,f,n) by A1,A4;
let i be Nat;
assume 1 <= i & i <= n - 1;
then 1 <= i & i < n by SPPOL_1:5;
hence thesis by A5;
end;
uniqueness
proof
let s1,s2 be Tuple of n,NAT such that
A6: s1.1 = Table2(m,e,f,n) &
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
A7: s2.1 = Table2(m,e,f,n) &
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;
A8: len s1 = n by FINSEQ_2:109;
then A9:len s1 = len s2 by FINSEQ_2:109;
defpred P[Nat] means 1 <= $1 & $1 <= n - 1 implies s1.$1 = s2.$1;
A10: P[0];
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;
assume A13: 1 <= kk + 1 & kk + 1 <= n - 1;
A14:0 = kk or 0 < kk & 0 + 1 = 1 by NAT_1:19;
per cases by A14,NAT_1:38;
suppose 0 = kk;
hence s1.(kk+1) = s2.(kk+1) by A6,A7;
suppose
A15: 1 <= kk;
A16: kk <= kk + 1 by NAT_1:29;
then A17: 1 <= kk & kk <= n - 1 by A13,A15,AXIOMS:22;
then consider i1,i2 be Nat such that
A18: i1 = s1.kk & i2 = s1.(kk+1) &
i2 = (((i1 |^ Radix(k)) mod f)*Table2(m,e,f,n-'kk)) mod f by A6;
consider i1,i2 be Nat such that
A19: i1 = s2.kk & i2 = s2.(kk+1) &
i2 = (((i1 |^ Radix(k)) mod f)*Table2(m,e,f,n-'kk)) mod f
by A7,A17;
thus s1.(kk+1) = s2.(kk+1) by A12,A13,A15,A16,A18,A19,AXIOMS:22;
end;
A20:for kk be Nat holds P[kk] from Ind (A10,A11);
A21:s1.n = s2.n
proof
A22: n - 1 >= 1 - 1 by A1,REAL_1:49;
then reconsider U1 = n - 1 as Nat by INT_1:16;
n = n + - 1 + 1 by XCMPLX_1:139;
then A23:n = n - 1 + 1 by XCMPLX_0:def 8;
now per cases by A22;
suppose U1 = 0;
then 0 + 1 = n by XCMPLX_1:27;
hence thesis by A6,A7;
suppose 0 < U1;
then A24:1 <= U1 & U1 <= U1 by RLVECT_1:99;
then consider i1,i2 be Nat such that
A25:i1 = s1.U1 & i2 = s1.(U1+1) and
A26:i2 = (((i1 |^ Radix(k)) mod f)*Table2(m,e,f,n-'U1)) mod f
by A6;
consider j1,j2 be Nat such that
A27:j1 = s2.U1 & j2 = s2.(U1+1) and
A28:j2 = (((j1 |^ Radix(k)) mod f)*Table2(m,e,f,n-'U1)) mod f
by A7,A24;
thus thesis by A20,A23,A24,A25,A26,A27,A28;
end;
hence thesis;
end;
for kk be Nat st 1 <= kk & kk <= len s1 holds s1.kk = s2.kk
proof
let kk be Nat;
assume A29:1 <= kk & kk <= len s1;
now per cases by A29,AXIOMS:21;
suppose A30:kk < len s1;
n - 1 >= 1 - 1 by A1,REAL_1:49;
then reconsider U1 = len s1 - 1 as Nat by A8,INT_1:16;
U1 + 1 = len s1 by XCMPLX_1:27;
then kk <= U1 by A30,NAT_1:38;
hence s1.kk = s2.kk by A8,A20,A29;
suppose kk = len s1;
hence s1.kk = s2.kk by A8,A21;
end;
hence thesis;
end;
hence s1 = s2 by A9,FINSEQ_1:18;
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:PP[1]
proof
let m,k,f,ie be Nat;
assume A2: ie is_represented_by 1,k & f>0;
let e be Tuple of 1,NAT;
assume A3: e = DecSD2(ie,1,k);
ie < (Radix(k) |^ 1) by A2,RADIX_1:def 12;
then A4: ie < Radix(k) by NEWTON:10;
A5:1 - 1 = 0;
A6: 1 in Seg 1 by FINSEQ_1:4,TARSKI:def 1;
len DecSD2(ie,1,k) = 1 by FINSEQ_2:109;
then 1 in dom DecSD2(ie,1,k) by A6,FINSEQ_1:def 3;
then e/.1 = DecSD2(ie,1,k).1 by A3,FINSEQ_4:def 4
.= DigitDC2(ie,1,k) by A6,Def5
.= (ie mod (Radix(k) |^ 1)) div (Radix(k) |^ (1 -'1)) by Def4
.= (ie mod (Radix(k) |^ 1)) div (Radix(k) |^ 0) by A5,BINARITH:def 3
.= (ie mod (Radix(k) |^ 1)) div 1 by NEWTON:9
.= ie mod (Radix(k) |^ 1) by NAT_2:6
.= ie mod Radix(k) by NEWTON:10
.= ie by A4,GR_CY_1:4;
then (m |^ ie) mod f = Table2(m,e,f,1) by Def8;
hence thesis by Def9;
end;
A7:for n be Nat st n >= 1 & PP[n] holds PP[n+1]
proof
let n be Nat;
assume A8: n >= 1 & PP[n];
A9: n+1 >= 1 by NAT_1:37;
let m,k,f,ie be Nat;
assume A10: ie is_represented_by (n+1),k & f>0;
let e be Tuple of (n+1),NAT;
assume A11: e = DecSD2(ie,(n+1),k);
deffunc F(Nat)=e.($1+1);
consider en being FinSequence of NAT such that
A12: len en = n and
A13: for i be Nat st i in Seg n holds en.i = F(i) from SeqLambdaD;
reconsider en as Tuple of n,NAT by A12,FINSEQ_2:110;
1 in Seg 1 by FINSEQ_1:4,TARSKI:def 1;
then A14:1 in Seg (1+n) by FINSEQ_2:9;
A15: n in Seg n by A8,FINSEQ_1:3;
A16: (n+1) in Seg (n+1) by A9,FINSEQ_1:3;
A17: for i be 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;
A18: Z[0] by FINSEQ_1:3;
A19: for i be Nat st Z[i] holds Z[i+1]
proof let i be Nat;
assume A20: i in Seg n implies
Pow_mod(m,en,f,k).i = Pow_mod(m,e,f,k).i;
assume A21: (i+1) in Seg n;
then 1 <= (i+1) & (i+1) <= n by FINSEQ_1:3;
then A22:(i+1)-1 <= n - 1 by REAL_1:49;
then A23: i <= n - 1 by XCMPLX_1:26;
(i=0 or i>0) by NAT_1:19;
then A24:(i=0 or i+1>1+0) by REAL_1:53;
A25: dom en = Seg n by A12,FINSEQ_1:def 3;
A26:dom e = Seg (len e) by FINSEQ_1:def 3;
then A27: dom e = Seg (n+1) by FINSEQ_2:109;
now per cases by A24,NAT_1:38;
case A28: i=0;
then Pow_mod(m,en,f,k).(i+1)
= Table2(m,en,f,n) by A8,Def9
.= (m |^ (en/.n)) mod f by Def8
.= (m |^ (en.n)) mod f by A15,A25,FINSEQ_4:def 4
.= (m |^ (e.(n+1))) mod f by A13,A15
.= (m |^ (e/.(n+1))) mod f by A16,A27,FINSEQ_4:def 4
.= Table2(m,e,f,n+1) by Def8
.= Pow_mod(m,e,f,k).1 by A9,Def9;
hence Pow_mod(m,en,f,k).(i+1) = Pow_mod(m,e,f,k).(i+1) by A28;
case A29: i>=1;
reconsider nn = n - 1 as Nat by A8,INT_1:18;
A30: 1 <= i & i <= n - 1 by A22,A29,XCMPLX_1:26;
A31:1 <= i & i <= nn + 1 by A23,A29,NAT_1:37;
then A32: 1 <= i & i <= n by XCMPLX_1:27;
A33: 1 <= i & i <= (n+1)-1 by A31,XCMPLX_1:29;
A34: 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 A8,A30,Def9;
A35: 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 A9,A33,Def9;
i + 1 <= n - 1 + 1 by A30,AXIOMS:24;
then 1 + i <= n by XCMPLX_1:27;
then 1 + i - i <= n - i by REAL_1:49;
then 1 <= n - i by XCMPLX_1:26;
then A36: 1 <= n -' i by A32,SCMFSA_7:3;
n -' i <= n by GOBOARD9:2;
then A37: (n -' i) in Seg n by A36,FINSEQ_1:3;
then A38: (n -' i) in dom en by A12,FINSEQ_1:def 3;
A39: (n+1) -' i <= n+1 by GOBOARD9:2;
i+1 <= n by A21,FINSEQ_1:3;
then i+1-1 <= n-1 by REAL_1:49;
then i <= n-1 by XCMPLX_1:26;
then A40: (n+1)-'i >= (n+1)-'nn by JORDAN3:4;
(n+1)-'nn >= (n+1)-nn by JORDAN3:3;
then A41: (n+1)-'i >= (n+1)-(n-1) by A40,AXIOMS:22;
(n+1)-(n-1) = (n+1)-n+1 by XCMPLX_1:37
.= 1+(n-n)+1 by XCMPLX_1:29
.= 1+0+1 by XCMPLX_1:14;
then 1 <= (n+1)-'i by A41,AXIOMS:22;
then ((n+1)-'i) in Seg (n+1) by A39,FINSEQ_1:3;
then A42: ((n+1) -' i) in dom e by A26,FINSEQ_2:109;
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 A20,A32,A34,Def8,FINSEQ_1:3
.= ((((Pow_mod(m,e,f,k).i) |^ Radix(k)) mod f)
* ((m |^ (en.(n-'i))) mod f)) mod f by A38,FINSEQ_4:def 4
.= ((((Pow_mod(m,e,f,k).i) |^ Radix(k)) mod f)
* ((m |^ (e.(n-'i+1))) mod f)) mod f by A13,A37
.= ((((Pow_mod(m,e,f,k).i) |^ Radix(k)) mod f)
* ((m |^ (e.((n+1) -'i))) mod f)) mod f by A32,JORDAN4:3
.= ((((Pow_mod(m,e,f,k).i) |^ Radix(k)) mod f)
* ((m |^ (e/.((n+1) -'i))) mod f)) mod f by A42,FINSEQ_4:def 4
.= ((((Pow_mod(m,e,f,k).i) |^ Radix(k)) mod f)
* Table2(m,e,f,(n+1)-'i)) mod f by Def8;
hence Pow_mod(m,en,f,k).(i+1)=Pow_mod(m,e,f,k).(i+1) by A35;
end;
hence Pow_mod(m,en,f,k).(i+1) = Pow_mod(m,e,f,k).(i+1);
end;
for i be Nat holds Z[i] from Ind(A18,A19);
hence thesis;
end;
n <> 0 by A8;
then A43: n in Seg n by FINSEQ_1:5;
set ien = SDDec2(en,k);
A44: ie = ien*Radix(k) + (e/.1)
proof
reconsider r2 = Radix(k) as Element of REAL;
deffunc F(Nat)=DigitSD2(en,k).$1;
consider rD being FinSequence of REAL such that
A45: len rD = n and
A46: for i be Nat st i in Seg n holds rD.i = F(i)
from SeqLambdaD;
reconsider rD as Tuple of n,REAL by A45,FINSEQ_2:110;
A47: dom DigitSD2(en,k) = Seg (len DigitSD2(en,k)) by FINSEQ_1:def 3
.= Seg n by FINSEQ_2:109;
A48: dom rD = Seg n by A45,FINSEQ_1:def 3;
A49:1 - 1 = 0;
A50: DigitSD2(e,k) = <*SubDigit2(e,1,k)*>^(Radix(k)*DigitSD2(en,k))
proof
A51:len DigitSD2(e,k) = n+1 by FINSEQ_2:109;
A52:len (Radix(k) * DigitSD2(en,k))
= len (r2 * rD) by A46,A47,A48,FINSEQ_1:17
.= n by FINSEQ_2:109;
A53:len <*SubDigit2(e,1,k)*> = 1 by FINSEQ_1:56;
A54:len (<*SubDigit2(e,1,k)*> ^ (Radix(k) * DigitSD2(en,k)))
= len <*SubDigit2(e,1,k)*> + len (Radix(k) * DigitSD2(en,k))
by FINSEQ_1:35
.= n+1 by A52,FINSEQ_2:109;
then A55:len DigitSD2(e,k)
= len (<*SubDigit2(e,1,k)*> ^ (Radix(k) * DigitSD2(en,k)))
by FINSEQ_2:109;
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 A56:1 <= i & i <= len DigitSD2(e,k);
then A57:i <= n+1 by FINSEQ_2:109;
then A58:i in Seg (n+1) by A56,FINSEQ_1:3;
then A59: i in dom DigitSD2(e,k) by A51,FINSEQ_1:def 3;
per cases;
suppose A60:i = 1;
then (<*SubDigit2(e,1,k)*> ^ (Radix(k)*DigitSD2(en,k))).i
= SubDigit2(e,1,k) by FINSEQ_1:58
.= (DigitSD2(e,k))/.1 by A14,Def2
.= DigitSD2(e,k).1 by A59,A60,FINSEQ_4:def 4;
hence thesis by A60;
suppose A61:i<>1;
1-1 <= i-1 by A56,REAL_1:49;
then reconsider i1 = i-1 as Nat by INT_1:16;
1<i by A56,A61,REAL_1:def 5;
then 1+1<=i by INT_1:20;
then A62: 1+1-1<=i-1 by REAL_1:49;
i-1<=n+1-1 by A57,REAL_1:49;
then A63:i-1<=n by XCMPLX_1:26;
then A64: i1 in Seg n by A62,FINSEQ_1:3;
A65: i1 in dom rD by A48,A62,A63,FINSEQ_1:3;
then reconsider rs = rD.(i-1) as Real by FINSEQ_2:13;
reconsider rs2 = DigitSD2(en,k).(i-1) as Nat
by A47,A48,A65,FINSEQ_2:13;
1 < i by A56,A61,REAL_1:def 5;
then (<*SubDigit2(e,1,k)*> ^ (Radix(k)*DigitSD2(en,k))).i
=(Radix(k)*DigitSD2(en,k)).(i - 1) by A53,A54,A57,FINSEQ_1:37
.=(r2*rD).(i-1) by A46,A47,A48,FINSEQ_1:17
.=r2*rs by A64,RVSUM_1:67
.=Radix(k)*rs2 by A46,A47,A48,FINSEQ_1:17
.=Radix(k)*((DigitSD2(en,k))/.i1)
by A47,A48,A65,FINSEQ_4:def 4
.=Radix(k)*SubDigit2(en,i1,k) by A64,Def2
.=Radix(k)*((Radix(k) |^ (i1-'1))*(en.i1)) by Def1
.=Radix(k)*(Radix(k) |^ (i1-'1))*(en.i1) by XCMPLX_1:4
.=(Radix(k) |^ (i1-'1+1))*(en.i1) by NEWTON:11
.=(Radix(k) |^ i1)*(en.i1) by A62,AMI_5:4
.=(Radix(k) |^ i1)*(e.(i1+1)) by A13,A64
.=(Radix(k) |^ (i-'1))*(e.(i1+1)) by A56,SCMFSA_7:3
.=(Radix(k) |^ (i-'1))*(e.i) by XCMPLX_1:27
.=SubDigit2(e,i,k) by Def1
.=(DigitSD2(e,k))/.i by A58,Def2;
hence thesis by A59,FINSEQ_4:def 4;
end;
hence thesis by A55,FINSEQ_1:18;
end;
dom e = Seg (len e) by FINSEQ_1:def 3;
then A66: 1 in dom e by A14,FINSEQ_2:109;
ie = SDDec2(e,k) by A9,A10,A11,Th15
.= Sum DigitSD2(e,k) by Def3
.= SubDigit2(e,1,k) + Sum(Radix(k) * DigitSD2(en,k)) by A50,RVSUM_1:106
.= SubDigit2(e,1,k) + Sum(r2 * rD) by A46,A47,A48,FINSEQ_1:17
.= SubDigit2(e,1,k) + r2 * Sum(rD) by RVSUM_1:117
.= SubDigit2(e,1,k) + Radix(k) * Sum(DigitSD2(en,k))
by A46,A47,A48,FINSEQ_1:17
.= SubDigit2(e,1,k) + Radix(k) * SDDec2(en,k) by Def3
.= (Radix(k) |^ (1 -' 1))*(e.1) + Radix(k) * ien by Def1
.= (Radix(k) |^ 0)*(e.1) + Radix(k) * ien by A49,BINARITH:def 3
.= 1*(e.1) + Radix(k) * ien by NEWTON:9;
hence thesis by A66,FINSEQ_4:def 4;
end;
then A67: ie >= ien * Radix(k) by INT_1:19;
A68: Radix(k) > 0 by Th6;
ie < (Radix(k) |^ (n+1)) by A10,RADIX_1:def 12;
then ien * Radix(k) < (Radix(k) |^ (n+1)) by A67,AXIOMS:22;
then ien * Radix(k) < (Radix(k) |^ n)* Radix(k) by NEWTON:11;
then ien < (Radix(k) |^ n) by A68,AXIOMS:25;
then A69: ien is_represented_by n,k by RADIX_1:def 12;
A70: en = DecSD2(ien,n,k)
proof
A71:len en = len DecSD2(ien,n,k) by A12,FINSEQ_2:109;
for i be Nat st 1 <= i & i <= len en holds en.i=DecSD2(ien,n,k).i
proof
let i be Nat;
assume A72: 1 <= i & i <= len en;
then A73: i in Seg n by A12,FINSEQ_1:3;
A74:i <= i+1 by REAL_1:69;
then 1 <= (i+1) & (i+1) <= (n+1) by A12,A72,AXIOMS:22,24;
then A75: (i+1) in Seg (n+1) by FINSEQ_1:3;
e.1 = DigitDC2(ie,1,k) by A11,A14,Def5
.= (ie mod (Radix(k) |^ 1)) div (Radix(k) |^ (1 -' 1)) by Def4
.= (ie mod (Radix(k) |^ 1)) div (Radix(k) |^ 0) by GOBOARD9:1
.= (ie mod (Radix(k) |^ 1)) div 1 by NEWTON:9
.= ie mod (Radix(k) |^ 1) by NAT_2:6
.= ie mod Radix(k) by NEWTON:10;
then A76: e.1 < Radix(k) by A68,NAT_1:46;
dom e = Seg (len e) by FINSEQ_1:def 3;
then A77:dom e = Seg (n+1) by FINSEQ_2:109;
A78:1 <= i+1 & 0 < Radix(k) by A72,A74,Th6,AXIOMS:22;
A79:Radix(k) <> 0 & i <> 0 by A72,Th6;
reconsider a = e.1 as Integer;
reconsider b = ien as Integer;
reconsider G = a + b*Radix(k) as Integer;
A80:(e.1 + ien*Radix(k)) div Radix(k)
= G div Radix(k) by SCMFSA9A:5
.= [\(e.1 + ien*Radix(k))/Radix(k)/] by INT_1:def 7
.= [\e.1/Radix(k) + ien/] by A78,XCMPLX_1:114
.= [\e.1/Radix(k)/] + ien by INT_1:51
.= a div Radix(k) + ien by INT_1:def 7
.= (e.1) div Radix(k) + ien by SCMFSA9A:5
.= 0 + ien by A76,JORDAN4:5;
en.i
= e.(i+1) by A13,A73
.= DigitDC2(ie,(i+1),k) by A11,A75,Def5
.= (ie mod (Radix(k) |^ (i+1))) div (Radix(k) |^ ((i+1) -'1)) by Def4
.= ((ien*Radix(k) + (e/.1)) div (Radix(k) |^ ((i+1)-'1)))
mod Radix(k) by A44,A78,Th4
.= ((ien*Radix(k) + e.1) div (Radix(k) |^ ((i+1)-'1)))
mod Radix(k)
by A14,A77,FINSEQ_4:def 4
.= ((ien*Radix(k) + e.1) div (Radix(k) |^ i))
mod Radix(k) by BINARITH:39
.= ((ien*Radix(k) + e.1) div (Radix(k)*(Radix(k) |^ (i -'1))))
mod Radix(k) by A79,PEPIN:27
.= (((e.1 + ien*Radix(k)) div Radix(k)) div (Radix(k) |^ (i -'1)))
mod Radix(k) by NAT_2:29
.= (ien mod (Radix(k) |^ i)) div (Radix(k) |^ (i -'1)) by A72,A78,A80,
Th4
.= DigitDC2(ien,i,k) by Def4;
hence thesis by A73,Def5;
end;
hence thesis by A71,FINSEQ_1:18;
end;
n <= n + (1 - 1);
then A81: n <= (n+1) - 1 by XCMPLX_1:29;
n+1 >= 1 by NAT_1:29;
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 A8,A81,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 A17,A43
.= (((((m |^ ien) mod f) |^ Radix(k)) mod f)
*Table2(m,e,f,(n+1)-'n)) mod f by A8,A10,A69,A70
.= ((((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:10
.= (m |^ (ien*Radix(k))*Table2(m,e,f,(n+1)-'n)) mod f by NEWTON:14
.= (m |^ (ien*Radix(k))*Table2(m,e,f,1)) mod f by BINARITH:39
.= (m |^ (ien*Radix(k))*((m |^ (e/.1)) mod f)) mod f by Def8
.= (m |^ (ien*Radix(k))*(m |^ (e/.1))) mod f by EULER_2:9
.= (m |^ (ien*Radix(k) + (e/.1))) mod f by NEWTON:13;
hence thesis by A44;
end;
for n be Nat st n >= 1 holds PP[n] from Ind1(A1,A7);
hence thesis;
end;