:: by Hiroyuki Okazaki , Koich Nagao and Yuichi Futa

::

:: Received March 11, 2019

:: Copyright (c) 2019 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;
let x be object ;

:: original: .

redefine func F . x -> Nat;

correctness

coherence

F . x is Nat;

;

definition

let n, m be Nat;

:: original: to_power

redefine func n to_power m -> Nat;

coherence

n to_power m is Nat ;

end;
:: original: to_power

redefine func n to_power m -> Nat;

coherence

n to_power m is Nat ;

definition

let a, b be object ;

let c be Nat;

correctness

coherence

( ( c = 0 implies a is object ) & ( not c = 0 implies b is object ) );

consistency

for b_{1} being object holds verum;

;

end;
let c be Nat;

correctness

coherence

( ( c = 0 implies a is object ) & ( not c = 0 implies b is object ) );

consistency

for b

;

:: 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 ) );

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;
:: original: BinBranch

redefine func BinBranch (a,b,c) -> Nat;

coherence

BinBranch (a,b,c) is Nat by defBB;

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 ;

ex b_{1} being Element of NAT ex A, B being sequence of NAT st

( b_{1} = 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))) ) ) )

for b_{1}, b_{2} being Element of NAT st ex A, B being sequence of NAT st

( b_{1} = 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

( b_{2} = 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

b_{1} = b_{2}
by Lm2;

end;
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 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))) ) ) );

ex b

( b

( 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 b

( b

( 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

( b

( 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

b

:: deftheorem Def1 defines ALGO_BPOW NTALGO_2:def 2 :

for a, n, m, b_{4} being Element of NAT holds

( b_{4} = ALGO_BPOW (a,n,m) iff ex A, B being sequence of NAT st

( b_{4} = 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))) ) ) ) );

for a, n, m, b

( b

( b

( 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

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

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;