:: deftheorem Def29 defines DES-like-CoDec DESCIP_1:def 29 :
for n, m, k being 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, b₈ being Element of (2 * n) -tuples_on BOOLEAN holds
( b₈ = DES-like-CoDec (M,F,IP,RK) iff 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))))) ) ) & b₈ = (IP ") . ((R . k) ^ (L . k)) ) );