:: deftheorem Def12 defines IDEAoperationB IDEA_1:def 12 :
for n being non zero Nat
for m, k, b₄ being FinSequence of NAT holds
( b₄ = IDEAoperationB (m,k,n) iff ( len b₄ = len m & ( for i being Nat st i in dom m holds
( ( i = 1 implies b₄ . i = 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)))) ) & ( i = 2 implies b₄ . i = 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)))) ) & ( i = 3 implies b₄ . i = 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)))) ) & ( i = 4 implies b₄ . i = 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)))) ) & ( i <> 1 & i <> 2 & i <> 3 & i <> 4 implies b₄ . i = m . i ) ) ) ) );