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))); :: 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
(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))) ) ) ) ; :: thesis: ( 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))) ) ) ) ; :: thesis: H1 = H2

now :: thesis: for input being Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)) holds H1 . input = H2 . input

let input be Element of m -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN)); :: thesis: 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 S₁[ 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: S₁[ 0 ] ;
PN1: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A1: S₁[i] ; :: thesis: S₁[i + 1]
assume A2: ( m <= i + 1 & i + 1 <= 4 * (7 + m) ) ; :: thesis: 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 C10: m = i + 1 ; :: thesis: for k being Element of NAT st 1 <= k & k <= i + 1 holds
(H1 . input) . k = (H2 . input) . k

thus for k being Element of NAT st 1 <= k & k <= i + 1 holds
(H1 . input) . k = (H2 . input) . k :: thesis: verum

proof

let k be Element of NAT ; :: thesis: ( 1 <= k & k <= i + 1 implies (H1 . input) . k = (H2 . input) . k )
assume B1: ( 1 <= k & k <= i + 1 ) ; :: thesis: (H1 . input) . k = (H2 . input) . k
k - 1 < k by XREAL_1:44;
then B2: k - 1 < m by C10, B1, XXREAL_0:2;
reconsider k1 = k - 1 as Element of NAT by XREAL_1:48, B1, INT_1:3;
thus (H1 . input) . k = input . (k1 + 1) by B2, AA1
.= (H2 . input) . k by B2, AA2 ; :: thesis: verum

end;

end;

suppose m <> i + 1 ; :: thesis: for k being Element of NAT st 1 <= k & k <= i + 1 holds
(H1 . input) . k = (H2 . input) . k

then 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 :: thesis: verum

proof

let k be Element of NAT ; :: thesis: ( 1 <= k & k <= i + 1 implies (H1 . input) . k = (H2 . input) . k )
assume C13: ( 1 <= k & k <= i + 1 ) ; :: thesis: (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 C14: k1 < m ; :: thesis: (H1 . input) . k = (H2 . input) . k

thus (H1 . input) . k = input . (k1 + 1) by C14, AA1
.= (H2 . input) . k by C14, AA2 ; :: thesis: verum

end;

suppose C15: m <= k1 ; :: thesis: (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; :: thesis: verum

end;

end;

end;

end;

end;

end;

L10: for i being Nat holds S₁[i] from NAT_1:sch 2(PN0, PN1);

L1: now :: thesis: for i being Element of NAT st m <= i & i <= 4 * (7 + m) holds
(H1 . input) . i = (H2 . input) . i

let i be Element of NAT ; :: thesis: ( m <= i & i <= 4 * (7 + m) implies (H1 . input) . i = (H2 . input) . i )
assume A1: ( m <= i & i <= 4 * (7 + m) ) ; :: thesis: (H1 . input) . i = (H2 . input) . i
( 1 <= i & i <= i ) by AS, A1, XXREAL_0:2;
hence (H1 . input) . i = (H2 . input) . i by L10, A1; :: thesis: verum

end;

now :: thesis: for i0 being Nat st 1 <= i0 & i0 <= len H1i holds
H1i . i0 = H2i . i0

let i0 be Nat; :: thesis: ( 1 <= i0 & i0 <= len H1i implies H1i . i0 = H2i . i0 )
assume P13: ( 1 <= i0 & i0 <= len H1i ) ; :: thesis: H1i . i0 = H2i . i0
then reconsider i = i0 - 1 as Element of NAT by XREAL_1:48, INT_1:3;

now :: thesis: H1i . i0 = H2i . i0

per cases ( i0 <= m or m < i0 ) ;

suppose C1: i0 <= m ; :: thesis: H1i . i0 = H2i . i0

i < i0 by XREAL_1:44;
then C11: i < m by C1, XXREAL_0:2;
thus H1i . i0 = input . (i + 1) by C11, AA1
.= H2i . i0 by C11, AA2 ; :: thesis: verum

end;

suppose C3: m < i0 ; :: thesis: H1i . i0 = H2i . i0

i + 1 in Seg (len H1i) by P13;
hence H1i . i0 = H2i . i0 by L1, C3, XX1, P13; :: thesis: verum

end;

end;

end;

hence H1i . i0 = H2i . i0 ; :: thesis: verum

end;

hence H1 . input = H2 . input by XX1, XX2, FINSEQ_1:def 18; :: thesis: verum

end;

hence H1 = H2 by FUNCT_2:63; :: thesis: verum