theorem LAST08: :: AESCIP_1:34

for SBT being Permutation of (8 -tuples_on BOOLEAN)
for m, i 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 eKeyi, dKeyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st ( m = 4 or m = 6 or m = 8 ) & i <= (7 + m) - 1 & eKeyi = ((KeyExpansion (SBT,m)) . Key) . ((7 + m) - i) & dKeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) holds
AddRoundKey . ((AddRoundKey . (text,eKeyi)),dKeyi) = text