let a, n, m be 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))) ) ) )
defpred S1[ Nat, Nat, Nat, Nat, Nat] means ( $4 = ($2 * $2) mod m & $5 = BinBranch ($3,(($3 * $2) mod m),((Nat2BL . n) . ($1 + 1))) );
A1:
for i being Nat
for x, y being Element of NAT ex x1, y1 being Element of NAT st S1[i,x,y,x1,y1]
proof
let i be
Nat;
for x, y being Element of NAT ex x1, y1 being Element of NAT st S1[i,x,y,x1,y1]let x,
y be
Element of
NAT ;
ex x1, y1 being Element of NAT st S1[i,x,y,x1,y1]
set x1 =
(x * x) mod m;
set y1 =
BinBranch (
y,
((y * x) mod m),
((Nat2BL . n) . (i + 1)));
(
(x * x) mod m is
Element of
NAT &
BinBranch (
y,
((y * x) mod m),
((Nat2BL . n) . (i + 1))) is
Element of
NAT )
by ORDINAL1:def 12;
hence
ex
x1,
y1 being
Element of
NAT st
S1[
i,
x,
y,
x1,
y1]
;
verum
end;
consider A, B being sequence of NAT such that
A2:
( A . 0 = a mod m & B . 0 = 1 & ( for n being Nat holds S1[n,A . n,B . n,A . (n + 1),B . (n + 1)] ) )
from RECDEF_2:sch 3(A1);
take
A
; ex 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))) ) ) )
take
B
; ( 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))) ) ) )
thus
( 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 A2; verum