:: deftheorem DefAddRoundKey defines AddRoundKey AESCIP_1:def 6 :
for b₁ being Function of [:(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))),(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))):],(4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))) holds
( b₁ = AddRoundKey iff for text, key being Element of 4 -tuples_on (4 -tuples_on (8 -tuples_on BOOLEAN))
for i, j being Nat st i in Seg 4 & j in Seg 4 holds
ex textij, keyij being Element of 8 -tuples_on BOOLEAN st
( textij = (text . i) . j & keyij = (key . i) . j & ((b₁ . (text,key)) . i) . j = Op-XOR (textij,keyij) ) );