:: deftheorem defines KeyExpansionX AESCIP_1:def 12 :
for SBT being Permutation of (8 -tuples_on BOOLEAN)
for m being Nat st ( m = 4 or m = 6 or m = 8 ) holds
for b₃ being Function of (m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),((4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) holds
( b₃ = KeyExpansionX (SBT,m) iff for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( ( for i being Element of NAT st i < m holds
(b₃ . Key) . (i + 1) = Key . (i + 1) ) & ( for i being Element of NAT st m <= i & i < 4 * (7 + m) holds
ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = (b₃ . Key) . ((i - m) + 1) & Q = (b₃ . Key) . i & (b₃ . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) ) );