theorem Th30:
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 being
Element of
(2 * n) -tuples_on BOOLEAN holds
DES-like-CoDec (
(DES-like-CoDec (M,F,IP,RK)),
F,
IP,
(Rev RK))
= M