:: deftheorem Def20 defines DES-DIV8 DESCIP_1:def 20 :
for r being Element of 48 -tuples_on BOOLEAN
for b₂ being Element of 8 -tuples_on (6 -tuples_on BOOLEAN) holds
( b₂ = DES-DIV8 r iff ( b₂ . 1 = Op-Left (r,6) & b₂ . 2 = Op-Left ((Op-Right (r,6)),6) & b₂ . 3 = Op-Left ((Op-Right (r,12)),6) & b₂ . 4 = Op-Left ((Op-Right (r,18)),6) & b₂ . 5 = Op-Left ((Op-Right (r,24)),6) & b₂ . 6 = Op-Left ((Op-Right (r,30)),6) & b₂ . 7 = Op-Left ((Op-Right (r,36)),6) & b₂ . 8 = Op-Right (r,42) ) );