let SBT be Permutation of (8 -tuples_on BOOLEAN); :: thesis:
let MCFunc be Permutation of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))); :: thesis:
let m be Nat; :: thesis:
let text be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis:
let Key be Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis:
1 + 0 < 7 + m by XREAL_1:8;
then N1: 0 < (7 + m) - 1 by XREAL_1:50;
then (7 + m) - 1 in NAT by INT_1:3;
then reconsider Nr = (7 + m) - 1 as Nat ;
A0: 1 <= Nr by NAT_1:14, N1;
assume AS: ( m = 4 or m = 6 or m = 8 ) ; :: thesis:
consider eseq being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
P1: ( len eseq = Nr & ex Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( Keyi1 = ((KeyExpansion (SBT,m)) . Key) . 1 & eseq . 1 = AddRoundKey . (text,Keyi1) ) & ( for i being Nat st 1 <= i & i < Nr holds
ex Keyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( Keyi = ((KeyExpansion (SBT,m)) . Key) . (i + 1) & eseq . (i + 1) = AddRoundKey . ((((MCFunc * ShiftRows) * (SubBytes SBT)) . (eseq . i)),Keyi) ) ) & ex KeyNr being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( KeyNr = ((KeyExpansion (SBT,m)) . Key) . (7 + m) & AES-ENC (SBT,MCFunc,text,Key) = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . (eseq . Nr)),KeyNr) ) ) by defENC;
consider dseq being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
P2: ( len dseq = Nr & ex Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( Keyi1 = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 & dseq . 1 = ((InvSubBytes SBT) * InvShiftRows) . (AddRoundKey . ((AES-ENC (SBT,MCFunc,text,Key)),Keyi1)) ) & ( for i being Nat st 1 <= i & i < Nr holds
ex Keyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( Keyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) & dseq . (i + 1) = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . ((dseq . i),Keyi)) ) ) & ex KeyNr being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) & AES-DEC (SBT,MCFunc,(AES-ENC (SBT,MCFunc,text,Key)),Key) = AddRoundKey . ((dseq . Nr),KeyNr) ) ) by defDEC;
consider eKeyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
P11: ( eKeyi1 = ((KeyExpansion (SBT,m)) . Key) . 1 & eseq . 1 = AddRoundKey . (text,eKeyi1) ) by P1;
consider eKeyNr being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
P12: ( eKeyNr = ((KeyExpansion (SBT,m)) . Key) . (7 + m) & AES-ENC (SBT,MCFunc,text,Key) = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . (eseq . Nr)),eKeyNr) ) by P1;
consider dKeyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
P21: ( dKeyi1 = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 & dseq . 1 = ((InvSubBytes SBT) * InvShiftRows) . (AddRoundKey . ((AES-ENC (SBT,MCFunc,text,Key)),dKeyi1)) ) by P2;
consider dKeyNr being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
P22: ( dKeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) & AES-DEC (SBT,MCFunc,(AES-ENC (SBT,MCFunc,text,Key)),Key) = AddRoundKey . ((dseq . Nr),dKeyNr) ) by P2;
defpred S₁[ Nat] means ( $1 < Nr implies dseq . ($1 + 1) = eseq . (Nr - $1) );
Nr in Seg Nr by A0;
then Nr in dom eseq by P1, FINSEQ_1:def 3;
then eseq . Nr in rng eseq by FUNCT_1:3;
then reconsider esqm = eseq . Nr as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
dseq . (1 + 0) = esqm by P12, P21, AS, LAST04
.= eseq . (Nr - 0) ;
then PN1: S₁[ 0 ] ;
PN2: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume A1: S₁[i] ; :: thesis:
assume A2: i + 1 < Nr ; :: thesis:
A4: i <= i + 1 by NAT_1:11;
consider dKeyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
A6: ( dKeyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . ((i + 1) + 1) & dseq . ((i + 1) + 1) = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . ((dseq . (i + 1)),dKeyi)) ) by P2, A2, NAT_1:11;
X11: 0 < Nr - (i + 1) by A2, XREAL_1:50;
then Nr - (i + 1) in NAT by INT_1:3;
then reconsider m7i1 = Nr - (i + 1) as Nat ;
1 <= m7i1 by NAT_1:14, X11;
then A9: ( 1 <= Nr - (i + 1) & Nr - (i + 1) < Nr ) by XREAL_1:44;
consider eKeyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
A10: ( eKeyi = ((KeyExpansion (SBT,m)) . Key) . (m7i1 + 1) & eseq . (m7i1 + 1) = AddRoundKey . ((((MCFunc * ShiftRows) * (SubBytes SBT)) . (eseq . m7i1)),eKeyi) ) by P1, A9;
m7i1 in Seg Nr by A9;
then m7i1 in dom eseq by P1, FINSEQ_1:def 3;
then eseq . m7i1 in rng eseq by FUNCT_1:3;
then reconsider esq7mi1 = eseq . m7i1 as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
reconsider MSSesq7mi1 = ((MCFunc * ShiftRows) * (SubBytes SBT)) . esq7mi1 as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
XXX: eKeyi = ((KeyExpansion (SBT,m)) . Key) . ((7 + m) - (i + 1)) by A10;
A12: AddRoundKey . ((eseq . (Nr - i)),dKeyi) = MSSesq7mi1 by A10, A2, AS, A6, XXX, LAST08;
thus dseq . ((i + 1) + 1) = eseq . (Nr - (i + 1)) by A6, A4, A2, XXREAL_0:2, A1, A12, LAST02; :: thesis:

end;

P30: for k being Nat holds S₁[k] from NAT_1:sch 2(PN1, PN2);
5 + m < 6 + m by XREAL_1:8;
then P31: dseq . ((5 + m) + 1) = eseq . (Nr - (5 + m)) by P30;
( 1 <= 1 & 1 <= 1 + (5 + m) ) by NAT_1:11;
then 1 in Seg Nr ;
then 1 in dom eseq by P1, FINSEQ_1:def 3;
then eseq . 1 in rng eseq by FUNCT_1:3;
then reconsider esq1 = eseq . 1 as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
thus AES-DEC (SBT,MCFunc,(AES-ENC (SBT,MCFunc,text,Key)),Key) = text by P22, P31, P11, AS, LAST07; :: thesis: