defpred S1[ Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)), Element of (7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))] means ex w being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( w = (KeyExpansionX (SBT,m)) . $1 & ( for i being Nat st i < 7 + m holds
$2 . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) );
A1:
for x being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex z being Element of (7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st S1[x,z]
proof
let x be
Element of
m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN));
ex z being Element of (7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) st S1[x,z]
reconsider w =
(KeyExpansionX (SBT,m)) . x as
Element of
(4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
w in (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
;
then XX1:
ex
s being
Element of
(4 -tuples_on (8 -tuples_on BOOLEAN)) * st
(
w = s &
len s = 4
* (7 + m) )
;
reconsider w0 =
w as
Element of
(4 -tuples_on (8 -tuples_on BOOLEAN)) * by XX1;
reconsider m7 = 7
+ m as
Element of
NAT by ORDINAL1:def 12;
reconsider m47 = 4
* (7 + m) as
Element of
NAT by ORDINAL1:def 12;
defpred S2[
Nat,
set ]
means ex
n being
Element of
NAT st
(
n = $1
- 1 & $2
= <*(w . ((4 * n) + 1)),(w . ((4 * n) + 2)),(w . ((4 * n) + 3)),(w . ((4 * n) + 4))*> );
P1:
for
k being
Nat st
k in Seg m7 holds
ex
z being
Element of 4
-tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
S2[
k,
z]
proof
let k be
Nat;
( k in Seg m7 implies ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S2[k,z] )
assume
k in Seg m7
;
ex z being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S2[k,z]
then ZZ1:
( 1
<= k &
k <= m7 )
by FINSEQ_1:1;
then reconsider n =
k - 1 as
Element of
NAT by XREAL_1:48, INT_1:3;
ZZ3:
4
* (n + 1) <= 4
* m7
by ZZ1, XREAL_1:64;
ZZ4:
0 + 1
<= (4 * n) + 1
by XREAL_1:7;
ZZ7:
(4 * n) + 1
<= (4 * n) + 4
by XREAL_1:7;
ZZ8:
(4 * n) + 2
<= (4 * n) + 4
by XREAL_1:7;
ZZ9:
(4 * n) + 3
<= (4 * n) + 4
by XREAL_1:7;
(4 * n) + 1
<= 4
* m7
by ZZ7, ZZ3, XXREAL_0:2;
then X1:
(4 * n) + 1
in Seg m47
by ZZ4;
ZZ10:
1
<= (4 * n) + 2
by ZZ4, XREAL_1:7;
(4 * n) + 2
<= 4
* m7
by ZZ8, ZZ3, XXREAL_0:2;
then X2:
(4 * n) + 2
in Seg m47
by ZZ10;
ZZ11:
1
<= (4 * n) + 3
by ZZ4, XREAL_1:7;
(4 * n) + 3
<= 4
* m7
by ZZ9, ZZ3, XXREAL_0:2;
then X3:
(4 * n) + 3
in Seg m47
by ZZ11;
ZZ12:
1
<= (4 * n) + 4
by ZZ4, XREAL_1:7;
X4:
(4 * n) + 4
in Seg m47
by ZZ3, ZZ12;
X5:
dom w = Seg m47
by FINSEQ_1:def 3, XX1;
w . ((4 * n) + 1) in rng w
by X5, X1, FUNCT_1:3;
then reconsider w1 =
w . ((4 * n) + 1) as
Element of 4
-tuples_on (8 -tuples_on BOOLEAN) ;
w . ((4 * n) + 2) in rng w
by X5, X2, FUNCT_1:3;
then reconsider w2 =
w . ((4 * n) + 2) as
Element of 4
-tuples_on (8 -tuples_on BOOLEAN) ;
w . ((4 * n) + 3) in rng w
by X5, X3, FUNCT_1:3;
then reconsider w3 =
w . ((4 * n) + 3) as
Element of 4
-tuples_on (8 -tuples_on BOOLEAN) ;
w . ((4 * n) + 4) in rng w
by X5, X4, FUNCT_1:3;
then reconsider w4 =
w . ((4 * n) + 4) as
Element of 4
-tuples_on (8 -tuples_on BOOLEAN) ;
reconsider z =
<*w1,w2,w3,w4*> as
Element of 4
-tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) by LMGSEQ4;
z = <*(w . ((4 * n) + 1)),(w . ((4 * n) + 2)),(w . ((4 * n) + 3)),(w . ((4 * n) + 4))*>
;
hence
ex
z being
Element of 4
-tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
S2[
k,
z]
;
verum
end;
consider p being
FinSequence of 4
-tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that P3:
(
dom p = Seg m7 & ( for
k being
Nat st
k in Seg m7 holds
S2[
k,
p . k] ) )
from FINSEQ_1:sch 5(P1);
P4:
len p = m7
by P3, FINSEQ_1:def 3;
p in (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) *
by FINSEQ_1:def 11;
then
p in m7 -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))
by P4;
then reconsider p =
p as
Element of
(7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) ;
take
p
;
S1[x,p]
now for i being Nat st i < 7 + m holds
p . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*>let i be
Nat;
( i < 7 + m implies p . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> )assume
i < 7
+ m
;
p . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*>then AA2:
i + 1
<= 7
+ m
by NAT_1:13;
1
<= i + 1
by NAT_1:11;
then
i + 1
in Seg m7
by AA2;
then
ex
n being
Element of
NAT st
(
n = (i + 1) - 1 &
p . (i + 1) = <*(w . ((4 * n) + 1)),(w . ((4 * n) + 2)),(w . ((4 * n) + 3)),(w . ((4 * n) + 4))*> )
by P3;
hence
p . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*>
;
verum end;
hence
S1[
x,
p]
;
verum
end;
consider I being Function of (m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),((7 + m) -tuples_on (4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)))) such that
A2:
for x being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds S1[x,I . x]
from FUNCT_2:sch 3(A1);
take
I
; for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex w being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(I . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) )
thus
for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex w being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( w = (KeyExpansionX (SBT,m)) . Key & ( for i being Nat st i < 7 + m holds
(I . Key) . (i + 1) = <*(w . ((4 * i) + 1)),(w . ((4 * i) + 2)),(w . ((4 * i) + 3)),(w . ((4 * i) + 4))*> ) )
by A2; verum