:: deftheorem Def30 defines DES-CoDec DESCIP_1:def 30 :
for RK being Element of 16 -tuples_on (48 -tuples_on BOOLEAN)
for F being Function of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):],(32 -tuples_on BOOLEAN)
for IP being Permutation of (64 -tuples_on BOOLEAN)
for M, b₅ being Element of 64 -tuples_on BOOLEAN holds
( b₅ = DES-CoDec (M,F,IP,RK) iff ex IPX being Permutation of ((2 * 32) -tuples_on BOOLEAN) ex MX being Element of (2 * 32) -tuples_on BOOLEAN st
( IPX = IP & MX = M & b₅ = DES-like-CoDec (MX,F,IPX,RK) ) );