:: deftheorem defines DES-KS DESCIP_1:def 28 :
for Key being Element of 64 -tuples_on BOOLEAN
for b₂ being Element of 16 -tuples_on (48 -tuples_on BOOLEAN) holds
( b₂ = DES-KS Key iff ex C, D being sequence of (28 -tuples_on BOOLEAN) st
( C . 0 = Op-Left ((DES-PC1 Key),28) & D . 0 = Op-Right ((DES-PC1 Key),28) & ( for i being Element of NAT st 0 <= i & i <= 15 holds
( b₂ . (i + 1) = DES-PC2 ((C . (i + 1)) ^ (D . (i + 1))) & C . (i + 1) = Op-Shift ((C . i),(bitshift_DES . i)) & D . (i + 1) = Op-Shift ((D . i),(bitshift_DES . i)) ) ) ) );