:: deftheorem defines AES-KeyInitState256 AESCIP_1:def 18 :
for r being Element of 256 -tuples_on BOOLEAN
for b₂ being Element of 8 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( b₂ = AES-KeyInitState256 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-Left ((Op-Right (r,184)),8))*> & b₂ . 7 = <*(Op-Left ((Op-Right (r,192)),8)),(Op-Left ((Op-Right (r,200)),8)),(Op-Left ((Op-Right (r,208)),8)),(Op-Left ((Op-Right (r,216)),8))*> & b₂ . 8 = <*(Op-Left ((Op-Right (r,224)),8)),(Op-Left ((Op-Right (r,232)),8)),(Op-Left ((Op-Right (r,240)),8)),(Op-Right (r,248))*> ) );