for SBT being Permutation of (8 -tuples_on BOOLEAN)
for m being Nat
for text, otext 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 Keyi1, KeyNr being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st ( m = 4 or m = 6 or m = 8 ) & Keyi1 = ((KeyExpansion (SBT,m)) . Key) . 1 & KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) & otext = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . text),KeyNr) holds
((InvSubBytes SBT) * InvShiftRows) . (AddRoundKey . (otext,Keyi1)) = text