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) ) ) :: thesis: ( ( 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 ; :: thesis: 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 :: thesis: ( ( m = 4 & i / m <= 10 ) or ( m = 6 & i / m <= 10 ) or ( m = 8 & i / m <= 10 ) )
per cases ( m = 4 or m = 6 or m = 8 ) by AS;
case m = 4 ; :: thesis: i / m <= 10
then i / m < 10 + 1 by AS, XREAL_1:74, LTT1;
hence i / m <= 10 by NAT_1:13, LTT4; :: thesis: verum
end;
case m = 6 ; :: thesis: i / m <= 10
hence i / m <= 10 by LTT5, XXREAL_0:2; :: thesis: verum
end;
case m = 8 ; :: thesis: i / m <= 10
hence i / m <= 10 by LTT5, XXREAL_0:2; :: thesis: verum
end;
end;
end;
hence i / m <= 10 ; :: thesis: 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) ) ; :: thesis: 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) ) ; :: thesis: ( 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 ) ; :: thesis: verum