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 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
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 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
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 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
let key be Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: 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
let dkeyi, ekeyi be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: ( ( m = 4 or m = 6 or m = 8 ) & dkeyi = (Rev ((KeyExpansion (SBT,m)) . key)) . 1 & ekeyi = ((KeyExpansion (SBT,m)) . key) . (7 + m) implies AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi) = text )
assume AS: ( ( m = 4 or m = 6 or m = 8 ) & dkeyi = (Rev ((KeyExpansion (SBT,m)) . key)) . 1 & ekeyi = ((KeyExpansion (SBT,m)) . key) . (7 + m) ) ; :: thesis: AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi) = text
set p = (KeyExpansion (SBT,m)) . key;
(KeyExpansion (SBT,m)) . key in (7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) ;
then B0: ex s being Element of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) * st
( (KeyExpansion (SBT,m)) . key = s & len s = 7 + m ) ;
1 + 0 < 7 + m by XREAL_1:8;
then 1 in Seg (7 + m) ;
then B1: 1 in dom ((KeyExpansion (SBT,m)) . key) by FINSEQ_1:def 3, B0;
A0: dkeyi = ((KeyExpansion (SBT,m)) . key) . (((len ((KeyExpansion (SBT,m)) . key)) - 1) + 1) by AS, FINSEQ_5:58, B1
.= ekeyi by B0, AS ;
now :: thesis: for i, j being Nat st i in Seg 4 & j in Seg 4 holds
((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = (text . i) . j
let i, j be Nat; :: thesis: ( i in Seg 4 & j in Seg 4 implies ((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = (text . i) . j )
assume A3: ( i in Seg 4 & j in Seg 4 ) ; :: thesis: ((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = (text . i) . j
then consider etextij, ekeyij being Element of 8 -tuples_on BOOLEAN such that
A4: ( etextij = (text . i) . j & ekeyij = (ekeyi . i) . j & ((AddRoundKey . (text,ekeyi)) . i) . j = Op-XOR (etextij,ekeyij) ) by DefAddRoundKey;
consider dtextij, dkeyij being Element of 8 -tuples_on BOOLEAN such that
A5: ( dtextij = ((AddRoundKey . (text,ekeyi)) . i) . j & dkeyij = (dkeyi . i) . j & ((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = Op-XOR (dtextij,dkeyij) ) by DefAddRoundKey, A3;
thus ((AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi)) . i) . j = (text . i) . j by A4, A5, A0, DESCIP_1:17; :: thesis: verum
end;
hence AddRoundKey . ((AddRoundKey . (text,ekeyi)),dkeyi) = text by LM01; :: thesis: verum