:: deftheorem defines RotWord AESCIP_1:def 8 :
for x being Element of 4 -tuples_on (8 -tuples_on BOOLEAN) holds RotWord x = Op-LeftShift x;