for x1, x2 being object st x1 in 128 -tuples_on BOOLEAN & x2 in 128 -tuples_on BOOLEAN & AES-Statearray . x1 = AES-Statearray . x2 holds
x1 = x2
proof
let x1,
x2 be
object ;
( x1 in 128 -tuples_on BOOLEAN & x2 in 128 -tuples_on BOOLEAN & AES-Statearray . x1 = AES-Statearray . x2 implies x1 = x2 )
assume A1:
(
x1 in 128
-tuples_on BOOLEAN &
x2 in 128
-tuples_on BOOLEAN &
AES-Statearray . x1 = AES-Statearray . x2 )
;
x1 = x2
then reconsider xx1 =
x1,
xx2 =
x2 as
Element of 128
-tuples_on BOOLEAN ;
P1:
ex
s being
Element of
BOOLEAN * st
(
xx1 = s &
len s = 128 )
by A1;
P2:
ex
s being
Element of
BOOLEAN * st
(
xx2 = s &
len s = 128 )
by A1;
now for k being Nat st 1 <= k & k <= len xx1 holds
xx1 . k = xx2 . klet k be
Nat;
( 1 <= k & k <= len xx1 implies xx1 . k = xx2 . k )assume P5:
( 1
<= k &
k <= len xx1 )
;
xx1 . k = xx2 . kconsider 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, P5, P1;
mid (
xx1,
((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),
(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) is
Element of
BOOLEAN *
by FINSEQ_1:def 11;
then reconsider A1ij =
((AES-Statearray . xx1) . i) . j as
FinSequence of
BOOLEAN by DefStatearray, A4;
mid (
xx2,
((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),
(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7)) is
Element of
BOOLEAN *
by FINSEQ_1:def 11;
then reconsider A2ij =
((AES-Statearray . xx2) . i) . j as
FinSequence of
BOOLEAN by DefStatearray, A4;
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;
F41:
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;
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;
Q110:
( 1
<= i &
i <= 4 )
by A4, 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 A4, 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
1
+ (((i -' 1) * 8) + ((j -' 1) * 32)) <= 1
+ 120
by XREAL_1:7;
then Q135:
((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7
<= 121
+ 7
by XREAL_1:6;
F5:
n <= ((((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7) - ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32))) + 1
by F41;
A6:
k = (n - 1) + ((1 + ((i -' 1) * 8)) + ((j -' 1) * 32))
;
thus xx1 . k =
(mid (xx1,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))) . n
by F1, F2, Q135, P1, A50, F5, A6, FINSEQ_6:122
.=
A2ij . n
by DefStatearray, A4, A1
.=
(mid (xx2,((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)),(((1 + ((i -' 1) * 8)) + ((j -' 1) * 32)) + 7))) . n
by DefStatearray, A4
.=
xx2 . k
by F1, F2, P2, Q135, A50, F5, A6, FINSEQ_6:122
;
verum end;
hence
x1 = x2
by P1, P2, FINSEQ_1:def 17;
verum
end;
hence
AES-Statearray is one-to-one
by FUNCT_2:19; verum