for y being object st y in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
ex x being object st
( x in 128 -tuples_on BOOLEAN & y = AES-Statearray . x )
proof
let y be object ; :: thesis: ( y in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) implies ex x being object st
( x in 128 -tuples_on BOOLEAN & y = AES-Statearray . x ) )
assume y in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ; :: thesis: ex x being object st
( x in 128 -tuples_on BOOLEAN & y = AES-Statearray . x )
then B10: ex s being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( y = s & len s = 4 ) ;
then reconsider z = y as Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * ;
defpred S1[ Nat, set ] means ex i, j, n being Nat ex zij being Element of 8 -tuples_on BOOLEAN st
( i in Seg 4 & j in Seg 4 & n in Seg 8 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= $1 & $1 <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 & n = $1 - (((i -' 1) * 8) + ((j -' 1) * 32)) & zij = (z . i) . j & $2 = zij . n );
Q12: for k being Nat st k in Seg 128 holds
ex z being Element of BOOLEAN st S1[k,z]
proof
let k be Nat; :: thesis: ( k in Seg 128 implies ex z being Element of BOOLEAN st S1[k,z] )
assume k in Seg 128 ; :: thesis: ex z being Element of BOOLEAN st S1[k,z]
then ( 1 <= k & k <= 128 ) by FINSEQ_1:1;
then consider i, j being Nat such that
A4: ( i in Seg 4 & j in Seg 4 & (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 ) by LMStat0;
i in dom z by FINSEQ_1:def 3, A4, B10;
then z . i in rng z by FUNCT_1:3;
then z . i in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then B10: ex s being Element of (8 -tuples_on BOOLEAN) * st
( z . i = s & len s = 4 ) ;
then reconsider zi = z . i as Element of (8 -tuples_on BOOLEAN) * ;
j in dom zi by B10, FINSEQ_1:def 3, A4;
then zi . j in rng zi by FUNCT_1:3;
then reconsider zij = (z . i) . j as Element of 8 -tuples_on BOOLEAN ;
A50: ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) - (((i -' 1) * 8) + ((j -' 1) * 32)) <= k - (((i -' 1) * 8) + ((j -' 1) * 32)) by A4, XREAL_1:9;
then reconsider n = k - (((i -' 1) * 8) + ((j -' 1) * 32)) as Element of NAT by INT_1:3;
k - (((i -' 1) * 8) + ((j -' 1) * 32)) <= (((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7) - (((i -' 1) * 8) + ((j -' 1) * 32)) by A4, XREAL_1:9;
then G4: n in Seg 8 by A50;
reconsider z = zij . n as Element of BOOLEAN ;
take z ; :: thesis: S1[k,z]
thus S1[k,z] by A4, G4; :: thesis: verum
end;
consider x being FinSequence of BOOLEAN such that
Q13: ( dom x = Seg 128 & ( for i being Nat st i in Seg 128 holds
S1[i,x . i] ) ) from FINSEQ_1:sch 5(Q12);
 Q14: len x = 128 by Q13, FINSEQ_1:def 3;
reconsider x = x as Element of BOOLEAN * by FINSEQ_1:def 11;
x in 128 -tuples_on BOOLEAN by Q14;
then reconsider x = x as Element of 128 -tuples_on BOOLEAN ;
P2: for i, j being Nat st i in Seg 4 & j in Seg 4 holds
(z . i) . j = mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))
proof
let i, j be Nat; :: thesis: ( i in Seg 4 & j in Seg 4 implies (z . i) . j = mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) )
assume P21: ( i in Seg 4 & j in Seg 4 ) ; :: thesis: (z . i) . j = mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))
then i in dom z by FINSEQ_1:def 3, B10;
then z . i in rng z by FUNCT_1:3;
then z . i in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then P8: ex s being Element of (8 -tuples_on BOOLEAN) * st
( z . i = s & len s = 4 ) ;
reconsider zi = z . i as Element of (8 -tuples_on BOOLEAN) * by P8;
j in dom zi by P8, FINSEQ_1:def 3, P21;
then zi . j in rng zi by FUNCT_1:3;
then zi . j in 8 -tuples_on BOOLEAN ;
then P11: ex s being Element of BOOLEAN * st
( zi . j = s & len s = 8 ) ;
reconsider zij = zi . j as Element of BOOLEAN * by P11;
Q110: ( 1 <= i & i <= 4 ) by P21, FINSEQ_1:1;
then 1 - 1 <= i - 1 by XREAL_1:9;
then i -' 1 = i - 1 by XREAL_0:def 2;
then i -' 1 <= 4 - 1 by Q110, XREAL_1:9;
then Q112: (i -' 1) * 8 <= 3 * 8 by XREAL_1:64;
Q130: ( 1 <= j & j <= 4 ) by P21, FINSEQ_1:1;
then 1 - 1 <= j - 1 by XREAL_1:9;
then j -' 1 = j - 1 by XREAL_0:def 2;
then j -' 1 <= 4 - 1 by Q130, XREAL_1:9;
then Q133: (j -' 1) * 32 <= 3 * 32 by XREAL_1:64;
((i -' 1) * 8) + ((j -' 1) * 32) <= 24 + 96 by Q133, Q112, XREAL_1:7;
then Q134: 1 + (((i -' 1) * 8) + ((j -' 1) * 32)) <= 1 + 120 by XREAL_1:7;
then G1: 1 + (((i -' 1) * 8) + ((j -' 1) * 32)) <= len x by XXREAL_0:2, Q14;
G0: 1 <= 1 + (((i -' 1) * 8) + ((j -' 1) * 32)) by NAT_1:11;
G2: 1 <= 1 + ((((i -' 1) * 8) + ((j -' 1) * 32)) + 7) by NAT_1:11;
G3: (1 + (((i -' 1) * 8) + ((j -' 1) * 32))) + 0 <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 by XREAL_1:7;
Q135: ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 <= 121 + 7 by XREAL_1:6, Q134;
then F3: ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 <= len x by Q13, FINSEQ_1:def 3;
P13: len (mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))) = ((((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7) -' ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32))) + 1 by G1, G2, G3, G0, F3, FINSEQ_6:118
.= ((((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7) - ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32))) + 1 by G3, XREAL_1:233
.= 8 ;
now :: thesis: for n being Nat st 1 <= n & n <= len zij holds
zij . n = (mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))) . n
let n be Nat; :: thesis: ( 1 <= n & n <= len zij implies zij . n = (mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))) . n )
assume F40: ( 1 <= n & n <= len zij ) ; :: thesis: zij . n = (mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))) . n
F1: 1 <= 1 + (((i -' 1) * 8) + ((j -' 1) * 32)) by NAT_1:11;
F2: (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 by NAT_1:11;
F5: n <= ((((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7) - ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32))) + 1 by F40, P11;
reconsider k = n + (((i -' 1) * 8) + ((j -' 1) * 32)) as Nat ;
A6: k = (n - 1) + ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) ;
n <= n + (((i -' 1) * 8) + ((j -' 1) * 32)) by NAT_1:11;
then H1: 1 <= k by F40, XXREAL_0:2;
reconsider k = n + (((i -' 1) * 8) + ((j -' 1) * 32)) as Nat ;
H3: k <= 8 + (((i -' 1) * 8) + ((j -' 1) * 32)) by F40, P11, XREAL_1:7;
then H2: k <= 128 by Q135, XXREAL_0:2;
then k in Seg 128 by H1;
then consider i0, j0, n0 being Nat, zi0j0 being Element of 8 -tuples_on BOOLEAN such that
AA1: ( i0 in Seg 4 & j0 in Seg 4 & n0 in Seg 8 & (1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32) <= k & k <= ((1 + ((i0 -' 1) * 8)) + ((j0 -' 1) * 32)) + 7 & n0 = k - (((i0 -' 1) * 8) + ((j0 -' 1) * 32)) & zi0j0 = (z . i0) . j0 & x . k = zi0j0 . n0 ) by Q13;
1 + (((i -' 1) * 8) + ((j -' 1) * 32)) <= n + (((i -' 1) * 8) + ((j -' 1) * 32)) by F40, XREAL_1:7;
then ( (1 + ((i -' 1) * 8)) + ((j -' 1) * 32) <= k & k <= ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7 ) by H3;
then ( i = i0 & j = j0 ) by LMStat2, AA1, P21, H1, H2;
hence zij . n = (mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))) . n by AA1, F1, F2, F3, F40, F5, A6, FINSEQ_6:122; :: thesis: verum
end;
hence (z . i) . j = mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) by FINSEQ_1:def 18, P11, P13; :: thesis: verum
end;
AES-Statearray . x in 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
then P3: ex s being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( AES-Statearray . x = s & len s = 4 ) ;
now :: thesis: for i being Nat st 1 <= i & i <= len (AES-Statearray . x) holds
(AES-Statearray . x) . i = z . i
let i be Nat; :: thesis: ( 1 <= i & i <= len (AES-Statearray . x) implies (AES-Statearray . x) . i = z . i )
assume ( 1 <= i & i <= len (AES-Statearray . x) ) ; :: thesis: (AES-Statearray . x) . i = z . i
then P6: i in Seg 4 by P3;
then i in dom (AES-Statearray . x) by FINSEQ_1:def 3, P3;
then (AES-Statearray . x) . i in rng (AES-Statearray . x) by FUNCT_1:3;
then (AES-Statearray . x) . i in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then P8: ex s being Element of (8 -tuples_on BOOLEAN) * st
( (AES-Statearray . x) . i = s & len s = 4 ) ;
reconsider H1i = (AES-Statearray . x) . i as Element of (8 -tuples_on BOOLEAN) * by P8;
i in dom z by FINSEQ_1:def 3, B10, P6;
then z . i in rng z by FUNCT_1:3;
then z . i in 4 -tuples_on (8 -tuples_on BOOLEAN) ;
then P11: ex s being Element of (8 -tuples_on BOOLEAN) * st
( z . i = s & len s = 4 ) ;
reconsider H2i = z . i as Element of (8 -tuples_on BOOLEAN) * by P11;
now :: thesis: for j being Nat st 1 <= j & j <= len H1i holds
H1i . j = H2i . j
let j be Nat; :: thesis: ( 1 <= j & j <= len H1i implies H1i . j = H2i . j )
assume ( 1 <= j & j <= len H1i ) ; :: thesis: H1i . j = H2i . j
then P14: j in Seg 4 by P8;
then ((AES-Statearray . x) . i) . j = mid (x,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) by DefStatearray, P6;
hence H1i . j = H2i . j by P2, P6, P14; :: thesis: verum
end;
hence (AES-Statearray . x) . i = z . i by P8, P11, FINSEQ_1:def 18; :: thesis: verum
end;
hence ex x being object st
( x in 128 -tuples_on BOOLEAN & y = AES-Statearray . x ) by P3, B10, FINSEQ_1:def 18; :: thesis: verum
end;
then 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) = rng AES-Statearray by FUNCT_2:10;
hence AES-Statearray is onto by FUNCT_2:def 3; :: thesis: verum