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

assume AS: ( 0 < n & m <= 1 ) ; :: thesis: ALGO_BPOW (a,n,m) = 0

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;

(LenBSeq n) - 1 in NAT by INT_1:5, NAT_1:14;

then reconsider fs = (LenBSeq n) - 1 as Nat ;

( m = 0 or m = 1 ) by NAT_1:25, AS;

then LZEROM: ((B . fs) * (A . fs)) mod m = 0 by RADIX_2:1;

ALGO_BPOW (a,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 LZEROM, defBB ;

hence ALGO_BPOW (a,n,m) = 0 ; :: thesis: verum

assume AS: ( 0 < n & m <= 1 ) ; :: thesis: ALGO_BPOW (a,n,m) = 0

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;

(LenBSeq n) - 1 in NAT by INT_1:5, NAT_1:14;

then reconsider fs = (LenBSeq n) - 1 as Nat ;

( m = 0 or m = 1 ) by NAT_1:25, AS;

then LZEROM: ((B . fs) * (A . fs)) mod m = 0 by RADIX_2:1;

ALGO_BPOW (a,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 LZEROM, defBB ;

hence ALGO_BPOW (a,n,m) = 0 ; :: thesis: verum