:: Maximum Number of Steps Taken by Modular Exponentiation and Euclidean Algorithm
:: by Hiroyuki Okazaki , Koich Nagao and Yuichi Futa
::
:: Received March 11, 2019
:: Copyright (c) 2019-2021 Association of Mizar Users


definition
let F be Element of BOOLEAN * ;
let x be object ;
:: original: .
redefine func F . x -> Nat;
correctness
coherence
F . x is Nat;
;
end;

definition
let n, m be Nat;
:: original: to_power
redefine func n to_power m -> Nat;
coherence
n to_power m is Nat ;
end;

definition
let a, b be object ;
let c be Nat;
func BinBranch (a,b,c) -> object equals :defBB: :: NTALGO_2:def 1
a if c = 0
otherwise b;
correctness
coherence
( ( c = 0 implies a is object ) & ( not c = 0 implies b is object ) );
consistency
for b1 being object holds verum;
;
end;

:: deftheorem defBB defines BinBranch NTALGO_2:def 1 :
for a, b being object
for c being Nat holds
( ( c = 0 implies BinBranch (a,b,c) = a ) & ( not c = 0 implies BinBranch (a,b,c) = b ) );

definition
let a, b, c be Nat;
:: original: BinBranch
redefine func BinBranch (a,b,c) -> Nat;
coherence
BinBranch (a,b,c) is Nat by defBB;
end;

Lm1: for a, n, m being Element of NAT ex A, B being sequence of NAT st
( 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))) ) ) )
proof end;

Lm2: for a, n, m being Element of NAT
for A1, B1, A2, B2 being sequence of NAT st A1 . 0 = a & B1 . 0 = 1 & ( for i being Nat holds
( A1 . (i + 1) = ((A1 . i) * (A1 . i)) mod m & B1 . (i + 1) = BinBranch ((B1 . i),(((B1 . i) * (A1 . i)) mod m),((Nat2BL . n) . (i + 1))) ) ) & A2 . 0 = a & B2 . 0 = 1 & ( for i being Nat holds
( A2 . (i + 1) = ((A2 . i) * (A2 . i)) mod m & B2 . (i + 1) = BinBranch ((B2 . i),(((B2 . i) * (A2 . i)) mod m),((Nat2BL . n) . (i + 1))) ) ) holds
( A1 = A2 & B1 = B2 )
proof end;

definition
let a, n, m be Element of NAT ;
func ALGO_BPOW (a,n,m) -> Element of NAT means :Def1: :: NTALGO_2:def 2
 ex A, B being sequence of NAT st
( it = 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))) ) ) );
existence
ex b1 being Element of NAT ex A, B being sequence of NAT st
( b1 = 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))) ) ) )
proof end;
uniqueness
for b1, b2 being Element of NAT st ex A, B being sequence of NAT st
( b1 = 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))) ) ) ) & ex A, B being sequence of NAT st
( b2 = 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))) ) ) ) holds
b1 = b2 by Lm2;
end;

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

theorem CBPOW1: :: NTALGO_2:1
for a, m, i being Nat
for A being sequence of NAT st A . 0 = a mod m & ( for j being Nat holds A . (j + 1) = ((A . j) * (A . j)) mod m ) holds
A . i = (a to_power (2 to_power i)) mod m
proof end;

CBPOW2: for a, m, i, n being Nat
for A being sequence of NAT st a <> 0 & A . 0 = a mod m & ( for j being Nat holds A . (j + 1) = ((A . j) * (A . j)) mod m ) holds
(((a to_power n) mod m) * (A . i)) mod m = (a to_power (n + (2 to_power i))) mod m
proof end;

theorem :: NTALGO_2:2
LenBSeq 0 = 1 by BINARI_6:def 1;

theorem EXL1: :: NTALGO_2:3
LenBSeq 1 = 1
proof end;

theorem :: NTALGO_2:4
for x being Nat st 2 <= x holds
1 < LenBSeq x
proof end;

theorem EXL2: :: NTALGO_2:5
for n being Nat st 0 < n holds
LenBSeq n = [\(log (2,n))/] + 1
proof end;

theorem zerobs: :: NTALGO_2:6
Nat2BL . 0 = <*0*>
proof end;

theorem :: NTALGO_2:7
Nat2BL . 1 = <*1*>
proof end;

theorem MMS1: :: NTALGO_2:8
for n being Element of NAT st 0 < n holds
(Nat2BL . n) . (LenBSeq n) = 1
proof end;

theorem :: NTALGO_2:9
Nat2BL . 2 = <*0,1*>
proof end;

theorem :: NTALGO_2:10
Nat2BL . 3 = <*1,1*>
proof end;

theorem :: NTALGO_2:11
Nat2BL . 4 = <*0,0,1*>
proof end;

theorem :: NTALGO_2:12
for n being Nat holds Nat2BL . (2 |^ n) = (0* n) ^ <*1*>
proof end;

theorem :: NTALGO_2:13
for m being Element of NAT holds ALGO_BPOW (0,0,m) = 1
proof end;

theorem :: NTALGO_2:14
for n, m being Element of NAT st 0 < n holds
ALGO_BPOW (0,n,m) = 0
proof end;

theorem :: NTALGO_2:15
for a, n, m being Element of NAT st 0 < n & m <= 1 holds
ALGO_BPOW (a,n,m) = 0
proof end;

theorem :: NTALGO_2:16
for a, n, m being Element of NAT st a <> 0 & 1 < m holds
ALGO_BPOW (a,n,m) = (a to_power n) mod m
proof end;

theorem LFIB5: :: NTALGO_2:17
Fib 5 = 5
proof end;

theorem THTU: :: NTALGO_2:18
1 < tau
proof end;

theorem THTU2: :: NTALGO_2:19
tau < 2
proof end;

theorem THTU3: :: NTALGO_2:20
log (tau,10) < 5
proof end;

theorem LTAUPOW: :: NTALGO_2:21
for n being Nat st 3 <= n holds
tau to_power (n - 2) < Fib n
proof end;

theorem :: NTALGO_2:22
for a, b being Element of INT st |.a.| > |.b.| & b > 1 holds
ex A, B being sequence of NAT ex C being Real_Sequence ex n being Element of NAT st
( A . 0 = |.a.| & B . 0 = |.b.| & ( for i being Nat holds
( A . (i + 1) = B . i & B . (i + 1) = (A . i) mod (B . i) ) ) & n = min* { i where i is Nat : B . i = 0 } & a gcd b = A . n & Fib (n + 1) <= |.b.| & n <= 5 * [/(log (10,|.b.|))\] & n <= C . |.b.| & C is polynomially-bounded )
proof end;