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:
Rev ((KeyExpansion (SBT,m)) . Key) in (Nr + 1) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
;
reconsider kky = Rev ((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 S1[ Nat, set , set ] means ex Keyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( Keyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . ($1 + 1) & $3 = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . ($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
(Rev ((KeyExpansion (SBT,m)) . Key)) . 1 in rng kky
by FUNCT_1:3;
then reconsider Keyi1 = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
reconsider I0 = ((InvSubBytes SBT) * InvShiftRows) . (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 S1[n,z,y]
proof
let n be
Nat;
( 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 S1[n,z,y] )
assume X11:
( 1
<= n &
n < Nr )
;
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 S1[n,z,y]
let z be
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 S1[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
(Rev ((KeyExpansion (SBT,m)) . Key)) . (n + 1) in rng kky
by FUNCT_1:3;
then reconsider Keyi =
(Rev ((KeyExpansion (SBT,m)) . Key)) . (n + 1) as
Element of 4
-tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
reconsider y =
(((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . (z,Keyi)) as
Element of 4
-tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
take
y
;
S1[n,z,y]
thus
S1[
n,
z,
y]
;
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
S1[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
(Rev ((KeyExpansion (SBT,m)) . Key)) . (Nr + 1) in rng kky
by FUNCT_1:3;
then reconsider KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (Nr + 1) as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
reconsider w = AddRoundKey . (seq10,KeyNr) as Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
w = AddRoundKey . ((seq . Nr),KeyNr)
;
hence
ex b1 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 = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 & seq . 1 = ((InvSubBytes SBT) * InvShiftRows) . (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 = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) & seq . (i + 1) = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . ((seq . 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) & b1 = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) )
by X2, XREAL_1:8; verum