let n, m be Element of NAT ; ( 0 < n implies ALGO_BPOW (0,n,m) = 0 )
assume AS:
0 < n
; ALGO_BPOW (0,n,m) = 0
consider A, B being sequence of NAT such that
ASC:
( ALGO_BPOW (0,n,m) = B . (LenBSeq n) & A . 0 = 0 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;
(LenBSeq n) - 1 in NAT
by INT_1:5, NAT_1:14;
then reconsider fs = (LenBSeq n) - 1 as Nat ;
QW: A . fs =
(0 to_power (2 to_power fs)) mod m
by CBPOW1, ASC
.=
0 mod m
by POWER:42
;
ALGO_BPOW (0,n,m) =
BinBranch ((B . fs),(((B . fs) * (A . fs)) mod m),((Nat2BL . n) . (fs + 1)))
by ASC
.=
BinBranch ((B . fs),(((B . fs) * (A . fs)) mod m),1)
by MMS1, AS
.=
0
by QW, defBB
;
hence
ALGO_BPOW (0,n,m) = 0
; verum