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 ;
ZZ1: (KeyExpansion (SBT,m)) . Key in (Nr + 1) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) ;
reconsider kky = (KeyExpansion (SBT,m)) . Key as Element of (Nr + 1) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) ;
XX12: ex s being Element of (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) * st
( kky = s & len s = Nr + 1 ) by ZZ1;
defpred S₁[ Nat, set , set ] means ex Keyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( Keyi = ((KeyExpansion (SBT,m)) . Key) . ($1 + 1) & $3 = AddRoundKey . ((((MCFunc * ShiftRows) * (SubBytes SBT)) . $2),Keyi) );
1 + 0 <= 7 + m by XREAL_1:7;
then 1 in Seg (Nr + 1) ;
then 1 in dom kky by FINSEQ_1:def 3, XX12;
then ((KeyExpansion (SBT,m)) . Key) . 1 in rng kky by FUNCT_1:3;
then reconsider Keyi1 = ((KeyExpansion (SBT,m)) . Key) . 1 as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
reconsider I0 = AddRoundKey . (text,Keyi1) as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
X1: for n being Nat st 1 <= n & n < Nr holds
for z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex y being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S₁[n,z,y]

proof

let n be Nat; :: thesis: ( 1 <= n & n < Nr implies for z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex y being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S₁[n,z,y] )
assume X11: ( 1 <= n & n < Nr ) ; :: thesis: for z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex y being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S₁[n,z,y]
let z be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: ex y being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S₁[n,z,y]
X111: n + 1 <= Nr + 1 by XREAL_1:7, X11;
0 + 1 <= n + 1 by XREAL_1:7;
then n + 1 in Seg (Nr + 1) by X111;
then n + 1 in dom kky by FINSEQ_1:def 3, XX12;
then ((KeyExpansion (SBT,m)) . Key) . (n + 1) in rng kky by FUNCT_1:3;
then reconsider Keyi = ((KeyExpansion (SBT,m)) . Key) . (n + 1) as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
reconsider y = AddRoundKey . ((((MCFunc * ShiftRows) * (SubBytes SBT)) . z),Keyi) as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
take y ; :: thesis: S₁[n,z,y]
thus S₁[n,z,y] ; :: thesis: verum

end;

consider seq being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
X2: ( len seq = Nr & ( seq . 1 = I0 or Nr = 0 ) & ( for i being Nat st 1 <= i & i < Nr holds
S₁[i,seq . i,seq . (i + 1)] ) ) from RECDEF_1:sch 4(X1);
Nr in Seg Nr by FINSEQ_1:3, N1;
then Nr in dom seq by FINSEQ_1:def 3, X2;
then seq . Nr in rng seq by FUNCT_1:3;
then reconsider seq10 = seq . Nr as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
Nr + 1 in Seg (Nr + 1) by FINSEQ_1:3;
then Nr + 1 in dom kky by FINSEQ_1:def 3, XX12;
then ((KeyExpansion (SBT,m)) . Key) . (Nr + 1) in rng kky by FUNCT_1:3;
then reconsider KeyNr = ((KeyExpansion (SBT,m)) . Key) . (Nr + 1) as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
reconsider w = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . seq10),KeyNr) as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
w = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . (seq . Nr)),KeyNr) ;
hence ex b₁ being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex seq being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( len seq = (7 + m) - 1 & ex Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( Keyi1 = ((KeyExpansion (SBT,m)) . Key) . 1 & seq . 1 = AddRoundKey . (text,Keyi1) ) & ( for i being Nat st 1 <= i & i < (7 + m) - 1 holds
ex Keyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( Keyi = ((KeyExpansion (SBT,m)) . Key) . (i + 1) & seq . (i + 1) = AddRoundKey . ((((MCFunc * ShiftRows) * (SubBytes SBT)) . (seq . 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) & b₁ = AddRoundKey . (((ShiftRows * (SubBytes SBT)) . (seq . ((7 + m) - 1))),KeyNr) ) ) by XREAL_1:8, X2; :: thesis: verum