:: deftheorem defines KeyExTemp AESCIP_1:def 11 :
for SBT being Permutation of (8 -tuples_on BOOLEAN)
for m, i being Nat
for w being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st ( m = 4 or m = 6 or m = 8 ) & i < 4 * (7 + m) & m <= i holds
for b₅ being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) holds
( ( i mod m = 0 implies ( b₅ = KeyExTemp (SBT,m,i,w) iff ex T3 being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( T3 = Rcon . (i / m) & b₅ = Op-WXOR ((SubWord (SBT,(RotWord w))),T3) ) ) ) & ( m = 8 & i mod 8 = 4 implies ( b₅ = KeyExTemp (SBT,m,i,w) iff b₅ = SubWord (SBT,w) ) ) & ( not i mod m = 0 & ( not m = 8 or not i mod 8 = 4 ) implies ( b₅ = KeyExTemp (SBT,m,i,w) iff b₅ = w ) ) );