let RK be Element of 16 -tuples_on (48 -tuples_on BOOLEAN); :: thesis: 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 being Element of 64 -tuples_on BOOLEAN holds DES-CoDec ((DES-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = M
let F be Function of [:(32 -tuples_on BOOLEAN),(48 -tuples_on BOOLEAN):],(32 -tuples_on BOOLEAN); :: thesis: for IP being Permutation of (64 -tuples_on BOOLEAN)
for M being Element of 64 -tuples_on BOOLEAN holds DES-CoDec ((DES-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = M
let IP be Permutation of (64 -tuples_on BOOLEAN); :: thesis: for M being Element of 64 -tuples_on BOOLEAN holds DES-CoDec ((DES-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = M
let M be Element of 64 -tuples_on BOOLEAN; :: thesis: DES-CoDec ((DES-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = M
reconsider IPX = IP as Permutation of ((2 * 32) -tuples_on BOOLEAN) ;
reconsider MX = M as Element of (2 * 32) -tuples_on BOOLEAN ;
reconsider EM = DES-like-CoDec (MX,F,IPX,RK) as Element of (2 * 32) -tuples_on BOOLEAN ;
reconsider EM64 = DES-CoDec (M,F,IP,RK) as Element of 64 -tuples_on BOOLEAN ;
EM = EM64 by Def30;
then DES-like-CoDec (EM,F,IPX,(Rev RK)) = DES-CoDec (EM64,F,IP,(Rev RK)) by Def30;
hence DES-CoDec ((DES-CoDec (M,F,IP,RK)),F,IP,(Rev RK)) = M by Th30; :: thesis: verum