let a, n, m be Element of NAT ; ( a <> 0 & 1 < m implies ALGO_BPOW (a,n,m) = (a to_power n) mod m )
assume AS:
( a <> 0 & 1 < m )
; ALGO_BPOW (a,n,m) = (a to_power n) mod m
consider A, B being sequence of NAT such that
ASC:
( ALGO_BPOW (a,n,m) = B . (LenBSeq n) & A . 0 = a mod m & B . 0 = 1 & ( for i being Nat holds
( A . (i + 1) = ((A . i) * (A . i)) mod m & B . (i + 1) = BinBranch ((B . i),(((B . i) * (A . i)) mod m),((Nat2BL . n) . (i + 1))) ) ) )
by Def1;
set NBS = Nat2BL . n;
Nat2BL . n = (LenBSeq n) -BinarySequence n
by BINARI_6:def 2;
then reconsider NBS = Nat2BL . n as Tuple of LenBSeq n, BOOLEAN ;
defpred S1[ Nat] means ( $1 < LenBSeq n implies ex SUBBS being Tuple of $1 + 1, BOOLEAN st
( SUBBS = (Nat2BL . n) | ($1 + 1) & B . ($1 + 1) = (a to_power (Absval SUBBS)) mod m ) );
LC1:
S1[ 0 ]
LC2:
for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume ASPi:
S1[
i]
;
S1[i + 1]
assume I1:
i + 1
< LenBSeq n
;
ex SUBBS being Tuple of (i + 1) + 1, BOOLEAN st
( SUBBS = (Nat2BL . n) | ((i + 1) + 1) & B . ((i + 1) + 1) = (a to_power (Absval SUBBS)) mod m )
i < LenBSeq n
then consider SUBBS being
Tuple of
i + 1,
BOOLEAN such that CLa:
(
SUBBS = (Nat2BL . n) | (i + 1) &
B . (i + 1) = (a to_power (Absval SUBBS)) mod m )
by ASPi;
set j =
i + 1;
thus
ex
SUBBS1 being
Tuple of
(i + 1) + 1,
BOOLEAN st
(
SUBBS1 = (Nat2BL . n) | ((i + 1) + 1) &
B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m )
verumproof
LINT:
(i + 1) + 1
<= LenBSeq n
by INT_1:7, I1;
1
<= (i + 1) + 1
by NAT_1:11;
then
(i + 1) + 1
in Seg (LenBSeq n)
by LINT;
then CHO:
(i + 1) + 1
in dom NBS
by FINSEQ_1:89;
set SUBBS1 =
(Nat2BL . n) | ((i + 1) + 1);
Lhyo:
(i + 1) + 1
<= len NBS
by FINSEQ_3:153, LINT;
Sho:
(Nat2BL . n) | ((i + 1) + 1) is
Element of
BOOLEAN *
by FINSEQ_1:def 11;
len ((Nat2BL . n) | ((i + 1) + 1)) = min (
((i + 1) + 1),
(len NBS))
by FINSEQ_2:21;
then
len ((Nat2BL . n) | ((i + 1) + 1)) = (i + 1) + 1
by Lhyo, XXREAL_0:def 9;
then
(Nat2BL . n) | ((i + 1) + 1) in ((i + 1) + 1) -tuples_on BOOLEAN
by Sho;
then reconsider SUBBS1 =
(Nat2BL . n) | ((i + 1) + 1) as
Tuple of
(i + 1) + 1,
BOOLEAN ;
set BC =
IFEQ (
(NBS . ((i + 1) + 1)),
FALSE,
0,
(2 to_power (i + 1)));
CCL2:
SUBBS1 = SUBBS ^ <*(NBS . ((i + 1) + 1))*>
by FINSEQ_5:10, CLa, CHO;
PO:
NBS . ((i + 1) + 1) is
Element of
BOOLEAN
by FINSEQ_1:84, CHO;
reconsider X =
NBS . ((i + 1) + 1) as
Nat ;
ZZ:
Absval SUBBS1 = (Absval SUBBS) + (IFEQ ((NBS . ((i + 1) + 1)),FALSE,0,(2 to_power (i + 1))))
by BINARITH:20, CCL2, PO;
LMT1:
B . ((i + 1) + 1) = BinBranch (
(B . (i + 1)),
(((B . (i + 1)) * (A . (i + 1))) mod m),
X)
by ASC;
take
SUBBS1
;
( SUBBS1 = (Nat2BL . n) | ((i + 1) + 1) & B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m )
thus
SUBBS1 = (Nat2BL . n) | ((i + 1) + 1)
;
B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m
thus
B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m
verum
end;
end;
LC3:
for i being Nat holds S1[i]
from NAT_1:sch 2(LC1, LC2);
(LenBSeq n) - 1 in NAT
by INT_1:5, NAT_1:14;
then reconsider fs = (LenBSeq n) - 1 as Nat ;
consider FSBS being Tuple of fs + 1, BOOLEAN such that
Lcfs:
( FSBS = (Nat2BL . n) | (fs + 1) & B . (fs + 1) = (a to_power (Absval FSBS)) mod m )
by LC3, XREAL_1:44;
reconsider FSBS = FSBS as Tuple of LenBSeq n, BOOLEAN ;
dom NBS = Seg (LenBSeq n)
by FINSEQ_1:89;
hence
ALGO_BPOW (a,n,m) = (a to_power n) mod m
by ASC, BINARI_6:10, Lcfs; verum