thus
( i mod m = 0 implies ex A, T3 being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( T3 = Rcon . (i / m) & A = Op-WXOR ((SubWord (SBT,(RotWord w))),T3) ) )
( ( m = 8 & i mod 8 = 4 implies ex b1 being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st b1 = SubWord (SBT,w) ) & ( not i mod m = 0 & ( not m = 8 or not i mod 8 = 4 ) implies ex b1 being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st b1 = w ) )proof
assume A1:
i mod m = 0
;
ex A, T3 being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st
( T3 = Rcon . (i / m) & A = Op-WXOR ((SubWord (SBT,(RotWord w))),T3) )
(
m <> 0 &
m divides i )
by A1, INT_1:62, AS;
then LTT0:
i / m is
Integer
by WSIERP_1:17;
LTT1:
(4 * (7 + m)) / m = (28 / m) + 4
by AS;
LTT2:
m / m <= i / m
by AS, XREAL_1:72;
LTT4:
i / m in NAT
by INT_1:3, LTT0;
LTT5:
i / m < (28 / m) + 4
by AS, XREAL_1:74, LTT1;
i / m <= 10
proof
now ( ( m = 4 & i / m <= 10 ) or ( m = 6 & i / m <= 10 ) or ( m = 8 & i / m <= 10 ) )end;
hence
i / m <= 10
;
verum
end;
then Q0:
i / m in Seg 10
by AS, LTT2, LTT4;
reconsider j =
i / m as
Nat by LTT4;
Rcon in 10
-tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
;
then
ex
v being
Element of
(4 -tuples_on (8 -tuples_on BOOLEAN)) * st
(
Rcon = v &
len v = 10 )
;
then
dom Rcon = Seg 10
by FINSEQ_1:def 3;
then
Rcon . j in rng Rcon
by Q0, FUNCT_1:3;
then reconsider T3 =
Rcon . j as
Element of 4
-tuples_on (8 -tuples_on BOOLEAN) ;
Op-WXOR (
(SubWord (SBT,(RotWord w))),
T3) is
Element of 4
-tuples_on (8 -tuples_on BOOLEAN)
;
hence
ex
A,
T3 being
Element of 4
-tuples_on (8 -tuples_on BOOLEAN) st
(
T3 = Rcon . (i / m) &
A = Op-WXOR (
(SubWord (SBT,(RotWord w))),
T3) )
;
verum
end;
thus
( m = 8 & i mod 8 = 4 implies ex A being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st A = SubWord (SBT,w) )
; ( not i mod m = 0 & ( not m = 8 or not i mod 8 = 4 ) implies ex b1 being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st b1 = w )
thus
( not i mod m = 0 & ( not m = 8 or not i mod 8 = 4 ) implies ex A being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) st A = w )
; verum