:: deftheorem Def1 defines ALGO_BPOW NTALGO_2:def 2 :
for a, n, m, b₄ being Element of NAT holds
( b₄ = ALGO_BPOW (a,n,m) iff ex A, B being sequence of NAT st
( b₄ = 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))) ) ) ) );