:: deftheorem defines AES-KeyInitState192 AESCIP_1:def 17 :
for r being Element of 192 -tuples_on BOOLEAN
for b₂ being Element of 6 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( b₂ = AES-KeyInitState192 r iff ( b₂ . 1 = <*(Op-Left (r,8)),(Op-Left ((Op-Right (r,8)),8)),(Op-Left ((Op-Right (r,16)),8)),(Op-Left ((Op-Right (r,24)),8))*> & b₂ . 2 = <*(Op-Left ((Op-Right (r,32)),8)),(Op-Left ((Op-Right (r,40)),8)),(Op-Left ((Op-Right (r,48)),8)),(Op-Left ((Op-Right (r,56)),8))*> & b₂ . 3 = <*(Op-Left ((Op-Right (r,64)),8)),(Op-Left ((Op-Right (r,72)),8)),(Op-Left ((Op-Right (r,80)),8)),(Op-Left ((Op-Right (r,88)),8))*> & b₂ . 4 = <*(Op-Left ((Op-Right (r,96)),8)),(Op-Left ((Op-Right (r,104)),8)),(Op-Left ((Op-Right (r,112)),8)),(Op-Left ((Op-Right (r,120)),8))*> & b₂ . 5 = <*(Op-Left ((Op-Right (r,128)),8)),(Op-Left ((Op-Right (r,136)),8)),(Op-Left ((Op-Right (r,144)),8)),(Op-Left ((Op-Right (r,152)),8))*> & b₂ . 6 = <*(Op-Left ((Op-Right (r,160)),8)),(Op-Left ((Op-Right (r,168)),8)),(Op-Left ((Op-Right (r,176)),8)),(Op-Right (r,184))*> ) );