let m, n, k be non zero Element of NAT ; for RK being Element of k -tuples_on (m -tuples_on BOOLEAN)
for F being Function of [:(n -tuples_on BOOLEAN),(m -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN)
for IP being Permutation of ((2 * n) -tuples_on BOOLEAN)
for M being Element of (2 * n) -tuples_on BOOLEAN ex OUT being Element of (2 * n) -tuples_on BOOLEAN ex L, R being sequence of (n -tuples_on BOOLEAN) st
( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) ) ) & OUT = (IP ") . ((R . k) ^ (L . k)) )
let RK be Element of k -tuples_on (m -tuples_on BOOLEAN); for F being Function of [:(n -tuples_on BOOLEAN),(m -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN)
for IP being Permutation of ((2 * n) -tuples_on BOOLEAN)
for M being Element of (2 * n) -tuples_on BOOLEAN ex OUT being Element of (2 * n) -tuples_on BOOLEAN ex L, R being sequence of (n -tuples_on BOOLEAN) st
( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) ) ) & OUT = (IP ") . ((R . k) ^ (L . k)) )
let F be Function of [:(n -tuples_on BOOLEAN),(m -tuples_on BOOLEAN):],(n -tuples_on BOOLEAN); for IP being Permutation of ((2 * n) -tuples_on BOOLEAN)
for M being Element of (2 * n) -tuples_on BOOLEAN ex OUT being Element of (2 * n) -tuples_on BOOLEAN ex L, R being sequence of (n -tuples_on BOOLEAN) st
( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) ) ) & OUT = (IP ") . ((R . k) ^ (L . k)) )
let IP be Permutation of ((2 * n) -tuples_on BOOLEAN); for M being Element of (2 * n) -tuples_on BOOLEAN ex OUT being Element of (2 * n) -tuples_on BOOLEAN ex L, R being sequence of (n -tuples_on BOOLEAN) st
( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) ) ) & OUT = (IP ") . ((R . k) ^ (L . k)) )
let M be Element of (2 * n) -tuples_on BOOLEAN; ex OUT being Element of (2 * n) -tuples_on BOOLEAN ex L, R being sequence of (n -tuples_on BOOLEAN) st
( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) ) ) & OUT = (IP ") . ((R . k) ^ (L . k)) )
defpred S1[ Nat, Element of n -tuples_on BOOLEAN, Element of n -tuples_on BOOLEAN, Element of n -tuples_on BOOLEAN, Element of n -tuples_on BOOLEAN] means ( $4 = $3 & $5 = Op-XOR ($2,(F . ($3,(RK /. ($1 + 1))))) );
A1:
for k being Nat
for x, y being Element of n -tuples_on BOOLEAN ex x1, y1 being Element of n -tuples_on BOOLEAN st S1[k,x,y,x1,y1]
;
consider L, R being sequence of (n -tuples_on BOOLEAN) such that
A2:
( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for n being Nat holds S1[n,L . n,R . n,L . (n + 1),R . (n + 1)] ) )
from RECDEF_2:sch 3(A1);
A3:
for i being Nat st 0 <= i & i <= k - 1 holds
( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) )
by A2;
reconsider RL = (R . k) ^ (L . k) as Element of (2 * n) -tuples_on BOOLEAN by FINSEQ_2:131;
(IP ") . RL is Element of (2 * n) -tuples_on BOOLEAN
;
hence
ex OUT being Element of (2 * n) -tuples_on BOOLEAN ex L, R being sequence of (n -tuples_on BOOLEAN) st
( L . 0 = SP-Left (IP . M) & R . 0 = SP-Right (IP . M) & ( for i being Nat st 0 <= i & i <= k - 1 holds
( L . (i + 1) = R . i & R . (i + 1) = Op-XOR ((L . i),(F . ((R . i),(RK /. (i + 1))))) ) ) & OUT = (IP ") . ((R . k) ^ (L . k)) )
by A3, A2; verum