:: deftheorem DefStatearray defines AES-Statearray AESCIP_1:def 1 :
for b₁ being Function of (128 -tuples_on BOOLEAN),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) holds
( b₁ = AES-Statearray iff for input being Element of 128 -tuples_on BOOLEAN
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((b₁ . input) . i) . j = mid (input,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) );