theorem LAST03: :: AESCIP_1:31

for SBT being Permutation of (8 -tuples_on BOOLEAN)
for m being Nat
for text being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for dkeyi, ekeyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st ( m = 4 or m = 6 or m = 8 ) & dkeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 & ekeyi = ((KeyExpansion (SBT,m)) . Key) . (7 + m) holds
AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi) = text