let m, k be FinSequence of NAT ; :: thesis: for n being non zero Nat st len m >= 4 holds
( (IDEAoperationB (m,k,n)) . 1 is_expressible_by n & (IDEAoperationB (m,k,n)) . 2 is_expressible_by n & (IDEAoperationB (m,k,n)) . 3 is_expressible_by n & (IDEAoperationB (m,k,n)) . 4 is_expressible_by n )
let n be non zero Nat; :: thesis: ( len m >= 4 implies ( (IDEAoperationB (m,k,n)) . 1 is_expressible_by n & (IDEAoperationB (m,k,n)) . 2 is_expressible_by n & (IDEAoperationB (m,k,n)) . 3 is_expressible_by n & (IDEAoperationB (m,k,n)) . 4 is_expressible_by n ) )
assume A1: len m >= 4 ; :: thesis: ( (IDEAoperationB (m,k,n)) . 1 is_expressible_by n & (IDEAoperationB (m,k,n)) . 2 is_expressible_by n & (IDEAoperationB (m,k,n)) . 3 is_expressible_by n & (IDEAoperationB (m,k,n)) . 4 is_expressible_by n )
then 1 <= len m by XXREAL_0:2;
then 1 in Seg (len m) by FINSEQ_1:1;
then 1 in dom m by FINSEQ_1:def 3;
then (IDEAoperationB (m,k,n)) . 1 = Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) by Def12;
then A2: (IDEAoperationB (m,k,n)) . 1 < 2 to_power n by BINARI_3:1;
3 <= len m by A1, XXREAL_0:2;
then 3 in Seg (len m) by FINSEQ_1:1;
then 3 in dom m by FINSEQ_1:def 3;
then (IDEAoperationB (m,k,n)) . 3 = Absval ((n -BinarySequence (m . 3)) 'xor' (n -BinarySequence (MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)))) by Def12;
then A3: (IDEAoperationB (m,k,n)) . 3 < 2 to_power n by BINARI_3:1;
2 <= len m by A1, XXREAL_0:2;
then 2 in Seg (len m) by FINSEQ_1:1;
then 2 in dom m by FINSEQ_1:def 3;
then (IDEAoperationB (m,k,n)) . 2 = Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) by Def12;
then A4: (IDEAoperationB (m,k,n)) . 2 < 2 to_power n by BINARI_3:1;
4 in Seg (len m) by A1, FINSEQ_1:1;
then 4 in dom m by FINSEQ_1:def 3;
then (IDEAoperationB (m,k,n)) . 4 = Absval ((n -BinarySequence (m . 4)) 'xor' (n -BinarySequence (ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(MUL_MOD ((ADD_MOD ((MUL_MOD ((Absval ((n -BinarySequence (m . 1)) 'xor' (n -BinarySequence (m . 3)))),(k . 5),n)),(Absval ((n -BinarySequence (m . 2)) 'xor' (n -BinarySequence (m . 4)))),n)),(k . 6),n)),n)))) by Def12;
then (IDEAoperationB (m,k,n)) . 4 < 2 to_power n by BINARI_3:1;
hence ( (IDEAoperationB (m,k,n)) . 1 is_expressible_by n & (IDEAoperationB (m,k,n)) . 2 is_expressible_by n & (IDEAoperationB (m,k,n)) . 3 is_expressible_by n & (IDEAoperationB (m,k,n)) . 4 is_expressible_by n ) by A2, A4, A3; :: thesis: verum