let a, n, m be Element of NAT ; :: thesis: ( a <> 0 & 1 < m implies ALGO_BPOW (a,n,m) = (a to_power n) mod m )

assume AS: ( a <> 0 & 1 < m ) ; :: thesis: 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 S_{1}[ 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: S_{1}[ 0 ]
_{1}[i] holds

S_{1}[i + 1]
_{1}[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; :: thesis: verum

assume AS: ( a <> 0 & 1 < m ) ; :: thesis: 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 S

( SUBBS = (Nat2BL . n) | ($1 + 1) & B . ($1 + 1) = (a to_power (Absval SUBBS)) mod m ) );

LC1: S

proof

LC2:
for i being Nat st S
NBS | (0 + 1) = <*(NBS . 1)*>
by FINSEQ_5:20;

reconsider NBS0 = NBS | (0 + 1) as Tuple of 1, BOOLEAN ;

PCJJ: B . (0 + 1) = BinBranch ((B . 0),(((B . 0) * (A . 0)) mod m),((Nat2BL . n) . (0 + 1))) by ASC;

then PCC0: B . 1 = BinBranch (1,(a mod m),((Nat2BL . n) . 1)) by EULER_2:5, ASC;

end;reconsider NBS0 = NBS | (0 + 1) as Tuple of 1, BOOLEAN ;

PCJJ: B . (0 + 1) = BinBranch ((B . 0),(((B . 0) * (A . 0)) mod m),((Nat2BL . n) . (0 + 1))) by ASC;

then PCC0: B . 1 = BinBranch (1,(a mod m),((Nat2BL . n) . 1)) by EULER_2:5, ASC;

per cases
( NBS0 = <*TRUE*> or NBS0 = <*FALSE*> )
by BINARITH:14;

end;

suppose LCT:
NBS0 = <*TRUE*>
; :: thesis: S_{1}[ 0 ]

then LCT1:
Absval NBS0 = 1
by BINARITH:16;

<*(NBS . 1)*> . 1 = <*TRUE*> . 1 by FINSEQ_5:20, LCT;

then B . 1 = (a to_power 1) mod m by defBB, PCC0, XBOOLEAN:def 2;

hence S_{1}[ 0 ]
by LCT1; :: thesis: verum

end;<*(NBS . 1)*> . 1 = <*TRUE*> . 1 by FINSEQ_5:20, LCT;

then B . 1 = (a to_power 1) mod m by defBB, PCC0, XBOOLEAN:def 2;

hence S

suppose LCF:
NBS0 = <*FALSE*>
; :: thesis: S_{1}[ 0 ]

then LCF1:
Absval NBS0 = 0
by BINARITH:15;

<*(NBS . 1)*> . 1 = <*FALSE*> . 1 by FINSEQ_5:20, LCF;

then B . 1 = 1 by defBB, ASC, PCJJ, XBOOLEAN:def 1

.= 1 mod m by NAT_D:14, AS

.= (a to_power 0) mod m by POWER:24 ;

hence S_{1}[ 0 ]
by LCF1; :: thesis: verum

end;<*(NBS . 1)*> . 1 = <*FALSE*> . 1 by FINSEQ_5:20, LCF;

then B . 1 = 1 by defBB, ASC, PCJJ, XBOOLEAN:def 1

.= 1 mod m by NAT_D:14, AS

.= (a to_power 0) mod m by POWER:24 ;

hence S

S

proof

LC3:
for i being Nat holds S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume ASPi: S_{1}[i]
; :: thesis: S_{1}[i + 1]

assume I1: i + 1 < LenBSeq n ; :: thesis: 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

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 ) :: thesis: verum

end;assume ASPi: S

assume I1: i + 1 < LenBSeq n ; :: thesis: 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

proof

then consider SUBBS being Tuple of i + 1, BOOLEAN such that
assume COV:
i >= LenBSeq n
; :: thesis: contradiction

(i + 1) - 1 < (LenBSeq n) - 0 by I1, XREAL_1:14;

hence contradiction by COV; :: thesis: verum

end;(i + 1) - 1 < (LenBSeq n) - 0 by I1, XREAL_1:14;

hence contradiction by COV; :: thesis: verum

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 ) :: thesis: verum

proof

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 ; :: thesis: ( SUBBS1 = (Nat2BL . n) | ((i + 1) + 1) & B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m )

thus SUBBS1 = (Nat2BL . n) | ((i + 1) + 1) ; :: thesis: B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m

thus B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m :: thesis: verum

end;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 ; :: thesis: ( SUBBS1 = (Nat2BL . n) | ((i + 1) + 1) & B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m )

thus SUBBS1 = (Nat2BL . n) | ((i + 1) + 1) ; :: thesis: B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m

thus B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m :: thesis: verum

proof
end;

per cases
( X = 0 or X <> 0 )
;

end;

suppose LPP:
X = 0
; :: thesis: B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m

then
IFEQ ((NBS . ((i + 1) + 1)),FALSE,0,(2 to_power (i + 1))) = 0
by FUNCOP_1:def 8, XBOOLEAN:def 1;

hence B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m by ZZ, CLa, LMT1, defBB, LPP; :: thesis: verum

end;hence B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m by ZZ, CLa, LMT1, defBB, LPP; :: thesis: verum

suppose LPP1:
X <> 0
; :: thesis: B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m

then B . ((i + 1) + 1) =
((B . (i + 1)) * (A . (i + 1))) mod m
by LMT1, defBB

.= (a to_power ((Absval SUBBS) + (2 to_power (i + 1)))) mod m by CBPOW2, ASC, AS, CLa ;

hence B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m by FUNCOP_1:def 8, XBOOLEAN:def 1, LPP1, ZZ; :: thesis: verum

end;.= (a to_power ((Absval SUBBS) + (2 to_power (i + 1)))) mod m by CBPOW2, ASC, AS, CLa ;

hence B . ((i + 1) + 1) = (a to_power (Absval SUBBS1)) mod m by FUNCOP_1:def 8, XBOOLEAN:def 1, LPP1, ZZ; :: thesis: verum

(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; :: thesis: verum