:: deftheorem defines DES-ENC DESCIP_1:def 31 :
for plaintext, secretkey being Element of 64 -tuples_on BOOLEAN holds DES-ENC (plaintext,secretkey) = DES-CoDec (plaintext,DES-FFUNC,DES-PIP,(DES-KS secretkey));