:: deftheorem defines KeyExpansion AESCIP_1:def 13 :
for SBT being Permutation of (8 -tuples_on BOOLEAN)
for m being Nat
for b₃ being Function of (m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),((7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))) holds
( b₃ = KeyExpansion (SBT,m) iff for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex w being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(b₃ . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) ) );