reconsider IPX = IP as Permutation of ((2 * 32) -tuples_on BOOLEAN) ;
reconsider MX = M as Element of (2 * 32) -tuples_on BOOLEAN ;
reconsider CM = DES-like-CoDec (MX,F,IPX,RK) as Element of 64 -tuples_on BOOLEAN ;
take CM ; :: thesis: 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 & CM = DES-like-CoDec (MX,F,IPX,RK) )
thus 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 & CM = DES-like-CoDec (MX,F,IPX,RK) ) ; :: thesis: verum