let SBT be Permutation of (8 -tuples_on BOOLEAN); :: thesis: 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 eKeyi, dKeyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st ( m = 4 or m = 6 or m = 8 ) & eKeyi = ((KeyExpansion (SBT,m)) . Key) . 1 & dKeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) holds
AddRoundKey . ((AddRoundKey . (text,eKeyi)),dKeyi) = text
let m be Nat; :: thesis: 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 ) & eKeyi = ((KeyExpansion (SBT,m)) . Key) . 1 & dKeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) holds
AddRoundKey . ((AddRoundKey . (text,eKeyi)),dKeyi) = text
let text 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 eKeyi, dKeyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st ( m = 4 or m = 6 or m = 8 ) & eKeyi = ((KeyExpansion (SBT,m)) . Key) . 1 & dKeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) holds
AddRoundKey . ((AddRoundKey . (text,eKeyi)),dKeyi) = text
let Key be Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: 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 ) & eKeyi = ((KeyExpansion (SBT,m)) . Key) . 1 & dKeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) holds
AddRoundKey . ((AddRoundKey . (text,eKeyi)),dKeyi) = text
let eKeyi, dKeyi be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: ( ( m = 4 or m = 6 or m = 8 ) & eKeyi = ((KeyExpansion (SBT,m)) . Key) . 1 & dKeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) implies AddRoundKey . ((AddRoundKey . (text,eKeyi)),dKeyi) = text )
assume AS: ( ( m = 4 or m = 6 or m = 8 ) & eKeyi = ((KeyExpansion (SBT,m)) . Key) . 1 & dKeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) ) ; :: thesis: AddRoundKey . ((AddRoundKey . (text,eKeyi)),dKeyi) = text
1 + 0 < 7 + m by XREAL_1:8;
then 0 < (7 + m) - 1 by XREAL_1:50;
then (7 + m) - 1 in NAT by INT_1:3;
then reconsider i = (7 + m) - 1 as Nat ;
P2: eKeyi = ((KeyExpansion (SBT,m)) . Key) . ((7 + m) - i) by AS;
dKeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) by AS;
hence AddRoundKey . ((AddRoundKey . (text,eKeyi)),dKeyi) = text by AS, P2, LAST08; :: thesis: verum