:: deftheorem defines AES-KeyInitState128 AESCIP_1:def 16 :
for r being Element of 128 -tuples_on BOOLEAN
for b₂ being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( b₂ = AES-KeyInitState128 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-Right (r,120))*> ) );