let m, n, k be non zero Element of NAT ; :: thesis: 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); :: thesis: 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); :: thesis: 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); :: thesis: 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; :: thesis: 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 S₁[ 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 S₁[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 S₁[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; :: thesis: verum