let SBT be Permutation of (8 -tuples_on BOOLEAN); :: thesis: 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
let m be Nat; :: thesis: 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
let text, otext be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: 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
let Key be Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: 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
let Keyi1, KeyNr be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: ( ( 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) implies ((InvSubBytes SBT) * InvShiftRows) . (AddRoundKey . (otext,Keyi1)) = text )
assume AS: ( ( 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) ) ; :: thesis: ((InvSubBytes SBT) * InvShiftRows) . (AddRoundKey . (otext,Keyi1)) = text
AddRoundKey . (otext,Keyi1) = (ShiftRows * (SubBytes SBT)) . text by AS, LAST05;
hence ((InvSubBytes SBT) * InvShiftRows) . (AddRoundKey . (otext,Keyi1)) = text by LAST01; :: thesis: verum