defpred S1[ Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)), Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))] means ( ( for i being Element of NAT st i < m holds
$2 . (i + 1) = $1 . (i + 1) ) & ( for i being Element of NAT st m <= i & i < 4 * (7 + m) holds
ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = $2 . ((i - m) + 1) & Q = $2 . i & $2 . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) );
A1: for x being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex z being Element of (4 * (7 + m)) -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)); :: thesis: ex z being Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S1[x,z]
defpred S2[ Nat, set , set ] means ex r, t being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( r = $2 & t = $3 & ex P0, Q0 being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P0 = r . 1 & Q0 = r . m & t . 1 = Op-WXOR (P0,(KeyExTemp (SBT,m,(m * $1),Q0))) ) & ( for i being Nat st 1 <= i & i < m holds
ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = r . (i + 1) & Q = t . i & t . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,((m * $1) + i),Q))) ) ) );
0 + m <= 7 + m by XREAL_1:6;
then LMMLT47M: 1 * m <= 4 * (7 + m) by XREAL_1:66;
reconsider N2 = ((4 * (7 + m)) div m) + 1 as Nat ;
YY1: for k being Nat st 1 <= k & k < N2 holds
for s being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex y being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S2[k,s,y]
proof
let k be Nat; :: thesis: ( 1 <= k & k < N2 implies for s being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex y being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S2[k,s,y] )
assume ( 1 <= k & k < N2 ) ; :: thesis: for s being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ex y being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S2[k,s,y]
let s be Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: ex y being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S2[k,s,y]
defpred S3[ Nat, set , set ] means ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = s . ($1 + 1) & Q = $2 & $3 = Op-WXOR (P,(KeyExTemp (SBT,m,((m * k) + $1),Q))) );
s in m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
then ex v being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( s = v & len v = m ) ;
then QQ3: dom s = Seg m by FINSEQ_1:def 3;
XX1: for i being Nat st 1 <= i & i < m holds
for z being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ex w being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S3[i,z,w]
proof
let i be Nat; :: thesis: ( 1 <= i & i < m implies for z being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ex w being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S3[i,z,w] )
assume AA1: ( 1 <= i & i < m ) ; :: thesis: for z being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ex w being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S3[i,z,w]
let z be Element of 4 -tuples_on (8 -tuples_on BOOLEAN); :: thesis: ex w being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S3[i,z,w]
( 1 <= i + 1 & i + 1 <= m ) by NAT_1:13, AA1;
then i + 1 in Seg m ;
then s . (i + 1) in rng s by QQ3, FUNCT_1:3;
then reconsider P = s . (i + 1) as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ;
reconsider Q = z as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ;
Op-WXOR (P,(KeyExTemp (SBT,m,((m * k) + i),Q))) is Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ;
hence ex w being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S3[i,z,w] ; :: thesis: verum
end;
1 in dom s by AS, QQ3;
then s . 1 in rng s by FUNCT_1:3;
then reconsider P0 = s . 1 as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ;
m in dom s by AS, QQ3;
then s . m in rng s by FUNCT_1:3;
then reconsider Q0 = s . m as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ;
reconsider A0 = Op-WXOR (P0,(KeyExTemp (SBT,m,(m * k),Q0))) as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ;
consider y being FinSequence of 4 -tuples_on (8 -tuples_on BOOLEAN) such that
A2: ( len y = m & ( y . 1 = A0 or m = 0 ) & ( for i being Nat st 1 <= i & i < m holds
S3[i,y . i,y . (i + 1)] ) ) from RECDEF_1:sch 4(XX1);
 y in (4 -tuples_on (8 -tuples_on BOOLEAN)) * by FINSEQ_1:def 11;
then y in m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) by A2;
hence ex y being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st S2[k,s,y] by AS, A2; :: thesis: verum
end;
consider z being FinSequence of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
A2: ( len z = N2 & ( z . 1 = x or N2 = 0 ) & ( for k being Nat st 1 <= k & k < N2 holds
S2[k,z . k,z . (k + 1)] ) ) from RECDEF_1:sch 4(YY1);
 defpred S3[ Nat, set ] means ex i, j being Element of NAT ex zi being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( ( $1 mod m <> 0 implies ( i = ($1 div m) + 1 & j = $1 mod m ) ) & ( $1 mod m = 0 implies ( i = $1 div m & j = m ) ) & zi = z . i & $2 = zi . j );
YY2: for k being Nat st k in Seg (4 * (7 + m)) holds
ex w being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S3[k,w]
proof
let k be Nat; :: thesis: ( k in Seg (4 * (7 + m)) implies ex w being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S3[k,w] )
assume A1: k in Seg (4 * (7 + m)) ; :: thesis: ex w being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S3[k,w]
QQ1: ( 1 <= k & k <= 4 * (7 + m) ) by A1, FINSEQ_1:1;
then QQ2: k div m <= (4 * (7 + m)) div m by NAT_2:24;
per cases ( k mod m <> 0 or k mod m = 0 ) ;
suppose C1: k mod m <> 0 ; :: thesis: ex w being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S3[k,w]
reconsider j = k mod m as Element of NAT ;
reconsider i = (k div m) + 1 as Element of NAT ;
( 1 <= i & i <= N2 ) by QQ2, XREAL_1:6, NAT_1:11;
then i in Seg N2 ;
then i in dom z by A2, FINSEQ_1:def 3;
then z . i in rng z by FUNCT_1:3;
then reconsider zi = z . i as Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
zi in m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
then ex v being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( zi = v & len v = m ) ;
then Q0: dom zi = Seg m by FINSEQ_1:def 3;
( 1 <= j & j <= m ) by C1, INT_1:58, AS, NAT_1:14;
then j in dom zi by Q0;
then zi . j in rng zi by FUNCT_1:3;
then reconsider w = zi . j as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ;
( ( k mod m <> 0 implies ( i = (k div m) + 1 & j = k mod m ) ) & ( k mod m = 0 implies ( i = k div m & j = m ) ) & zi = z . i & w = zi . j ) by C1;
hence ex w being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S3[k,w] ; :: thesis: verum
end;
suppose C2: k mod m = 0 ; :: thesis: ex w being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S3[k,w]
reconsider j = m as Element of NAT by ORDINAL1:def 12;
reconsider i = k div m as Element of NAT ;
QQ3: 1 <= i by NAT_D:24, QQ1, C2, NAT_2:13, AS;
(k div m) + 0 <= ((4 * (7 + m)) div m) + 1 by QQ2, XREAL_1:7;
then i in Seg N2 by QQ3;
then i in dom z by A2, FINSEQ_1:def 3;
then z . i in rng z by FUNCT_1:3;
then reconsider zi = z . i as Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
zi in m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
then ex v being Element of (4 -tuples_on (8 -tuples_on BOOLEAN)) * st
( zi = v & len v = m ) ;
then Q0: dom zi = Seg m by FINSEQ_1:def 3;
j in Seg m by AS;
then zi . j in rng zi by Q0, FUNCT_1:3;
then reconsider w = zi . j as Element of 4 -tuples_on (8 -tuples_on BOOLEAN) ;
( ( k mod m <> 0 implies ( i = (k div m) + 1 & j = k mod m ) ) & ( k mod m = 0 implies ( i = k div m & j = m ) ) & zi = z . i & w = zi . j ) by C2;
hence ex w being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st S3[k,w] ; :: thesis: verum
end;
end;
end;
consider u being FinSequence of 4 -tuples_on (8 -tuples_on BOOLEAN) such that
YY3: ( dom u = Seg (4 * (7 + m)) & ( for k being Nat st k in Seg (4 * (7 + m)) holds
S3[k,u . k] ) ) from FINSEQ_1:sch 5(YY2);
 4 * (7 + m) is Element of NAT by ORDINAL1:def 12;
then YY4: len u = 4 * (7 + m) by YY3, FINSEQ_1:def 3;
u in (4 -tuples_on (8 -tuples_on BOOLEAN)) * by FINSEQ_1:def 11;
then u in (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) by YY4;
then reconsider u = u as Element of (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) ;
take u ; :: thesis: S1[x,u]
LX3: for i being Element of NAT st i < m holds
u . (i + 1) = x . (i + 1)
proof
let k be Element of NAT ; :: thesis: ( k < m implies u . (k + 1) = x . (k + 1) )
assume k < m ; :: thesis: u . (k + 1) = x . (k + 1)
then LX31: ( 1 <= k + 1 & k + 1 <= m ) by NAT_1:11, NAT_1:13;
then ( 1 <= k + 1 & k + 1 <= 4 * (7 + m) ) by LMMLT47M, XXREAL_0:2;
then k + 1 in Seg (4 * (7 + m)) ;
then consider i, j being Element of NAT , zi being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
LX34: ( ( (k + 1) mod m <> 0 implies ( i = ((k + 1) div m) + 1 & j = (k + 1) mod m ) ) & ( (k + 1) mod m = 0 implies ( i = (k + 1) div m & j = m ) ) & zi = z . i & u . (k + 1) = zi . j ) by YY3;
per cases ( (k + 1) mod m <> 0 or (k + 1) mod m = 0 ) ;
suppose C1: (k + 1) mod m <> 0 ; :: thesis: u . (k + 1) = x . (k + 1)
C11: k + 1 < m
proof
assume not k + 1 < m ; :: thesis: contradiction
then k + 1 = m by XXREAL_0:1, LX31;
hence contradiction by NAT_D:25, C1; :: thesis: verum
end;
then (k + 1) div m = 0 by NAT_D:27;
hence u . (k + 1) = x . (k + 1) by C11, NAT_D:24, LX34, A2; :: thesis: verum
end;
suppose C2: (k + 1) mod m = 0 ; :: thesis: u . (k + 1) = x . (k + 1)
k + 1 = m
proof
assume not k + 1 = m ; :: thesis: contradiction
then k + 1 < m by LX31, XXREAL_0:1;
hence contradiction by NAT_D:24, C2; :: thesis: verum
end;
hence u . (k + 1) = x . (k + 1) by LX34, C2, INT_1:49, A2; :: thesis: verum
end;
end;
end;
for k being Element of NAT st m <= k & k < 4 * (7 + m) holds
ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = u . ((k - m) + 1) & Q = u . k & u . (k + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,k,Q))) )
proof
let k be Element of NAT ; :: thesis: ( m <= k & k < 4 * (7 + m) implies ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = u . ((k - m) + 1) & Q = u . k & u . (k + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,k,Q))) ) )
assume AS1: ( m <= k & k < 4 * (7 + m) ) ; :: thesis: ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = u . ((k - m) + 1) & Q = u . k & u . (k + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,k,Q))) )
then ( 1 <= k & k <= 4 * (7 + m) ) by XXREAL_0:2, AS;
then k in Seg (4 * (7 + m)) ;
then consider i, j being Element of NAT , zi being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
LX34: ( ( k mod m <> 0 implies ( i = (k div m) + 1 & j = k mod m ) ) & ( k mod m = 0 implies ( i = k div m & j = m ) ) & zi = z . i & u . k = zi . j ) by YY3;
NLX32: ( 1 <= k + 1 & k + 1 <= 4 * (7 + m) ) by AS1, NAT_1:11, NAT_1:13;
then k + 1 in Seg (4 * (7 + m)) ;
then consider i1, j1 being Element of NAT , zi1 being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
NLX34: ( ( (k + 1) mod m <> 0 implies ( i1 = ((k + 1) div m) + 1 & j1 = (k + 1) mod m ) ) & ( (k + 1) mod m = 0 implies ( i1 = (k + 1) div m & j1 = m ) ) & zi1 = z . i1 & u . (k + 1) = zi1 . j1 ) by YY3;
reconsider km0 = k - m as Element of NAT by AS1, XREAL_1:48, INT_1:3;
reconsider km1 = km0 + 1 as Element of NAT ;
(k + 1) - m <= (4 * (7 + m)) - 0 by NLX32, XREAL_1:13;
then ( 1 <= km1 & km1 <= 4 * (7 + m) ) by NAT_1:11;
then km1 in Seg (4 * (7 + m)) ;
then consider i2, j2 being Element of NAT , zi2 being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
LLX34: ( ( km1 mod m <> 0 implies ( i2 = (km1 div m) + 1 & j2 = km1 mod m ) ) & ( km1 mod m = 0 implies ( i2 = km1 div m & j2 = m ) ) & zi2 = z . i2 & u . km1 = zi2 . j2 ) by YY3;
per cases ( k mod m <> 0 or k mod m = 0 ) ;
suppose C1: k mod m <> 0 ; :: thesis: ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = u . ((k - m) + 1) & Q = u . k & u . (k + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,k,Q))) )
reconsider i0 = k div m as Element of NAT ;
DD1: ((4 * (7 + m)) div m) + 0 < ((4 * (7 + m)) div m) + 1 by XREAL_1:8;
k div m <= (4 * (7 + m)) div m by AS1, NAT_2:24;
then ( 1 <= i0 & i0 < N2 ) by DD1, XXREAL_0:2, AS, NAT_2:13, AS1;
then consider r, t being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
C16: ( r = z . i0 & t = z . (i0 + 1) & ex P0, Q0 being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P0 = r . 1 & Q0 = r . m & t . 1 = Op-WXOR (P0,(KeyExTemp (SBT,m,(m * i0),Q0))) ) & ( for n being Nat st 1 <= n & n < m holds
ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = r . (n + 1) & Q = t . n & t . (n + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,((i0 * m) + n),Q))) ) ) ) by A2;
( 1 <= j & j < m ) by AS, INT_1:58, LX34, C1, NAT_1:14;
then consider P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) such that
C18: ( P = r . (j + 1) & Q = t . j & t . (j + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,((i0 * m) + j),Q))) ) by C16;
per cases ( (k + 1) mod m <> 0 or (k + 1) mod m = 0 ) ;
suppose NC1: (k + 1) mod m <> 0 ; :: thesis: ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = u . ((k - m) + 1) & Q = u . k & u . (k + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,k,Q))) )
NC16: zi1 = zi by NLX34, NC1, AS, XLMOD01, LX34, C1;
C21: u . (k + 1) = t . (j + 1) by NLX34, NC16, NC1, AS, XLMOD02, LX34, C1, C16;
C22X: km1 = (k + 1) - m ;
LC12: i2 = (((k + 1) div m) - 1) + 1 by NC1, XLMOD03, C22X, LLX34, AS, XLMOD04
.= i0 by AS, XLMOD01, NC1 ;
LC13: j2 = j1 by LLX34, C22X, XLMOD03, NLX34;
C19: u . ((k - m) + 1) = r . (j + 1) by LLX34, LC13, LC12, C16, NLX34, NC1, AS, XLMOD02, LX34, C1;
C22: k = (i0 * m) + j by AS, INT_1:59, LX34, C1;
thus ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = u . ((k - m) + 1) & Q = u . k & u . (k + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,k,Q))) ) by C18, C19, C16, LX34, C1, C21, C22; :: thesis: verum
end;
suppose MC1: (k + 1) mod m = 0 ; :: thesis: ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = u . ((k - m) + 1) & Q = u . k & u . (k + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,k,Q))) )
NC13: j1 = (m - 1) + 1 by NLX34, MC1
.= j + 1 by AS, XLMOD02X, MC1, LX34 ;
C21: u . (k + 1) = t . (j + 1) by NLX34, MC1, XLMOD01X, NC13, C16;
C22X: km1 = (k + 1) - m ;
LC12: i2 = ((k + 1) div m) - 1 by C22X, MC1, XLMOD03, LLX34, AS, XLMOD04
.= ((k div m) + 1) - 1 by AS, XLMOD01X, MC1
.= i0 ;
C19: u . ((k - m) + 1) = r . (j + 1) by LLX34, C22X, XLMOD03, NLX34, LC12, C16, NC13;
C22: k = (i0 * m) + j by AS, INT_1:59, LX34, C1;
thus ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = u . ((k - m) + 1) & Q = u . k & u . (k + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,k,Q))) ) by C18, C19, LX34, C16, C1, C21, C22; :: thesis: verum
end;
end;
end;
suppose C2: k mod m = 0 ; :: thesis: ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = u . ((k - m) + 1) & Q = u . k & u . (k + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,k,Q))) )
DD1: ((4 * (7 + m)) div m) + 0 < ((4 * (7 + m)) div m) + 1 by XREAL_1:8;
k div m <= (4 * (7 + m)) div m by AS1, NAT_2:24;
then ( 1 <= i & i < N2 ) by DD1, XXREAL_0:2, C2, LX34, AS, NAT_2:13, AS1;
then consider r, t being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) such that
C16: ( r = z . i & t = z . (i + 1) & ex P0, Q0 being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P0 = r . 1 & Q0 = r . m & t . 1 = Op-WXOR (P0,(KeyExTemp (SBT,m,(m * i),Q0))) ) & ( for n being Nat st 1 <= n & n < m holds
ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = r . (n + 1) & Q = t . n & t . (n + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,((i * m) + n),Q))) ) ) ) by A2;
NC1X: (k + 1) mod m = (0 + 1) mod m by C2, NAT_D:23
.= 1 by NAT_D:14, AS ;
C21: u . (k + 1) = t . 1 by NLX34, NC1X, AS, XLMOD01, C2, LX34, C16;
C22X: km1 = (k + 1) - m ;
LC12: i2 = (((k + 1) div m) - 1) + 1 by NC1X, XLMOD03, C22X, LLX34, AS, XLMOD04
.= i by AS, XLMOD01, NC1X, C2, LX34 ;
C19: u . ((k - m) + 1) = r . 1 by LLX34, XLMOD03, C22X, LC12, C16, NC1X;
C22: k = ((k div m) * m) + (k mod m) by AS, INT_1:59
.= i * m by C2, LX34 ;
thus ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = u . ((k - m) + 1) & Q = u . k & u . (k + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,k,Q))) ) by C19, LX34, C16, C2, C21, C22; :: thesis: verum
end;
end;
end;
hence S1[x,u] by LX3; :: thesis: verum
end;
consider I being Function of (m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),((4 * (7 + m)) -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 ; :: thesis: for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( ( for i being Element of NAT st i < m holds
(I . Key) . (i + 1) = Key . (i + 1) ) & ( for i being Element of NAT st m <= i & i < 4 * (7 + m) holds
ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = (I . Key) . ((i - m) + 1) & Q = (I . Key) . i & (I . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) )
thus for Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds
( ( for i being Element of NAT st i < m holds
(I . Key) . (i + 1) = Key . (i + 1) ) & ( for i being Element of NAT st m <= i & i < 4 * (7 + m) holds
ex P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( P = (I . Key) . ((i - m) + 1) & Q = (I . Key) . i & (I . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) ) by A2; :: thesis: verum