let s1, s2 be Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: ( 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) & s1 = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) ) & 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) & s2 = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) ) implies s1 = s2 )
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 Nr = (7 + m) - 1 as Nat ;
assume A1: 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) & s1 = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) ) ; :: thesis: ( for seq being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( not len seq = (7 + m) - 1 or for Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( not Keyi1 = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 or not seq . 1 = ((InvSubBytes SBT) * InvShiftRows) . (AddRoundKey . (text,Keyi1)) ) or ex i being Nat st
( 1 <= i & i < (7 + m) - 1 & ( for Keyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( not Keyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) or not seq . (i + 1) = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . ((seq . i),Keyi)) ) ) ) or for KeyNr being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( not KeyNr = (Rev ((KeyExpansion (SBT,m)) . Key)) . (7 + m) or not s2 = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) ) or s1 = s2 )
assume A2: 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) & s2 = AddRoundKey . ((seq . ((7 + m) - 1)),KeyNr) ) ) ; :: thesis: s1 = s2
consider seq1 being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
P1: ( len seq1 = Nr & ex Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( Keyi1 = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 & seq1 . 1 = ((InvSubBytes SBT) * InvShiftRows) . (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 = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) & seq1 . (i + 1) = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . ((seq1 . 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) & s1 = AddRoundKey . ((seq1 . ((7 + m) - 1)),KeyNr) ) ) by A1;
consider seq2 being FinSequence of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
P2: ( len seq2 = Nr & ex Keyi1 being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( Keyi1 = (Rev ((KeyExpansion (SBT,m)) . Key)) . 1 & seq2 . 1 = ((InvSubBytes SBT) * InvShiftRows) . (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 = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) & seq2 . (i + 1) = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . ((seq2 . 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) & s2 = AddRoundKey . ((seq2 . ((7 + m) - 1)),KeyNr) ) ) by A2;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len seq1 implies seq1 . $1 = seq2 . $1 );
Q50: S₁[ 0 ] ;
Q51: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume Q52: S₁[i] ; :: thesis: S₁[i + 1]
assume ( 1 <= i + 1 & i + 1 <= len seq1 ) ; :: thesis: seq1 . (i + 1) = seq2 . (i + 1)
then Q54: ( 1 - 1 <= (i + 1) - 1 & (i + 1) - 1 <= (len seq1) - 1 ) by XREAL_1:9;
Q550: (len seq1) - 1 <= (len seq1) - 0 by XREAL_1:13;

per cases ( i = 0 or i <> 0 ) ;

suppose C1: i = 0 ; :: thesis: seq1 . (i + 1) = seq2 . (i + 1)

thus seq1 . (i + 1) = seq2 . (i + 1) by C1, P1, P2; :: thesis: verum

end;

suppose Q560: i <> 0 ; :: thesis: seq1 . (i + 1) = seq2 . (i + 1)

Nr - 1 < Nr - 0 by XREAL_1:15;
then XX1: ( 1 <= i & i < Nr ) by Q560, NAT_1:14, P1, Q54, XXREAL_0:2;
then Q60: ex Keyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( Keyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) & seq1 . (i + 1) = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . ((seq1 . i),Keyi)) ) by P1;
ex Keyi being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( Keyi = (Rev ((KeyExpansion (SBT,m)) . Key)) . (i + 1) & seq2 . (i + 1) = (((InvSubBytes SBT) * InvShiftRows) * (MCFunc ")) . (AddRoundKey . ((seq2 . i),Keyi)) ) by P2, XX1;
hence seq1 . (i + 1) = seq2 . (i + 1) by Q560, NAT_1:14, Q550, Q54, XXREAL_0:2, Q52, Q60; :: thesis: verum

end;

end;

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(Q50, Q51);
hence s1 = s2 by FINSEQ_1:14, P1, P2; :: thesis: verum