let H1, H2 be Function of (m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),((4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))); ( ( 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
(H1 . 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 = (H1 . Key) . ((i - m) + 1) & Q = (H1 . Key) . i & (H1 . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) ) ) & ( 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
(H2 . 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 = (H2 . Key) . ((i - m) + 1) & Q = (H2 . Key) . i & (H2 . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) ) ) implies H1 = H2 )
assume AA1:
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
(H1 . 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 = (H1 . Key) . ((i - m) + 1) & Q = (H1 . Key) . i & (H1 . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) )
; ( ex Key being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) st
( ( for i being Element of NAT st i < m holds
(H2 . Key) . (i + 1) = Key . (i + 1) ) implies ex i being Element of NAT st
( m <= i & i < 4 * (7 + m) & ( for P, Q being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) holds
( not P = (H2 . Key) . ((i - m) + 1) or not Q = (H2 . Key) . i or not (H2 . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) ) ) or H1 = H2 )
assume AA2:
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
(H2 . 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 = (H2 . Key) . ((i - m) + 1) & Q = (H2 . Key) . i & (H2 . Key) . (i + 1) = Op-WXOR (P,(KeyExTemp (SBT,m,i,Q))) ) ) )
; H1 = H2
now for input being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds H1 . input = H2 . inputlet input be
Element of
m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN));
H1 . input = H2 . input
H1 . input 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
(
H1 . input = s &
len s = 4
* (7 + m) )
;
reconsider H1i =
H1 . input as
Element of
(4 -tuples_on (8 -tuples_on BOOLEAN)) * by XX1;
H2 . input in (4 * (7 + m)) -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
;
then XX2:
ex
s being
Element of
(4 -tuples_on (8 -tuples_on BOOLEAN)) * st
(
H2 . input = s &
len s = 4
* (7 + m) )
;
reconsider H2i =
H2 . input as
Element of
(4 -tuples_on (8 -tuples_on BOOLEAN)) * by XX2;
defpred S1[
Nat]
means (
m <= $1 & $1
<= 4
* (7 + m) implies for
k being
Element of
NAT st 1
<= k &
k <= $1 holds
(H1 . input) . k = (H2 . input) . k );
PN0:
S1[
0 ]
;
PN1:
for
i being
Nat st
S1[
i] holds
S1[
i + 1]
proof
let i be
Nat;
( S1[i] implies S1[i + 1] )
assume A1:
S1[
i]
;
S1[i + 1]
assume A2:
(
m <= i + 1 &
i + 1
<= 4
* (7 + m) )
;
for k being Element of NAT st 1 <= k & k <= i + 1 holds
(H1 . input) . k = (H2 . input) . k
per cases
( m = i + 1 or m <> i + 1 )
;
suppose
m <> i + 1
;
for k being Element of NAT st 1 <= k & k <= i + 1 holds
(H1 . input) . k = (H2 . input) . kthen C10X:
m < i + 1
by A2, XXREAL_0:1;
i < i + 1
by XREAL_1:29;
then C11Z:
i < 4
* (7 + m)
by A2, XXREAL_0:2;
thus
for
k being
Element of
NAT st 1
<= k &
k <= i + 1 holds
(H1 . input) . k = (H2 . input) . k
verumproof
let k be
Element of
NAT ;
( 1 <= k & k <= i + 1 implies (H1 . input) . k = (H2 . input) . k )
assume C13:
( 1
<= k &
k <= i + 1 )
;
(H1 . input) . k = (H2 . input) . k
then reconsider k1 =
k - 1 as
Element of
NAT by XREAL_1:48, INT_1:3;
per cases
( k1 < m or m <= k1 )
;
suppose C15:
m <= k1
;
(H1 . input) . k = (H2 . input) . k
k - 1
<= (i + 1) - 1
by C13, XREAL_1:9;
then C16:
(
m <= k1 &
k1 < 4
* (7 + m) )
by C11Z, XXREAL_0:2, C15;
then consider PP1,
QQ1 being
Element of 4
-tuples_on (8 -tuples_on BOOLEAN) such that C17:
(
PP1 = (H1 . input) . ((k1 - m) + 1) &
QQ1 = (H1 . input) . k1 &
(H1 . input) . (k1 + 1) = Op-WXOR (
PP1,
(KeyExTemp (SBT,m,k1,QQ1))) )
by AA1;
consider PP2,
QQ2 being
Element of 4
-tuples_on (8 -tuples_on BOOLEAN) such that C18:
(
PP2 = (H2 . input) . ((k1 - m) + 1) &
QQ2 = (H2 . input) . k1 &
(H2 . input) . (k1 + 1) = Op-WXOR (
PP2,
(KeyExTemp (SBT,m,k1,QQ2))) )
by AA2, C16;
C190:
k - 1
<= (i + 1) - 1
by XREAL_1:9, C13;
then C191:
( 1
<= k1 &
k1 <= i )
by C15, AS, XXREAL_0:2;
C24X:
0 <= k1 - m
by C15, XREAL_1:48;
then C25X:
1
+ 0 <= (k1 - m) + 1
by XREAL_1:6;
k1 - (m - 1) <= k1
by AS, XREAL_1:43;
then C25:
( 1
<= (k1 - m) + 1 &
(k1 - m) + 1
<= i )
by C190, XXREAL_0:2, C25X;
reconsider k1m1 =
(k1 - m) + 1 as
Element of
NAT by C24X, INT_1:3;
C21:
(H1 . input) . k1m1 = (H2 . input) . k1m1
by A2, C10X, NAT_1:13, A1, C25;
thus
(H1 . input) . k = (H2 . input) . k
by C21, C17, C18, C191, A2, C10X, NAT_1:13, A1;
verum end; end;
end; end; end;
end; L10:
for
i being
Nat holds
S1[
i]
from NAT_1:sch 2(PN0, PN1);
hence
H1 . input = H2 . input
by XX1, XX2, FINSEQ_1:def 17;
verum end;
hence
H1 = H2
by FUNCT_2:63; verum